Lax Lean Archive

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

Polynomial size and approximation gap after sampling

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

    For a verifier with soundness 2−t2^{-t} and at most 2f2^f accepting views, repeat k=c(⌈log⁡2(m+2)⌉+3)k=c(\lceil\log_2(m+2)\rceil+3) times and sample (m+2)2tk(m+2)2^{tk} choices. The sampled consistency graph has at most (m+2)2(t+f)k(m+2)2^{(t+f)k} vertices and its low-clique threshold is 4(m+2)4(m+2).

    If c(εt−(1−ε)f)≥1c(\varepsilon t-(1-\varepsilon)f)\geq1, this separates an n1−εn^{1-\varepsilon} approximation. The vertex bound is polynomial in the proof length, with a degree depending only on the fixed verifier and approximation parameters. These are size bounds, not machine running-time certificates.

    Concept map
    13 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 approximation_gap proven

    2 choose_multiplier proven

    3 polynomial_bound proven

    Lean source view on GitHub

    1import Lax253009.TestRepetition
    2import Mathlib.Data.Nat.Log
    3
    4/-!
    5---
    6title: Polynomial size and approximation gap after sampling
    7type: theorem
    8---
    9For a verifier with soundness 2−t2^{-t} and at most 2f2^f accepting views,
    10repeat k=c(⌈log⁡2(m+2)⌉+3)k=c(\lceil\log_2(m+2)\rceil+3) times and sample
    11(m+2)2tk(m+2)2^{tk} choices. The sampled consistency graph has at most
    12(m+2)2(t+f)k(m+2)2^{(t+f)k} vertices and its low-clique threshold is 4(m+2)4(m+2).
    13
    14If c(εt−(1−ε)f)≥1c(\varepsilon t-(1-\varepsilon)f)\geq1, this separates an
    15n1−εn^{1-\varepsilon} approximation. The vertex bound is polynomial in the
    16proof length, with a degree depending only on the fixed verifier and
    17approximation parameters. These are size bounds, not machine running-time
    18certificates.
    19-/
    20
    21namespace Lax253009.SamplingParameters
    22
    23def repetitions (c m : ℕ) : ℕ := c * (Nat.clog 2 (m + 2) + 3)
    24
    25def sampleCount (t k m : ℕ) : ℕ := (m + 2) * 2 ^ (t * k)
    26
    27def vertexBound (f t k m : ℕ) : ℕ := (m + 2) * 2 ^ ((t + f) * k)
    28
    29def threshold (m : ℕ) : ℕ := 4 * (m + 2)
    30
    31axiom polynomial_bound (f t c m : ℕ) :
    32 vertexBound f t (repetitions c m) m ≤
    33 16 ^ ((t + f) * c) * (m + 2) ^ ((t + f) * c + 1)
    34
    35axiom approximation_gap (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1)
    36 (f t c : ℕ) (hmargin : 1 ≤ (c : ℝ) * ((t : ℝ) * ε - (f : ℝ) * (1 - ε))) (m : ℕ) :
    37 Real.rpow (vertexBound f t (repetitions c m) m : ℝ) (1 - ε) * threshold m <
    38 sampleCount t (repetitions c m) m
    39
    40axiom choose_multiplier (ε : ℝ) (f t : ℕ)
    41 (hmargin : 0 < (t : ℝ) * ε - (f : ℝ) * (1 - ε)) :
    42 ∃ c : ℕ, 0 < c ∧ 1 ≤ (c : ℝ) * ((t : ℝ) * ε - (f : ℝ) * (1 - ε))
    43
    44end Lax253009.SamplingParameters
    45
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…