Proof of `Theorem 3` (2nd statement)
groundedproofs/Lax496464Proofs/Ram/W3Final.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 6 of this submission's paper
Description
The endpoint sweep of Section 4 as a word RAM program: read the word, sort the jobs by start time (), build the arrays of the sorted instance and the order of the due dates, then sweep the events — the start of a job takes a free slot (or a fresh one, doubling the mask range ), the due date frees it — updating a table with one entry for every set of occupied slots and every weight up to , by a flat pass of cells per event. The number of slots is at most the width , so every event costs and the run is within . The domain restricts to positive processing times, the paper's standing assumption for the sweep.