OAI/Computability/BinPacking/CookLevin/VerifierCircuit.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.decodePairAux line 13
2. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.decodePair line 19
3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.decodePairAux_frame line 22
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.decodePair_pairBits line 32
5. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.pairBits_injective line 38
6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.pairBits_length line 43
7. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.pairEncoding line 48
8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.NPVerifier.acceptedLanguage_inNP line 53
9. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.PolynomialThreeSATReduction line 56
10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.NPVerifier.horizon line 61
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.NPVerifier.input_time_le_horizon line 65
12. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.NPVerifier.runWithinHorizon line 74
13. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.Bits line 92
14. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.selector line 94
15. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.payload line 97
16. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.pack line 100
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.selector_pack line 105
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.payload_pack line 110
19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.Valid line 116
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.valid_iff_local line 119
21. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.selectedLength line 140
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.selectedLength_eq line 143
23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.decode line 148
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.decode_length_le line 151
25. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.decode_length_eq line 154
26. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.encode line 159
27. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.selector_encode line 163
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.payload_encode line 169
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.encode_valid line 174
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.selectedLength_encode line 178
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.decode_encode line 182
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.exists_valid_iff line 193
33. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.present line 202
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.present_eq line 205
35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.witnessCell line 210
36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.witnessCell_eq_getElem? line 215
37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.witnessCell_end line 222
38. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.inputPrefix line 226
39. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.inputPrefix_length line 228
40. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.pairCell line 233
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.pairCell_eq_getElem? line 237
42. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.pairBits_decode_length_le line 245
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.pairCells_eq_stackEncoding line 252
44. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.freeInputPolynomial line 259
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.freeInputPolynomial_eval line 261
46. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.localConstraintSites line 265
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.localConstraintSites_le line 267
48. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.localConstraintPolynomial line 271
49. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.localConstraintSites_le_eval line 273
50. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.initial line 279
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.initial_control line 284
52. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.initial_state line 287
53. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.initial_input_stack line 290
54. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.initial_other_stack line 295
55. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.initial_input_cell line 300
56. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.initial_input_end line 306
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.initial_stack_length_le line 313
58. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.initial_encode line 324
59. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessEncoding.accepts_iff_valid_assignment line 331
60. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.bool_ext line 343
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_disjoin_ofFn_true line 346
62. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.selectorExpr line 357
63. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.payloadExpr line 360
64. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_selectorExpr line 363
65. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_payloadExpr line 366
66. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.nonemptyExpr line 369
67. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.clashPairExpr line 372
68. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.clashExpr line 375
69. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.validityExpr line 378
70. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_nonemptyExpr line 381
71. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_clashPairExpr line 385
72. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_clashExpr line 390
73. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_validityExpr line 395
74. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.presenceExpr line 414
75. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_presenceExpr line 418
76. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.payloadSymbolExpr line 428
77. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_payloadSymbolExpr line 433
78. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.inputCellExpr line 439
79. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_inputCellExpr line 449
80. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_selectorExpr line 465
81. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_payloadExpr line 468
82. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_mux line 471
83. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_nonemptyExpr_le line 476
84. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_clashPairExpr_le line 484
85. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_clashExpr_le line 488
86. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_validityExpr_le line 505
87. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_presenceExpr_le line 511
88. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_payloadSymbolExpr line 520
89. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_inputCellExpr_le line 525
90. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.initialCellExpr line 547
91. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_initialCellExpr line 556
92. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.initExpr line 569
93. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.eval_initExpr line 576
94. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_initialCellExpr_le line 588
95. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.size_initExpr_le line 599
96. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.validityCircuit line 611
97. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.validityCircuit_eval line 613
98. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.WitnessCircuit.validityCircuit_gates_le line 619
99. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.initializationPolynomial line 629
100. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.validationPolynomial line 632
101. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.initializationPolynomial_eval line 635
102. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.validationPolynomial_eval line 639
103. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.gatesPolynomial line 643
104. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.gatesPolynomial_eval line 651
105. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.bitsPolynomial line 663
106. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.machineGatesPolynomial line 669
107. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.machineBitsPolynomial line 674
108. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.machineGatesPolynomial_eval line 679
109. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.toFormula_bits_le line 691
110. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierBounds.toFormula_bits_le_machinePolynomial line 708
111. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.capacity line 739
112. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.capacity_pos line 742
113. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.FreeBits line 746
114. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.machineInput line 749
115. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.actualRun line 752
116. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.accepting line 755
117. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.stackCapacity_le line 758
118. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.actualRun_stack_le line 765
119. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.actualRun_stepSafe line 771
120. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.accepting_stack_le line 781
121. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.actualRun_accepting_iff line 788
122. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.Bit line 808
123. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.indexing line 811
124. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.width line 815
125. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.bitEquiv line 818
126. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.bitWire line 821
127. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.stateEncoding line 824
128. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.stateEncoding_last line 829
129. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.stateEncoding_bitWire line 834
130. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.initialExpressions line 840
131. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.stepExpressions line 846
132. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.initialExpressions_eval line 852
133. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.stepExpressions_eval line 864
134. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.initialFrame line 879
135. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.timeFrame line 883
136. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.initialFrame_eval line 887
137. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.timeFrame_validity line 896
138. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.timeFrame_eval line 911
139. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.mismatchExpr line 929
140. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.acceptanceExpr line 934
141. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.mismatchExpr_eval line 938
142. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.acceptanceExpr_eval line 947
143. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.acceptanceExpr_stateEncoding line 981
144. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier line 998
145. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_inputs line 1002
146. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_eval line 1005
147. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_accepts_iff line 1012
148. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_correct line 1035
149. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.mismatchExpr_size_le line 1041
150. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.acceptanceExpr_size_le line 1046
151. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.stepExpressions_size_le line 1056
152. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.initialExpressions_cost_le line 1065
153. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_gate_count line 1081
154. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_gates_le line 1095
155. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.widthPolynomial line 1107
156. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.widthPolynomial_eval line 1112
157. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.gatePolynomial line 1117
158. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.formulaPolynomial line 1123
159. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_gates_le_polynomial line 1129
160. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_formulaBits_length_le line 1137