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.

Read the Lean proof on GitHub

Description

p−Hitting−Set≤fptp−WDhsp-Hitting-Set ≤fpt p-WD_hs. On the word of (P,k)(P, k) the reduction writes, when k≤nk ≤ n, the structure of the compressed instance (universe: the first occurrences of the members plus minkmmin k m spare elements, then one element per set; VERTVERT, EDGEEDGE and the incidence relation II) with weight minkmmin k m, and a fixed no-instance when k>nk > n; the witnesses of hs(X)hs(X) of that weight are the hitting sets of that size, and compression keeps the answer. The new parameter is at most k+1k + 1, and an IMP+ program computes the reduction within 100000(∣x∣+1)3100000 (|x| + 1)^3 steps.