While this submission is a draft, it cannot be used by other submissions.

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.

Read the Lean proof on GitHub

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 mm 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 mm 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 mm, with the exponent of the polynomial growing with mm.