Proof of `Two tests from the words up: NP-hardness of 1|r_j|L_max and Smith's rule` (1st statement)
groundedproofs/Lax434175Proofs/Sanity.lean · lax-434175
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
Every language in NP reduces to single-machine scheduling with release times, deadlines and lengths in (lax-391470). A Turing machine turns the binary word into its bits, and two word RAM programs, transferred to Turing machines (lax-759944), read the instance off the bits (the tokenizer of lax-391470) and write the standard word of : every time is shifted up by the largest absolute value, release times become release dates and deadlines due dates, and the threshold is . A word that is not an instance on the two lengths goes to the instance without jobs and threshold .