Proof of `Day-Independent Due Dates` (2nd statement)
groundedproofs/Lax117284Proofs/Theorem3_Days.lean · lax-117284
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
The language is decided by a reduction to 2-satisfiability, which is in polynomial time, that carries out the decision itself and writes a formula with no clause for a yes-instance and an unsatisfiable formula for every other word. At zero days every schedule is vacuously fair, so a word RAM program decides it directly from the day count, the parameter and the client count, with no dynamic program needed. At a positive number of days, a word RAM program reads the instance, checks that every job takes some time and is not due before it starts, checks that the due dates are day-independent, orders the clients by due date, and runs a dynamic program over them that carries for each of the days the time at which its machine is next free, deciding whether the parameter is met. The number of days is a constant of the reduction rather than part of its input, so the algorithm and its running time depend on , with the exponent of the polynomial growing with .