Lax Lean Archive

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

Clique number equals the maximum number of accepting random choices

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

    A proof accepted on kk random choices yields a clique of size kk in the consistency graph. Conversely, the local views of any clique extend to one global proof accepted on at least as many random choices. Consequently the clique number equals the maximum number of random choices on which a proof is accepted.

    If every proof is accepted on at most ss choices, the clique number is at most ss. Perfect completeness gives a clique of size rr. If each random choice has at most AA accepting views, the graph has at most rArA vertices; in particular ff free bits give the bound r2fr2^f.

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

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

    1 cliqueNumber_eq_optimum proven

    2 completeness proven

    3 perfect_completeness proven

    4 soundness proven

    5 soundness_bound proven

    6 vertex_bound proven

    7 vertex_count proven

    Lean source view on GitHub

    1import Lax253009.ConsistencyGraph
    2
    3/-!
    4---
    5title: Clique number equals the maximum number of accepting random choices
    6type: theorem
    7---
    8A proof accepted on kk random choices yields a clique of size kk in the
    9consistency graph. Conversely, the local views of any clique extend to
    10one global proof accepted on at least as many random choices.
    11Consequently the clique number equals the maximum number of random choices
    12on which a proof is accepted.
    13
    14If every proof is accepted on at most ss choices, the clique number is at
    15most ss. Perfect completeness gives a clique of size rr. If each random
    16choice has at most AA accepting views, the graph has at most rArA vertices;
    17in particular ff free bits give the bound r2fr2^f.
    18-/
    19
    20namespace Lax253009.CliqueCorrespondence
    21
    22open LocalTests ConsistencyGraph
    23
    24axiom completeness {r m : ℕ} (C : System r m) (π : Oracle m) :
    25 ∃ s : Finset (Vertex C), (graph C).IsClique s ∧ s.card = (C.acceptedSeeds π).card
    26
    27axiom soundness {r m : ℕ} (C : System r m) (s : Finset (Vertex C))
    28 (hs : (graph C).IsClique s) :
    29 ∃ π : Oracle m, s.card ≤ (C.acceptedSeeds π).card
    30
    31axiom cliqueNumber_eq_optimum {r m : ℕ} (C : System r m) :
    32 (graph C).cliqueNum = C.optimum
    33
    34axiom vertex_count {r m : ℕ} (C : System r m) :
    35 Fintype.card (Vertex C) = ∑ seed, (C.accepting seed).card
    36
    37axiom vertex_bound {r m : ℕ} (C : System r m) (A : ℕ)
    38 (hA : ∀ seed, (C.accepting seed).card ≤ A) :
    39 Fintype.card (Vertex C) ≤ r * A
    40
    41axiom perfect_completeness {r m : ℕ} (C : System r m)
    42 (h : ∃ π : Oracle m, ∀ seed, seed ∈ C.acceptedSeeds π) :
    43 (graph C).cliqueNum = r
    44
    45axiom soundness_bound {r m : ℕ} (C : System r m) (s : ℕ)
    46 (h : ∀ π : Oracle m, (C.acceptedSeeds π).card ≤ s) :
    47 (graph C).cliqueNum ≤ s
    48
    49end Lax253009.CliqueCorrespondence
    50
    Show ProofShow ProofShow ProofShow ProofShow 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…