OAI/Computability/BinPacking/PCP/BinaryFormula.lean

GitHub source file

205 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BinPackingGames.Foundations.PCP.ClauseAnswer line 11
2. inductive OAI.BinPackingGames.Foundations.PCP.Slot line 17
3. def OAI.BinPackingGames.Foundations.PCP.answerAt line 23
4. def OAI.BinPackingGames.Foundations.PCP.nameAt line 28
5. def OAI.BinPackingGames.Foundations.PCP.literalValue line 33
6. def OAI.BinPackingGames.Foundations.PCP.localSatisfies line 36
7. def OAI.BinPackingGames.Foundations.PCP.honestAnswer line 41
8. theorem OAI.BinPackingGames.Foundations.PCP.honest_satisfies line 45
9. theorem OAI.BinPackingGames.Foundations.PCP.honest_answerAt line 48
10. def OAI.BinPackingGames.Foundations.PCP.matchingSlots line 53
11. theorem OAI.BinPackingGames.Foundations.PCP.matchingSlots_le line 58
12. theorem OAI.BinPackingGames.Foundations.PCP.matchingSlots_eq_three line 63
13. def OAI.BinPackingGames.Foundations.PCP.acceptedSlots line 68
14. def OAI.BinPackingGames.Foundations.PCP.clauseFailure line 71
15. theorem OAI.BinPackingGames.Foundations.PCP.local_rejection_bound line 74
16. def OAI.BinPackingGames.Foundations.PCP.clauseAt line 96
17. abbrev OAI.BinPackingGames.Foundations.PCP.RandomEvent line 99
18. abbrev OAI.BinPackingGames.Foundations.PCP.AliceStrategy line 100
19. abbrev OAI.BinPackingGames.Foundations.PCP.BobStrategy line 101
20. def OAI.BinPackingGames.Foundations.PCP.accepts line 103
21. def OAI.BinPackingGames.Foundations.PCP.acceptedCount line 108
22. def OAI.BinPackingGames.Foundations.PCP.failureCount line 114
23. theorem OAI.BinPackingGames.Foundations.PCP.total_rejection_bound line 119
24. def OAI.BinPackingGames.Foundations.PCP.allIndices line 130
25. theorem OAI.BinPackingGames.Foundations.PCP.hastad_basic_verifier_soundness line 133
26. theorem OAI.BinPackingGames.Foundations.PCP.honest_accepts line 144
27. theorem OAI.BinPackingGames.Foundations.PCP.verifier_completeness line 152
28. abbrev OAI.BinPackingGames.Foundations.PCP.LeftLabel line 159
29. def OAI.BinPackingGames.Foundations.PCP.edgeProjection line 162
30. theorem OAI.BinPackingGames.Foundations.PCP.verifier_eq_projection line 165
31. def OAI.BinPackingGames.Foundations.PCP.eventsAt line 173
32. def OAI.BinPackingGames.Foundations.PCP.enumerateEvents line 176
33. theorem OAI.BinPackingGames.Foundations.PCP.length_enumerateEvents line 181
34. theorem OAI.BinPackingGames.Foundations.PCP.accepted_eventsAt line 190
35. theorem OAI.BinPackingGames.Foundations.PCP.accepted_enumerateEvents line 202
36. def OAI.BinPackingGames.Foundations.PCP.allEvents line 212
37. theorem OAI.BinPackingGames.Foundations.PCP.length_allEvents line 215
38. theorem OAI.BinPackingGames.Foundations.PCP.allEvents_nonempty line 219
39. theorem OAI.BinPackingGames.Foundations.PCP.verifier_event_soundness line 228
40. def OAI.BinPackingGames.Foundations.PCP.occurrencesAt line 238
41. def OAI.BinPackingGames.Foundations.PCP.occurrenceCount line 243
42. theorem OAI.BinPackingGames.Foundations.PCP.variable_eventsAt line 248
43. theorem OAI.BinPackingGames.Foundations.PCP.variable_enumerateEvents line 258
44. theorem OAI.BinPackingGames.Foundations.PCP.regular_bob_marginal line 269
45. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.clauseNames line 284
46. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.sourceNames line 287
47. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.activeNames line 290
48. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.literal_mem_active line 293
49. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.compactIndex line 302
50. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.decodeName line 306
51. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.compactLiteral line 309
52. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.compactClause line 313
53. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.compactClauses line 319
54. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.compact line 322
55. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.restrictAssignment line 326
56. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.extendAssignment line 329
57. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.decode_compactIndex line 333
58. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.eval_compact_restrict line 337
59. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.eval_compact_extend line 343
60. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.map_attach_val line 353
61. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.evaluationList line 357
62. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.satisfiedCount line 360
63. def OAI.BinPackingGames.Foundations.PCP.NameCompaction.failedCount line 363
64. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.evaluationList_restrict line 366
65. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.evaluationList_extend line 372
66. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.satisfiedCount_restrict line 383
67. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.failedCount_restrict line 387
68. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.satisfiedCount_extend line 391
69. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.failedCount_extend line 395
70. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.clauseNames_flat_length line 399
71. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.compact_clause_count line 408
72. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.length_eraseDups_le line 412
73. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.compact_active_bound line 426
74. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.compact_completeness line 431
75. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.compact_reflects line 440
76. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.compact_satisfiable_iff line 451
77. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.compact_preserves_gap line 455
78. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.compact_encoding_bound line 462
79. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.failureCount_evaluations line 480
80. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.evaluations_allIndices line 490
81. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.verifier_failureCount line 498
82. theorem OAI.BinPackingGames.Foundations.PCP.NameCompaction.compact_verifier_soundness line 503
83. abbrev OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.BoolTriple line 523
84. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.tripleValue line 525
85. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.chainView line 527
86. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.fillBits line 532
87. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.chainView_length line 540
88. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.chainView_sound line 564
89. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.fillBits_length line 591
90. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.fillBits_correct line 607
91. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.zero_false_count_iff_all line 626
92. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.chainView_failed line 632
93. abbrev OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.Pattern line 644
94. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.patterns line 646
95. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.flatMap_pair_length line 650
96. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.patterns_length line 659
97. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.mem_patterns line 666
98. abbrev OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.PatternIndex line 687
99. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.patternAt line 688
100. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.patternAt_surjective line 690
101. structure OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.FiniteVerifier line 695
102. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.eventValue line 701
103. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.rejectedEventCount line 704
104. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.auxiliaryCount line 707
105. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.outputVariables line 710
106. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.oldIndex line 712
107. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.freshIndex line 715
108. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.freshIndex_value line 719
109. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.liftLiteral line 725
110. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral line 728
111. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.forbiddenClause line 732
112. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.auxiliaryNames line 736
113. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.splitLong line 740
114. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.tautology line 746
115. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.block line 751
116. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.eventBlock line 756
117. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.convert line 760
118. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.clauseFailures line 764
119. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.splitLong_values line 767
120. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.splitLong_length line 790
121. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.restrictAssignment line 799
122. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.mismatchBits line 803
123. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.mismatchBits_length line 807
124. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral_false line 811
125. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.forbiddenClause_values line 817
126. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.mismatchBits_false line 824
127. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.mismatchBits_true line 834
128. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.mismatchFill_length line 853
129. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.mismatchFill line 860
130. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.extendAssignment line 867
131. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.extend_old line 874
132. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.extend_fresh line 879
133. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.restrict_extend line 887
134. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.ofFn_getElem_of_length line 892
135. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.extended_auxiliary_values line 897
136. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.tautology_satisfied line 903
137. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.block_length line 908
138. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.block_honest line 921
139. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.length_flatMap_constant line 937
140. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.eventBlock_length line 948
141. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.convert_clause_count line 953
142. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.convert_nonempty line 959
143. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.convert_completeness line 968
144. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.clauseFailures_append line 976
145. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.clauseFailures_le_flatMap line 980
146. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.block_failed line 994
147. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.eventBlock_failed line 1011
148. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.count_false_map_sum line 1023
149. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.clauseFailures_flatMap line 1029
150. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.nat_sum_map_le line 1037
151. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.convert_count_bridge line 1045
152. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.convert_gap line 1058
153. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.twelve_query_factor line 1073
154. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.twelve_query_clause_count line 1075
155. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.padLiteral line 1079
156. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.padClause line 1082
157. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.padTautology line 1085
158. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.padInput line 1089
159. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.padClause_eval line 1093
160. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.padTautology_satisfied line 1096
161. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.padInput_satisfiable_iff line 1100
162. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.padInput_clause_count line 1121
163. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.padInput_nonempty line 1124
164. def OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.prepareInput line 1130
165. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.prepareInput_satisfiable_iff line 1132
166. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.prepareInput_clause_count line 1136
167. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.prepareInput_nonempty line 1140
168. theorem OAI.BinPackingGames.Foundations.PCP.VerifierToCNF.prepareInput_variable_bound line 1146
169. structure OAI.BinPackingCompleteness.BinaryFormula.Literal line 1156
170. def OAI.BinPackingCompleteness.BinaryFormula.Literal.eval line 1161
171. abbrev OAI.BinPackingCompleteness.BinaryFormula.Clause line 1164
172. def OAI.BinPackingCompleteness.BinaryFormula.Clause.eval line 1166
173. structure OAI.BinPackingCompleteness.BinaryFormula.Formula line 1169
174. def OAI.BinPackingCompleteness.BinaryFormula.Formula.Satisfiable line 1172
175. def OAI.BinPackingCompleteness.BinaryFormula.clauseNames line 1175
176. def OAI.BinPackingCompleteness.BinaryFormula.sourceNames line 1178
177. def OAI.BinPackingCompleteness.BinaryFormula.activeNames line 1181
178. theorem OAI.BinPackingCompleteness.BinaryFormula.literal_mem_active line 1184
179. def OAI.BinPackingCompleteness.BinaryFormula.compactIndex line 1192
180. def OAI.BinPackingCompleteness.BinaryFormula.decodeName line 1196
181. def OAI.BinPackingCompleteness.BinaryFormula.compactLiteral line 1199
182. def OAI.BinPackingCompleteness.BinaryFormula.compactClause line 1203
183. def OAI.BinPackingCompleteness.BinaryFormula.compactClauses line 1209
184. def OAI.BinPackingCompleteness.BinaryFormula.dense line 1212
185. def OAI.BinPackingCompleteness.BinaryFormula.restrictAssignment line 1216
186. def OAI.BinPackingCompleteness.BinaryFormula.extendAssignment line 1219
187. theorem OAI.BinPackingCompleteness.BinaryFormula.decode_compactIndex line 1223
188. theorem OAI.BinPackingCompleteness.BinaryFormula.compactIndex_injective line 1227
189. theorem OAI.BinPackingCompleteness.BinaryFormula.compactLiteral_positive line 1233
190. theorem OAI.BinPackingCompleteness.BinaryFormula.eval_compact_restrict line 1236
191. theorem OAI.BinPackingCompleteness.BinaryFormula.eval_compact_extend line 1242
192. def OAI.BinPackingCompleteness.BinaryFormula.evaluationList line 1252
193. theorem OAI.BinPackingCompleteness.BinaryFormula.evaluationList_restrict line 1255
194. theorem OAI.BinPackingCompleteness.BinaryFormula.evaluationList_extend line 1263
195. def OAI.BinPackingCompleteness.BinaryFormula.failedCount line 1277
196. theorem OAI.BinPackingCompleteness.BinaryFormula.failedCount_restrict line 1280
197. theorem OAI.BinPackingCompleteness.BinaryFormula.failedCount_extend line 1284
198. theorem OAI.BinPackingCompleteness.BinaryFormula.clauseNames_flat_length line 1288
199. theorem OAI.BinPackingCompleteness.BinaryFormula.dense_clause_count line 1297
200. theorem OAI.BinPackingCompleteness.BinaryFormula.dense_variable_bound line 1301
201. theorem OAI.BinPackingCompleteness.BinaryFormula.dense_completeness line 1306
202. theorem OAI.BinPackingCompleteness.BinaryFormula.dense_reflects line 1315
203. theorem OAI.BinPackingCompleteness.BinaryFormula.dense_satisfiable_iff line 1325
204. theorem OAI.BinPackingCompleteness.BinaryFormula.dense_preserves_gap line 1329
205. theorem OAI.BinPackingCompleteness.BinaryFormula.dense_encoding_bound line 1336