OAI/Computability/DirectedFeedback/Games/InitialGraph.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.PCP.InitialGraph.Label line 10
2. abbrev OAI.DFVSGames.Foundations.PCP.InitialGraph.Vertex line 11
3. abbrev OAI.DFVSGames.Foundations.PCP.InitialGraph.Dart line 12
4. instance OAI.DFVSGames.Foundations.PCP.InitialGraph.slotFintype line 14
5. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.card_slot line 18
6. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.card_label line 19
7. def OAI.DFVSGames.Foundations.PCP.InitialGraph.variableVertex line 22
8. def OAI.DFVSGames.Foundations.PCP.InitialGraph.clauseVertex line 23
9. def OAI.DFVSGames.Foundations.PCP.InitialGraph.dummyVertex line 24
10. def OAI.DFVSGames.Foundations.PCP.InitialGraph.dummyDart line 25
11. instance OAI.DFVSGames.Foundations.PCP.InitialGraph.vertexNonempty line 27
12. instance OAI.DFVSGames.Foundations.PCP.InitialGraph.dartNonempty line 28
13. def OAI.DFVSGames.Foundations.PCP.InitialGraph.reverse line 30
14. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.reverse_involutive line 34
15. def OAI.DFVSGames.Foundations.PCP.InitialGraph.reverseEquiv line 40
16. def OAI.DFVSGames.Foundations.PCP.InitialGraph.tail line 46
17. def OAI.DFVSGames.Foundations.PCP.InitialGraph.toClauseAnswer line 51
18. def OAI.DFVSGames.Foundations.PCP.InitialGraph.fromClauseAnswer line 52
19. def OAI.DFVSGames.Foundations.PCP.InitialGraph.variableLabel line 53
20. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.to_fromClauseAnswer line 55
21. def OAI.DFVSGames.Foundations.PCP.InitialGraph.variableValid line 59
22. def OAI.DFVSGames.Foundations.PCP.InitialGraph.incidenceAccept line 62
23. def OAI.DFVSGames.Foundations.PCP.InitialGraph.predicate line 68
24. def OAI.DFVSGames.Foundations.PCP.InitialGraph.raw line 73
25. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.raw_forward line 84
26. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.incidenceAccept_true line 89
27. def OAI.DFVSGames.Foundations.PCP.InitialGraph.honestLabeling line 96
28. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.incidence_honest line 101
29. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.raw_completeness line 109
30. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.clauseAnswer_eq_of_slots line 118
31. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.raw_reflects line 127
32. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.raw_satisfiable_iff line 146
33. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.card_vertex line 149
34. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.card_dart line 153
35. abbrev OAI.DFVSGames.Foundations.PCP.InitialGraph.CompactVertex line 158
36. abbrev OAI.DFVSGames.Foundations.PCP.InitialGraph.CompactDart line 159
37. def OAI.DFVSGames.Foundations.PCP.InitialGraph.build line 161
38. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.build_satisfiable_iff line 164
39. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.build_vertex_bound line 168
40. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.build_dart_count line 174
41. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.build_initial_gap line 178
42. theorem OAI.DFVSGames.Foundations.PCP.InitialGraph.build_inverse_size_gap line 184
43. def OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.pullback line 198
44. theorem OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.edgeSatisfied_pullback line 205
45. theorem OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.rejectionCount_pullback line 210
46. theorem OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.satisfiable_pullback_iff line 215
47. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.Label64 line 227
48. def OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.decode64 line 229
49. def OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.encode64 line 231
50. theorem OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.decode_encode64 line 234
51. def OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.initial64 line 239
52. theorem OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.initial64_satisfiable_iff line 243
53. theorem OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.initial64_alphabet line 248
54. theorem OAI.DFVSGames.Foundations.PCP.AlphabetRetraction.initial64_inverse_size_gap line 251
55. def OAI.DFVSGames.Foundations.PCP.RawInitialTables.unitOrder line 263
56. def OAI.DFVSGames.Foundations.PCP.RawInitialTables.slotOrder line 269
57. def OAI.DFVSGames.Foundations.PCP.RawInitialTables.binaryOrder line 278
58. def OAI.DFVSGames.Foundations.PCP.RawInitialTables.labelOrder line 287
59. def OAI.DFVSGames.Foundations.PCP.RawInitialTables.vertexOrder line 289
60. def OAI.DFVSGames.Foundations.PCP.RawInitialTables.eventOrder line 293
61. def OAI.DFVSGames.Foundations.PCP.RawInitialTables.dartOrder line 296
62. def OAI.DFVSGames.Foundations.PCP.RawInitialTables.raw64 line 300
63. def OAI.DFVSGames.Foundations.PCP.RawInitialTables.table line 304
64. theorem OAI.DFVSGames.Foundations.PCP.RawInitialTables.table_vertices line 307
65. theorem OAI.DFVSGames.Foundations.PCP.RawInitialTables.table_darts line 310
66. theorem OAI.DFVSGames.Foundations.PCP.RawInitialTables.table_vertices_positive line 312
67. theorem OAI.DFVSGames.Foundations.PCP.RawInitialTables.table_darts_positive line 315
68. theorem OAI.DFVSGames.Foundations.PCP.RawInitialTables.raw64_satisfiable_iff line 318
69. theorem OAI.DFVSGames.Foundations.PCP.RawInitialTables.table_semantics line 323
70. theorem OAI.DFVSGames.Foundations.PCP.RawInitialTables.table_satisfiable_iff line 331
71. theorem OAI.DFVSGames.Foundations.PCP.RawInitialTables.initial_rejection line 337
72. theorem OAI.DFVSGames.Foundations.PCP.RawInitialTables.initial_size line 343
73. structure OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle line 354
74. instance OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeVertex line 368
75. instance OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeDart line 369
76. instance OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqVertex line 370
77. instance OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqDart line 371
78. instance OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyDart line 372
79. instance OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyVertex line 374
80. def OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph line 378
81. def OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.size line 390
82. def OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.Satisfiable line 392
83. def OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.rejectionCount line 394
84. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.size_positive line 397
85. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.dartCard_le_size line 400
86. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_graph line 403
87. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_size line 407
88. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_satisfiable line 411
89. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_rejectionCount line 415
90. def OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.minimumRejections line 422
91. def OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.gap line 424
92. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.exists_minimizer line 426
93. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.gap_nonnegative line 430
94. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.gap_le_one line 432
95. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.gap_eq_zero_iff line 434
96. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.le_gap_iff line 437
97. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.inverse_card_le_gap_of_unsatisfiable line 442
98. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.one_le_dartCard_mul_gap line 446
99. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.one_le_size_mul_gap line 452
100. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_minimumRejections line 459
101. theorem OAI.DFVSGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_gap line 463
102. def OAI.DFVSGames.Foundations.PCP.FinalConstants.alphabet line 475
103. def OAI.DFVSGames.Foundations.PCP.FinalConstants.compositionLoss line 476
104. def OAI.DFVSGames.Foundations.PCP.FinalConstants.denominator line 477
105. def OAI.DFVSGames.Foundations.PCP.FinalConstants.windowHalf line 478
106. def OAI.DFVSGames.Foundations.PCP.FinalConstants.windowSize line 479
107. def OAI.DFVSGames.Foundations.PCP.FinalConstants.smoothingScale line 480
108. def OAI.DFVSGames.Foundations.PCP.FinalConstants.endpointLength line 481
109. def OAI.DFVSGames.Foundations.PCP.FinalConstants.walkLength line 482
110. def OAI.DFVSGames.Foundations.PCP.FinalConstants.gain line 484
111. def OAI.DFVSGames.Foundations.PCP.FinalConstants.cap line 485
112. theorem OAI.DFVSGames.Foundations.PCP.FinalConstants.denominator_positive line 487
113. theorem OAI.DFVSGames.Foundations.PCP.FinalConstants.windowHalf_positive line 490
114. theorem OAI.DFVSGames.Foundations.PCP.FinalConstants.walkLength_positive line 493
115. theorem OAI.DFVSGames.Foundations.PCP.FinalConstants.gain_large line 496
116. theorem OAI.DFVSGames.Foundations.PCP.FinalConstants.cap_positive line 503
117. theorem OAI.DFVSGames.Foundations.PCP.FinalConstants.cap_le_one line 506
118. theorem OAI.DFVSGames.Foundations.PCP.FinalConstants.composed_gap line 510
119. abbrev OAI.DFVSGames.Foundations.PCP.RoundTables.BaseTable line 534
120. opaque OAI.DFVSGames.Foundations.PCP.RoundTables.fixedWalkParameter line 536
121. def OAI.DFVSGames.Foundations.PCP.RoundTables.walkParameter line 539
122. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.walkParameter_eq line 541
123. def OAI.DFVSGames.Foundations.PCP.RoundTables.alphabet line 544
124. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.alphabet_positive line 546
125. def OAI.DFVSGames.Foundations.PCP.RoundTables.powered line 550
126. def OAI.DFVSGames.Foundations.PCP.RoundTables.build line 553
127. def OAI.DFVSGames.Foundations.PCP.RoundTables.sizeFactor line 556
128. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.degree_positive line 559
129. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.dartFactor_positive line 563
130. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.sizeFactor_positive line 567
131. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.powered_vertices line 574
132. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.powered_darts line 577
133. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.build_darts_positive line 581
134. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.build_size_le line 589
135. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.build_completeness line 616
136. abbrev OAI.DFVSGames.Foundations.PCP.RoundTables.Input line 625
137. instance OAI.DFVSGames.Foundations.PCP.RoundTables.(instance at line 627) line 627
138. def OAI.DFVSGames.Foundations.PCP.RoundTables.step line 629
139. def OAI.DFVSGames.Foundations.PCP.RoundTables.initial line 632
140. def OAI.DFVSGames.Foundations.PCP.RoundTables.size line 635
141. def OAI.DFVSGames.Foundations.PCP.RoundTables.Satisfiable line 637
142. def OAI.DFVSGames.Foundations.PCP.RoundTables.gap line 639
143. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.size_positive line 641
144. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.gap_nonnegative line 644
145. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.gap_eq_zero_iff line 647
146. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.one_le_size_mul_gap line 650
147. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.initial_satisfiable_iff line 662
148. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.step_completeness line 665
149. theorem OAI.DFVSGames.Foundations.PCP.RoundTables.step_size line 668
150. def OAI.DFVSGames.Foundations.PCP.AmplificationIteration.run line 675
151. theorem OAI.DFVSGames.Foundations.PCP.AmplificationIteration.min_double_min_inline_AmplificationIteration line 679
152. theorem OAI.DFVSGames.Foundations.PCP.AmplificationIteration.run_gap line 687
153. theorem OAI.DFVSGames.Foundations.PCP.AmplificationIteration.run_preserves line 702
154. theorem OAI.DFVSGames.Foundations.PCP.AmplificationIteration.run_size line 709
155. def OAI.DFVSGames.Foundations.PCP.AmplificationIteration.rounds line 718
156. theorem OAI.DFVSGames.Foundations.PCP.AmplificationIteration.rounds_large line 720
157. theorem OAI.DFVSGames.Foundations.PCP.AmplificationIteration.rounds_power_le line 724
158. theorem OAI.DFVSGames.Foundations.PCP.AmplificationIteration.blowup_rounds_le line 729
159. theorem OAI.DFVSGames.Foundations.PCP.AmplificationIteration.run_size_polynomial line 737
160. theorem OAI.DFVSGames.Foundations.PCP.AmplificationIteration.run_reaches_cap line 744