Lax Lean Archive

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

Promise-gap hardness of Max Independent Set

Lax47.IndependentSetGapHardness · concepts/Lax47/IndependentSetGapHardness.lean · lax-47

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

    Håstad's general-graph inapproximability result supplies the hardness theorem used by the reduction. We use its rational promise-gap form. For every integer q>2q>2, a bounded-error polynomial-step algorithm distinguishing nn-vertex graphs HH with α(H)≤n1/q\alpha(H)\leq n^{1/q} from those with n1−1/q≤α(H)n^{1-1/q}\leq\alpha(H) would imply NP⊆BPPNP\subseteq BPP.

    This result is assumed without proof.

    Concept map
    11 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 Lax47.Gap
    2import Lax434930.NondeterministicPolynomialTime
    3import Lax666725.RandomizedPolynomialTime
    4
    5/-!
    6---
    7title: Promise-gap hardness of Max Independent Set
    8type: theorem
    9---
    10Håstad's general-graph inapproximability result supplies the hardness theorem
    11used by the reduction. We use its rational promise-gap form. For
    12every integer q>2q>2, a bounded-error polynomial-step algorithm distinguishing
    13nn-vertex graphs HH with α(H)≤n1/q\alpha(H)\leq n^{1/q} from those with
    14n1−1/q≤α(H)n^{1-1/q}\leq\alpha(H) would imply NP⊆BPPNP\subseteq BPP.
    15
    16This result is assumed without proof.
    17-/
    18
    19set_option autoImplicit false
    20
    21namespace Lax47.IndependentSetGapHardness
    22
    23open Lax47.Gap
    24open Lax434930.NondeterministicPolynomialTime
    25open Lax666725.RandomizedPolynomialTime
    26
    27/-- Håstad's general-graph promise-gap inapproximability theorem. -/
    28axiom gapSolver_implies_np_subset_bpp :
    29 ∀ q : ℕ, 3 ≤ q → MISGapSolver q → NP ⊆ BPP
    30
    31end Lax47.IndependentSetGapHardness
    32
    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…