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

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.

Read the Lean proof on GitHub

Description

Every language in NP reduces to single-machine scheduling with release times, deadlines and lengths in 3,2{3, 2} (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 1∣rj∣Lmax1|r_j|L_max: every time is shifted up by the largest absolute value, release times become release dates and deadlines due dates, and the threshold is 00. A word that is not an instance on the two lengths goes to the instance without jobs and threshold −1-1.