Lax Lean Archive

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

The finite randomized PCP-to-clique transfer

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

    Repeat the local tests and sample their random choices independently. With 2f2^f accepting views per choice and soundness 2−t2^{-t}, the graph size is bounded by the explicit polynomial in SamplingParameters, and its clique number is below 4(m+2)4(m+2) except on an event of probability at most 1/41/4. Perfect completeness holds for every sample.

    Consequently an n1−εn^{1-\varepsilon} approximation yields a decision rule with perfect completeness and false-positive probability at most 1/41/4 whenever εt>(1−ε)f\varepsilon t>(1-\varepsilon)f. Empty graphs are rejected. The estimator is the given polynomial-time estimator. This finite theorem does not assert a machine implementation of graph construction or sampling.

    Concept map
    15 concepts; 1 descendant 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_decision proven

    2 soundness proven

    3 vertex_bound proven

    Lean source view on GitHub

    1import Lax253009.SamplingParameters
    2import Lax253009.FreshBitSampling
    3
    4/-!
    5---
    6title: The finite randomized PCP-to-clique transfer
    7type: theorem
    8---
    9Repeat the local tests and sample their random choices independently. With
    102f2^f accepting views per choice and soundness 2−t2^{-t}, the graph size is
    11bounded by the explicit polynomial in SamplingParameters, and its clique
    12number is below 4(m+2)4(m+2) except on an event of probability at most 1/41/4.
    13Perfect completeness holds for every sample.
    14
    15Consequently an n1−εn^{1-\varepsilon} approximation yields a decision rule
    16with perfect completeness and false-positive probability at most 1/41/4
    17whenever εt>(1−ε)f\varepsilon t>(1-\varepsilon)f. Empty graphs are rejected.
    18The estimator is the given polynomial-time estimator. This finite theorem
    19does not assert a machine implementation of graph construction or sampling.
    20-/
    21
    22namespace Lax253009.RandomizedReduction
    23
    24open LocalTests ConsistencyGraph TestSampling TestRepetition SamplingParameters FiniteProbability
    25open Lax434930.PolynomialTime
    26
    27noncomputable def tests {r m : ℕ} (C : System r m) (t k : ℕ)
    28 (z : Fin (sampleCount t k m) → Fin (r ^ k)) : System (sampleCount t k m) m :=
    29 sampled (repeated C k) z
    30
    31def Accept {r m : ℕ} (estimate : Word → ℕ) (C : System r m) (t k : ℕ)
    32 (z : Fin (sampleCount t k m) → Fin (r ^ k)) : Prop :=
    33 0 < Fintype.card (Vertex (tests C t k z)) ∧
    34 threshold m < estimate (EncodedReduction.output (tests C t k z)).encode
    35
    36def CoinAccept {r m : ℕ} (estimate : Word → ℕ) (C : System r m) (hr : 0 < r) (t k : ℕ)
    37 (coins : Fin (sampleCount t k m * FreshBitSampling.bitsPerDraw (sampleCount t k m) (r ^ k)) → Bool) :
    38 Prop := Accept estimate C t k (FreshBitSampling.sampleFlat (pow_pos hr k) coins)
    39
    40axiom vertex_bound {r m : ℕ} (C : System r m) (f t k : ℕ)
    41 (hfree : ∀ seed, (C.accepting seed).card ≤ 2 ^ f)
    42 (z : Fin (sampleCount t k m) → Fin (r ^ k)) :
    43 Fintype.card (Vertex (tests C t k z)) ≤ vertexBound f t k m
    44
    45axiom soundness {r m : ℕ} (hr : 0 < r) (C : System r m) (t k : ℕ)
    46 (hsound : Sound C ((1 / 2 : ℝ) ^ t)) :
    47 probability (fun z : Fin (sampleCount t k m) → Fin (r ^ k) ↦
    48 threshold m ≤ (EncodedReduction.output (tests C t k z)).cliqueNumber) ≤ 1 / 4
    49
    50axiom approximation_decision (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1)
    51 (happrox : Approximation.Approximable ε) :
    52 ∃ estimate : Word → ℕ,
    53 Nonempty (Turing.TM2ComputableInPolyTime id Computability.encodeNat estimate) ∧
    54 ∀ (f t c : ℕ), 1 ≤ (c : ℝ) * ((t : ℝ) * ε - (f : ℝ) * (1 - ε)) →
    55 ∀ (r m : ℕ), 0 < r → ∀ C : System r m,
    56 (∀ seed, (C.accepting seed).card ≤ 2 ^ f) →
    57 (Complete C → ∀ z, Accept estimate C t (repetitions c m) z) ∧
    58 (Sound C ((1 / 2 : ℝ) ^ t) →
    59 probability (Accept estimate C t (repetitions c m)) ≤ 1 / 4)
    60
    61end Lax253009.RandomizedReduction
    62
    Show 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…