forked from lalalune/ArkLib
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathArkLib.lean
More file actions
1551 lines (1551 loc) · 85.4 KB
/
Copy pathArkLib.lean
File metadata and controls
1551 lines (1551 loc) · 85.4 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
import ArkLib.AGM.Basic
import ArkLib.AGM.RepresentationLemmas
import ArkLib.AxiomCheck62
import ArkLib.AxiomCheck62FrontD
import ArkLib.CommitmentScheme.Basic
import ArkLib.CommitmentScheme.Fold
import ArkLib.CommitmentScheme.MerkleTree.Extraction
import ArkLib.CommitmentScheme.Transparent
import ArkLib.Commitments.Functional.Basic
import ArkLib.Commitments.Functional.CommitmentScheme
import ArkLib.Commitments.Functional.Hachi.Gadget
import ArkLib.Commitments.Functional.Hachi.GadgetNorms
import ArkLib.Commitments.Functional.Hachi.InnerOuter
import ArkLib.Commitments.Functional.Hachi.InnerOuter.Arithmetic
import ArkLib.Commitments.Functional.Hachi.InnerOuter.Correctness
import ArkLib.Commitments.Functional.Hachi.InnerOuter.Scheme
import ArkLib.Commitments.Functional.Hachi.InnerOuter.Security
import ArkLib.Commitments.Functional.Hachi.PolynomialEvalSplit
import ArkLib.Commitments.Functional.KZG.Algebra
import ArkLib.Commitments.Functional.KZG.Basic
import ArkLib.Commitments.Functional.KZG.Binding
import ArkLib.Commitments.Functional.KZG.Correctness
import ArkLib.Commitments.Functional.KZG.FunctionBinding.Basic
import ArkLib.Commitments.Functional.KZG.FunctionBinding.DegreeConflict
import ArkLib.Commitments.Functional.KZG.FunctionBinding.EvaluationBindingConflict
import ArkLib.Commitments.Functional.KZG.FunctionBinding.Support
import ArkLib.Commitments.Functional.KZG.FunctionBinding.TauInQueries
import ArkLib.Commitments.Functional.KZG.HardnessAssumptions
import ArkLib.Commitments.Functional.KZG.Sampling
import ArkLib.Commitments.Functional.MerkleTree.Batch
import ArkLib.Commitments.Functional.MerkleTree.Extraction
import ArkLib.Commitments.Functional.MerkleTree.Hiding
import ArkLib.Commitments.Functional.Transparent
import ArkLib.Commitments.Ordinary.Ajtai.Simple
import ArkLib.Commitments.Ordinary.Ajtai.Simple.Correctness
import ArkLib.Commitments.Ordinary.Ajtai.Simple.Scheme
import ArkLib.Commitments.Ordinary.Ajtai.Simple.Security
import ArkLib.Commitments.Ordinary.Basic
import ArkLib.Commitments.Ordinary.SimpleRO
import ArkLib.Data.Array.Lemmas
import ArkLib.Data.Classes.FunEquiv
import ArkLib.Data.Classes.HasSize
import ArkLib.Data.Classes.Initialize
import ArkLib.Data.Classes.Serde
import ArkLib.Data.Classes.Slice
import ArkLib.Data.CodingTheory.AGL24AgreementForcing
import ArkLib.Data.CodingTheory.AGL24AgreementHypergraph
import ArkLib.Data.CodingTheory.AGL24AppendixAssembly
import ArkLib.Data.CodingTheory.AGL24ConditionalAssembly
import ArkLib.Data.CodingTheory.AGL24CutNetChange
import ArkLib.Data.CodingTheory.AGL24CutSupply
import ArkLib.Data.CodingTheory.AGL24DeletionRobustness
import ArkLib.Data.CodingTheory.AGL24DetDegree
import ArkLib.Data.CodingTheory.AGL24DeterministicChain
import ArkLib.Data.CodingTheory.AGL24DualSpan
import ArkLib.Data.CodingTheory.AGL24DualZeroPatternPinned
import ArkLib.Data.CodingTheory.AGL24EvalToSymbolic
import ArkLib.Data.CodingTheory.AGL24ExtensionLift
import ArkLib.Data.CodingTheory.AGL24FrankDescent
import ArkLib.Data.CodingTheory.AGL24FrankInterface
import ArkLib.Data.CodingTheory.AGL24FrankUncrossingStep
import ArkLib.Data.CodingTheory.AGL24FrontDoorBridge
import ArkLib.Data.CodingTheory.AGL24GMMDSInterface
import ArkLib.Data.CodingTheory.AGL24GenericZeroPattern
import ArkLib.Data.CodingTheory.AGL24GrandAssembly
import ArkLib.Data.CodingTheory.AGL24Issue354Discharge
import ArkLib.Data.CodingTheory.AGL24KernelAgreement
import ArkLib.Data.CodingTheory.AGL24KernelVector
import ArkLib.Data.CodingTheory.AGL24ListDecodingBridge
import ArkLib.Data.CodingTheory.AGL24NonzeroMinor
import ArkLib.Data.CodingTheory.AGL24Orientation
import ArkLib.Data.CodingTheory.AGL24PinnedConnector
import ArkLib.Data.CodingTheory.AGL24ProbDischarge
import ArkLib.Data.CodingTheory.AGL24RIMPermutation
import ArkLib.Data.CodingTheory.AGL24RSInstance
import ArkLib.Data.CodingTheory.AGL24ReducedIntersectionMatrix
import ArkLib.Data.CodingTheory.AGL24RevealStep
import ArkLib.Data.CodingTheory.AGL24SubfamilyTransport
import ArkLib.Data.CodingTheory.AGL24Submatrix
import ArkLib.Data.CodingTheory.AGL24Submodular
import ArkLib.Data.CodingTheory.AGL24SymbolicRank
import ArkLib.Data.CodingTheory.AGL24Types
import ArkLib.Data.CodingTheory.AGL24UnionBound
import ArkLib.Data.CodingTheory.AGL24VertexDegree
import ArkLib.Data.CodingTheory.AGL24WeakPartition
import ArkLib.Data.CodingTheory.AsymptoticGVBound
import ArkLib.Data.CodingTheory.Basic.CosetFarCount
import ArkLib.Data.CodingTheory.Basic.DecodingRadius
import ArkLib.Data.CodingTheory.Basic.Distance
import ArkLib.Data.CodingTheory.Basic.Entropy
import ArkLib.Data.CodingTheory.Basic.LinearCode
import ArkLib.Data.CodingTheory.Basic.MDSCode
import ArkLib.Data.CodingTheory.Basic.RelDistTranslation
import ArkLib.Data.CodingTheory.Basic.RelativeDistance
import ArkLib.Data.CodingTheory.BerlekampWelch.BerlekampWelch
import ArkLib.Data.CodingTheory.BerlekampWelch.Condition
import ArkLib.Data.CodingTheory.BerlekampWelch.ElocPoly
import ArkLib.Data.CodingTheory.BerlekampWelch.Existence
import ArkLib.Data.CodingTheory.BerlekampWelch.Sorries
import ArkLib.Data.CodingTheory.BinomialEntropyBallBound
import ArkLib.Data.CodingTheory.BinomialEntropyBound
import ArkLib.Data.CodingTheory.CodeGeometry
import ArkLib.Data.CodingTheory.Connections.EpsMCABadGlue
import ArkLib.Data.CodingTheory.Connections.GCXK25SecondMoment
import ArkLib.Data.CodingTheory.Connections.GKL24FirstMoment
import ArkLib.Data.CodingTheory.Connections.GKL24MaxCorrCommonZeroCover
import ArkLib.Data.CodingTheory.Connections.GKL24MaxDomainExists
import ArkLib.Data.CodingTheory.Connections.GKL24PetalWitnessCover
import ArkLib.Data.CodingTheory.Connections.GKL24SunflowerCore
import ArkLib.Data.CodingTheory.Connections.ListDecodingAndCA
import ArkLib.Data.CodingTheory.DivergenceOfSets
import ArkLib.Data.CodingTheory.EntropyBallNcard
import ArkLib.Data.CodingTheory.EntropyCapacityValue
import ArkLib.Data.CodingTheory.EntropyConcave
import ArkLib.Data.CodingTheory.EntropyGVBound
import ArkLib.Data.CodingTheory.EntropyGVBoundDiv
import ArkLib.Data.CodingTheory.EntropyHammingBound
import ArkLib.Data.CodingTheory.EntropyVolumeBound
import ArkLib.Data.CodingTheory.EntropyVolumeListSize
import ArkLib.Data.CodingTheory.EntropyVolumeUpper
import ArkLib.Data.CodingTheory.EntropyVolumeUpperBall
import ArkLib.Data.CodingTheory.EntropyVolumeUpperBound
import ArkLib.Data.CodingTheory.Erasure
import ArkLib.Data.CodingTheory.ExtensionCodes
import ArkLib.Data.CodingTheory.ExternalDebt
import ArkLib.Data.CodingTheory.GMMDS.LovettBaseCase
import ArkLib.Data.CodingTheory.GMMDS.LovettBlockDecomp
import ArkLib.Data.CodingTheory.GMMDS.LovettBlockDim
import ArkLib.Data.CodingTheory.GMMDS.LovettBlockSpan
import ArkLib.Data.CodingTheory.GMMDS.LovettCombinatorial
import ArkLib.Data.CodingTheory.GMMDS.LovettCoordMerge
import ArkLib.Data.CodingTheory.GMMDS.LovettCounting
import ArkLib.Data.CodingTheory.GMMDS.LovettDivisibility
import ArkLib.Data.CodingTheory.GMMDS.LovettDualRowsDischarge
import ArkLib.Data.CodingTheory.GMMDS.LovettDualSpanConnector
import ArkLib.Data.CodingTheory.GMMDS.LovettFractionField
import ArkLib.Data.CodingTheory.GMMDS.LovettInduction
import ArkLib.Data.CodingTheory.GMMDS.LovettLemma22
import ArkLib.Data.CodingTheory.GMMDS.LovettLemma24
import ArkLib.Data.CodingTheory.GMMDS.LovettLemma2456
import ArkLib.Data.CodingTheory.GMMDS.LovettLemma24Finish
import ArkLib.Data.CodingTheory.GMMDS.LovettLemma25
import ArkLib.Data.CodingTheory.GMMDS.LovettLemma25Opening
import ArkLib.Data.CodingTheory.GMMDS.LovettMeetReplace
import ArkLib.Data.CodingTheory.GMMDS.LovettMergeBranch
import ArkLib.Data.CodingTheory.GMMDS.LovettMergeDescent
import ArkLib.Data.CodingTheory.GMMDS.LovettMergeIdentity
import ArkLib.Data.CodingTheory.GMMDS.LovettMergeIndepProof
import ArkLib.Data.CodingTheory.GMMDS.LovettMergeMeet
import ArkLib.Data.CodingTheory.GMMDS.LovettMergeReduction
import ArkLib.Data.CodingTheory.GMMDS.LovettMergeReindex
import ArkLib.Data.CodingTheory.GMMDS.LovettMergeSubstitution
import ArkLib.Data.CodingTheory.GMMDS.LovettMergeVStar
import ArkLib.Data.CodingTheory.GMMDS.LovettNLtK
import ArkLib.Data.CodingTheory.GMMDS.LovettPairwise
import ArkLib.Data.CodingTheory.GMMDS.LovettPolynomial
import ArkLib.Data.CodingTheory.GMMDS.LovettPrimitiveDischarge
import ArkLib.Data.CodingTheory.GMMDS.LovettPrimitiveDistinctDegree
import ArkLib.Data.CodingTheory.GMMDS.LovettRIMKernelTrivial
import ArkLib.Data.CodingTheory.GMMDS.LovettRaise
import ArkLib.Data.CodingTheory.GMMDS.LovettReducibleDischarge
import ArkLib.Data.CodingTheory.GMMDS.LovettReduction
import ArkLib.Data.CodingTheory.GMMDS.LovettSeparateStep
import ArkLib.Data.CodingTheory.GMMDS.LovettSeparation
import ArkLib.Data.CodingTheory.GMMDS.LovettSubstitutionDvd
import ArkLib.Data.CodingTheory.GMMDS.LovettSymbolicMinorDischarge
import ArkLib.Data.CodingTheory.GMMDS.LovettThm17Reduction
import ArkLib.Data.CodingTheory.GMMDS.LovettToGMMDSBridge
import ArkLib.Data.CodingTheory.GMMDS.LovettToGZPDualBridgeReduction
import ArkLib.Data.CodingTheory.GMMDS.LovettUnconditionalWiring
import ArkLib.Data.CodingTheory.GMMDS.LovettUnion
import ArkLib.Data.CodingTheory.GMMDS.LovettVStarReduce
import ArkLib.Data.CodingTheory.GMMDS.LovettWitnessCounterexample
import ArkLib.Data.CodingTheory.GMMDS.SchwartzZippelMinorSpecialization
import ArkLib.Data.CodingTheory.GMMDS.SymbolicFullRankLovettFree
import ArkLib.Data.CodingTheory.GVCounting
import ArkLib.Data.CodingTheory.GilbertVarshamov
import ArkLib.Data.CodingTheory.GilbertVarshamovExistence
import ArkLib.Data.CodingTheory.GuruswamiSudan
import ArkLib.Data.CodingTheory.GuruswamiSudan.Basic
import ArkLib.Data.CodingTheory.GuruswamiSudan.DictionaryBridge
import ArkLib.Data.CodingTheory.GuruswamiSudan.DictionaryHasse
import ArkLib.Data.CodingTheory.GuruswamiSudan.FeasibilityArith
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSAffinePair
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSCellProduction
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSCurveInterpolantZDegree
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSCurveTuple
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSDecodedSeparationOverRatFunc
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSDiscriminantOverRatFunc
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSFactorAssignment
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSFactorDegreeOverRatFunc
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSFactorizationOverRatFunc
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSIntegerRepresentative
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSIntegralFactorAssignment
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSInterpolantSloped
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSInterpolantSlopedCurve
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSInterpolantSlopedCurveCapped
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSInterpolantZDegree
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSInterpolantZDegreeCurve
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSInterpolantZDegreeGraded
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSInterpolantZDegreeTight
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSLargeCharSeparable
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSListSizeOverRatFunc
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSOverRatFunc
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSPerScalarCapture
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSSeparabilityCharZero
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSSeparableContraction
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSSeparableCoreDescent
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSSpecializedConditions
import ArkLib.Data.CodingTheory.GuruswamiSudan.GSSquarefreePart
import ArkLib.Data.CodingTheory.GuruswamiSudan.GuruswamiSudan
import ArkLib.Data.CodingTheory.GuruswamiSudan.Hab25FactorWeld
import ArkLib.Data.CodingTheory.GuruswamiSudan.Hab25S4Wire
import ArkLib.Data.CodingTheory.GuruswamiSudan.Hab25SeparableSupply
import ArkLib.Data.CodingTheory.GuruswamiSudan.ListSizeBound
import ArkLib.Data.CodingTheory.GuruswamiSudan.MCAEventDecodedBridge
import ArkLib.Data.CodingTheory.GuruswamiSudan.MonomialCount
import ArkLib.Data.CodingTheory.GuruswamiSudan.MultiplicityInterpolation
import ArkLib.Data.CodingTheory.GuruswamiSudan.PerPairCoverData
import ArkLib.Data.CodingTheory.GuruswamiSudan.ToPolyDegree
import ArkLib.Data.CodingTheory.GuruswamiSudan.TrivariateDivisibility
import ArkLib.Data.CodingTheory.GuruswamiSudan.TrivariateFeasibility
import ArkLib.Data.CodingTheory.GuruswamiSudan.TrivariateInterpolation
import ArkLib.Data.CodingTheory.HammingBallBasics
import ArkLib.Data.CodingTheory.HammingBallEntropyUpperBound
import ArkLib.Data.CodingTheory.HammingBallVolume
import ArkLib.Data.CodingTheory.HammingBallVolumeBasics
import ArkLib.Data.CodingTheory.HammingBound
import ArkLib.Data.CodingTheory.HammingBoundRate
import ArkLib.Data.CodingTheory.HigherOrderMDS
import ArkLib.Data.CodingTheory.HigherOrderMDSFrame
import ArkLib.Data.CodingTheory.HigherOrderMDSList
import ArkLib.Data.CodingTheory.HigherOrderMDSListGenPos
import ArkLib.Data.CodingTheory.HigherOrderMDSOrderKNormal
import ArkLib.Data.CodingTheory.HigherOrderMDSOrderThreeChar
import ArkLib.Data.CodingTheory.HigherOrderMDSOrderThreeFail
import ArkLib.Data.CodingTheory.HigherOrderMDSOrderTwo
import ArkLib.Data.CodingTheory.HigherOrderMDSReedSolomon
import ArkLib.Data.CodingTheory.HigherOrderMDSReedSolomonCode
import ArkLib.Data.CodingTheory.InterleavedArityMono
import ArkLib.Data.CodingTheory.InterleavedCode
import ArkLib.Data.CodingTheory.InterleavedFinOneEq
import ArkLib.Data.CodingTheory.InterleavedLambdaGe
import ArkLib.Data.CodingTheory.InterleavedListSize
import ArkLib.Data.CodingTheory.InterleavedRowDistance
import ArkLib.Data.CodingTheory.JohnsonBound.Basic
import ArkLib.Data.CodingTheory.JohnsonBound.Choose2
import ArkLib.Data.CodingTheory.JohnsonBound.CodeListSize
import ArkLib.Data.CodingTheory.JohnsonBound.Expectations
import ArkLib.Data.CodingTheory.JohnsonBound.Family
import ArkLib.Data.CodingTheory.JohnsonBound.FamilyRefutation
import ArkLib.Data.CodingTheory.JohnsonBound.FamilyRefutationComplete
import ArkLib.Data.CodingTheory.JohnsonBound.Lemmas
import ArkLib.Data.CodingTheory.JohnsonBound.ListSize
import ArkLib.Data.CodingTheory.JohnsonBound.ReedSolomonJohnsonLambda
import ArkLib.Data.CodingTheory.JohnsonBound.ReedSolomonListSize
import ArkLib.Data.CodingTheory.LineListBound
import ArkLib.Data.CodingTheory.ListDecodability
import ArkLib.Data.CodingTheory.ListDecoding.AGL23Barrier
import ArkLib.Data.CodingTheory.ListDecoding.BKR06SubspacePoly
import ArkLib.Data.CodingTheory.ListDecoding.Bounds
import ArkLib.Data.CodingTheory.ListDecoding.Bounds.BCHKS25
import ArkLib.Data.CodingTheory.ListDecoding.Bounds.CapacityBoundsProofs
import ArkLib.Data.CodingTheory.ListDecoding.Bounds.GKL24
import ArkLib.Data.CodingTheory.ListDecoding.Bounds.General
import ArkLib.Data.CodingTheory.ListDecoding.Bounds.GuruswamiSudanListSize
import ArkLib.Data.CodingTheory.ListDecoding.Bounds.RandomAndReedSolomon
import ArkLib.Data.CodingTheory.ListDecoding.Bounds.SubspaceDesign
import ArkLib.Data.CodingTheory.ListDecoding.Bounds.SubstitutionMultiplicity
import ArkLib.Data.CodingTheory.ListDecoding.CZ25CapacityPropEndpoint
import ArkLib.Data.CodingTheory.ListDecoding.CZ25CapacityReduction
import ArkLib.Data.CodingTheory.ListDecoding.CZ25DesignToLambda
import ArkLib.Data.CodingTheory.ListDecoding.CZ25GeomCapacity
import ArkLib.Data.CodingTheory.ListDecoding.CZ25SpanBoundBridge
import ArkLib.Data.CodingTheory.ListDecoding.CZ25SpanDimension
import ArkLib.Data.CodingTheory.ListDecoding.CZ25UniqueDecodingSlice
import ArkLib.Data.CodingTheory.ListDecoding.FPRUNEGoodCoord
import ArkLib.Data.CodingTheory.ListDecoding.FPRUNEListBound
import ArkLib.Data.CodingTheory.ListDecoding.FPRUNEPotential
import ArkLib.Data.CodingTheory.ListDecoding.FPRUNERealStep
import ArkLib.Data.CodingTheory.ListDecoding.FirstMomentListBound
import ArkLib.Data.CodingTheory.ListDecoding.GHSZ02Foundations
import ArkLib.Data.CodingTheory.ListDecoding.GuruswamiSudan.Basic
import ArkLib.Data.CodingTheory.ListDecoding.JH01
import ArkLib.Data.CodingTheory.ListDecoding.JH02
import ArkLib.Data.CodingTheory.ListDecoding.Seq
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyAdditive
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyBiUnion
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyBoundedSupport
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyCompSub
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyDecomp
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyDvd
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyFaithful
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyGeneralSupport
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyKernel
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyLineSupport
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyLinearMap
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyLinearized
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyRank
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyRecursion
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyTop
import ArkLib.Data.CodingTheory.ListDecoding.SubspacePolyTranslate
import ArkLib.Data.CodingTheory.ListDecoding.UniqueDecodingPairwise
import ArkLib.Data.CodingTheory.ListSizeVolumeBound
import ArkLib.Data.CodingTheory.MDSIncidenceBound
import ArkLib.Data.CodingTheory.MDSIncidenceFrame
import ArkLib.Data.CodingTheory.PlaneIncidenceBound
import ArkLib.Data.CodingTheory.PlotkinBound
import ArkLib.Data.CodingTheory.PlotkinBoundCard
import ArkLib.Data.CodingTheory.PolishchukSpielman
import ArkLib.Data.CodingTheory.PolishchukSpielman.Degrees
import ArkLib.Data.CodingTheory.PolishchukSpielman.Existence
import ArkLib.Data.CodingTheory.PolishchukSpielman.PolishchukSpielman
import ArkLib.Data.CodingTheory.PolishchukSpielman.Resultant
import ArkLib.Data.CodingTheory.Prelims
import ArkLib.Data.CodingTheory.ProximityCA
import ArkLib.Data.CodingTheory.ProximityGap
import ArkLib.Data.CodingTheory.ProximityGap.AHIV22
import ArkLib.Data.CodingTheory.ProximityGap.AHIV22Support
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AffineLines.BWMatrix
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AffineLines.GoodCoeffs
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AffineLines.JointAgreement
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AffineLines.Main
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AffineLines.UniqueDecoding
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AffineSpaces
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AlphaWeight
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AlphaWeightClearedObstruction
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AlphaWeightDivisibility
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.BCoeffVanishing
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.ClearingProduct
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Curves
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Curves.Assembly
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Curves.CoeffExtraction
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Curves.CoeffExtractionResidual
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Curves.CoeffExtractionVacuous
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Curves.GoodCoeffs
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Curves.JointAgreement
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Curves.UniqueDecoding
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.ErrorBound
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.FaaDiBrunoBijectionPieces
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.GammaGenuine
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.HenselNumerator
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.ListDecoding.Agreement
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.ListDecoding.Extraction
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.ListDecoding.Guruswami
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.ListDecoding.RootClearing
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.LocalSeriesProducer
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.MonicFaaDiBrunoMatchAlt
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P1BetaOneRefutation
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P1MonicIntegrality
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2Assembly
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2Bijection
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2BijectionApply
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2Close
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2FilterDrop
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2KeystoneReindex
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2Match
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2MatchMonic
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2MatchProof
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2MatchRoot
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2MonicConsequences
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2MonicOrderZero
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2Reabsorb
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2Reindex
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2RootBridge
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2Vanish
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Pigeonhole
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Prelude
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.ReedSolomonGap
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.RemainingCore
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.RestrictedFaaDiBrunoExtract
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.RestrictedFaaDiBrunoXiTelescope
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.S5Genuine
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.S5GenuineMonic
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.StrictCoeffLargeReduction
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.StrictCoeffProducer
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.UnclearedEmbedding
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.WPowerInjective
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.WeightedAgreement
import ArkLib.Data.CodingTheory.ProximityGap.BCKHS25.AffineLineJointAgreement
import ArkLib.Data.CodingTheory.ProximityGap.BCKHS25.CollinearProximates
import ArkLib.Data.CodingTheory.ProximityGap.BCKHS25.Interpolation
import ArkLib.Data.CodingTheory.ProximityGap.Basic
import ArkLib.Data.CodingTheory.ProximityGap.BivariateVanishing
import ArkLib.Data.CodingTheory.ProximityGap.BoundaryCardResidual
import ArkLib.Data.CodingTheory.ProximityGap.BoundaryCardResidualRefutation
import ArkLib.Data.CodingTheory.ProximityGap.BoundaryCardStrictInteriorRefutation
import ArkLib.Data.CodingTheory.ProximityGap.BoundaryLatticeThresholdLeaf
import ArkLib.Data.CodingTheory.ProximityGap.BoundaryThresholdFloorCell
import ArkLib.Data.CodingTheory.ProximityGap.CS25BallEntropy
import ArkLib.Data.CodingTheory.ProximityGap.CS25CoveringExistence
import ArkLib.Data.CodingTheory.ProximityGap.CS25SecondMomentReduction
import ArkLib.Data.CodingTheory.ProximityGap.CapacityBounds
import ArkLib.Data.CodingTheory.ProximityGap.Collapse
import ArkLib.Data.CodingTheory.ProximityGap.CoveringFromFarCount
import ArkLib.Data.CodingTheory.ProximityGap.CurveUDRBadCount
import ArkLib.Data.CodingTheory.ProximityGap.CurveUDRBound
import ArkLib.Data.CodingTheory.ProximityGap.CurveUDRCoefficients
import ArkLib.Data.CodingTheory.ProximityGap.DG25
import ArkLib.Data.CodingTheory.ProximityGap.DG25.Basic
import ArkLib.Data.CodingTheory.ProximityGap.DG25.Contrapositive
import ArkLib.Data.CodingTheory.ProximityGap.DG25.MainResults
import ArkLib.Data.CodingTheory.ProximityGap.DG25.ReedSolomon
import ArkLib.Data.CodingTheory.ProximityGap.Errors
import ArkLib.Data.CodingTheory.ProximityGap.Folding
import ArkLib.Data.CodingTheory.ProximityGap.GK16Admissible
import ArkLib.Data.CodingTheory.ProximityGap.GK16Claim16Transport
import ArkLib.Data.CodingTheory.ProximityGap.GK16DegreeBudget
import ArkLib.Data.CodingTheory.ProximityGap.GK16FrsTransport
import ArkLib.Data.CodingTheory.ProximityGap.GK16Lemma12
import ArkLib.Data.CodingTheory.ProximityGap.GK16RootCounting
import ArkLib.Data.CodingTheory.ProximityGap.GK16Wronskian
import ArkLib.Data.CodingTheory.ProximityGap.GSCounting
import ArkLib.Data.CodingTheory.ProximityGap.GSFactorExtract
import ArkLib.Data.CodingTheory.ProximityGap.GSKernelAffineDescent
import ArkLib.Data.CodingTheory.ProximityGap.GrandChallenges
import ArkLib.Data.CodingTheory.ProximityGap.Hab25AffineCapture
import ArkLib.Data.CodingTheory.ProximityGap.Hab25AlgebraicBridge
import ArkLib.Data.CodingTheory.ProximityGap.Hab25CaptureKernel
import ArkLib.Data.CodingTheory.ProximityGap.Hab25CaptureKernelUD
import ArkLib.Data.CodingTheory.ProximityGap.Hab25CellWiring
import ArkLib.Data.CodingTheory.ProximityGap.Hab25Claim1
import ArkLib.Data.CodingTheory.ProximityGap.Hab25ConjectureGlue
import ArkLib.Data.CodingTheory.ProximityGap.Hab25Core
import ArkLib.Data.CodingTheory.ProximityGap.Hab25CurveCellProduction
import ArkLib.Data.CodingTheory.ProximityGap.Hab25ErrStarArith
import ArkLib.Data.CodingTheory.ProximityGap.Hab25FiberPigeonhole
import ArkLib.Data.CodingTheory.ProximityGap.Hab25GradedNumericEdge
import ArkLib.Data.CodingTheory.ProximityGap.Hab25Johnson
import ArkLib.Data.CodingTheory.ProximityGap.Hab25JohnsonArith
import ArkLib.Data.CodingTheory.ProximityGap.Hab25JohnsonArithmetic
import ArkLib.Data.CodingTheory.ProximityGap.Hab25JohnsonNumericBridge
import ArkLib.Data.CodingTheory.ProximityGap.Hab25K4FiberReduction
import ArkLib.Data.CodingTheory.ProximityGap.Hab25K4Seam
import ArkLib.Data.CodingTheory.ProximityGap.Hab25Multiplicity
import ArkLib.Data.CodingTheory.ProximityGap.Hab25MultiplicityBridge
import ArkLib.Data.CodingTheory.ProximityGap.HasseMonomial
import ArkLib.Data.CodingTheory.ProximityGap.LDThreshold
import ArkLib.Data.CodingTheory.ProximityGap.LDThresholdElias
import ArkLib.Data.CodingTheory.ProximityGap.LDThresholdJohnsonSq
import ArkLib.Data.CodingTheory.ProximityGap.Lattice
import ArkLib.Data.CodingTheory.ProximityGap.Lattice2
import ArkLib.Data.CodingTheory.ProximityGap.Lattice2.Core
import ArkLib.Data.CodingTheory.ProximityGap.Lattice2.ListThreshold
import ArkLib.Data.CodingTheory.ProximityGap.Lattice2.Spec
import ArkLib.Data.CodingTheory.ProximityGap.Lattice2.Witnesses
import ArkLib.Data.CodingTheory.ProximityGap.LineDecoding
import ArkLib.Data.CodingTheory.ProximityGap.LineDecoding2
import ArkLib.Data.CodingTheory.ProximityGap.LineDecodingCoverage
import ArkLib.Data.CodingTheory.ProximityGap.MCABadCount
import ArkLib.Data.CodingTheory.ProximityGap.MCABadCountRatio
import ArkLib.Data.CodingTheory.ProximityGap.MCACurveEvent
import ArkLib.Data.CodingTheory.ProximityGap.MCAEndpointLower
import ArkLib.Data.CodingTheory.ProximityGap.MCAGenerator
import ArkLib.Data.CodingTheory.ProximityGap.MCALowerBound
import ArkLib.Data.CodingTheory.ProximityGap.MCASecondMoment
import ArkLib.Data.CodingTheory.ProximityGap.MCAUDRBound
import ArkLib.Data.CodingTheory.ProximityGap.MultiplicativeRigidityZMod
import ArkLib.Data.CodingTheory.ProximityGap.ProximityGapP
import ArkLib.Data.CodingTheory.ProximityGap.ProximityGenerators
import ArkLib.Data.CodingTheory.ProximityGap.RSDistinctness
import ArkLib.Data.CodingTheory.ProximityGap.RSListSize
import ArkLib.Data.CodingTheory.ProximityGap.RadiusOne
import ArkLib.Data.CodingTheory.ProximityGap.RadiusOneExact
import ArkLib.Data.CodingTheory.ProximityGap.ReedSolomonUniqueDecode
import ArkLib.Data.CodingTheory.ProximityGap.StackJointAgreement
import ArkLib.Data.CodingTheory.ProximityGap.SubsetSumErdosHeilbronn
import ArkLib.Data.CodingTheory.ProximityGap.SubsetSumRadiusOne
import ArkLib.Data.CodingTheory.ProximityGap.TwoLineExtraction
import ArkLib.Data.CodingTheory.ProximityGap.UDRBadCount
import ArkLib.Data.CodingTheory.ProximityGap.VandermondeMCAExtract
import ArkLib.Data.CodingTheory.ProximityLeaves
import ArkLib.Data.CodingTheory.ProximityLeaves2
import ArkLib.Data.CodingTheory.QEntropyMonotone
import ArkLib.Data.CodingTheory.QEntropySelfBound
import ArkLib.Data.CodingTheory.Quarantine.DerandomizationHasse
import ArkLib.Data.CodingTheory.Quarantine.DisproofFoldedRS
import ArkLib.Data.CodingTheory.Quarantine.DisproofLoop4
import ArkLib.Data.CodingTheory.Quarantine.DisproofLoop5
import ArkLib.Data.CodingTheory.Quarantine.DisproofLoop6
import ArkLib.Data.CodingTheory.Quarantine.DisproofLoop7
import ArkLib.Data.CodingTheory.Quarantine.DisproofLoop8
import ArkLib.Data.CodingTheory.Quarantine.Hypotheses
import ArkLib.Data.CodingTheory.Quarantine.HypothesesRefutations
import ArkLib.Data.CodingTheory.Quarantine.ProofLoop9
import ArkLib.Data.CodingTheory.RSCodewordWeight
import ArkLib.Data.CodingTheory.RSNearCount
import ArkLib.Data.CodingTheory.RSVanishingDim
import ArkLib.Data.CodingTheory.RSWeightEnumerator
import ArkLib.Data.CodingTheory.RSWeightEnumeratorExact
import ArkLib.Data.CodingTheory.RandomLinearCodeCodewordCount
import ArkLib.Data.CodingTheory.RandomLinearCodeEquidistribution
import ArkLib.Data.CodingTheory.RandomLinearCodeFirstMoment
import ArkLib.Data.CodingTheory.RandomLinearCodeFirstMomentExists
import ArkLib.Data.CodingTheory.RandomLinearCodeFullRankProb
import ArkLib.Data.CodingTheory.RandomLinearCodeMatrixEquidist
import ArkLib.Data.CodingTheory.RandomLinearCodePairwiseProb
import ArkLib.Data.CodingTheory.RandomLinearCodeParallelProb
import ArkLib.Data.CodingTheory.RandomLinearCodeRankEquidist
import ArkLib.Data.CodingTheory.ReedSolomon
import ArkLib.Data.CodingTheory.ReedSolomon.AdmissibleDischarge
import ArkLib.Data.CodingTheory.ReedSolomon.AdmissibleSubspaceDesign
import ArkLib.Data.CodingTheory.ReedSolomon.FRSGeomSubspaceDesign
import ArkLib.Data.CodingTheory.ReedSolomon.Folded
import ArkLib.Data.CodingTheory.ReedSolomon.Interleaved
import ArkLib.Data.CodingTheory.ReedSolomon.Multilinear
import ArkLib.Data.CodingTheory.ReedSolomon.Multiplicity
import ArkLib.Data.CodingTheory.RootCountingEngine
import ArkLib.Data.CodingTheory.SingletonBound
import ArkLib.Data.CodingTheory.SingletonBoundRate
import ArkLib.Data.CodingTheory.SubspaceDesign
import ArkLib.Data.CodingTheory.SubspaceDesign.Basic
import ArkLib.Data.CodingTheory.SubspaceDesign.NormTorus
import ArkLib.Data.CompPoly.Basic
import ArkLib.Data.Domain.CosetFftDomain.Defs
import ArkLib.Data.Domain.CosetFftDomain.Log
import ArkLib.Data.Domain.CosetFftDomain.Mem
import ArkLib.Data.Domain.CosetFftDomain.Ops
import ArkLib.Data.Domain.CosetFftDomain.Subdomain
import ArkLib.Data.Domain.CosetFftDomain.ToFftDomain
import ArkLib.Data.Domain.CosetFftDomain.ToList
import ArkLib.Data.Domain.FftDomain.Defs
import ArkLib.Data.Domain.FftDomain.Mem
import ArkLib.Data.Domain.FftDomain.Ops
import ArkLib.Data.Domain.FftDomain.Subdomain
import ArkLib.Data.Domain.FftDomain.ToSubgroup
import ArkLib.Data.EllipticCurve.BN254
import ArkLib.Data.FieldTheory.AdditiveNTT.AdditiveNTT
import ArkLib.Data.FieldTheory.AdditiveNTT.Domain
import ArkLib.Data.FieldTheory.AdditiveNTT.NovelPolynomialBasis
import ArkLib.Data.FieldTheory.BinaryField.Tower.TensorAlgebra
import ArkLib.Data.FieldTheory.NonBinaryField.Basic
import ArkLib.Data.Fin.Basic
import ArkLib.Data.Fin.BigOperators
import ArkLib.Data.Fin.Fold
import ArkLib.Data.Fin.Lift
import ArkLib.Data.Fin.Sigma
import ArkLib.Data.Fin.Tuple.Defs
import ArkLib.Data.Fin.Tuple.Lemmas
import ArkLib.Data.Fin.Tuple.Notation
import ArkLib.Data.Fin.Tuple.TakeDrop
import ArkLib.Data.Finset.PickSubset
import ArkLib.Data.GroupTheory.PrimeOrder
import ArkLib.Data.GroupTheory.Smooth
import ArkLib.Data.Hash.DomainSep
import ArkLib.Data.Hash.DuplexSponge
import ArkLib.Data.Hash.Keccak
import ArkLib.Data.Hash.Poseidon2
import ArkLib.Data.Lattices.CyclotomicRing.Core
import ArkLib.Data.Lattices.CyclotomicRing.Core.Basic
import ArkLib.Data.Lattices.CyclotomicRing.Core.Modulus
import ArkLib.Data.Lattices.CyclotomicRing.Galois
import ArkLib.Data.Lattices.CyclotomicRing.Galois.Automorphism
import ArkLib.Data.Lattices.CyclotomicRing.Galois.FixedSubring
import ArkLib.Data.Lattices.CyclotomicRing.Galois.Group
import ArkLib.Data.Lattices.CyclotomicRing.Galois.Order
import ArkLib.Data.Lattices.CyclotomicRing.Galois.Trace
import ArkLib.Data.Lattices.CyclotomicRing.NormBounds
import ArkLib.Data.Lattices.CyclotomicRing.NormBounds.Basic
import ArkLib.Data.Lattices.CyclotomicRing.NormBounds.LsCore
import ArkLib.Data.Lattices.CyclotomicRing.NormBounds.LyubashevskySeiler
import ArkLib.Data.Lattices.CyclotomicRing.NormBounds.MicciancioYoung
import ArkLib.Data.Lattices.CyclotomicRing.Norms
import ArkLib.Data.Lattices.CyclotomicRing.PowTwo
import ArkLib.Data.Lattices.CyclotomicRing.Rq
import ArkLib.Data.Lattices.CyclotomicRing.Subfield
import ArkLib.Data.Lattices.CyclotomicRing.Subfield.Basis
import ArkLib.Data.Lattices.CyclotomicRing.Subfield.Bijectivity
import ArkLib.Data.Lattices.CyclotomicRing.Subfield.Cardinality
import ArkLib.Data.Lattices.CyclotomicRing.Subfield.Factorization
import ArkLib.Data.Lattices.CyclotomicRing.Subfield.Field
import ArkLib.Data.Lattices.CyclotomicRing.Subfield.NormBound
import ArkLib.Data.Lattices.CyclotomicRing.Subfield.Packing
import ArkLib.Data.Lattices.CyclotomicRing.Subfield.TraceInnerProduct
import ArkLib.Data.Lattices.CyclotomicRing.Subfield.TraceVanishing
import ArkLib.Data.Lattices.ModuleSIS
import ArkLib.Data.Lattices.Vectors
import ArkLib.Data.List.Lemmas
import ArkLib.Data.Matrix.Basic
import ArkLib.Data.Matrix.Sparse
import ArkLib.Data.Matrix.Vandermonde
import ArkLib.Data.Misc.Basic
import ArkLib.Data.MvPolynomial.ComputableDegreeLE
import ArkLib.Data.MvPolynomial.Degrees
import ArkLib.Data.MvPolynomial.EvenAndOdd
import ArkLib.Data.MvPolynomial.Interpolation
import ArkLib.Data.MvPolynomial.LinearMvExtension
import ArkLib.Data.MvPolynomial.LowDegreeAgreement
import ArkLib.Data.MvPolynomial.Multilinear
import ArkLib.Data.MvPolynomial.MultilinearComputational
import ArkLib.Data.MvPolynomial.MultilinearSchwartzZippel
import ArkLib.Data.MvPolynomial.RestrictDegree
import ArkLib.Data.MvPolynomial.RestrictDegreeVar
import ArkLib.Data.MvPolynomial.SchwartzZippelCounting
import ArkLib.Data.Nat.Bitwise
import ArkLib.Data.Polynomial.Bivariate
import ArkLib.Data.Polynomial.ClearDenomY
import ArkLib.Data.Polynomial.DegreeLTDimension
import ArkLib.Data.Polynomial.FoldingPolynomial
import ArkLib.Data.Polynomial.Frobenius
import ArkLib.Data.Polynomial.FunctionFieldZLinear
import ArkLib.Data.Polynomial.GammaSubstObstruction
import ArkLib.Data.Polynomial.HenselBranchRigidity
import ArkLib.Data.Polynomial.HenselExistence
import ArkLib.Data.Polynomial.HenselSeriesCoeff
import ArkLib.Data.Polynomial.Indicator
import ArkLib.Data.Polynomial.Interface
import ArkLib.Data.Polynomial.MonomialBasis
import ArkLib.Data.Polynomial.MultinomialChainRule
import ArkLib.Data.Polynomial.Multivariate.HasseDerivative
import ArkLib.Data.Polynomial.Multivariate.Interpolation
import ArkLib.Data.Polynomial.NewtonLinearization
import ArkLib.Data.Polynomial.PowerSeriesComposition
import ArkLib.Data.Polynomial.Prelims
import ArkLib.Data.Polynomial.RationalFunctions
import ArkLib.Data.Polynomial.RationalFunctionsCore
import ArkLib.Data.Polynomial.RationalFunctionsStrong
import ArkLib.Data.Polynomial.SplitFold
import ArkLib.Data.Polynomial.Trivariate
import ArkLib.Data.Polynomial.UnivariateAgreement
import ArkLib.Data.Polynomial.WeightZLinear
import ArkLib.Data.Probability.Combinatorial
import ArkLib.Data.Probability.DistinctTuples
import ArkLib.Data.Probability.IndexedMarginalBound
import ArkLib.Data.Probability.Instances
import ArkLib.Data.Probability.MarginalBound
import ArkLib.Data.Probability.Notation
import ArkLib.Data.Probability.PrUnionBound
import ArkLib.Data.Probability.ProductMarginal
import ArkLib.Data.Probability.ProductMarginalBound
import ArkLib.Data.Probability.RandomSubsetInclusion
import ArkLib.Data.Probability.RandomSubsetInclusionExists
import ArkLib.Data.Probability.TensorSchwartzZippel
import ArkLib.Data.Probability.UniformPushforward
import ArkLib.Data.Probability.UniformSubset
import ArkLib.Data.RingTheory.TowerOfAlgebra
import ArkLib.Data.UniPoly.Basic
import ArkLib.Interaction.Oracle.Core
import ArkLib.Interaction.Oracle.Spec
import ArkLib.Interaction.Reduction
import ArkLib.MCACapacityTrivial
import ArkLib.OracleReduction.BCS.AppendSoundnessMsg
import ArkLib.OracleReduction.BCS.BCSCompilerProof
import ArkLib.OracleReduction.BCS.Basic
import ArkLib.OracleReduction.BCS.CompletenessPreservation
import ArkLib.OracleReduction.BCS.FrontierBricks
import ArkLib.OracleReduction.Basic
import ArkLib.OracleReduction.Cast
import ArkLib.OracleReduction.CastInOut
import ArkLib.OracleReduction.Completeness
import ArkLib.OracleReduction.Composition.Parallel.Basic
import ArkLib.OracleReduction.Composition.Sequential.Append
import ArkLib.OracleReduction.Composition.Sequential.AppendChallengeKeystoneOracle
import ArkLib.OracleReduction.Composition.Sequential.AppendChallengeSeam
import ArkLib.OracleReduction.Composition.Sequential.AppendChallengeSeamChallenge
import ArkLib.OracleReduction.Composition.Sequential.AppendCompletenessEmptyErr
import ArkLib.OracleReduction.Composition.Sequential.AppendCompletenessHelper
import ArkLib.OracleReduction.Composition.Sequential.AppendCompletenessMsgKeystone
import ArkLib.OracleReduction.Composition.Sequential.AppendCompletenessNonPerfect
import ArkLib.OracleReduction.Composition.Sequential.AppendEmptyKeystoneOracle
import ArkLib.OracleReduction.Composition.Sequential.AppendKnowledgeOracleTransport
import ArkLib.OracleReduction.Composition.Sequential.AppendPerfectCompleteness
import ArkLib.OracleReduction.Composition.Sequential.AppendPerfectCompletenessChallenge
import ArkLib.OracleReduction.Composition.Sequential.AppendPerfectCompletenessEmpty
import ArkLib.OracleReduction.Composition.Sequential.AppendPerfectCompletenessMsg
import ArkLib.OracleReduction.Composition.Sequential.AppendPerfectCompletenessOracle
import ArkLib.OracleReduction.Composition.Sequential.AppendPerfectCompletenessOracleChallenge
import ArkLib.OracleReduction.Composition.Sequential.AppendPerfectCompletenessProof
import ArkLib.OracleReduction.Composition.Sequential.AppendPerfectCompletenessReductionDischarge
import ArkLib.OracleReduction.Composition.Sequential.AppendPerfectCompletenessTotal
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKeystone
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgeChallenge
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgeChallengeBody
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgeChallengeOracleLift
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgeEmpty
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgeFailingDet
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgeFailingDetChallenge
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgeFailingDetEmpty
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgeOracleLift
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgePerRoundDischarge
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgePhase2ReconcileProof
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgeSeamZero
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgeStateCollapse
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrKnowledgeStateFunction
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrSoundnessOracleLift
import ArkLib.OracleReduction.Composition.Sequential.AppendRbrSoundnessPhase2Proof
import ArkLib.OracleReduction.Composition.Sequential.AppendResidualDischarges
import ArkLib.OracleReduction.Composition.Sequential.AppendResidualDischargesSeams
import ArkLib.OracleReduction.Composition.Sequential.AppendRightPartialProjections
import ArkLib.OracleReduction.Composition.Sequential.AppendRunEvalDist
import ArkLib.OracleReduction.Composition.Sequential.AppendRunEvalDistChallenge
import ArkLib.OracleReduction.Composition.Sequential.AppendSeamBridges
import ArkLib.OracleReduction.Composition.Sequential.AppendSeamBridges2
import ArkLib.OracleReduction.Composition.Sequential.AppendSeamBridges3
import ArkLib.OracleReduction.Composition.Sequential.AppendSoundnessChallengeProof
import ArkLib.OracleReduction.Composition.Sequential.AppendSoundnessMsgProof
import ArkLib.OracleReduction.Composition.Sequential.AppendSoundnessOracleMsg
import ArkLib.OracleReduction.Composition.Sequential.AppendSoundnessProof
import ArkLib.OracleReduction.Composition.Sequential.AppendSoundnessSeamTransfer
import ArkLib.OracleReduction.Composition.Sequential.AppendSoundnessTotal
import ArkLib.OracleReduction.Composition.Sequential.AppendToVerifierKeystone
import ArkLib.OracleReduction.Composition.Sequential.AppendVerifierFusion
import ArkLib.OracleReduction.Composition.Sequential.AppendVerifierFusionCore
import ArkLib.OracleReduction.Composition.Sequential.ChallengeOracleFintype
import ArkLib.OracleReduction.Composition.Sequential.ChallengeSeamBridge
import ArkLib.OracleReduction.Composition.Sequential.EmptyAppend
import ArkLib.OracleReduction.Composition.Sequential.EmptyAppendChallenge
import ArkLib.OracleReduction.Composition.Sequential.EmptyAppendReduction
import ArkLib.OracleReduction.Composition.Sequential.General
import ArkLib.OracleReduction.Composition.Sequential.SeamChallengeRestriction
import ArkLib.OracleReduction.Composition.Sequential.SeamCompleteness
import ArkLib.OracleReduction.Composition.Sequential.SeamDecomposition
import ArkLib.OracleReduction.Composition.Sequential.SeamDecompositionRun
import ArkLib.OracleReduction.Composition.Sequential.SeamDecompositionRunPartial
import ArkLib.OracleReduction.Composition.Sequential.SeamDecompositionRunPartialChallenge
import ArkLib.OracleReduction.Composition.Sequential.SeamDecompositionRunWithLog
import ArkLib.OracleReduction.Composition.Sequential.SeqComposeFailingDet
import ArkLib.OracleReduction.Composition.Sequential.SeqComposeMsgCompleteness
import ArkLib.OracleReduction.Composition.Sequential.SeqComposeOracleCompleteness
import ArkLib.OracleReduction.Composition.Sequential.SeqComposePerfectCompletenessChallengeThreaded
import ArkLib.OracleReduction.Composition.Sequential.SeqComposePerfectCompletenessThreaded
import ArkLib.OracleReduction.Composition.Sequential.SeqComposeRbrKnowledgeProof
import ArkLib.OracleReduction.Composition.Sequential.SeqComposeVerifierBricks
import ArkLib.OracleReduction.ContinueFromToSupport
import ArkLib.OracleReduction.DecisionTail
import ArkLib.OracleReduction.Equiv
import ArkLib.OracleReduction.Execution
import ArkLib.OracleReduction.FiatShamir.Basic
import ArkLib.OracleReduction.FiatShamir.BasicCompleteness
import ArkLib.OracleReduction.FiatShamir.ChallengeOracleSampling
import ArkLib.OracleReduction.FiatShamir.CompletenessUnroll
import ArkLib.OracleReduction.FiatShamir.Desugar
import ArkLib.OracleReduction.FiatShamir.DuplexSponge
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Basic
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Defs
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Preliminaries
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.AbortAnalysis
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Backtrack
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.BadEvents
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.BadEventsPaper
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.BirthdayBound
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.BirthdayBoundPaper
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.BudgetCover
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.CacheProvenance
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Completeness
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.ConsistencyPaper
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.ConsistencyPaperCascade
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Correspondence
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.EagerFalse
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.EagerLazyDS
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Extraction
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Flag
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.ForkFalse
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.ForkPaper
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.ForkPaperFork
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Freshness
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.HashHalf
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.HashPaper
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.HonestConsistency
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.HonestConsistencyPaper
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Hyb23Bricks
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Hyb23CouplingEngine
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Hyb23FreshPath
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Hyb23StepCoupling
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Hyb23TableComap
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Hyb34LogShapeFalse
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Hyb4ChallengeEntry
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.KeyLemma
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.KeyLemmaAssembly
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.KeyLemmaFoundations
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.KeyLemmaHybrids
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.KeyLemmaSalted
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma512Honest
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma512HonestPaper
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma512Paper
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma512PaperCascade
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma514ForkFalse
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma514Paper
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma514PaperFork
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma516HashHalf
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma516Paper
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma516TimePFalse
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma58CacheProvenance
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma58Correspondence
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma58EagerFalse
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma58Extraction
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma58Flag
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma58Freshness
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lemma58Reduction
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.LiftCoherence
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lookahead
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.PaperBadEvents
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.PaperBadEventsCoincidence
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.PaperBadEventsEngine
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.ProverTransform
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Reduction
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.RunCollapse
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.RunEqHonest
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.SimulatorBudgets
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Soundness
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.TimePFalse
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.TraceDataStructures
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.TraceTransform
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.VerifierReplay
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.State
import ArkLib.OracleReduction.FiatShamir.HVZKCanonicalClose
import ArkLib.OracleReduction.FiatShamir.HVZKCoupling
import ArkLib.OracleReduction.FiatShamir.HVZKCouplingFoundations
import ArkLib.OracleReduction.FiatShamir.HVZKCouplingStep
import ArkLib.OracleReduction.FiatShamir.HVZKKernelClose
import ArkLib.OracleReduction.FiatShamir.HVZKKernelInfra
import ArkLib.OracleReduction.FiatShamir.HVZKLazyImpl
import ArkLib.OracleReduction.FiatShamir.HVZKLazyVerifier
import ArkLib.OracleReduction.FiatShamir.HVZKNoChallenge
import ArkLib.OracleReduction.FiatShamir.HVZKPerStateClose
import ArkLib.OracleReduction.FiatShamir.HVZKTransferReduction
import ArkLib.OracleReduction.FiatShamir.ProverRunCharacterization
import ArkLib.OracleReduction.FiatShamir.RunEqHonestExecution
import ArkLib.OracleReduction.FiatShamir.SingleSalt
import ArkLib.OracleReduction.FiatShamir.StateRestorationTransport
import ArkLib.OracleReduction.FiatShamir.ZKResidualBridge
import ArkLib.OracleReduction.FiatShamir.ZKTransport
import ArkLib.OracleReduction.FiatShamirRunCollapseProof
import ArkLib.OracleReduction.FullPredKSF
import ArkLib.OracleReduction.LiftContext.Coherence
import ArkLib.OracleReduction.LiftContext.HonestKnowledgeLens
import ArkLib.OracleReduction.LiftContext.Lens
import ArkLib.OracleReduction.LiftContext.OracleReduction
import ArkLib.OracleReduction.LiftContext.OracleStatementPreserving
import ArkLib.OracleReduction.LiftContext.Reduction
import ArkLib.OracleReduction.OracleInterface
import ArkLib.OracleReduction.Prelude
import ArkLib.OracleReduction.ProbOneBindCompose
import ArkLib.OracleReduction.ProcessRoundSupport
import ArkLib.OracleReduction.ProtocolSpec.Basic
import ArkLib.OracleReduction.ProtocolSpec.Cast
import ArkLib.OracleReduction.ProtocolSpec.SeqCompose
import ArkLib.OracleReduction.ProtocolSpec.TranscriptRecompose
import ArkLib.OracleReduction.RunUnroll
import ArkLib.OracleReduction.Salt
import ArkLib.OracleReduction.Security.Basic
import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness
import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Basic
import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Composition
import ArkLib.OracleReduction.Security.EchoHVZK
import ArkLib.OracleReduction.Security.Implications
import ArkLib.OracleReduction.Security.ImplicationsCore
import ArkLib.OracleReduction.Security.OracleDistribution
import ArkLib.OracleReduction.Security.OracleZeroKnowledge
import ArkLib.OracleReduction.Security.RbrKnowledgeConjoin
import ArkLib.OracleReduction.Security.RbrKnowledgeFlip
import ArkLib.OracleReduction.Security.RbrKnowledgeTruncate
import ArkLib.OracleReduction.Security.Rewinding
import ArkLib.OracleReduction.Security.RoundByRound
import ArkLib.OracleReduction.Security.RunPrefixMarginal
import ArkLib.OracleReduction.Security.SpecialSoundness
import ArkLib.OracleReduction.Security.StateRestoration
import ArkLib.OracleReduction.Security.TranscriptTree
import ArkLib.OracleReduction.Security.TranscriptTree.Basic
import ArkLib.OracleReduction.Security.TranscriptTree.Composition
import ArkLib.OracleReduction.Security.ZeroKnowledge
import ArkLib.OracleReduction.Security.ZeroKnowledgeKernel
import ArkLib.OracleReduction.SimOracleFoldlM
import ArkLib.OracleReduction.SimulateQ
import ArkLib.OracleReduction.StateCollapse
import ArkLib.OracleReduction.VectorIOR
import ArkLib.ProofSystem.BCS.ErrorAccounting
import ArkLib.ProofSystem.BCS.TransparentEndToEnd
import ArkLib.ProofSystem.BatchedFri.CosetInjectivity
import ArkLib.ProofSystem.BatchedFri.QueryRoundAnalysis
import ArkLib.ProofSystem.BatchedFri.QueryRoundProbability
import ArkLib.ProofSystem.BatchedFri.QueryRoundRSAffineLineSoundness
import ArkLib.ProofSystem.BatchedFri.QueryRoundRSCurveSoundness
import ArkLib.ProofSystem.BatchedFri.QueryRoundSoundness
import ArkLib.ProofSystem.BatchedFri.Security
import ArkLib.ProofSystem.BatchedFri.Spec.General
import ArkLib.ProofSystem.BatchedFri.Spec.SingleRound
import ArkLib.ProofSystem.Binius.BBFSmallFieldIOPCS
import ArkLib.ProofSystem.Binius.BinaryBasefold.BaseFoldDetBrick
import ArkLib.ProofSystem.Binius.BinaryBasefold.Basic
import ArkLib.ProofSystem.Binius.BinaryBasefold.BitsOfIndex
import ArkLib.ProofSystem.Binius.BinaryBasefold.Code
import ArkLib.ProofSystem.Binius.BinaryBasefold.Compliance
import ArkLib.ProofSystem.Binius.BinaryBasefold.CoreInteractionPhase
import ArkLib.ProofSystem.Binius.BinaryBasefold.ExtractMLPCorrectness
import ArkLib.ProofSystem.Binius.BinaryBasefold.FiberDependence
import ArkLib.ProofSystem.Binius.BinaryBasefold.FoldDetDischarge
import ArkLib.ProofSystem.Binius.BinaryBasefold.FoldDetSplit
import ArkLib.ProofSystem.Binius.BinaryBasefold.General
import ArkLib.ProofSystem.Binius.BinaryBasefold.MultilinearWeightRecursion
import ArkLib.ProofSystem.Binius.BinaryBasefold.Prelude
import ArkLib.ProofSystem.Binius.BinaryBasefold.QueryPhase
import ArkLib.ProofSystem.Binius.BinaryBasefold.Reconstruct.FinalConstantWeld
import ArkLib.ProofSystem.Binius.BinaryBasefold.Reconstruct.FinalOracleBridge
import ArkLib.ProofSystem.Binius.BinaryBasefold.Reconstruct.IncrementalHelpers
import ArkLib.ProofSystem.Binius.BinaryBasefold.Reconstruct.IteratedFoldAdvances
import ArkLib.ProofSystem.Binius.BinaryBasefold.Reconstruct.IteratedFoldToLevel
import ArkLib.ProofSystem.Binius.BinaryBasefold.Reconstruct.ProjectToMidLastEval
import ArkLib.ProofSystem.Binius.BinaryBasefold.Reconstruct.ProjectToMidSucc
import ArkLib.ProofSystem.Binius.BinaryBasefold.Reconstruct.ProjectToNextSumEq
import ArkLib.ProofSystem.Binius.BinaryBasefold.Reconstruct.UDRCongruence
import ArkLib.ProofSystem.Binius.BinaryBasefold.ReductionLogic
import ArkLib.ProofSystem.Binius.BinaryBasefold.Relations
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.BadBlocks
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.FoldDistance
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.Incremental
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.IncrementalCase1
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.Lift
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorClosest
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorCodeDistance
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorDisagreement
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorDistance
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorFar
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorFiber
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorHamming
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorInjectivity
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorMultilinear
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorSurjectivity
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorUDR
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.PreTensorWitness
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.QueryPhaseFirstOracle
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.QueryPhaseFoldBridge
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.QueryPhaseFoldedValue
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.QueryPhaseHelpers
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.QueryPhasePrelims
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.QueryPhaseSoundness
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.QueryPhaseSuffix
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.SoundnessCase1Bridge
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.SoundnessCase1Discharge
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.SoundnessCase2Assembly
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.SoundnessCase2Discharge
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.SoundnessCase2FarLift
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.SoundnessCase2Probability
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.SoundnessProposition
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.SuffixAlignCore
import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.SuffixFiberAlignment
import ArkLib.ProofSystem.Binius.BinaryBasefold.Spec
import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps
import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps.Commit
import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps.FinalSumcheck
import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps.Fold
import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps.Relay
import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps.VerifierDeterminism
import ArkLib.ProofSystem.Binius.FRIBinius.CoreInteractionPhase
import ArkLib.ProofSystem.Binius.FRIBinius.General
import ArkLib.ProofSystem.Binius.FRIBinius.Prelude
import ArkLib.ProofSystem.Component.CheckClaim
import ArkLib.ProofSystem.Component.DoNothing
import ArkLib.ProofSystem.Component.NoInteraction
import ArkLib.ProofSystem.Component.RandomQuery
import ArkLib.ProofSystem.Component.ReduceClaim
import ArkLib.ProofSystem.Component.SendClaim
import ArkLib.ProofSystem.Component.SendWitness
import ArkLib.ProofSystem.ConstraintSystem.Basic
import ArkLib.ProofSystem.ConstraintSystem.Examples
import ArkLib.ProofSystem.ConstraintSystem.Lookup
import ArkLib.ProofSystem.ConstraintSystem.MemoryChecking
import ArkLib.ProofSystem.ConstraintSystem.Plonk
import ArkLib.ProofSystem.ConstraintSystem.PlonkGateIdentities
import ArkLib.ProofSystem.ConstraintSystem.R1CS
import ArkLib.ProofSystem.Fri.AuxLemmas
import ArkLib.ProofSystem.Fri.Domain
import ArkLib.ProofSystem.Fri.EvenAndOdd
import ArkLib.ProofSystem.Fri.EvenAndOdd.Def
import ArkLib.ProofSystem.Fri.EvenAndOdd.Lemmas
import ArkLib.ProofSystem.Fri.PolySplit
import ArkLib.ProofSystem.Fri.RoundConsistency
import ArkLib.ProofSystem.Fri.Spec.Completeness
import ArkLib.ProofSystem.Fri.Spec.General
import ArkLib.ProofSystem.Fri.Spec.SingleRound
import ArkLib.ProofSystem.Fri.Spec.Soundness
import ArkLib.ProofSystem.Logup.Common
import ArkLib.ProofSystem.Logup.LogupGrandSumIdentity
import ArkLib.ProofSystem.Logup.Protocol
import ArkLib.ProofSystem.Logup.SZTotalDegree
import ArkLib.ProofSystem.Logup.Security.BatchingSZ
import ArkLib.ProofSystem.Logup.Security.BridgeAndAppendResiduals
import ArkLib.ProofSystem.Logup.Security.Completeness
import ArkLib.ProofSystem.Logup.Security.ConsistentClaimCore
import ArkLib.ProofSystem.Logup.Security.LogupBatchingBinding
import ArkLib.ProofSystem.Logup.Security.LogupClaimBatchAffine
import ArkLib.ProofSystem.Logup.Security.LogupClearedGrandSum
import ArkLib.ProofSystem.Logup.Security.LogupCompletenessClose
import ArkLib.ProofSystem.Logup.Security.LogupCompletenessEmptyOracle
import ArkLib.ProofSystem.Logup.Security.LogupCompletenessFinal
import ArkLib.ProofSystem.Logup.Security.LogupCompletenessMsgSeam
import ArkLib.ProofSystem.Logup.Security.LogupCompletenessUncond
import ArkLib.ProofSystem.Logup.Security.LogupCompletenessUncondSumcheck
import ArkLib.ProofSystem.Logup.Security.LogupCompletenessWired
import ArkLib.ProofSystem.Logup.Security.LogupHonestSupport
import ArkLib.ProofSystem.Logup.Security.LogupInitImplFacts
import ArkLib.ProofSystem.Logup.Security.LogupOuterCompletenessDischarge
import ArkLib.ProofSystem.Logup.Security.LogupProtocol2Status
import ArkLib.ProofSystem.Logup.Security.LogupResidualDischarge
import ArkLib.ProofSystem.Logup.Security.LogupSoundnessClose
import ArkLib.ProofSystem.Logup.Security.LogupSoundnessMsgSeam
import ArkLib.ProofSystem.Logup.Security.LogupSoundnessPointwise
import ArkLib.ProofSystem.Logup.Security.LogupSoundnessUncond