Lax Lean Archive

Proof of `Independent Set Reduces to Multicoloured Clique` (3rd statement)

groundedproofs/Lax496464Proofs/WHierarchy/MccNP/HardnessFinal.lean · lax-496464

What this proof establishes

no assumptions

thm✓Lax496464.WH_F4_IndependentSetToMcc (3rd statement)

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

Independent Set fpt-reduces to Multicoloured Clique with gk=(k+1)2g k = (k + 1) ^ 2 and hk=kh k = k: the map is correct, sends words of instances to words of instances, preserves the parameter kk, and runs in time c∗(k+1)2∗(∣x∣+1)c * (k + 1) ^ 2 * (|x| + 1).