Lax Lean Archive

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

Finite quantitative soundness of the CNA test with side conditions

Lax253009.CNAQuantitativeSoundness · concepts/Lax253009/CNAQuantitativeSoundness.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 soundness at each evaluation point with concentration of random label fibers. Every accepted run agrees with an entire fiber. Unless a fiber is unusually small, averaging over the possible evaluation points costs only a factor twice the number of labels, independently of the number of words. Projection makes the decoding set independent of the side condition.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax253009.CNAPointSoundness
    2import Lax253009.CNASoundness
    3import Lax253009.RandomFibers
    4
    5/-!
    6---
    7title: Finite quantitative soundness of the CNA test with side conditions
    8type: theorem
    9---
    10Combine soundness at each evaluation point with concentration of random
    11label fibers. Every accepted run agrees with an entire fiber. Unless a
    12fiber is unusually small, averaging over the possible evaluation points
    13costs only a factor twice the number of labels, independently of the
    14number of words. Projection makes the decoding set independent of the
    15side condition.
    16-/
    17
    18namespace Lax253009.CNAQuantitativeSoundness
    19
    20open LongCode BooleanFourier CNAPointSoundness CNASoundness FiniteProbability
    21
    22noncomputable def totalBound (l m r s w : ℕ) (τ q : ℝ) : ℝ :=
    23 (2 : ℝ) ^ s * Real.exp (-((2 : ℝ) ^ w) / (8 * ((2 : ℝ) ^ s) ^ 2)) +
    24 2 * (2 : ℝ) ^ s * pointBound l m r (2 ^ s) τ q
    25
    26axiom quantitative_soundness (w s l m r : ℕ) (hs : 0 < s)
    27 (hl : 0 < l) (hlN : l < 2 ^ s)
    28 (τ q : ℝ) (hτ : 0 < τ) (hq : 0 ≤ q) (hq1 : q ≤ 1)
    29 (hr : 2 * r ≤ m) (hm : Even m)
    30 (hlarge : (l : ℝ) / ((2 : ℝ) ^ s - l) / τ ≤ 1 / 3)
    31 (A : Table w) (h : Coordinate w) :
    32 probability (BadWithCondition (s := s) A (decoding (fun g ↦ sign (A g)) l τ) h) ≤
    33 totalBound l m r s w τ q
    34
    35end Lax253009.CNAQuantitativeSoundness
    36
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…