Proof of `Theorem 5` (4th statement)
groundedproofs/Lax496464Proofs/Ram/F5WFinal.lean · lax-496464
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.
In the paper
- page 7 of this submission's paper
Description
The endpoint sweep of Section 4 as a word RAM approximation scheme. Read the instance and the accuracy (in the place of the threshold), sort the jobs by start time, build the sorted arrays and the due-date order (as in the exact program), zero the weight of every unfit job, take , replace every weight by , set the threshold , run the exact endpoint sweep (, unchanged) on the rescaled weights, scan the finished row for the last finite cell , and write if and otherwise (). The cost is that of the exact program with threshold , that is , plus the sort; the guarantee is .