OAI/Computability/UniqueGames/PCP/ClauseVerifierLemmas.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniqueGamesTheorem.Foundations.PCP.ClauseAnswer line 13
2. inductive OAI.UniqueGamesTheorem.Foundations.PCP.Slot line 19
3. def OAI.UniqueGamesTheorem.Foundations.PCP.answerAt line 25
4. def OAI.UniqueGamesTheorem.Foundations.PCP.nameAt line 30
5. def OAI.UniqueGamesTheorem.Foundations.PCP.literalValue line 35
6. def OAI.UniqueGamesTheorem.Foundations.PCP.localSatisfies line 38
7. def OAI.UniqueGamesTheorem.Foundations.PCP.honestAnswer line 43
8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.honest_satisfies line 47
9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.honest_answerAt line 50
10. def OAI.UniqueGamesTheorem.Foundations.PCP.matchingSlots line 55
11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.matchingSlots_le line 60
12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.matchingSlots_eq_three line 65
13. def OAI.UniqueGamesTheorem.Foundations.PCP.acceptedSlots line 70
14. def OAI.UniqueGamesTheorem.Foundations.PCP.clauseFailure line 73
15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.local_rejection_bound line 77

    Source documentation

    A failed Bob clause forces one rejection among its three incidence events.

    theorem local_rejection_bound {n : Nat} (clause : Clause n) (alice : ClauseAnswer)
        (bob : Fin n → Bool) :
        acceptedSlots clause alice (honestAnswer clause bob) + clauseFailure clause bob ≤ 3 := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ClauseAnswer, OAI.UniqueGamesTheorem.Foundations.PCP.acceptedSlots, OAI.UniqueGamesTheorem.Foundations.PCP.honestAnswer, OAI.UniqueGamesTheorem.Foundations.PCP.clauseFailure

16. def OAI.UniqueGamesTheorem.Foundations.PCP.clauseAt line 99
17. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.RandomEvent line 102
18. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AliceStrategy line 103
19. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.BobStrategy line 104
20. def OAI.UniqueGamesTheorem.Foundations.PCP.accepts line 108

    Source documentation

    Explicit finite verifier. The occurrence and slot are randomness, never an additional argument supplied to Bob's strategy.

    def accepts (formula : Formula) (alice : AliceStrategy formula) (bob : BobStrategy formula)
        (event : RandomEvent formula) : Bool :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AliceStrategy, OAI.UniqueGamesTheorem.Foundations.PCP.BobStrategy, OAI.UniqueGamesTheorem.Foundations.PCP.RandomEvent

21. def OAI.UniqueGamesTheorem.Foundations.PCP.acceptedCount line 113
22. def OAI.UniqueGamesTheorem.Foundations.PCP.failureCount line 119
23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.total_rejection_bound line 124
24. def OAI.UniqueGamesTheorem.Foundations.PCP.allIndices line 135
25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.hastad_basic_verifier_soundness line 140

    Source documentation

    Count form of Håstad Lemma 3.1: a fraction a/b of failed clauses gives a fraction at least a/(3*b) of failed verifier events.

    theorem hastad_basic_verifier_soundness (formula : Formula) (a b : Nat)
        (sourceGap : ∀ bob : BobStrategy formula,
          a * formula.clauses.length ≤ b * failureCount formula bob (allIndices formula))
        (alice : AliceStrategy formula) (bob : BobStrategy formula) :
        b * acceptedCount formula alice bob (allIndices formula) + a * formula.clauses.length ≤
          b * (3 * formula.clauses.length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.BobStrategy, OAI.UniqueGamesTheorem.Foundations.PCP.failureCount, OAI.UniqueGamesTheorem.Foundations.PCP.allIndices, OAI.UniqueGamesTheorem.Foundations.PCP.AliceStrategy, OAI.UniqueGamesTheorem.Foundations.PCP.acceptedCount

26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.honest_accepts line 151
27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.verifier_completeness line 160

    Source documentation

    Pointwise perfect completeness, including the exact input syntax.

    theorem verifier_completeness (formula : Formula) (sat : formula.Satisfiable) :
        ∃ (alice : AliceStrategy formula) (bob : BobStrategy formula),
          ∀ event : RandomEvent formula, accepts formula alice bob event = true := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AliceStrategy, OAI.UniqueGamesTheorem.Foundations.PCP.BobStrategy, OAI.UniqueGamesTheorem.Foundations.PCP.RandomEvent, OAI.UniqueGamesTheorem.Foundations.PCP.accepts

28. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.LeftLabel line 169

    Source documentation

    The valid left labels and projection maps give the concrete Label Cover presentation. Their alphabet depends on the clause, with at most 8 bit triples.

    abbrev LeftLabel (formula : Formula) (i : Fin formula.clauses.length) :=
    …

29. def OAI.UniqueGamesTheorem.Foundations.PCP.edgeProjection line 172
30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.verifier_eq_projection line 175
31. def OAI.UniqueGamesTheorem.Foundations.PCP.eventsAt line 184

    Source documentation

    A materialized list of all three slot events at an occurrence.

    def eventsAt (formula : Formula) (i : Fin formula.clauses.length) : List (RandomEvent formula) :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.RandomEvent

32. def OAI.UniqueGamesTheorem.Foundations.PCP.enumerateEvents line 187
33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.length_enumerateEvents line 192
34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.accepted_eventsAt line 201
35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.accepted_enumerateEvents line 215

    Source documentation

    The rejection-count proof counts exactly the explicit verifier's accepted random events; it is not a separate abstract score.

    theorem accepted_enumerateEvents (formula : Formula) (alice : AliceStrategy formula)
        (bob : BobStrategy formula) (indices : List (Fin formula.clauses.length)) :
        ((enumerateEvents formula indices).filter (accepts formula alice bob)).length =
          acceptedCount formula alice bob indices := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AliceStrategy, OAI.UniqueGamesTheorem.Foundations.PCP.BobStrategy, OAI.UniqueGamesTheorem.Foundations.PCP.enumerateEvents, OAI.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.acceptedCount

36. def OAI.UniqueGamesTheorem.Foundations.PCP.allEvents line 225
37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.length_allEvents line 228
38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.allEvents_nonempty line 232
39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.verifier_event_soundness line 244

    Source documentation

    Soundness stated solely in terms of filtering the generated event list. For b>0 and a nonempty input, division by b*|allEvents| gives the usual normalized acceptance probability.

    theorem verifier_event_soundness (formula : Formula) (a b : Nat)
        (sourceGap : ∀ bob : BobStrategy formula,
          a * formula.clauses.length ≤ b * failureCount formula bob (allIndices formula))
        (alice : AliceStrategy formula) (bob : BobStrategy formula) :
        b * ((allEvents formula).filter (accepts formula alice bob)).length +
          a * formula.clauses.length ≤ b * (allEvents formula).length := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.BobStrategy, OAI.UniqueGamesTheorem.Foundations.PCP.failureCount, OAI.UniqueGamesTheorem.Foundations.PCP.allIndices, OAI.UniqueGamesTheorem.Foundations.PCP.AliceStrategy, OAI.UniqueGamesTheorem.Foundations.PCP.allEvents, OAI.UniqueGamesTheorem.Foundations.PCP.accepts

40. def OAI.UniqueGamesTheorem.Foundations.PCP.occurrencesAt line 255

    Source documentation

    Count the syntactic occurrences of one variable in each three-slot clause.

    def occurrencesAt {n : Nat} (clause : Clause n) (v : Fin n) : Nat :=
    …

41. def OAI.UniqueGamesTheorem.Foundations.PCP.occurrenceCount line 260
42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.variable_eventsAt line 265
43. theorem OAI.UniqueGamesTheorem.Foundations.PCP.variable_enumerateEvents line 275
44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.regular_bob_marginal line 286
45. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.clauseAnswerEquiv line 306

    Source documentation

    Executable tuple encoding of the eight clause answers.

    def clauseAnswerEquiv : ClauseAnswer ≃ Bool × Bool × Bool where
    …

46. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.clauseAnswerFinEquiv line 312
47. instance OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.clauseAnswerFintype line 318
48. instance OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.clauseAnswerInhabited line 321
49. instance OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.slotFintype line 323
50. instance OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.slotInhabited line 327
51. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.card_clauseAnswer line 329
52. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.card_slot line 333
53. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.I line 335
54. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.J line 336
55. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.ClauseContext line 337
56. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.VariableContext line 338
57. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.SlotContext line 339
58. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.card_I line 341
59. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.card_J line 342
60. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.card_ClauseContext line 343
61. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.card_VariableContext line 345
62. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.card_SlotContext line 347
63. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.localConsistent line 350
64. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.localConsistent_eq_true_iff line 354
65. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.validJ line 362

    Source documentation

    Satisfaction and consistency over all 3*u occurrence slots.

    def validJ (F : Formula) {u : ℕ} (c : ClauseContext F u) (j : J u) : Bool :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.ClauseContext, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.J

66. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.validJ_eq_true_iff line 367
67. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.validJ_satisfies line 375
68. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.validJ_consistent line 380
69. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.validJ_localConsistent line 387
70. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.canonicalSlot line 396

    Source documentation

    First matching visible occurrence, with the third slot as an off-support default. Its inputs contain no hidden incidence choice.

    def canonicalSlot {n : ℕ} (clause : Clause n) (v : Fin n) : Slot :=
    …

71. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.canonicalSlot_name line 400
72. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.pi line 412
73. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.sampledVariables line 416
74. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.sampledVariables_supported line 420
75. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.sampled_eq_pi line 425
76. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.sampled_answers_eq_of_visible_eq line 435

    Source documentation

    Two hidden choices with the same visible variable tuple give the same selected answers for every valid label.

    theorem sampled_answers_eq_of_visible_eq (F : Formula) {u : ℕ}
        (c : ClauseContext F u) (s s' : SlotContext u) (j : J u)
        (hj : validJ F c j = true)
        (hvisible : sampledVariables F c s = sampledVariables F c s') :
        (fun t => answerAt (j t) (s t)) = fun t => answerAt (j t) (s' t) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.ClauseContext, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.SlotContext, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.J, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.validJ, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.sampledVariables

77. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.honestJ line 443
78. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.honestI line 447
79. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.honestJ_valid line 451
80. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.pi_honest line 463
81. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.pi_honest_sampled line 471
82. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.baseAccepts line 477
83. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.baseAccepts_eq_true_iff line 483
84. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.projection_implies_coordinate_accepts line 491
85. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.baseAccepts_implies_sampled line 498
86. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.projection_implies_sampled_accepts line 510

    Source documentation

    Every coordinate of the original repeated clause-slot verifier accepts the decoded answers. Each answer tuple may depend on its whole private context.

    theorem projection_implies_sampled_accepts (F : Formula) {u : ℕ}
        (c : ClauseContext F u) (s : SlotContext u) (i : I u) (j : J u)
        (hj : validJ F c j = true) (hpi : pi F c (sampledVariables F c s) j = i) :
        ∀ t, (localSatisfies (clauseAt F (c t)) (j t) &&
          decide (answerAt (j t) (s t) = i t)) = true := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.ClauseContext, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.SlotContext, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.I, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.J, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.validJ, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.pi, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.sampledVariables

87. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.Position line 529
88. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.NameProfile line 530
89. structure OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.Signature line 534

    Source documentation

    All local control data have sizes determined solely by the repetition parameter. Global variable and clause indices are absent.

    structure Signature (u : ℕ) where
    …

90. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureEquiv line 540
91. instance OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureFintype line 547
92. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.card_position line 551
93. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.card_signature line 555

    Source documentation

    A finite control alphabet bound, not a claim about evaluation time.

    theorem card_signature (u : ℕ) :
        Fintype.card (Signature u) =
          2 ^ (3 * u) * ((2 ^ (3 * u)) ^ (3 * u) * 3 ^ u) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.Signature

94. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.positiveAt line 561
95. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.occurrenceName line 566
96. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.contextNameProfile line 572

    Source documentation

    The equality matrix can be supplied by a separate field-comparison procedure after an explicit reindexing of the 3*u positions.

    def contextNameProfile (F : Formula) {u : ℕ} (c : ClauseContext F u) : NameProfile u :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.NameProfile

97. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.ofContext line 575
98. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.ofContext_signs line 581
99. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.ofContext_sameName line 585
100. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.ofContext_selected line 590
101. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureSatisfies line 594

     Source documentation

     Local clause truth is computed from signs and the three answer bits.

     def signatureSatisfies {u : ℕ} (σ : Signature u) (j : J u) (t : Fin u) : Bool :=
     …

     Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.Signature

102. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureValid line 599
103. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureSatisfies_ofContext line 604
104. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signature_validJ line 611

     Source documentation

     Exact equality with the actual contextual validity predicate, for every answer tuple, including repeated variables within or across clauses.

     theorem signature_validJ (F : Formula) {u : ℕ} (c : ClauseContext F u)
         (s : SlotContext u) (j : J u) :
         signatureValid (ofContext F c s) j = validJ F c j := by
     …

     Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureValid, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.ofContext

105. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureCanonicalSlot line 636

     Source documentation

     The first slot matching the visible selected name, computed using only the equality matrix. The selected slot guarantees visible support.

     def signatureCanonicalSlot {u : ℕ} (σ : Signature u) (t : Fin u) : Slot :=
     …

     Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.Signature

106. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureProjection line 640
107. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureCanonicalSlot_ofContext line 643
108. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signature_pi line 660

     Source documentation

     The actual canonical projection factors through the finite signature on every label, without a validity hypothesis.

     theorem signature_pi (F : Formula) {u : ℕ} (c : ClauseContext F u)
         (s : SlotContext u) (j : J u) :
         signatureProjection (ofContext F c s) j = pi F c (sampledVariables F c s) j := by
     …

     Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureProjection, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.ofContext

109. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signature_projection_selected line 668

     Source documentation

     On valid labels, canonical projection also agrees with the actual selected occurrence answers.

     theorem signature_projection_selected (F : Formula) {u : ℕ}
         (c : ClauseContext F u) (s : SlotContext u) (j : J u)
         (hj : signatureValid (ofContext F c s) j = true) :
         signatureProjection (ofContext F c s) j = fun t => answerAt (j t) (s t) := by
     …

     Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureValid, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.ofContext, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.signatureProjection

110. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.validJ_eq_of_signature_eq line 679

     Source documentation

     The same finite signature gives the same validity decision even across formulas having different global index types.

     theorem validJ_eq_of_signature_eq (F G : Formula) {u : ℕ}
         (c : ClauseContext F u) (d : ClauseContext G u) (s s' : SlotContext u)
         (h : ofContext F c s = ofContext G d s') (j : J u) :
         validJ F c j = validJ G d j := by
     …

     Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.ofContext

111. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalSignature.pi_eq_of_signature_eq line 685