Proof of `Per-Client Fairness Parameters Reduce to a Uniform One` (4th statement)
groundedproofs/Lax117284Proofs/Machine/PerFinal.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 and its parameters, a first pass over the table checks that every job takes some time and is not due before it starts, a second pass checks that no parameter exceeds the number of days, a third finds the largest due date, and the numbers of the image are written cell by cell, the closed form of every cell being computed from its row and column: the original jobs on the original days, the private unit job of each client on each additional day, placed in the stretch of the two new clients or after it according to its parameter, and the common job of the two new clients. An instance without clients is answered with a fixed yes-instance, and a word that is not the code of an admissible instance with the rejected word. 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.