Lax Lean Archive

The FAF verifier as a finite local-test system

Lax323828.FAFLocalTests · concepts/Lax323828/FAFLocalTests.lean · lax-323828

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 Lax323828.FAFComposition
    2import Lax323828.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 Lax323828.FAFLocalTests
    22
    23open scoped Classical
    24
    25open LongCode LocalTests LongCodePatterns TestRepetition TestSampling
    26
    27/-- All coordinates of the reference tables and the larger tables, kept as two separate families. -/
    28abbrev Index (U W : Type) (u w : ℕ) := (U × Coordinate u) ⊕ (W × Coordinate w)
    29
    30/-- A reference question together with all random choices made by its local test. -/
    31abbrev Randomness (U Ω : Type) (u w n s q : ℕ) :=
    32 U × FAFStrategyExtraction.Seed Ω u w n s q
    33
    34/-- Number the proof coordinates consecutively. -/
    35noncomputable def indexEquiv (U W : Type) [Fintype U] [Fintype W] (u w : ℕ) :
    36 Index U W u w ≃ Fin (Fintype.card (Index U W u w)) := Fintype.equivFin _
    37
    38/-- Number the possible random choices consecutively. -/
    39noncomputable def randomEquiv (U Ω : Type) [Fintype U] [Fintype Ω] (u w n s q : ℕ) :
    40 Randomness U Ω u w n s q ≃ Fin (Fintype.card (Randomness U Ω u w n s q)) :=
    41 Fintype.equivFin _
    42
    43/-- Read one reference table from the global Boolean proof. -/
    44noncomputable def reference {U W : Type} [Fintype U] [Fintype W] {u w : ℕ}
    45 (π : Oracle (Fintype.card (Index U W u w))) (v : U) : Table u :=
    46 fun g ↦ π (indexEquiv U W u w (Sum.inl (v, g)))
    47
    48/-- Read one larger table from the global Boolean proof. -/
    49noncomputable def larger {U W : Type} [Fintype U] [Fintype W] {u w : ℕ}
    50 (π : Oracle (Fintype.card (Index U W u w))) (v : W) : Table w :=
    51 fun g ↦ π (indexEquiv U W u w (Sum.inr (v, g)))
    52
    53/-- Translate the reference answers and the larger-table patterns into partial assignments to the global proof. -/
    54noncomputable def parts {U Ω W : Type} [Fintype U] [Fintype W] {u w n s q : ℕ}
    55 (question : U → Ω → W) (z : Randomness U Ω u w n s q)
    56 (p : LongCode.Word q × (Fin n → Pattern w)) :
    57 Fin (q + n) → View (Fintype.card (Index U W u w)) :=
    58 Fin.addCases
    59 (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)
    60 (fun i x ↦ match (indexEquiv U W u w).symm x with
    61 | .inl _ => none
    62 | .inr (v, g) => if v = question z.1 (z.2.1.1 i) then p.2 i g else none)
    63
    64/-- For each random choice, merge exactly the mutually consistent accepting partial assignments. -/
    65noncomputable def system {U Ω W : Type} [Fintype U] [Fintype Ω] [Fintype W]
    66 {u w n s q : ℕ} (question : U → Ω → W)
    67 (ρ : U → Ω → LongCode.Word w → LongCode.Word u) (valid : U → Ω → Coordinate w) :
    68 System (Fintype.card (Randomness U Ω u w n s q)) (Fintype.card (Index U W u w)) :=
    69 ⟨fun seed ↦
    70 let z := (randomEquiv U Ω u w n s q).symm seed
    71 ((FAFPatterns.patterns (ρ z.1) (valid z.1) z.2.1.1 z.2.1.2 z.2.2).filter
    72 (fun p ↦ Coherent (parts question z p))).image (fun p ↦ merge (parts question z p))⟩
    73
    74axiom passes_iff {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 (π : Oracle (Fintype.card (Index U W u w)))
    78 (z : Randomness U Ω u w n s q) :
    79 Passes (system (n := n) (s := s) (q := q) question ρ valid) π (randomEquiv U Ω u w n s q z) ↔
    80 FAFStrategyExtraction.Accepts question ρ valid (reference π) (larger π) z
    81
    82axiom free_bits {U Ω W : Type} [Fintype U] [Fintype Ω] [Fintype W]
    83 {u w n s q : ℕ} (question : U → Ω → W)
    84 (ρ : U → Ω → LongCode.Word w → LongCode.Word u) (valid : U → Ω → Coordinate w) :
    85 ∀ seed, ((system (n := n) (s := s) (q := q) question ρ valid).accepting seed).card ≤ 2 ^ (q + n * s)
    86
    87axiom acceptance_probability {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 (π : Oracle (Fintype.card (Index U W u w))) :
    91 FiniteProbability.probability (Passes (system (n := n) (s := s) (q := q) question ρ valid) π) =
    92 FiniteProbability.probability
    93 (FAFStrategyExtraction.Accepts (n := n) (s := s) (q := q) question ρ valid (reference π) (larger π))
    94
    95axiom perfect_completeness {U Ω W : Type} [Fintype U] [Fintype Ω] [Fintype W]
    96 {u w n s q : ℕ} (question : U → Ω → W)
    97 (ρ : U → Ω → LongCode.Word w → LongCode.Word u) (valid : U → Ω → Coordinate w)
    98 (P : W → LongCode.Word w) (Q : U → LongCode.Word u)
    99 (hvalid : ∀ v ω, valid v ω (P (question v ω)) = true)
    100 (hproject : ∀ v ω, ρ v ω (P (question v ω)) = Q v) :
    101 Complete (system (n := n) (s := s) (q := q) question ρ valid)
    102
    103axiom soundness (l : ℕ) (hl : 0 < l) :
    104 ∃ s₀ : ℕ, ∀ s : ℕ, s₀ ≤ s → ∃ w₀ : ℕ, ∀ w : ℕ, w₀ ≤ w →
    105 ∀ {U Ω W : Type} [Fintype U] [Nonempty U] [Fintype Ω] [Nonempty Ω]
    106 [Fintype W] [DecidableEq W],
    107 ∀ u : ℕ, ∀ (question : U → Ω → W)
    108 (ρ : U → Ω → LongCode.Word w → LongCode.Word u) (valid : U → Ω → Coordinate w),
    109 (∀ (P : W → Option (LongCode.Word w)) (Q : U → Option (LongCode.Word u)),
    110 FiniteProbability.probability (DecodedStrategies.Wins question
    111 (FAFStrategyExtraction.Relation ρ valid) P Q) < FAFComposition.gameThreshold l s) →
    112 Sound (system (n := 10 * l) (s := s) (q := 10 * l * s) question ρ valid)
    113 ((1 / 2 : ℝ) ^ (20 * l * l * s))
    114
    115axiom proof_length (U W : Type) [Fintype U] [Fintype W] (u w : ℕ) :
    116 Fintype.card (Index U W u w) = Fintype.card U * 2 ^ (2 ^ u) + Fintype.card W * 2 ^ (2 ^ w)
    117
    118axiom random_choices (U Ω : Type) [Fintype U] [Fintype Ω] (u w n s q : ℕ) :
    119 Fintype.card (Randomness U Ω u w n s q) =
    120 Fintype.card U * (Fintype.card Ω ^ n * (2 ^ (2 ^ u)) ^ q * ((2 ^ (2 ^ w)) ^ s) ^ n)
    121
    122end Lax323828.FAFLocalTests
    123
    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…