Lax Lean Archive

Independent Set Is W[1]-Complete

Lax496464.WH_D11_IndependentSet · concepts/Lax496464/WH_D11_IndependentSet.lean · lax-496464

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

    pp-Independent-Set is W[1]-complete under fpt-reductions [FG06, Corollary 6.2].

    A set of vertices is independent in GG exactly when it is a clique in the complement G‾\overline G, so (G,k)↦(G‾,k)(G, k) \mapsto (\overline G, k) reduces each problem to the other. The complement is computable in polynomial time and the parameter is unchanged. Completeness follows from that of Clique (WHD10CliqueW1CompleteWH_D10_CliqueW1Complete).

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

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

    1 clique_le_independentSet proven

    2 independentSet_isParameterized proven

    3 independentSet_le_clique proven

    4 independentSet_W1_complete proven

    Lean source view on GitHub

    1import Lax496464.WH_B4_Hierarchies
    2import Lax496464.WH_C1_GraphProblems
    3
    4/-!
    5---
    6title: Independent Set Is W[1]-Complete
    7type: theorem
    8---
    9pp-Independent-Set is W[1]-complete under fpt-reductions [FG06, Corollary 6.2].
    10
    11A set of vertices is independent in GG exactly when it is a clique in the complement G‾\overline G, so
    12(G,k)↦(G‾,k)(G, k) \mapsto (\overline G, k) reduces each problem to the other. The complement is computable in
    13polynomial time and the parameter is unchanged. Completeness follows from that of Clique
    14(`WH_D10_CliqueW1Complete`).
    15-/
    16
    17namespace Lax496464.WH_D11_IndependentSet
    18
    19open Lax496464.WH_B4_Hierarchies Lax496464.WH_A2_FptReductions Lax496464.WH_C1_GraphProblems
    20
    21/-- The parameter of `p-Independent-Set` is computable in polynomial time. -/
    22axiom independentSet_isParameterized : IsParameterized IndependentSet
    23
    24/-- **`p-Clique ≤fpt p-Independent-Set`**, by the complement graph. -/
    25axiom clique_le_independentSet : Clique ≤ᶠᵖᵗ IndependentSet
    26
    27/-- **`p-Independent-Set ≤fpt p-Clique`**, by the complement graph. -/
    28axiom independentSet_le_clique : IndependentSet ≤ᶠᵖᵗ Clique
    29
    30/-- **`p-Independent-Set` is W[1]-complete.** -/
    31axiom independentSet_W1_complete : Complete (W 1) IndependentSet
    32
    33end Lax496464.WH_D11_IndependentSet
    34
    Show ProofShow ProofShow ProofShow Proof
    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…