Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Projection games from regular constraint systems

Lax253009.ProjectionGames · concepts/Lax253009/ProjectionGames.lean · lax-253009

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    A regular constraint system gives a two-prover projection game. The first prover labels both ends of a dart; the second labels one uniformly chosen endpoint. Reversing darts preserves the uniform distribution, so the verifier can equivalently start with a uniformly chosen vertex and extension.

    Perfect completeness is preserved. If every vertex assignment violates at least a fraction γ\gamma of the constraints, every pair of prover strategies wins with probability at most 1−γ/21-\gamma/2. The bound also allows provers to return no answer.

    Concept map
    3 concepts; 5 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 completeness proven

    2 soundness proven

    Lean source view on GitHub

    1import Lax253009.DecodedStrategies
    2import Mathlib.Data.Fintype.Prod
    3
    4/-!
    5---
    6title: Projection games from regular constraint systems
    7type: theorem
    8---
    9A regular constraint system gives a two-prover projection game. The first
    10prover labels both ends of a dart; the second labels one uniformly chosen
    11endpoint. Reversing darts preserves the uniform distribution, so the verifier
    12can equivalently start with a uniformly chosen vertex and extension.
    13
    14Perfect completeness is preserved. If every vertex assignment violates at
    15least a fraction γ\gamma of the constraints, every pair of prover strategies
    16wins with probability at most 1−γ/21-\gamma/2. The bound also allows provers to
    17return no answer.
    18-/
    19
    20namespace Lax253009.ProjectionGames
    21
    22open FiniteProbability
    23
    24structure System (V D A : Type) where
    25 reverse : V × D → V × D
    26 reverse_involutive : Function.Involutive reverse
    27 relation : V × D → A → A → Bool
    28
    29namespace System
    30
    31variable {V D A : Type} (C : System V D A)
    32
    33def question (v : V) (ω : D × Bool) : V × D :=
    34 if ω.2 then C.reverse (v, ω.1) else (v, ω.1)
    35
    36def endpoint (z : V × D) (b : Bool) : V :=
    37 if b then (C.reverse z).1 else z.1
    38
    39def project (b : Bool) (p : A × A) : A := if b then p.2 else p.1
    40
    41def Test (v : V) (ω : D × Bool) (p : A × A) (a : A) : Prop :=
    42 C.relation (C.question v ω) p.1 p.2 = true ∧ project ω.2 p = a
    43
    44def Violated (a : V → A) (z : V × D) : Prop :=
    45 C.relation z (a z.1) (a (C.reverse z).1) ≠ true
    46
    47def Satisfiable : Prop := ∃ a : V → A, ∀ z, ¬ C.Violated a z
    48
    49def Sound [Fintype V] [Fintype D] (γ : ℝ) : Prop :=
    50 ∀ a : V → A, γ ≤ probability (C.Violated a)
    51
    52end System
    53
    54axiom completeness {V D A : Type} (C : System V D A) (h : C.Satisfiable) :
    55 ∃ P : V × D → A × A, ∃ Q : V → A,
    56 ∀ v ω, C.Test v ω (P (C.question v ω)) (Q v)
    57
    58axiom soundness {V D A : Type} [Fintype V] [Nonempty V]
    59 [Fintype D] [Nonempty D] [Nonempty A]
    60 (C : System V D A) (γ : ℝ) (h : C.Sound γ)
    61 (P : V × D → Option (A × A)) (Q : V → Option A) :
    62 probability (DecodedStrategies.Wins C.question C.Test P Q) ≤ 1 - γ / 2
    63
    64end Lax253009.ProjectionGames
    65
    Show ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…