OAI/Computability/BinPacking/PCP/AlphabetRetraction.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BinPackingGames.Foundations.PCP.QueryIncidence.Verifier line 13
2. abbrev OAI.BinPackingGames.Foundations.PCP.QueryIncidence.Label line 17
3. abbrev OAI.BinPackingGames.Foundations.PCP.QueryIncidence.Vertex line 18
4. abbrev OAI.BinPackingGames.Foundations.PCP.QueryIncidence.Dart line 19
5. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.response line 23
6. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.zeroSlot line 26
7. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.decodeRight line 28
8. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.encodeRight line 30
9. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.decode_encodeRight line 32
10. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.canonicalSlot line 35
11. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.canonicalSlot_query line 38
12. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.RepeatedConsistent line 42
13. instance OAI.BinPackingGames.Foundations.PCP.QueryIncidence.repeatedConsistentDecidable line 45
14. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.LeftValid line 51
15. instance OAI.BinPackingGames.Foundations.PCP.QueryIncidence.leftValidDecidable line 54
16. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.incidenceAccept line 60
17. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.reverse line 65
18. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.reverse_involutive line 67
19. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.reverseEquiv line 71
20. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.tail line 77
21. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.predicate line 81
22. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.graph line 86
23. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.edgeSatisfied_eq_incidence line 96
24. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.honestLabeling line 104
25. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.honest_leftValid line 108
26. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.honest_incidence line 115
27. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.perfect_completeness line 126
28. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.satisfiable_of_verifier_satisfiable line 134
29. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.decodedAssignment line 142
30. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.incidenceAccept_true line 145
31. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.all_incidences_imply_event line 154
32. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.rejected_event_forces_slot line 169
33. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.rejectedEvents line 187
34. def OAI.BinPackingGames.Foundations.PCP.QueryIncidence.verifierRejectionCount line 190
35. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.rejection_count_bound line 193
36. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.card_label line 222
37. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.card_vertex line 225
38. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.card_dart line 229
39. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.gap_transfer line 233
40. theorem OAI.BinPackingGames.Foundations.PCP.QueryIncidence.six_query_alphabet line 248
41. abbrev OAI.BinPackingGames.Foundations.PCP.InitialGraph.Label line 257
42. abbrev OAI.BinPackingGames.Foundations.PCP.InitialGraph.Vertex line 258
43. abbrev OAI.BinPackingGames.Foundations.PCP.InitialGraph.Dart line 259
44. instance OAI.BinPackingGames.Foundations.PCP.InitialGraph.slotFintype line 261
45. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.card_slot line 265
46. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.card_label line 266
47. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.variableVertex line 269
48. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.clauseVertex line 270
49. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.dummyVertex line 271
50. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.dummyDart line 272
51. instance OAI.BinPackingGames.Foundations.PCP.InitialGraph.vertexNonempty line 274
52. instance OAI.BinPackingGames.Foundations.PCP.InitialGraph.dartNonempty line 275
53. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.reverse line 277
54. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.reverse_involutive line 281
55. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.reverseEquiv line 287
56. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.tail line 293
57. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.toClauseAnswer line 298
58. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.fromClauseAnswer line 299
59. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.variableLabel line 300
60. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.to_fromClauseAnswer line 302
61. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.variableValid line 306
62. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.incidenceAccept line 309
63. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.predicate line 315
64. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.raw line 320
65. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.raw_forward line 331
66. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.incidenceAccept_true line 336
67. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.honestLabeling line 343
68. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.incidence_honest line 348
69. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.raw_completeness line 356
70. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.clauseAnswer_eq_of_slots line 365
71. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.raw_reflects line 374
72. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.raw_satisfiable_iff line 393
73. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.card_vertex line 396
74. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.card_dart line 400
75. abbrev OAI.BinPackingGames.Foundations.PCP.InitialGraph.CompactVertex line 405
76. abbrev OAI.BinPackingGames.Foundations.PCP.InitialGraph.CompactDart line 406
77. def OAI.BinPackingGames.Foundations.PCP.InitialGraph.build line 408
78. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.build_satisfiable_iff line 411
79. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.build_vertex_bound line 415
80. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.build_dart_count line 421
81. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.build_initial_gap line 425
82. theorem OAI.BinPackingGames.Foundations.PCP.InitialGraph.build_inverse_size_gap line 431
83. def OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.pullback line 445
84. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.edgeSatisfied_pullback line 452
85. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.rejectionCount_pullback line 457
86. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.satisfiable_pullback_iff line 462
87. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.Label64 line 474
88. def OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.decode64 line 476
89. def OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.encode64 line 478
90. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.decode_encode64 line 481
91. def OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.initial64 line 486
92. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.initial64_satisfiable_iff line 490
93. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.initial64_alphabet line 495
94. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetRetraction.initial64_inverse_size_gap line 498