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.

Read the Lean proof on GitHub

Description

p-Clique ≤fpt Multicoloured Clique. For k≤nk ≤ n, take kk copies of the vertex set, the copy cc coloured cc, and join (c,u)(c, u) and (c′,v)(c', v) when c≠c′c ≠ c' and uvuv is an edge; a multicoloured clique picks kk distinct pairwise adjacent vertices, and conversely. For k>nk > n the word of a fixed no-instance (one colour, no vertices) is written. The number of colours is at most kk, and the map is computed in polynomial time.