Lax Lean Archive

The finite few-amortized-free-bits test

Lax323828.FAFTest · concepts/Lax323828/FAFTest.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

    Fix a small variable set and a distribution of larger sets. Each larger set carries a purported long code and a constraint predicate. The verifier reads qq random functions on the small set, then checks nn independently chosen larger tables using the CNA test with side conditions enforcing both the constraints and agreement with the reference answers.

    The rejection bound combines CNA decoding errors and the many-table agreement estimate. It is uniform in the reference table, which need not be a genuine long code. The projections and constraints are explicit finite data; efficient construction from an NP input is a separate obligation.

    Concept map
    5 concepts; 6 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 acceptance_bound proven

    2 perfect_completeness proven

    Lean source view on GitHub

    1import Lax323828.LongCode
    2import Lax323828.CNASoundness
    3import Lax323828.ManyTableConsistency
    4
    5/-!
    6---
    7title: The finite few-amortized-free-bits test
    8type: theorem
    9---
    10Fix a small variable set and a distribution of larger sets. Each larger
    11set carries a purported long code and a constraint predicate. The verifier
    12reads qq random functions on the small set, then checks nn independently
    13chosen larger tables using the CNA test with side conditions enforcing both
    14the constraints and agreement with the reference answers.
    15
    16The rejection bound combines CNA decoding errors and the many-table
    17agreement estimate. It is uniform in the reference table, which need not
    18be a genuine long code. The projections and constraints are explicit finite
    19data; efficient construction from an NP input is a separate obligation.
    20-/
    21
    22namespace Lax323828.FAFTest
    23
    24open LongCode FiniteProbability CNASoundness
    25
    26noncomputable def condition {Ω : Type} {u w q : ℕ}
    27 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w)
    28 (R : Table u) (ω : Ω) (g : Fin q → Coordinate u) : Coordinate w :=
    29 fun y ↦ valid ω y && decide (∀ j, g j (ρ ω y) = R (g j))
    30
    31def Accepts {Ω : Type} {u w n s q : ℕ}
    32 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w)
    33 (R : Table u) (A : Ω → Table w)
    34 (ω : Fin n → Ω) (g : Fin q → Coordinate u)
    35 (f : Fin n → Fin s → Coordinate w) : Prop :=
    36 ∀ i, AcceptsWithCondition (A (ω i)) (f i) (condition ρ valid R (ω i) g)
    37
    38axiom perfect_completeness {Ω : Type} {u w n s q : ℕ}
    39 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w)
    40 (x : Word u) (y : Ω → Word w)
    41 (hvalid : ∀ ω, valid ω (y ω) = true) (hproject : ∀ ω, ρ ω (y ω) = x)
    42 (ω : Fin n → Ω) (g : Fin q → Coordinate u) (f : Fin n → Fin s → Coordinate w) :
    43 Accepts ρ valid (evaluation x) (fun ω ↦ evaluation (y ω)) ω g f
    44
    45noncomputable def projected {Ω : Type} {u w : ℕ}
    46 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w)
    47 (D : Ω → Finset (Word w)) (ω : Ω) : Finset (Word u) :=
    48 ((D ω).filter (fun y ↦ valid ω y = true)).image (ρ ω)
    49
    50axiom acceptance_bound {Ω : Type} [Fintype Ω] [Nonempty Ω]
    51 (u w n s q : ℕ) (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w)
    52 (R : Table u) (A : Ω → Table w) (D : Ω → Finset (Word w))
    53 (B k : ℕ) (p δ : ℝ) (hp : 0 ≤ p)
    54 (hB : ∀ ω, (D ω).card ≤ B)
    55 (hdecode : ∀ ω h, probability (BadWithCondition (s := s) (A ω) (D ω) h) ≤ δ)
    56 (hpoint : ∀ x, probability (fun ω ↦ x ∈ projected ρ valid D ω) ≤ p)
    57 (hsmall : (n : ℝ) * B * p ≤ 1) :
    58 probability (fun z : ((Fin n → Ω) × (Fin q → Coordinate u)) ×
    59 (Fin n → Fin s → Coordinate w) ↦ Accepts ρ valid R A z.1.1 z.1.2 z.2) ≤
    60 n * δ + (2 : ℝ) ^ n * ((n : ℝ) * B * p) ^ (n - k) +
    61 (B : ℝ) ^ n * (2 * (1 / 2 : ℝ) ^ (k + 1)) ^ q
    62
    63end Lax323828.FAFTest
    64
    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…