Lax Lean Archive

The consistency graph as an approximation input

Lax323828.EncodedReduction · concepts/Lax323828/EncodedReduction.lean · lax-323828

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

    Numbering the vertices of the consistency graph produces an input to the clique approximation problem whose clique number is exactly the optimum acceptance count of the local tests.

    An N1−εN^{1-\varepsilon}-approximation separates optimum acceptance counts at most aa from counts at least bb whenever N1−εa<bN^{1-\varepsilon}a<b, provided N>0N>0. The separating predicate compares the returned integer with aa. The same polynomial-time estimator works for every such system and gap.

    This statement supplies the graph-theoretic and numerical transfer. Efficiently producing the accepting views and the numbered graph from a language input remains a separate machine-construction obligation.

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

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

    1 approximation_separates proven

    2 cliqueNumber_output proven

    Lean source view on GitHub

    1import Lax323828.CliqueCorrespondence
    2import Lax323828.GraphEncoding
    3import Lax323828.Approximation
    4
    5/-!
    6---
    7title: The consistency graph as an approximation input
    8type: theorem
    9---
    10Numbering the vertices of the consistency graph produces an input to the
    11clique approximation problem whose clique number is exactly the optimum
    12acceptance count of the local tests.
    13
    14An N1−εN^{1-\varepsilon}-approximation separates optimum acceptance counts
    15at most aa from counts at least bb whenever
    16N1−εa<bN^{1-\varepsilon}a<b, provided N>0N>0. The separating predicate compares
    17the returned integer with aa. The same polynomial-time estimator works
    18for every such system and gap.
    19
    20This statement supplies the graph-theoretic and numerical transfer.
    21Efficiently producing the accepting views and the numbered graph from a
    22language input remains a separate machine-construction obligation.
    23-/
    24
    25namespace Lax323828.EncodedReduction
    26
    27open scoped Classical
    28
    29open LocalTests ConsistencyGraph Lax434930.PolynomialTime
    30
    31/-- The consistency graph with consecutively numbered vertices, in the approximation algorithm’s input format. -/
    32noncomputable def output {r m : ℕ} (C : System r m) :
    33 Graphs.Graph (Fintype.card (Vertex C)) :=
    34 GraphEncoding.numbered (graph C) (Fintype.equivFin (Vertex C)).symm
    35
    36axiom cliqueNumber_output {r m : ℕ} (C : System r m) :
    37 (output C).cliqueNumber = C.optimum
    38
    39axiom approximation_separates (ε : ℝ) (hε : Approximation.Approximable ε) :
    40 ∃ estimate : Word → ℕ,
    41 Nonempty (Turing.TM2ComputableInPolyTime id Computability.encodeNat estimate) ∧
    42 ∀ (r m : ℕ) (C : System r m), 0 < Fintype.card (Vertex C) →
    43 ∀ a b : ℕ,
    44 Real.rpow (Fintype.card (Vertex C) : ℝ) (1 - ε) * (a : ℝ) < (b : ℝ) →
    45 (C.optimum ≤ a → estimate (output C).encode ≤ a) ∧
    46 (b ≤ C.optimum → a < estimate (output C).encode)
    47
    48end Lax323828.EncodedReduction
    49
    Show 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…