Proof of `Interval scheduling is W[1]-hard for the number of machines`
groundedproofs/Lax470956Proofs/Construction1Main.lean · lax-470956
What this proof establishes
no assumptions
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
The reduction is Construction 1 as a map on words. It sends instances to instances and preserves and reflects yes-instances because the construction is correct and its word encodes it; the image has one machine per pair of colours and one more, a function of the number of colours alone; and it is computed by one word RAM program.
The program copies the word into an array, ranks the vertices in the paper's order by sweeping them once per colour, enumerates the edges by one scan of the target array with a pointer to the vertex owning the current slot, and then writes the six blocks of the instance encoding and the threshold, one counted pass per block. Every pass recomputes the numbers of job through one shared command, so the construction's arithmetic is verified once. The sweep costs steps and each pass a constant per job, and there are at most jobs, so the whole is within machine instructions.