Lax Lean Archive

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

The consistency graph as an approximation input

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

    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 Lax253009.CliqueCorrespondence
    2import Lax253009.GraphEncoding
    3import Lax253009.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 Lax253009.EncodedReduction
    26
    27open LocalTests ConsistencyGraph Lax434930.PolynomialTime
    28
    29noncomputable def output {r m : ℕ} (C : System r m) :
    30 Graphs.Graph (Fintype.card (Vertex C)) := by
    31 classical
    32 exact GraphEncoding.numbered (graph C) (Fintype.equivFin (Vertex C)).symm
    33
    34axiom cliqueNumber_output {r m : ℕ} (C : System r m) :
    35 (output C).cliqueNumber = C.optimum
    36
    37axiom approximation_separates (ε : ℝ) (hε : Approximation.Approximable ε) :
    38 ∃ estimate : Word → ℕ,
    39 Nonempty (Turing.TM2ComputableInPolyTime id Computability.encodeNat estimate) ∧
    40 ∀ (r m : ℕ) (C : System r m), 0 < Fintype.card (Vertex C) →
    41 ∀ a b : ℕ,
    42 Real.rpow (Fintype.card (Vertex C) : ℝ) (1 - ε) * (a : ℝ) < (b : ℝ) →
    43 (C.optimum ≤ a → estimate (output C).encode ≤ a) ∧
    44 (b ≤ C.optimum → a < estimate (output C).encode)
    45
    46end Lax253009.EncodedReduction
    47
    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…