Lax Lean Archive

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

The FAF verifier as a finite local-test system

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

    Number all coordinates of all reference and larger tables to form a single Boolean proof. For each random choice, convert the enumerated FAF transcripts into partial assignments. Filter out inconsistent assignments to repeated coordinates and merge the remainder.

    The resulting system accepts exactly when the original FAF verifier does, and has at most 2q+ns2^{q+ns} accepting views per choice. Thus the finite FAF soundness theorem applies directly to the graph reduction. Numbering and enumeration here are finite mathematical constructions; their efficient machine implementations are separate obligations.

    Concept map
    22 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 acceptance_probability proven

    2 free_bits proven

    3 passes_iff proven

    4 perfect_completeness proven

    5 proof_length proven

    6 random_choices proven

    7 soundness proven

    Lean source view on GitHub

    1import Lax253009.FAFComposition
    2import Lax253009.TestRepetition
    3
    4/-!
    5---
    6title: The FAF verifier as a finite local-test system
    7type: theorem
    8---
    9Number all coordinates of all reference and larger tables to form a
    10single Boolean proof. For each random choice, convert the enumerated FAF
    11transcripts into partial assignments. Filter out inconsistent assignments
    12to repeated coordinates and merge the remainder.
    13
    14The resulting system accepts exactly when the original FAF verifier does,
    15and has at most 2q+ns2^{q+ns} accepting views per choice. Thus the finite FAF
    16soundness theorem applies directly to the graph reduction. Numbering and
    17enumeration here are finite mathematical constructions; their efficient
    18machine implementations are separate obligations.
    19-/
    20
    21namespace Lax253009.FAFLocalTests
    22
    23open LongCode LocalTests LongCodePatterns TestRepetition TestSampling
    24
    25abbrev Index (U W : Type) (u w : ℕ) := (U × Coordinate u) ⊕ (W × Coordinate w)
    26
    27abbrev Randomness (U Ω : Type) (u w n s q : ℕ) :=
    28 U × FAFStrategyExtraction.Seed Ω u w n s q
    29
    30noncomputable def indexEquiv (U W : Type) [Fintype U] [Fintype W] (u w : ℕ) :
    31 Index U W u w ≃ Fin (Fintype.card (Index U W u w)) := Fintype.equivFin _
    32
    33noncomputable def randomEquiv (U Ω : Type) [Fintype U] [Fintype Ω] (u w n s q : ℕ) :
    34 Randomness U Ω u w n s q ≃ Fin (Fintype.card (Randomness U Ω u w n s q)) :=
    35 Fintype.equivFin _
    36
    37noncomputable def reference {U W : Type} [Fintype U] [Fintype W] {u w : ℕ}
    38 (π : Oracle (Fintype.card (Index U W u w))) (v : U) : Table u :=
    39 fun g ↦ π (indexEquiv U W u w (Sum.inl (v, g)))
    40
    41noncomputable def larger {U W : Type} [Fintype U] [Fintype W] {u w : ℕ}
    42 (π : Oracle (Fintype.card (Index U W u w))) (v : W) : Table w :=
    43 fun g ↦ π (indexEquiv U W u w (Sum.inr (v, g)))
    44
    45noncomputable def parts {U Ω W : Type} [Fintype U] [Fintype W] {u w n s q : ℕ}
    46 (question : U → Ω → W) (z : Randomness U Ω u w n s q)
    47 (p : LongCode.Word q × (Fin n → Pattern w)) :
    48 Fin (q + n) → View (Fintype.card (Index U W u w)) := by
    49 classical
    50 exact Fin.addCases
    51 (fun j x ↦ if x = indexEquiv U W u w (Sum.inl (z.1, z.2.1.2 j)) then some (p.1 j) else none)
    52 (fun i x ↦ match (indexEquiv U W u w).symm x with
    53 | .inl _ => none
    54 | .inr (v, g) => if v = question z.1 (z.2.1.1 i) then p.2 i g else none)
    55
    56noncomputable def system {U Ω W : Type} [Fintype U] [Fintype Ω] [Fintype W]
    57 {u w n s q : ℕ} (question : U → Ω → W)
    58 (ρ : U → Ω → LongCode.Word w → LongCode.Word u) (valid : U → Ω → Coordinate w) :
    59 System (Fintype.card (Randomness U Ω u w n s q)) (Fintype.card (Index U W u w)) := by
    60 classical
    61 exact ⟨fun seed ↦
    62 let z := (randomEquiv U Ω u w n s q).symm seed
    63 ((FAFPatterns.patterns (ρ z.1) (valid z.1) z.2.1.1 z.2.1.2 z.2.2).filter
    64 (fun p ↦ Coherent (parts question z p))).image (fun p ↦ merge (parts question z p))⟩
    65
    66axiom passes_iff {U Ω W : Type} [Fintype U] [Fintype Ω] [Fintype W]
    67 {u w n s q : ℕ} (question : U → Ω → W)
    68 (ρ : U → Ω → LongCode.Word w → LongCode.Word u) (valid : U → Ω → Coordinate w)
    69 (π : Oracle (Fintype.card (Index U W u w)))
    70 (z : Randomness U Ω u w n s q) :
    71 Passes (system (n := n) (s := s) (q := q) question ρ valid) π (randomEquiv U Ω u w n s q z) ↔
    72 FAFStrategyExtraction.Accepts question ρ valid (reference π) (larger π) z
    73
    74axiom free_bits {U Ω W : Type} [Fintype U] [Fintype Ω] [Fintype W]
    75 {u w n s q : ℕ} (question : U → Ω → W)
    76 (ρ : U → Ω → LongCode.Word w → LongCode.Word u) (valid : U → Ω → Coordinate w) :
    77 ∀ seed, ((system (n := n) (s := s) (q := q) question ρ valid).accepting seed).card ≤ 2 ^ (q + n * s)
    78
    79axiom acceptance_probability {U Ω W : Type} [Fintype U] [Fintype Ω] [Fintype W]
    80 {u w n s q : ℕ} (question : U → Ω → W)
    81 (ρ : U → Ω → LongCode.Word w → LongCode.Word u) (valid : U → Ω → Coordinate w)
    82 (π : Oracle (Fintype.card (Index U W u w))) :
    83 FiniteProbability.probability (Passes (system (n := n) (s := s) (q := q) question ρ valid) π) =
    84 FiniteProbability.probability
    85 (FAFStrategyExtraction.Accepts (n := n) (s := s) (q := q) question ρ valid (reference π) (larger π))
    86
    87axiom perfect_completeness {U Ω W : Type} [Fintype U] [Fintype Ω] [Fintype W]
    88 {u w n s q : ℕ} (question : U → Ω → W)
    89 (ρ : U → Ω → LongCode.Word w → LongCode.Word u) (valid : U → Ω → Coordinate w)
    90 (P : W → LongCode.Word w) (Q : U → LongCode.Word u)
    91 (hvalid : ∀ v ω, valid v ω (P (question v ω)) = true)
    92 (hproject : ∀ v ω, ρ v ω (P (question v ω)) = Q v) :
    93 Complete (system (n := n) (s := s) (q := q) question ρ valid)
    94
    95axiom soundness (l : ℕ) (hl : 0 < l) :
    96 ∃ s₀ : ℕ, ∀ s : ℕ, s₀ ≤ s → ∃ w₀ : ℕ, ∀ w : ℕ, w₀ ≤ w →
    97 ∀ {U Ω W : Type} [Fintype U] [Nonempty U] [Fintype Ω] [Nonempty Ω]
    98 [Fintype W] [DecidableEq W],
    99 ∀ u : ℕ, ∀ (question : U → Ω → W)
    100 (ρ : U → Ω → LongCode.Word w → LongCode.Word u) (valid : U → Ω → Coordinate w),
    101 (∀ (P : W → Option (LongCode.Word w)) (Q : U → Option (LongCode.Word u)),
    102 FiniteProbability.probability (DecodedStrategies.Wins question
    103 (FAFStrategyExtraction.Relation ρ valid) P Q) < FAFComposition.gameThreshold l s) →
    104 Sound (system (n := 10 * l) (s := s) (q := 10 * l * s) question ρ valid)
    105 ((1 / 2 : ℝ) ^ (20 * l * l * s))
    106
    107axiom proof_length (U W : Type) [Fintype U] [Fintype W] (u w : ℕ) :
    108 Fintype.card (Index U W u w) = Fintype.card U * 2 ^ (2 ^ u) + Fintype.card W * 2 ^ (2 ^ w)
    109
    110axiom random_choices (U Ω : Type) [Fintype U] [Fintype Ω] (u w n s q : ℕ) :
    111 Fintype.card (Randomness U Ω u w n s q) =
    112 Fintype.card U * (Fintype.card Ω ^ n * (2 ^ (2 ^ u)) ^ q * ((2 ^ (2 ^ w)) ^ s) ^ n)
    113
    114end Lax253009.FAFLocalTests
    115
    Show 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…