OAI/Computability/MinUncut/PCP/PoweringTableSemantics.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.RawLabeling line 10
2. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling line 13
3. def OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling line 16
4. def OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling line 20
5. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling_encodeLabeling line 24
6. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling_decodeLabeling line 30
7. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_encoded line 36
8. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_decoded line 48
9. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_eq_path line 58
10. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_encoded line 73
11. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_decoded line 83
12. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.card_darts_eq_table line 91
13. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.satisfiable_iff line 98
14. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.preserves_satisfiability line 115
15. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.path_rejection_mean_eq_table_fraction line 123
16. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap_iff line 138
17. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap line 157
18. structure OAI.MinUncutGames.Foundations.PCP.QueryIncidence.Verifier line 171
19. abbrev OAI.MinUncutGames.Foundations.PCP.QueryIncidence.Label line 175
20. abbrev OAI.MinUncutGames.Foundations.PCP.QueryIncidence.Vertex line 176
21. abbrev OAI.MinUncutGames.Foundations.PCP.QueryIncidence.Dart line 177
22. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.response line 181
23. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.zeroSlot line 184
24. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.decodeRight line 186
25. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.encodeRight line 188
26. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.decode_encodeRight line 190
27. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.canonicalSlot line 193
28. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.canonicalSlot_query line 196
29. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.RepeatedConsistent line 200
30. instance OAI.MinUncutGames.Foundations.PCP.QueryIncidence.repeatedConsistentDecidable line 203
31. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.LeftValid line 209
32. instance OAI.MinUncutGames.Foundations.PCP.QueryIncidence.leftValidDecidable line 212
33. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.incidenceAccept line 218
34. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.reverse line 223
35. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.reverse_involutive line 225
36. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.reverseEquiv line 229
37. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.tail line 235
38. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.predicate line 239
39. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.graph line 244
40. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.edgeSatisfied_eq_incidence line 254
41. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.honestLabeling line 262
42. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.honest_leftValid line 266
43. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.honest_incidence line 273
44. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.perfect_completeness line 284
45. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.satisfiable_of_verifier_satisfiable line 292
46. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.decodedAssignment line 300
47. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.incidenceAccept_true line 303
48. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.all_incidences_imply_event line 312
49. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.rejected_event_forces_slot line 327
50. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.rejectedEvents line 345
51. def OAI.MinUncutGames.Foundations.PCP.QueryIncidence.verifierRejectionCount line 348
52. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.rejection_count_bound line 351
53. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.card_label line 380
54. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.card_vertex line 383
55. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.card_dart line 387
56. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.gap_transfer line 391
57. theorem OAI.MinUncutGames.Foundations.PCP.QueryIncidence.six_query_alphabet line 406
58. def OAI.MinUncutGames.Foundations.PCP.CodeComposition.disagreement line 418
59. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.disagreement_self line 420
60. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.disagreement_nonnegative line 423
61. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.disagreement_le_one line 426
62. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.disagreement_comm line 429
63. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.disagreement_triangle line 432
64. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.disagreement_eq_sign line 436
65. def OAI.MinUncutGames.Foundations.PCP.CodeComposition.relativeDistance line 440
66. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.relativeDistance_self line 443
67. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.relativeDistance_nonnegative line 447
68. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.relativeDistance_comm line 451
69. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.relativeDistance_triangle line 455
70. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.relativeDistance_eq_sign line 461
71. def OAI.MinUncutGames.Foundations.PCP.CodeComposition.codeword line 468
72. def OAI.MinUncutGames.Foundations.PCP.CodeComposition.singletonMask line 470
73. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.walsh_singletonMask line 473
74. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.singletonMask_ne line 483
75. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.codeword_distance line 489
76. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.exists_nearest line 500
77. def OAI.MinUncutGames.Foundations.PCP.CodeComposition.nearest line 508
78. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.nearest_minimal line 511
79. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.distance_from_other_codeword line 516
80. def OAI.MinUncutGames.Foundations.PCP.CodeComposition.pairWord line 524
81. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.pairWord_distance line 527
82. theorem OAI.MinUncutGames.Foundations.PCP.CodeComposition.rejected_pair_far line 536