Lax Lean Archive

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

From FAF acceptance to two-prover success

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

    Combine the finite FAF soundness bound with extraction of two globally consistent prover strategies. If the FAF test accepts with probability aa and its no-common-answer error bound is EE, the two-prover game has strategies succeeding with probability at least (a−E)p/(B+1)(a-E)p/(B+1).

    The bound is quantitative and applies to arbitrary finite question spaces. The CNA error and decoding-set bounds are explicit hypotheses so that the independently proved CNA theorem can be applied uniformly to all tables.

    Concept map
    7 concepts; 4 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 finite_extraction proven

    2 uniform_extraction proven

    Lean source view on GitHub

    1import Lax253009.FAFTest
    2import Lax253009.DecodedStrategies
    3
    4/-!
    5---
    6title: From FAF acceptance to two-prover success
    7type: theorem
    8---
    9Combine the finite FAF soundness bound with extraction of two globally
    10consistent prover strategies. If the FAF test accepts with probability
    11aa and its no-common-answer error bound is EE, the two-prover game has
    12strategies succeeding with probability at least (a−E)p/(B+1)(a-E)p/(B+1).
    13
    14The bound is quantitative and applies to arbitrary finite question spaces.
    15The CNA error and decoding-set bounds are explicit hypotheses so that
    16the independently proved CNA theorem can be applied uniformly to all tables.
    17-/
    18
    19namespace Lax253009.FAFStrategyExtraction
    20
    21open LongCode FiniteProbability
    22
    23abbrev Seed (Ω : Type) (u w n s q : ℕ) :=
    24 ((Fin n → Ω) × (Fin q → Coordinate u)) × (Fin n → Fin s → Coordinate w)
    25
    26def Relation {U Ω : Type} {u w : ℕ}
    27 (ρ : U → Ω → Word w → Word u) (valid : U → Ω → Coordinate w)
    28 (v : U) (ω : Ω) (y : Word w) (x : Word u) : Prop :=
    29 valid v ω y = true ∧ ρ v ω y = x
    30
    31def Accepts {U Ω W : Type} {u w n s q : ℕ} (question : U → Ω → W)
    32 (ρ : U → Ω → Word w → Word u) (valid : U → Ω → Coordinate w)
    33 (R : U → Table u) (A : W → Table w) (z : U × Seed Ω u w n s q) : Prop :=
    34 FAFTest.Accepts (ρ z.1) (valid z.1) (R z.1) (fun ω ↦ A (question z.1 ω))
    35 z.2.1.1 z.2.1.2 z.2.2
    36
    37noncomputable def errorBound (n B k q : ℕ) (p δ : ℝ) : ℝ :=
    38 n * δ + (2 : ℝ) ^ n * ((n : ℝ) * B * p) ^ (n - k) +
    39 (B : ℝ) ^ n * (2 * (1 / 2 : ℝ) ^ (k + 1)) ^ q
    40
    41axiom finite_extraction {U Ω W : Type}
    42 [Fintype U] [Nonempty U] [Fintype Ω] [Nonempty Ω]
    43 [Fintype W] [DecidableEq W]
    44 (u w n s q : ℕ) (question : U → Ω → W)
    45 (ρ : U → Ω → Word w → Word u) (valid : U → Ω → Coordinate w)
    46 (R : U → Table u) (A : W → Table w) (D : W → Finset (Word w))
    47 (B k : ℕ) (p δ : ℝ) (hp : 0 ≤ p) (hδ : 0 ≤ δ)
    48 (hB : ∀ a, (D a).card ≤ B)
    49 (hdecode : ∀ a h, probability (CNASoundness.BadWithCondition (s := s) (A a) (D a) h) ≤ δ)
    50 (hsmall : (n : ℝ) * B * p ≤ 1) :
    51 ∃ P : W → Option (Word w), ∃ Q : U → Option (Word u),
    52 (probability (Accepts (n := n) (s := s) (q := q) question ρ valid R A) -
    53 errorBound n B k q p δ) * p / (B + 1) ≤
    54 probability (DecodedStrategies.Wins question (Relation ρ valid) P Q)
    55
    56/-- Apply the proved asymptotic CNA theorem uniformly to the entire family
    57of first-prover tables. No decoding or soundness hypothesis is required. -/
    58axiom uniform_extraction (K : ℕ) (hK : 0 < K) :
    59 ∃ s₀ : ℕ, ∀ s : ℕ, s₀ ≤ s → ∃ w₀ : ℕ, ∀ w : ℕ, w₀ ≤ w →
    60 ∀ {U Ω W : Type} [Fintype U] [Nonempty U] [Fintype Ω] [Nonempty Ω]
    61 [Fintype W] [DecidableEq W],
    62 ∀ u n q k : ℕ, ∀ (question : U → Ω → W)
    63 (ρ : U → Ω → Word w → Word u) (valid : U → Ω → Coordinate w)
    64 (R : U → Table u) (A : W → Table w) (p : ℝ),
    65 0 ≤ p → (n : ℝ) * (2 : ℝ) ^ s * p ≤ 1 →
    66 ∃ P : W → Option (Word w), ∃ Q : U → Option (Word u),
    67 (probability (Accepts (n := n) (s := s) (q := q) question ρ valid R A) -
    68 errorBound n (2 ^ s) k q p (Real.rpow 2 (-(K : ℝ) * (s : ℝ)))) * p / ((2 : ℝ) ^ s + 1) ≤
    69 probability (DecodedStrategies.Wins question (Relation ρ valid) P Q)
    70
    71end Lax253009.FAFStrategyExtraction
    72
    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…