Lax Lean Archive

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

Fortification by uniformly sampled tuples

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

    Replace each prover question by a uniform tuple with the original question planted at a hidden uniformly chosen coordinate, and ask the prover to answer every coordinate. This preserves perfect completeness, soundness, and uniform question marginals. For tuple length t, the resulting game is fortified with additive error at most 4r whenever 1/t ≤ r².

    The construction uses all tuples. Its size is polynomial in the original question count for each fixed t; its mixing bound is independent of the prover-answer alphabet.

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

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

    1 completeness proven

    2 fortification proven

    3 left_uniform proven

    4 right_uniform proven

    5 soundness proven

    Lean source view on GitHub

    1import Lax253009.FortifiedSquaring
    2import Mathlib.Data.Fintype.Pi
    3
    4/-!
    5---
    6title: Fortification by uniformly sampled tuples
    7type: theorem
    8---
    9Replace each prover question by a uniform tuple with the original question
    10planted at a hidden uniformly chosen coordinate, and ask the prover to
    11answer every coordinate. This preserves perfect completeness, soundness,
    12and uniform question marginals. For tuple length t, the resulting game is
    13fortified with additive error at most 4r whenever 1/t ≤ r².
    14
    15The construction uses all tuples. Its size is polynomial in the original
    16question count for each fixed t; its mixing bound is independent of the
    17prover-answer alphabet.
    18-/
    19
    20namespace Lax253009.TupleFortification
    21
    22open FortifiedSquaring
    23open scoped BigOperators
    24
    25abbrev History (t : ℕ) (W : Type) := Fin t × (Fin t → W)
    26
    27def plant {W : Type} {t : ℕ} (w : W) (h : History t W) : Fin t → W :=
    28 Function.update h.2 h.1 w
    29
    30def lift {Z W A B : Type} (G : Game Z W A B) (t : ℕ) :
    31 Game (Z × (History t W × History t W)) (Fin t → W) (Fin t → A) B where
    32 left z := plant (G.left z.1) z.2.1
    33 right z := plant (G.right z.1) z.2.2
    34 validLeft z a := G.validLeft z.1 (a z.2.1.1)
    35 validRight z b := G.validRight z.1 (b z.2.2.1)
    36 projectLeft z a := G.projectLeft z.1 (a z.2.1.1)
    37 projectRight z b := G.projectRight z.1 (b z.2.2.1)
    38
    39axiom soundness {Z W A B : Type} [Fintype Z] [Fintype W] [DecidableEq W]
    40 [Nonempty W] [Fintype A] (G : Game Z W A B) (t : ℕ) (ht : 0 < t)
    41 (s : ℝ) (hG : G.Sound s) : (lift G t).Sound s
    42
    43axiom fortification {Z W A B : Type}
    44 [Fintype Z] [Nonempty Z] [Fintype W] [DecidableEq W] [Nonempty W]
    45 [Fintype A] [Nonempty A]
    46 (G : Game Z W A B)
    47 (hl : ∀ f : W → ℝ, (𝔼 z, f (G.left z)) = (𝔼 w, f w))
    48 (hr : ∀ f : W → ℝ, (𝔼 z, f (G.right z)) = (𝔼 w, f w))
    49 (s : ℝ) (hs : 0 ≤ s) (hs1 : s ≤ 1) (hG : G.Sound s)
    50 (t : ℕ) (ht : 0 < t) (r : ℝ) (hr0 : 0 ≤ r) (htr : 1 / (t : ℝ) ≤ r ^ 2) :
    51 (lift G t).Fortified s (4 * r)
    52
    53axiom left_uniform {Z W A B : Type} [Fintype Z] [Fintype W] [Nonempty W]
    54 (G : Game Z W A B)
    55 (hl : ∀ f : W → ℝ, (𝔼 z, f (G.left z)) = (𝔼 w, f w))
    56 (t : ℕ) (ht : 0 < t) (f : (Fin t → W) → ℝ) :
    57 (𝔼 z, f ((lift G t).left z)) = 𝔼 w, f w
    58
    59axiom right_uniform {Z W A B : Type} [Fintype Z] [Fintype W] [Nonempty W]
    60 (G : Game Z W A B)
    61 (hr : ∀ f : W → ℝ, (𝔼 z, f (G.right z)) = (𝔼 w, f w))
    62 (t : ℕ) (ht : 0 < t) (f : (Fin t → W) → ℝ) :
    63 (𝔼 z, f ((lift G t).right z)) = 𝔼 w, f w
    64
    65axiom completeness {Z W A B : Type} (G : Game Z W A B)
    66 (P Q : W → A) (h : ∀ z, G.Wins P Q z) (t : ℕ) :
    67 ∀ z, (lift G t).Wins (fun w i ↦ P (w i)) (fun w i ↦ Q (w i)) z
    68
    69end Lax253009.TupleFortification
    70
    Show ProofShow ProofShow ProofShow 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…