Lax Lean Archive

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

Randomized promise-gap hardness of Max Independent Set

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

open

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

    For every integer q≥3q\geq3, a bounded-error randomized polynomial-time algorithm distinguishing α(G)≤n1/q\alpha(G)\leq n^{1/q} from α(G)≥n1−1/q\alpha(G)\geq n^{1-1/q} on all sufficiently large nn-vertex graphs would imply NP⊆BPP\mathrm{NP}\subseteq\mathrm{BPP}.

    This randomized promise-gap form of Håstad's hardness result is assumed without proof. It is separate from the proved deterministic clique-approximation statements. NP and BPP are the registered binary-language classes from lax-434930 and lax-666725.

    Concept map
    10 concepts
    100%
    Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    No proof in the archive yet — this claim is open.

    Lean source view on GitHub

    1import Lax253009.IndependentSetGap
    2import Lax434930.NondeterministicPolynomialTime
    3import Lax666725.RandomizedPolynomialTime
    4
    5/-!
    6---
    7title: Randomized promise-gap hardness of Max Independent Set
    8type: theorem
    9---
    10For every integer q≥3q\geq3, a bounded-error randomized polynomial-time
    11algorithm distinguishing α(G)≤n1/q\alpha(G)\leq n^{1/q} from
    12α(G)≥n1−1/q\alpha(G)\geq n^{1-1/q} on all sufficiently large nn-vertex graphs
    13would imply NP⊆BPP\mathrm{NP}\subseteq\mathrm{BPP}.
    14
    15This randomized promise-gap form of Håstad's hardness result is assumed
    16without proof. It is separate from the proved deterministic
    17clique-approximation statements. NP and BPP are the registered binary-language
    18classes from lax-434930 and lax-666725.
    19-/
    20
    21namespace Lax253009.IndependentSetGapHardness
    22
    23open Lax434930.NondeterministicPolynomialTime
    24open Lax666725.RandomizedPolynomialTime
    25
    26/-- Håstad's randomized promise-gap hardness, assumed without proof. -/
    27axiom gapSolver_implies_np_subset_bpp (q : ℕ) (hq : 3 ≤ q) :
    28 IndependentSetGap.Solver q → NP ⊆ BPP
    29
    30end Lax253009.IndependentSetGapHardness
    31
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…