OAI/Computability/MaxCut/PCP/ClauseVerifier.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MaxCutGames.Foundations.PCP.ClauseAnswer line 10
2. inductive OAI.MaxCutGames.Foundations.PCP.Slot line 16
3. def OAI.MaxCutGames.Foundations.PCP.answerAt line 22
4. def OAI.MaxCutGames.Foundations.PCP.nameAt line 27
5. def OAI.MaxCutGames.Foundations.PCP.literalValue line 32
6. def OAI.MaxCutGames.Foundations.PCP.localSatisfies line 35
7. def OAI.MaxCutGames.Foundations.PCP.honestAnswer line 40
8. theorem OAI.MaxCutGames.Foundations.PCP.honest_satisfies line 44
9. theorem OAI.MaxCutGames.Foundations.PCP.honest_answerAt line 47
10. def OAI.MaxCutGames.Foundations.PCP.matchingSlots line 52
11. theorem OAI.MaxCutGames.Foundations.PCP.matchingSlots_le line 57
12. theorem OAI.MaxCutGames.Foundations.PCP.matchingSlots_eq_three line 62
13. def OAI.MaxCutGames.Foundations.PCP.acceptedSlots line 67
14. def OAI.MaxCutGames.Foundations.PCP.clauseFailure line 70
15. theorem OAI.MaxCutGames.Foundations.PCP.local_rejection_bound line 74

    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.MaxCutGames.Foundations.PCP.ClauseAnswer, OAI.MaxCutGames.Foundations.PCP.acceptedSlots, OAI.MaxCutGames.Foundations.PCP.honestAnswer, OAI.MaxCutGames.Foundations.PCP.clauseFailure

16. def OAI.MaxCutGames.Foundations.PCP.clauseAt line 96
17. abbrev OAI.MaxCutGames.Foundations.PCP.RandomEvent line 99
18. abbrev OAI.MaxCutGames.Foundations.PCP.AliceStrategy line 100
19. abbrev OAI.MaxCutGames.Foundations.PCP.BobStrategy line 101
20. def OAI.MaxCutGames.Foundations.PCP.accepts line 105

    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.MaxCutGames.Foundations.PCP.AliceStrategy, OAI.MaxCutGames.Foundations.PCP.BobStrategy, OAI.MaxCutGames.Foundations.PCP.RandomEvent

21. def OAI.MaxCutGames.Foundations.PCP.acceptedCount line 110
22. def OAI.MaxCutGames.Foundations.PCP.failureCount line 116
23. theorem OAI.MaxCutGames.Foundations.PCP.total_rejection_bound line 121
24. def OAI.MaxCutGames.Foundations.PCP.allIndices line 132
25. theorem OAI.MaxCutGames.Foundations.PCP.hastad_basic_verifier_soundness line 137

    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.MaxCutGames.Foundations.PCP.BobStrategy, OAI.MaxCutGames.Foundations.PCP.failureCount, OAI.MaxCutGames.Foundations.PCP.allIndices, OAI.MaxCutGames.Foundations.PCP.AliceStrategy, OAI.MaxCutGames.Foundations.PCP.acceptedCount

26. theorem OAI.MaxCutGames.Foundations.PCP.honest_accepts line 148
27. theorem OAI.MaxCutGames.Foundations.PCP.verifier_completeness line 157

    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.MaxCutGames.Foundations.PCP.AliceStrategy, OAI.MaxCutGames.Foundations.PCP.BobStrategy, OAI.MaxCutGames.Foundations.PCP.RandomEvent, OAI.MaxCutGames.Foundations.PCP.accepts

28. abbrev OAI.MaxCutGames.Foundations.PCP.LeftLabel line 166

    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.MaxCutGames.Foundations.PCP.edgeProjection line 169
30. theorem OAI.MaxCutGames.Foundations.PCP.verifier_eq_projection line 172
31. def OAI.MaxCutGames.Foundations.PCP.eventsAt line 180

    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.MaxCutGames.Foundations.PCP.RandomEvent

32. def OAI.MaxCutGames.Foundations.PCP.enumerateEvents line 183
33. theorem OAI.MaxCutGames.Foundations.PCP.length_enumerateEvents line 188
34. theorem OAI.MaxCutGames.Foundations.PCP.accepted_eventsAt line 197
35. theorem OAI.MaxCutGames.Foundations.PCP.accepted_enumerateEvents line 211

    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.MaxCutGames.Foundations.PCP.AliceStrategy, OAI.MaxCutGames.Foundations.PCP.BobStrategy, OAI.MaxCutGames.Foundations.PCP.enumerateEvents, OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.acceptedCount

36. def OAI.MaxCutGames.Foundations.PCP.allEvents line 221
37. theorem OAI.MaxCutGames.Foundations.PCP.length_allEvents line 224
38. theorem OAI.MaxCutGames.Foundations.PCP.allEvents_nonempty line 228
39. theorem OAI.MaxCutGames.Foundations.PCP.verifier_event_soundness line 240

    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.MaxCutGames.Foundations.PCP.BobStrategy, OAI.MaxCutGames.Foundations.PCP.failureCount, OAI.MaxCutGames.Foundations.PCP.allIndices, OAI.MaxCutGames.Foundations.PCP.AliceStrategy, OAI.MaxCutGames.Foundations.PCP.allEvents, OAI.MaxCutGames.Foundations.PCP.accepts

40. def OAI.MaxCutGames.Foundations.PCP.occurrencesAt line 251

    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.MaxCutGames.Foundations.PCP.occurrenceCount line 256
42. theorem OAI.MaxCutGames.Foundations.PCP.variable_eventsAt line 261
43. theorem OAI.MaxCutGames.Foundations.PCP.variable_enumerateEvents line 271
44. theorem OAI.MaxCutGames.Foundations.PCP.regular_bob_marginal line 282