OAI/Computability/MinUncut/PCP/RawInitialTables.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.PCP.RawInitialTables.unitOrder line 13
2. def OAI.MinUncutGames.Foundations.PCP.RawInitialTables.slotOrder line 19
3. def OAI.MinUncutGames.Foundations.PCP.RawInitialTables.binaryOrder line 28
4. def OAI.MinUncutGames.Foundations.PCP.RawInitialTables.labelOrder line 37
5. def OAI.MinUncutGames.Foundations.PCP.RawInitialTables.vertexOrder line 39
6. def OAI.MinUncutGames.Foundations.PCP.RawInitialTables.eventOrder line 43
7. def OAI.MinUncutGames.Foundations.PCP.RawInitialTables.dartOrder line 46
8. def OAI.MinUncutGames.Foundations.PCP.RawInitialTables.raw64 line 50
9. def OAI.MinUncutGames.Foundations.PCP.RawInitialTables.table line 54
10. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialTables.table_vertices line 57
11. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialTables.table_darts line 60
12. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialTables.table_vertices_positive line 62
13. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialTables.table_darts_positive line 65
14. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialTables.raw64_satisfiable_iff line 68
15. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialTables.table_semantics line 73
16. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialTables.table_satisfiable_iff line 81
17. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialTables.initial_rejection line 87
18. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialTables.initial_size line 93
19. structure OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle line 106
20. instance OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeVertex line 120
21. instance OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeDart line 121
22. instance OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqVertex line 122
23. instance OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqDart line 123
24. instance OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyDart line 124
25. instance OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyVertex line 126
26. def OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph line 130
27. def OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.size line 142
28. def OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.Satisfiable line 144
29. def OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.rejectionCount line 146
30. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.size_positive line 149
31. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.dartCard_le_size line 152
32. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_graph line 155
33. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_size line 159
34. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_satisfiable line 163
35. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_rejectionCount line 167
36. def OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.minimumRejections line 176
37. def OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.gap line 178
38. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.exists_minimizer line 180
39. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.gap_nonnegative line 184
40. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.gap_le_one line 186
41. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.gap_eq_zero_iff line 188
42. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.le_gap_iff line 191
43. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.inverse_card_le_gap_of_unsatisfiable line 196
44. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.one_le_dartCard_mul_gap line 200
45. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.one_le_size_mul_gap line 206
46. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_minimumRejections line 213
47. theorem OAI.MinUncutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_gap line 217
48. def OAI.MinUncutGames.Foundations.PCP.FinalConstants.alphabet line 232
49. def OAI.MinUncutGames.Foundations.PCP.FinalConstants.compositionLoss line 233
50. def OAI.MinUncutGames.Foundations.PCP.FinalConstants.denominator line 234
51. def OAI.MinUncutGames.Foundations.PCP.FinalConstants.windowHalf line 235
52. def OAI.MinUncutGames.Foundations.PCP.FinalConstants.windowSize line 236
53. def OAI.MinUncutGames.Foundations.PCP.FinalConstants.smoothingScale line 237
54. def OAI.MinUncutGames.Foundations.PCP.FinalConstants.endpointLength line 238
55. def OAI.MinUncutGames.Foundations.PCP.FinalConstants.walkLength line 239
56. def OAI.MinUncutGames.Foundations.PCP.FinalConstants.gain line 241
57. def OAI.MinUncutGames.Foundations.PCP.FinalConstants.cap line 242
58. theorem OAI.MinUncutGames.Foundations.PCP.FinalConstants.denominator_positive line 244
59. theorem OAI.MinUncutGames.Foundations.PCP.FinalConstants.windowHalf_positive line 247
60. theorem OAI.MinUncutGames.Foundations.PCP.FinalConstants.walkLength_positive line 250
61. theorem OAI.MinUncutGames.Foundations.PCP.FinalConstants.gain_large line 253
62. theorem OAI.MinUncutGames.Foundations.PCP.FinalConstants.cap_positive line 260
63. theorem OAI.MinUncutGames.Foundations.PCP.FinalConstants.cap_le_one line 263
64. theorem OAI.MinUncutGames.Foundations.PCP.FinalConstants.composed_gap line 267
65. abbrev OAI.MinUncutGames.Foundations.PCP.RoundTables.BaseTable line 293
66. opaque OAI.MinUncutGames.Foundations.PCP.RoundTables.fixedWalkParameter line 295
67. def OAI.MinUncutGames.Foundations.PCP.RoundTables.walkParameter line 298
68. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.walkParameter_eq line 300
69. def OAI.MinUncutGames.Foundations.PCP.RoundTables.alphabet line 303
70. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.alphabet_positive line 305
71. def OAI.MinUncutGames.Foundations.PCP.RoundTables.powered line 309
72. def OAI.MinUncutGames.Foundations.PCP.RoundTables.build line 312
73. def OAI.MinUncutGames.Foundations.PCP.RoundTables.sizeFactor line 315
74. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.degree_positive line 318
75. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.dartFactor_positive line 322
76. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.sizeFactor_positive line 326
77. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.powered_vertices line 333
78. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.powered_darts line 336
79. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.build_darts_positive line 340
80. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.build_size_le line 348
81. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.build_completeness line 375
82. abbrev OAI.MinUncutGames.Foundations.PCP.RoundTables.Input line 384
83. instance OAI.MinUncutGames.Foundations.PCP.RoundTables.(instance at line 386) line 386
84. def OAI.MinUncutGames.Foundations.PCP.RoundTables.step line 388
85. def OAI.MinUncutGames.Foundations.PCP.RoundTables.initial line 391
86. def OAI.MinUncutGames.Foundations.PCP.RoundTables.size line 394
87. def OAI.MinUncutGames.Foundations.PCP.RoundTables.Satisfiable line 396
88. def OAI.MinUncutGames.Foundations.PCP.RoundTables.gap line 398
89. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.size_positive line 400
90. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.gap_nonnegative line 403
91. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.gap_eq_zero_iff line 406
92. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.one_le_size_mul_gap line 409
93. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.initial_satisfiable_iff line 421
94. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.step_completeness line 424
95. theorem OAI.MinUncutGames.Foundations.PCP.RoundTables.step_size line 427
96. def OAI.MinUncutGames.Foundations.PCP.AmplificationIteration.run line 436
97. theorem OAI.MinUncutGames.Foundations.PCP.AmplificationIteration.min_double_min line 440
98. theorem OAI.MinUncutGames.Foundations.PCP.AmplificationIteration.run_gap line 448
99. theorem OAI.MinUncutGames.Foundations.PCP.AmplificationIteration.run_preserves line 463
100. theorem OAI.MinUncutGames.Foundations.PCP.AmplificationIteration.run_size line 470
101. def OAI.MinUncutGames.Foundations.PCP.AmplificationIteration.rounds line 479
102. theorem OAI.MinUncutGames.Foundations.PCP.AmplificationIteration.rounds_large line 481
103. theorem OAI.MinUncutGames.Foundations.PCP.AmplificationIteration.rounds_power_le line 485
104. theorem OAI.MinUncutGames.Foundations.PCP.AmplificationIteration.blowup_rounds_le line 490
105. theorem OAI.MinUncutGames.Foundations.PCP.AmplificationIteration.run_size_polynomial line 498
106. theorem OAI.MinUncutGames.Foundations.PCP.AmplificationIteration.run_reaches_cap line 505
107. abbrev OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.BoolTriple line 525
108. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.tripleValue line 527
109. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.chainView line 529
110. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.fillBits line 534
111. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.chainView_length line 542
112. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.chainView_sound line 566
113. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.fillBits_length line 593
114. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.fillBits_correct line 609
115. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.zero_false_count_iff_all line 628
116. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.chainView_failed line 634
117. abbrev OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.Pattern line 646
118. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.patterns line 648
119. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.flatMap_pair_length line 652
120. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.patterns_length line 661
121. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.mem_patterns line 668
122. abbrev OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.PatternIndex line 689
123. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.patternAt line 690
124. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.patternAt_surjective line 692
125. structure OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.FiniteVerifier line 697
126. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.eventValue line 703
127. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.rejectedEventCount line 706
128. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.auxiliaryCount line 709
129. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.outputVariables line 712
130. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.oldIndex line 714
131. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.freshIndex line 717
132. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.freshIndex_value line 721
133. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.liftLiteral line 727
134. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral line 730
135. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.forbiddenClause line 734
136. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.auxiliaryNames line 738
137. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.splitLong line 742
138. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.tautology line 748
139. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.block line 753
140. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.eventBlock line 758
141. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.convert line 762
142. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.clauseFailures line 766
143. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.splitLong_values line 769
144. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.splitLong_length line 792
145. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.restrictAssignment line 801
146. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.mismatchBits line 805
147. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.mismatchBits_length line 809
148. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral_false line 813
149. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.forbiddenClause_values line 819
150. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.mismatchBits_false line 826
151. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.mismatchBits_true line 836
152. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.mismatchFill_length line 855
153. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.mismatchFill line 862
154. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.extendAssignment line 869
155. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.extend_old line 876
156. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.extend_fresh line 881
157. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.restrict_extend line 889
158. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.ofFn_getElem_of_length line 894
159. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.extended_auxiliary_values line 899
160. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.tautology_satisfied line 905
161. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.block_length line 910
162. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.block_honest line 923
163. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.length_flatMap_constant line 939
164. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.eventBlock_length line 950
165. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.convert_clause_count line 955
166. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.convert_nonempty line 961
167. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.convert_completeness line 970
168. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.clauseFailures_append line 978
169. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.clauseFailures_le_flatMap line 982
170. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.block_failed line 996
171. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.eventBlock_failed line 1013
172. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.count_false_map_sum line 1025
173. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.clauseFailures_flatMap line 1031
174. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.nat_sum_map_le line 1039
175. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.convert_count_bridge line 1047
176. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.convert_gap line 1060
177. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.twelve_query_factor line 1075
178. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.twelve_query_clause_count line 1077
179. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.padLiteral line 1081
180. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.padClause line 1084
181. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.padTautology line 1087
182. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.padInput line 1091
183. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.padClause_eval line 1095
184. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.padTautology_satisfied line 1098
185. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.padInput_satisfiable_iff line 1102
186. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.padInput_clause_count line 1123
187. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.padInput_nonempty line 1126
188. def OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.prepareInput line 1132
189. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.prepareInput_satisfiable_iff line 1134
190. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.prepareInput_clause_count line 1138
191. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.prepareInput_nonempty line 1142
192. theorem OAI.MinUncutGames.Foundations.PCP.VerifierToCNF.prepareInput_variable_bound line 1148