Multicoloured Clique Is W[1]-Complete
Lax496464.WH_D12_MulticolouredClique · concepts/Lax496464/WH_D12_MulticolouredClique.lean · lax-496464
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Multicoloured Clique — given a graph whose vertices are properly coloured with colours, is there a clique with one vertex of each colour? — is W[1]-complete under fpt-reductions, parameterized by [CFK+15, Theorem 13.7]. It is the usual starting point of W[1]-hardness proofs.
- -Clique Multicoloured Clique. Take copies of the vertex set, copy coloured , and join and when and is an edge. A multicoloured clique picks distinct pairwise adjacent vertices, and conversely.
- Multicoloured Clique -Clique. Forget the colours: adjacent vertices have different colours, so a clique of vertices in a -coloured graph has one vertex of each colour.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax496464.WH_B4_Hierarchies |
| 2 | import Lax496464.WH_C1_GraphProblems |
| 3 | import Lax888481.MulticolouredClique |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Multicoloured Clique Is W[1]-Complete |
| 8 | type: theorem |
| 9 | --- |
| 10 | Multicoloured Clique — given a graph whose vertices are properly coloured with colours, is |
| 11 | there a clique with one vertex of each colour? — is W[1]-complete under fpt-reductions, |
| 12 | parameterized by [CFK+15, Theorem 13.7]. It is the usual starting point of W[1]-hardness |
| 13 | proofs. |
| 14 | |
| 15 | * **-Clique Multicoloured Clique.** Take copies of the vertex set, copy coloured , |
| 16 | and join and when and is an edge. A multicoloured clique picks |
| 17 | distinct pairwise adjacent vertices, and conversely. |
| 18 | * **Multicoloured Clique -Clique.** Forget the colours: adjacent vertices have different |
| 19 | colours, so a clique of vertices in a -coloured graph has one vertex of each colour. |
| 20 | |
| 21 | # Formalization Notes |
| 22 | |
| 23 | Multicoloured Clique is the archive's `Lax888481.MulticolouredClique.problem`: the compressed sparse |
| 24 | row encoding with sorted adjacency lists, one colour per vertex, and the number of colours. |
| 25 | -/ |
| 26 | |
| 27 | namespace Lax496464.WH_D12_MulticolouredClique |
| 28 | |
| 29 | open Lax496464.WH_B4_Hierarchies Lax496464.WH_A2_FptReductions Lax496464.WH_C1_GraphProblems |
| 30 | |
| 31 | /-- The parameter of Multicoloured Clique is computable in polynomial time. -/ |
| 32 | axiom multicolouredClique_isParameterized : |
| 33 | IsParameterized Lax888481.MulticolouredClique.problem |
| 34 | |
| 35 | /-- **`p-Clique ≤fpt Multicoloured Clique`.** -/ |
| 36 | axiom clique_le_multicolouredClique : Clique ≤ᶠᵖᵗ Lax888481.MulticolouredClique.problem |
| 37 | |
| 38 | /-- **`Multicoloured Clique ≤fpt p-Clique`.** -/ |
| 39 | axiom multicolouredClique_le_clique : Lax888481.MulticolouredClique.problem ≤ᶠᵖᵗ Clique |
| 40 | |
| 41 | /-- **Multicoloured Clique is W[1]-complete.** -/ |
| 42 | axiom multicolouredClique_W1_complete : Complete (W 1) Lax888481.MulticolouredClique.problem |
| 43 | |
| 44 | end Lax496464.WH_D12_MulticolouredClique |
| 45 |
Formalization Notes
Multicoloured Clique is the archive's : the compressed sparse row encoding with sorted adjacency lists, one colour per vertex, and the number of colours.
Used by
none
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments