OAI/Computability/MinUncut/PCP/ClauseVerifier.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MinUncutGames.Foundations.PCP.ClauseAnswer line 11
2. inductive OAI.MinUncutGames.Foundations.PCP.Slot line 17
3. def OAI.MinUncutGames.Foundations.PCP.answerAt line 23
4. def OAI.MinUncutGames.Foundations.PCP.nameAt line 28
5. def OAI.MinUncutGames.Foundations.PCP.literalValue line 33
6. def OAI.MinUncutGames.Foundations.PCP.localSatisfies line 36
7. def OAI.MinUncutGames.Foundations.PCP.honestAnswer line 41
8. theorem OAI.MinUncutGames.Foundations.PCP.honest_satisfies line 45
9. theorem OAI.MinUncutGames.Foundations.PCP.honest_answerAt line 48
10. def OAI.MinUncutGames.Foundations.PCP.matchingSlots line 53
11. theorem OAI.MinUncutGames.Foundations.PCP.matchingSlots_le line 58
12. theorem OAI.MinUncutGames.Foundations.PCP.matchingSlots_eq_three line 63
13. def OAI.MinUncutGames.Foundations.PCP.acceptedSlots line 68
14. def OAI.MinUncutGames.Foundations.PCP.clauseFailure line 71
15. theorem OAI.MinUncutGames.Foundations.PCP.local_rejection_bound line 74
16. def OAI.MinUncutGames.Foundations.PCP.clauseAt line 96
17. abbrev OAI.MinUncutGames.Foundations.PCP.RandomEvent line 99
18. abbrev OAI.MinUncutGames.Foundations.PCP.AliceStrategy line 100
19. abbrev OAI.MinUncutGames.Foundations.PCP.BobStrategy line 101
20. def OAI.MinUncutGames.Foundations.PCP.accepts line 103
21. def OAI.MinUncutGames.Foundations.PCP.acceptedCount line 108
22. def OAI.MinUncutGames.Foundations.PCP.failureCount line 114
23. theorem OAI.MinUncutGames.Foundations.PCP.total_rejection_bound line 119
24. def OAI.MinUncutGames.Foundations.PCP.allIndices line 130
25. theorem OAI.MinUncutGames.Foundations.PCP.hastad_basic_verifier_soundness line 133
26. theorem OAI.MinUncutGames.Foundations.PCP.honest_accepts line 144
27. theorem OAI.MinUncutGames.Foundations.PCP.verifier_completeness line 152
28. abbrev OAI.MinUncutGames.Foundations.PCP.LeftLabel line 159
29. def OAI.MinUncutGames.Foundations.PCP.edgeProjection line 162
30. theorem OAI.MinUncutGames.Foundations.PCP.verifier_eq_projection line 165
31. def OAI.MinUncutGames.Foundations.PCP.eventsAt line 173
32. def OAI.MinUncutGames.Foundations.PCP.enumerateEvents line 176
33. theorem OAI.MinUncutGames.Foundations.PCP.length_enumerateEvents line 181
34. theorem OAI.MinUncutGames.Foundations.PCP.accepted_eventsAt line 190
35. theorem OAI.MinUncutGames.Foundations.PCP.accepted_enumerateEvents line 202
36. def OAI.MinUncutGames.Foundations.PCP.allEvents line 212
37. theorem OAI.MinUncutGames.Foundations.PCP.length_allEvents line 215
38. theorem OAI.MinUncutGames.Foundations.PCP.allEvents_nonempty line 219
39. theorem OAI.MinUncutGames.Foundations.PCP.verifier_event_soundness line 228
40. def OAI.MinUncutGames.Foundations.PCP.occurrencesAt line 238
41. def OAI.MinUncutGames.Foundations.PCP.occurrenceCount line 243
42. theorem OAI.MinUncutGames.Foundations.PCP.variable_eventsAt line 248
43. theorem OAI.MinUncutGames.Foundations.PCP.variable_enumerateEvents line 258
44. theorem OAI.MinUncutGames.Foundations.PCP.regular_bob_marginal line 269
45. def OAI.MinUncutGames.Foundations.Hastad.SourceContexts.clauseAnswerEquiv line 286
46. def OAI.MinUncutGames.Foundations.Hastad.SourceContexts.clauseAnswerFinEquiv line 292
47. instance OAI.MinUncutGames.Foundations.Hastad.SourceContexts.clauseAnswerFintype line 298
48. instance OAI.MinUncutGames.Foundations.Hastad.SourceContexts.clauseAnswerInhabited line 301
49. instance OAI.MinUncutGames.Foundations.Hastad.SourceContexts.slotFintype line 303
50. instance OAI.MinUncutGames.Foundations.Hastad.SourceContexts.slotInhabited line 307
51. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.card_clauseAnswer line 309
52. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.card_slot line 313
53. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContexts.I line 315
54. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContexts.J line 316
55. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContexts.ClauseContext line 317
56. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContexts.VariableContext line 318
57. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContexts.SlotContext line 319
58. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.card_I line 321
59. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.card_J line 322
60. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.card_ClauseContext line 323
61. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.card_VariableContext line 325
62. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.card_SlotContext line 327
63. def OAI.MinUncutGames.Foundations.Hastad.SourceContexts.localConsistent line 330
64. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.localConsistent_eq_true_iff line 334
65. def OAI.MinUncutGames.Foundations.Hastad.SourceContexts.validJ line 341
66. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.validJ_eq_true_iff line 346
67. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.validJ_satisfies line 354
68. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.validJ_consistent line 359
69. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.validJ_localConsistent line 366
70. def OAI.MinUncutGames.Foundations.Hastad.SourceContexts.canonicalSlot line 373
71. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.canonicalSlot_name line 377
72. def OAI.MinUncutGames.Foundations.Hastad.SourceContexts.pi line 389
73. def OAI.MinUncutGames.Foundations.Hastad.SourceContexts.sampledVariables line 393
74. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.sampledVariables_supported line 397
75. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.sampled_eq_pi line 402
76. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.sampled_answers_eq_of_visible_eq line 410
77. def OAI.MinUncutGames.Foundations.Hastad.SourceContexts.honestJ line 418
78. def OAI.MinUncutGames.Foundations.Hastad.SourceContexts.honestI line 422
79. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.honestJ_valid line 426
80. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.pi_honest line 438
81. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.pi_honest_sampled line 446
82. def OAI.MinUncutGames.Foundations.Hastad.SourceContexts.baseAccepts line 452
83. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.baseAccepts_eq_true_iff line 458
84. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.projection_implies_coordinate_accepts line 466
85. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.baseAccepts_implies_sampled line 473
86. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContexts.projection_implies_sampled_accepts line 483