Proof of `Open parameters of The Scheduling Zoo`
groundedproofs/Lax434175Proofs/ZooOpenParams.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
Take the value of the parameter for which the problem is NP-hard. A language of NP reduces to the problem restricted to that value, always landing on a word of an instance; the polynomial decider for that value, simulated by a Turing machine, answers there; a last machine reads the answer bit.