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.

Read the Lean proof on GitHub

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 (O(nlogn)O(n log n)), build the arrays of the sorted instance and the order of the due dates, then sweep the 2n2n events — the start of a job takes a free slot (or a fresh one, doubling the mask range MK=2nextMK = 2^next), the due date frees it — updating a table with one entry for every set of occupied slots and every weight up to WW, by a flat pass of MK⋅(W+1)MK · (W+1) cells per event. The number of slots is at most the width ωω, so every event costs O(2ω⋅(W+1))O(2^ω · (W+1)) and the run is within c⋅(W+1)⋅2ω⋅(n+1)+c⋅sortCostc · (W+1) · 2^ω · (n+1) + c · sortCost. The domain restricts to positive processing times, the paper's standing assumption for the sweep.