Multicoloured Clique Is W[1]-Complete

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

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

    Multicoloured Clique — given a graph whose vertices are properly coloured with kk colours, is there a clique with one vertex of each colour? — is W[1]-complete under fpt-reductions, parameterized by kk [CFK+15, Theorem 13.7]. It is the usual starting point of W[1]-hardness proofs.

    • pp-Clique ≤\le Multicoloured Clique. Take kk copies of the vertex set, copy cc coloured cc, and join (c,u)(c, u) and (c′,v)(c', v) when c≠c′c \ne c' and uvuv is an edge. A multicoloured clique picks kk distinct pairwise adjacent vertices, and conversely.
    • Multicoloured Clique ≤\le pp-Clique. Forget the colours: adjacent vertices have different colours, so a clique of kk vertices in a kk-coloured graph has one vertex of each colour.
    Concept map
    16 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Lean source view on GitHub

    1import Lax496464.WH_B4_Hierarchies
    2import Lax496464.WH_C1_GraphProblems
    3import Lax888481.MulticolouredClique
    4
    5/-!
    6---
    7title: Multicoloured Clique Is W[1]-Complete
    8type: theorem
    9---
    10Multicoloured Clique — given a graph whose vertices are properly coloured with kk colours, is
    11there a clique with one vertex of each colour? — is W[1]-complete under fpt-reductions,
    12parameterized by kk [CFK+15, Theorem 13.7]. It is the usual starting point of W[1]-hardness
    13proofs.
    14
    15* **pp-Clique ≤\le Multicoloured Clique.** Take kk copies of the vertex set, copy cc coloured cc,
    16 and join (c,u)(c, u) and (c′,v)(c', v) when c≠c′c \ne c' and uvuv is an edge. A multicoloured clique picks
    17 kk distinct pairwise adjacent vertices, and conversely.
    18* **Multicoloured Clique ≤\le pp-Clique.** Forget the colours: adjacent vertices have different
    19 colours, so a clique of kk vertices in a kk-coloured graph has one vertex of each colour.
    20
    21# Formalization Notes
    22
    23Multicoloured Clique is the archive's `Lax888481.MulticolouredClique.problem`: the compressed sparse
    24row encoding with sorted adjacency lists, one colour per vertex, and the number of colours.
    25-/
    26
    27namespace Lax496464.WH_D12_MulticolouredClique
    28
    29open Lax496464.WH_B4_Hierarchies Lax496464.WH_A2_FptReductions Lax496464.WH_C1_GraphProblems
    30
    31/-- The parameter of Multicoloured Clique is computable in polynomial time. -/
    32axiom multicolouredClique_isParameterized :
    33 IsParameterized Lax888481.MulticolouredClique.problem
    34
    35/-- **`p-Clique ≤fpt Multicoloured Clique`.** -/
    36axiom clique_le_multicolouredClique : Clique ≤ᶠᵖᵗ Lax888481.MulticolouredClique.problem
    37
    38/-- **`Multicoloured Clique ≤fpt p-Clique`.** -/
    39axiom multicolouredClique_le_clique : Lax888481.MulticolouredClique.problem ≤ᶠᵖᵗ Clique
    40
    41/-- **Multicoloured Clique is W[1]-complete.** -/
    42axiom multicolouredClique_W1_complete : Complete (W 1) Lax888481.MulticolouredClique.problem
    43
    44end Lax496464.WH_D12_MulticolouredClique
    45
    Show ProofShow ProofShow ProofShow Proof
    Formalization Notes

    Multicoloured Clique is the archive's Lax888481.MulticolouredClique.problemLax888481.MulticolouredClique.problem: the compressed sparse row encoding with sorted adjacency lists, one colour per vertex, and the number of colours.

    Discussion

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

    Loading discussion…