Lax Lean Archive

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

Random sparsification of a consistency graph

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

    Sample NN independent random choices of a finite local-test system, with replacement, and construct its consistency graph. Every sampled choice keeps its own index, including repeated choices. Perfect completeness is preserved for every sample, and AA accepting views per choice give at most NANA vertices.

    If every proof is accepted with probability at most pp and Np≥m+2Np\geq m+2, where mm is the proof length, then with probability at least 3/43/4 the sampled graph has clique number less than 4Np4Np. The bound holds simultaneously for every proof, including proofs chosen after sampling.

    Concept map
    11 concepts; 5 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 perfect_completeness proven

    2 soundness proven

    3 vertex_bound proven

    Lean source view on GitHub

    1import Lax253009.LocalTests
    2import Lax253009.EncodedReduction
    3import Lax253009.BernoulliSampling
    4
    5/-!
    6---
    7title: Random sparsification of a consistency graph
    8type: theorem
    9---
    10Sample NN independent random choices of a finite local-test system, with
    11replacement, and construct its consistency graph. Every sampled choice
    12keeps its own index, including repeated choices. Perfect completeness is
    13preserved for every sample, and AA accepting views per choice give at most
    14NANA vertices.
    15
    16If every proof is accepted with probability at most pp and Np≥m+2Np\geq m+2,
    17where mm is the proof length, then with probability at least 3/43/4 the
    18sampled graph has clique number less than 4Np4Np. The bound holds
    19simultaneously for every proof, including proofs chosen after sampling.
    20-/
    21
    22namespace Lax253009.TestSampling
    23
    24open LocalTests FiniteProbability ConsistencyGraph
    25
    26def Passes {r m : ℕ} (C : System r m) (π : Oracle m) (seed : Fin r) : Prop :=
    27 ∃ a ∈ C.accepting seed, Extends π a
    28
    29def Complete {r m : ℕ} (C : System r m) : Prop := ∃ π, ∀ seed, Passes C π seed
    30
    31def Sound {r m : ℕ} (C : System r m) (p : ℝ) : Prop :=
    32 ∀ π, probability (Passes C π) ≤ p
    33
    34def sampled {r m N : ℕ} (C : System r m) (z : Fin N → Fin r) : System N m :=
    35 ⟨fun i ↦ C.accepting (z i)⟩
    36
    37axiom vertex_bound {r m N : ℕ} (C : System r m) (z : Fin N → Fin r)
    38 (A : ℕ) (hA : ∀ seed, (C.accepting seed).card ≤ A) :
    39 Fintype.card (Vertex (sampled C z)) ≤ N * A
    40
    41axiom perfect_completeness {r m N : ℕ} (C : System r m) (hC : Complete C)
    42 (z : Fin N → Fin r) :
    43 (EncodedReduction.output (sampled C z)).cliqueNumber = N
    44
    45axiom soundness {r m N : ℕ} (hr : 0 < r) (C : System r m) (p : ℝ) (hp : 0 ≤ p)
    46 (hC : Sound C p) (hN : (m : ℝ) + 2 ≤ N * p) :
    47 probability (fun z : Fin N → Fin r ↦
    48 4 * N * p ≤ ((EncodedReduction.output (sampled C z)).cliqueNumber : ℝ)) ≤ 1 / 4
    49
    50end Lax253009.TestSampling
    51
    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…