Lax Lean Archive

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

Soundness of the finite FAF composition

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

    For each positive integer ℓ\ell, sufficiently large ss and then ww give a finite FAF verifier with soundness below 2−20ℓ2s2^{-20\ell^2s} whenever the underlying two-prover game has sufficiently small positive soundness. The test uses n=10ℓn=10\ell larger tables and q=10ℓsq=10\ell s reference queries. Its proved free-bit bound is q+ns=20ℓsq+ns=20\ell s.

    This is the finite composition underlying Theorem 5.1. The game threshold is stated explicitly and is positive; exponentially decreasing game soundness is more than sufficient. The theorem does not provide the bounded-occurrence gap reduction, parallel repetition, logarithmic random bit implementation, or polynomial-time verifier construction.

    Concept map
    10 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 soundness proven

    2 threshold_positive proven

    Lean source view on GitHub

    1import Lax253009.FAFStrategyExtraction
    2import Lax253009.FAFPatterns
    3
    4/-!
    5---
    6title: Soundness of the finite FAF composition
    7type: theorem
    8---
    9For each positive integer ℓ\ell, sufficiently large ss and then ww
    10give a finite FAF verifier with soundness below 2−20ℓ2s2^{-20\ell^2s} whenever
    11the underlying two-prover game has sufficiently small positive soundness.
    12The test uses n=10ℓn=10\ell larger tables and q=10ℓsq=10\ell s reference queries.
    13Its proved free-bit bound is q+ns=20ℓsq+ns=20\ell s.
    14
    15This is the finite composition underlying Theorem 5.1. The game threshold
    16is stated explicitly and is positive; exponentially decreasing game
    17soundness is more than sufficient. The theorem does not provide the
    18bounded-occurrence gap reduction, parallel repetition, logarithmic random
    19bit implementation, or polynomial-time verifier construction.
    20-/
    21
    22namespace Lax253009.FAFComposition
    23
    24open LongCode FiniteProbability FAFStrategyExtraction
    25
    26noncomputable def gameThreshold (l s : ℕ) : ℝ :=
    27 ((1 / 2 : ℝ) ^ (20 * l * l * s) / 2) * (1 / 2 : ℝ) ^ (20 * l * s) /
    28 ((2 : ℝ) ^ s + 1)
    29
    30axiom threshold_positive (l s : ℕ) : 0 < gameThreshold l s
    31
    32axiom soundness (l : ℕ) (hl : 0 < l) :
    33 ∃ s₀ : ℕ, ∀ s : ℕ, s₀ ≤ s → ∃ w₀ : ℕ, ∀ w : ℕ, w₀ ≤ w →
    34 ∀ {U Ω W : Type} [Fintype U] [Nonempty U] [Fintype Ω] [Nonempty Ω]
    35 [Fintype W] [DecidableEq W],
    36 ∀ u : ℕ, ∀ (question : U → Ω → W)
    37 (ρ : U → Ω → Word w → Word u) (valid : U → Ω → Coordinate w)
    38 (R : U → Table u) (A : W → Table w),
    39 (∀ (P : W → Option (Word w)) (Q : U → Option (Word u)),
    40 probability (DecodedStrategies.Wins question (Relation ρ valid) P Q) < gameThreshold l s) →
    41 probability (FAFStrategyExtraction.Accepts (n := 10 * l) (s := s) (q := 10 * l * s)
    42 question ρ valid R A) < (1 / 2 : ℝ) ^ (20 * l * l * s)
    43
    44end Lax253009.FAFComposition
    45
    Show 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…