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

Håstad's clique inapproximability theorem

Lax253009.CliqueHardness · concepts/Lax253009/CliqueHardness.lean · lax-253009

proven

Loading review…

Sign in with ORCID

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

    For every fixed real ε>0\varepsilon>0, a deterministic polynomial-time n1−εn^{1-\varepsilon}-approximation of the clique number would imply NP=ZPP\mathrm{NP}=\mathrm{ZPP}. Equivalently, if NP≠ZPP\mathrm{NP}\ne\mathrm{ZPP}, no such approximation exists. This is Theorem 5.2 of Håstad's paper.

    The approximation convention includes a single uniform algorithm and all nonempty finite graphs. NP is the binary-language class from lax-434930; ZPP is the bounded-time, failure-allowed class from lax-666725. No complexity class is redefined here. The proof implements the reductions in these machine models, with an explicit polynomial clock and exact preservation of the finite fair-coin output distribution.

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

    Lean source view on GitHub

    1import Lax253009.Approximation
    2import Lax434930.NondeterministicPolynomialTime
    3import Lax666725.ZeroError
    4
    5/-!
    6---
    7title: Håstad's clique inapproximability theorem
    8type: theorem
    9---
    10For every fixed real ε>0\varepsilon>0, a deterministic polynomial-time
    11n1−εn^{1-\varepsilon}-approximation of the clique number would imply
    12NP=ZPP\mathrm{NP}=\mathrm{ZPP}. Equivalently, if NP≠ZPP\mathrm{NP}\ne\mathrm{ZPP},
    13no such approximation exists. This is Theorem 5.2 of Håstad's paper.
    14
    15The approximation convention includes a single uniform algorithm and all
    16nonempty finite graphs. NP is the binary-language class from lax-434930;
    17ZPP is the bounded-time, failure-allowed class from lax-666725. No complexity
    18class is redefined here. The proof implements the reductions in these machine
    19models, with an explicit polynomial clock and exact preservation of the
    20finite fair-coin output distribution.
    21-/
    22
    23namespace Lax253009.CliqueHardness
    24
    25open Approximation
    26open Lax434930.NondeterministicPolynomialTime Lax666725.ZeroError
    27
    28axiom approximation_implies_np_eq_zpp (ε : ℝ) (hε : 0 < ε) :
    29 Approximable ε → NP = ZPP
    30
    31axiom not_approximable (ε : ℝ) (hε : 0 < ε) (hne : NP ≠ ZPP) :
    32 ¬ Approximable ε
    33
    34end Lax253009.CliqueHardness
    35
    Show ProofShow Proof

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…