OAI/Computability/BinPacking/PCP/Queries.lean

GitHub source file

167 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.UniformRestriction.restrict line 23
2. def OAI.BinPackingGames.Foundations.PCP.UniformRestriction.extend line 27
3. def OAI.BinPackingGames.Foundations.PCP.UniformRestriction.canonicalize line 30
4. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.restrict_apply line 33
5. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.extend_apply_of_mem line 36
6. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.extend_apply_of_not_mem line 40
7. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.restrict_extend line 44
8. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.canonicalize_apply_of_mem line 49
9. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.canonicalize_apply_of_not_mem line 53
10. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.restrict_canonicalize line 57
11. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.canonicalize_idempotent line 61
12. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.canonicalize_eq_iff line 65
13. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.expect_restrict line 75
14. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.expect_canonicalize line 91
15. theorem OAI.BinPackingGames.Foundations.PCP.UniformRestriction.expect_restrict_pair line 96
16. def OAI.BinPackingGames.Foundations.PCP.CodeComposition.disagreement line 113
17. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.disagreement_self line 115
18. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.disagreement_nonnegative line 118
19. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.disagreement_le_one line 121
20. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.disagreement_comm line 124
21. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.disagreement_triangle line 127
22. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.disagreement_eq_sign line 131
23. def OAI.BinPackingGames.Foundations.PCP.CodeComposition.relativeDistance line 135
24. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.relativeDistance_self line 138
25. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.relativeDistance_nonnegative line 142
26. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.relativeDistance_comm line 146
27. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.relativeDistance_triangle line 150
28. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.relativeDistance_eq_sign line 156
29. def OAI.BinPackingGames.Foundations.PCP.CodeComposition.codeword line 163
30. def OAI.BinPackingGames.Foundations.PCP.CodeComposition.singletonMask line 165
31. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.walsh_singletonMask line 168
32. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.singletonMask_ne line 178
33. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.codeword_distance line 184
34. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.exists_nearest line 195
35. def OAI.BinPackingGames.Foundations.PCP.CodeComposition.nearest line 203
36. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.nearest_minimal line 206
37. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.distance_from_other_codeword line 211
38. def OAI.BinPackingGames.Foundations.PCP.CodeComposition.pairWord line 219
39. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.pairWord_distance line 222
40. theorem OAI.BinPackingGames.Foundations.PCP.CodeComposition.rejected_pair_far line 231
41. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.truth line 260
42. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.disagree line 262
43. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.truth_nonneg line 264
44. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.disagree_nonneg line 266
45. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.disagree_eq line 269
46. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.disagree_xor_le line 273
47. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.parity line 277
48. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.bitSign_parity line 280
49. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.bitSign_injective line 288
50. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.parity_xor line 292
51. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.cubeXor_comm line 298
52. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.cubeXor_right_twice line 303
53. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.expect_cubeXor line 309
54. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.distance line 324
55. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.distance_nonneg line 327
56. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.distance_parity line 333
57. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.blrReject line 341
58. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.blrReject_nonneg line 344
59. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.blr_correlation line 351
60. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.blrReject_fourier line 370
61. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.blr_near_parity line 378
62. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.selfCorrect line 408
63. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.parity_selfCorrect line 411
64. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.selfCorrect_error line 416
65. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.singleMask line 430
66. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.flipAt line 432
67. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.flipAt_twice line 436
68. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.flipAt_eq_xor line 441
69. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.expect_flipAt line 445
70. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.walsh_singleMask line 450
71. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.parity_singleMask line 460
72. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.parity_flipAt line 464
73. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.cubeAnd line 469
74. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.andLawFailure line 471
75. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.andLawFailure_flipAt_second line 474
76. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.four_truth_lower line 491
77. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.parity_and_rejection line 495
78. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.truth_xor line 524
79. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.disagree_triangle line 527
80. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.and_disagree_transfer line 531
81. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.andReject line 537
82. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.unitReject line 542
83. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.inputReject line 547
84. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.testerReject line 550
85. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.andReject_nonneg line 553
86. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.unitReject_nonneg line 566
87. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.inputReject_nonneg line 572
88. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.andReject_transfer line 580
89. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.parity_zero line 604
90. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.unitReject_zero_parity line 609
91. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.parity_singleMask_eval line 622
92. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.inputReject_transfer line 627
93. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.tester_proximity_soundness line 644
94. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.selfCorrect_dictator line 692
95. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.tester_perfect_completeness line 698
96. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.eventQueries line 710
97. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.eventAccepts line 726
98. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.oracleAnswer line 732
99. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.eventReject line 735
100. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.truth_not_decide_eq line 740
101. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.eventReject_blr line 744
102. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.eventReject_and line 751
103. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.eventReject_unit line 760
104. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.eventReject_input line 771
105. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.event_perfect_completeness line 779
106. def OAI.BinPackingGames.Foundations.PCP.AssignmentTester.explicitTesterReject line 794
107. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.explicitTesterReject_eq line 798
108. theorem OAI.BinPackingGames.Foundations.PCP.AssignmentTester.explicit_proximity_soundness line 805
109. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetReduction.LegalPair line 821
110. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetReduction.InputCoordinate line 824
111. def OAI.BinPackingGames.Foundations.PCP.AlphabetReduction.pairEncoding line 826
112. def OAI.BinPackingGames.Foundations.PCP.AlphabetReduction.edgeTesterReject line 830
113. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetReduction.rejected_edge_tester_bound line 834
114. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetReduction.honest_edge_tester line 850
115. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.Address line 866
116. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.LocalEvent line 868
117. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.Event line 871
118. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.legal line 875
119. instance OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.legalDecidable line 878
120. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.restrictTape line 882
121. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.extendTape line 885
122. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.globalizeQuery line 889
123. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.verifier line 894
124. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.vertexBlock line 901
125. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.edgeOracle line 904
126. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.oracleAnswer_globalize line 909
127. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.response_eq_local line 921
128. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.eventReject line 934
129. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.eventReject_eq_local line 939
130. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.expect_prod line 952
131. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.localAverage line 957
132. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.expect_restrict_five line 960
133. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.localAverage_eq_tester line 997
134. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.average line 1015
135. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.average_eq_testers line 1020
136. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.decodedLabeling line 1029
137. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.local_gap line 1032
138. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.average_gap line 1049
139. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.expect_rejection_eq_count line 1057
140. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.average_eq_count line 1070
141. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.card_event line 1077
142. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.card_localEvent line 1082
143. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.card_address line 1089
144. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.rejection_count_bound line 1095
145. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.honestAssignment line 1122
146. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.honest_vertexBlock line 1127
147. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.honest_edgeOracle line 1131
148. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.honest_event line 1140
149. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.graph line 1152
150. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.perfect_completeness line 1157
151. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.gap_transfer line 1163
152. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraph.alphabet_card line 1189
153. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.RawQuery line 1197
154. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.LocalEvent line 1200
155. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.mask line 1202
156. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.xorTape line 1205
157. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.andTape line 1207
158. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.inputPairTape line 1209
159. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.query line 1212
160. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.globalize line 1233
161. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.mask_idempotent line 1238
162. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.mask_of_empty line 1243
163. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.query_is_masked line 1249
164. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.extendQuery line 1259
165. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.query_eq_extend_eventQueries line 1265
166. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.globalize_extendQuery line 1280
167. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Queries.globalize_query line 1290