Proof of `Clique Is in W[1]` (2nd statement)

groundedproofs/Lax496464Proofs/WHierarchy/Reductions/CliqueLogic/CliqueWD.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≤fptp−WDcliquep-Clique ≤fpt p-WD_clique. A graph becomes the structure with universe its vertices and one binary relation, its edges (listed from the adjacency matrix, so without repetition), and kk stays kk. The witnesses of clique(X)clique(X) of weight kk are the kk-cliques, the parameter is unchanged, and the map is computed by an IMP+ program in O(∣x∣3)O(|x|³) steps.