Proof of `Multicoloured Clique Is W[1]-Complete` (1st statement)
groundedproofs/Lax496464Proofs/WHierarchy/Reductions/CliqueMCC/ProdFinal.lean · lax-496464
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
p-Clique ≤fpt Multicoloured Clique. For , take copies of the vertex set, the copy coloured , and join and when and is an edge; a multicoloured clique picks distinct pairwise adjacent vertices, and conversely. For the word of a fixed no-instance (one colour, no vertices) is written. The number of colours is at most , and the map is computed in polynomial time.