Proof of `Hitting Set Is in W[2]` (2nd statement)
groundedproofs/Lax496464Proofs/WHierarchy/HittingSet/WDFinal.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
. On the word of the reduction writes, when , the structure of the compressed instance (universe: the first occurrences of the members plus spare elements, then one element per set; , and the incidence relation ) with weight , and a fixed no-instance when ; the witnesses of of that weight are the hitting sets of that size, and compression keeps the answer. The new parameter is at most , and an IMP+ program computes the reduction within steps.