Proof of `The Fairness Parameter One Below the Number of Days` (4th statement)
groundedproofs/Lax117284Proofs/Machine/T9Final.lean · lax-117284
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 a word RAM program on the zeros and ones of its input: a one-pass tokenizer reads the numbers of the instance, a pass over the table checks that every job takes some time and is not due before it starts, the number of variables and of clauses are written, and then every conflict clause and every validation clause is written, its two variables and their signs being computed from its index alone — for a conflict clause from the day and the two clients its index names, the four numbers of their jobs being read off the table and compared. A word that is not the code of an instance whose parameter is one below its number of days is answered with the fixed unsatisfiable formula. The numbers may be exponential in the length of the input, which the word length of a polynomial-time word RAM accommodates, and polynomial time on the word RAM transfers to a Turing machine.