Lax Lean Archive

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

Soundness amplification for centered projection games

Lax253009.CenteredProjection · concepts/Lax253009/CenteredProjection.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

    Two independently sampled extensions of a common center define a symmetric projection test. Its value is at most the original game's value, while original value at most the square root of symmetric value follows from Cauchy–Schwarz. Fortification followed by tensor squaring preserves this centered structure and has value at most s² + 4|X|r.

    Regular constraint systems supply uniformly distributed questions in this model. Both transformations preserve perfect completeness and uniform question marginals.

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

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

    1 center_sound_of_sym proven

    2 fortify_complete proven

    3 fortify_square_sound proven

    4 fortify_uniform proven

    5 from_constraints_complete proven

    6 from_constraints_sound proven

    7 from_constraints_uniform proven

    8 symmetrize_sound proven

    9 tensor_complete proven

    10 tensor_uniform proven

    Lean source view on GitHub

    1import Lax253009.TupleFortification
    2import Lax253009.ProjectionGames
    3
    4/-!
    5---
    6title: Soundness amplification for centered projection games
    7type: theorem
    8---
    9Two independently sampled extensions of a common center define a symmetric
    10projection test. Its value is at most the original game's value, while
    11original value at most the square root of symmetric value follows from
    12Cauchy–Schwarz. Fortification followed by tensor squaring preserves this
    13centered structure and has value at most s² + 4|X|r.
    14
    15Regular constraint systems supply uniformly distributed questions in this
    16model. Both transformations preserve perfect completeness and uniform
    17question marginals.
    18-/
    19
    20namespace Lax253009.CenteredProjection
    21
    22open FiniteProbability FortifiedSquaring TupleFortification
    23open scoped BigOperators
    24
    25structure System (U Ω W X Y : Type) where
    26 question : U → Ω → W
    27 valid : U → Ω → Y → Bool
    28 project : U → Ω → Y → X
    29
    30namespace System
    31
    32variable {U Ω W X Y : Type} (G : System U Ω W X Y)
    33
    34def Test (u : U) (ω : Ω) (y : Y) (x : X) : Prop :=
    35 G.valid u ω y = true ∧ G.project u ω y = x
    36
    37def Complete : Prop := ∃ P : W → Y, ∃ Q : U → X,
    38 ∀ u ω, G.Test u ω (P (G.question u ω)) (Q u)
    39
    40def Sound [Fintype U] [Fintype Ω] (s : ℝ) : Prop :=
    41 ∀ (P : W → Y) (Q : U → X),
    42 probability (fun z : U × Ω ↦ G.Test z.1 z.2 (P (G.question z.1 z.2)) (Q z.1)) ≤ s
    43
    44def Uniform [Fintype U] [Fintype Ω] [Fintype W] : Prop :=
    45 ∀ f : W → ℝ, (𝔼 u, 𝔼 ω, f (G.question u ω)) = 𝔼 w, f w
    46
    47def symmetrize : Game (U × (Ω × Ω)) W Y X where
    48 left z := G.question z.1 z.2.1
    49 right z := G.question z.1 z.2.2
    50 validLeft z y := G.valid z.1 z.2.1 y
    51 validRight z y := G.valid z.1 z.2.2 y
    52 projectLeft z y := G.project z.1 z.2.1 y
    53 projectRight z y := G.project z.1 z.2.2 y
    54
    55def fortify (t : ℕ) : System U (Ω × History t W) (Fin t → W) X (Fin t → Y) where
    56 question u ω := plant (G.question u ω.1) ω.2
    57 valid u ω y := G.valid u ω.1 (y ω.2.1)
    58 project u ω y := G.project u ω.1 (y ω.2.1)
    59
    60def tensor : System (U × U) (Ω × Ω) (W × W) (X × X) (Y × Y) where
    61 question u ω := (G.question u.1 ω.1, G.question u.2 ω.2)
    62 valid u ω y := G.valid u.1 ω.1 y.1 && G.valid u.2 ω.2 y.2
    63 project u ω y := (G.project u.1 ω.1 y.1, G.project u.2 ω.2 y.2)
    64
    65end System
    66
    67def fromConstraints {V D A : Type} (C : ProjectionGames.System V D A) :
    68 System V (D × Bool) (V × D) A (A × A) where
    69 question := C.question
    70 valid v ω p := C.relation (C.question v ω) p.1 p.2
    71 project _ ω p := ProjectionGames.System.project ω.2 p
    72
    73axiom symmetrize_sound {U Ω W X Y : Type}
    74 [Fintype U] [Fintype Ω] [Nonempty Ω]
    75 (G : System U Ω W X Y) (s : ℝ) (h : G.Sound s) : G.symmetrize.Sound s
    76
    77axiom fortify_complete {U Ω W X Y : Type}
    78 (G : System U Ω W X Y) (h : G.Complete) (t : ℕ) : (G.fortify t).Complete
    79
    80axiom tensor_complete {U Ω W X Y : Type}
    81 (G : System U Ω W X Y) (h : G.Complete) : G.tensor.Complete
    82
    83axiom fortify_uniform {U Ω W X Y : Type}
    84 [Fintype U] [Fintype Ω] [Fintype W] [Nonempty W]
    85 (G : System U Ω W X Y) (h : G.Uniform) (t : ℕ) (ht : 0 < t) :
    86 (G.fortify t).Uniform
    87
    88axiom tensor_uniform {U Ω W X Y : Type}
    89 [Fintype U] [Fintype Ω] [Fintype W]
    90 (G : System U Ω W X Y) (h : G.Uniform) : G.tensor.Uniform
    91
    92axiom fortify_square_sound {U Ω W X Y : Type}
    93 [Fintype U] [Nonempty U] [Fintype Ω] [Nonempty Ω]
    94 [Fintype W] [Nonempty W] [DecidableEq W]
    95 [Fintype X] [Fintype Y] [Nonempty Y]
    96 (G : System U Ω W X Y) (hu : G.Uniform)
    97 (t : ℕ) (ht : 0 < t) (s : ℝ) (hs : 0 ≤ s) (hs1 : s ≤ 1)
    98 (h : G.symmetrize.Sound s) (r : ℝ) (hr : 0 ≤ r) (htr : 1 / (t : ℝ) ≤ r ^ 2) :
    99 (G.fortify t).tensor.symmetrize.Sound (s ^ 2 + (Fintype.card X : ℝ) * (4 * r))
    100
    101axiom center_sound_of_sym {U Ω W X Y : Type}
    102 [Fintype U] [Nonempty U] [Fintype Ω]
    103 (G : System U Ω W X Y) (s : ℝ) (hs : 0 ≤ s)
    104 (h : G.symmetrize.Sound (s ^ 2)) : G.Sound s
    105
    106axiom from_constraints_complete {V D A : Type}
    107 (C : ProjectionGames.System V D A) (h : C.Satisfiable) : (fromConstraints C).Complete
    108
    109axiom from_constraints_sound {V D A : Type} [Fintype V] [Nonempty V]
    110 [Fintype D] [Nonempty D] [Nonempty A]
    111 (C : ProjectionGames.System V D A) (γ : ℝ) (h : C.Sound γ) :
    112 (fromConstraints C).Sound (1 - γ / 2)
    113
    114axiom from_constraints_uniform {V D A : Type} [Fintype V] [Fintype D]
    115 (C : ProjectionGames.System V D A) : (fromConstraints C).Uniform
    116
    117end Lax253009.CenteredProjection
    118
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…