Proof of `Theorem 4`

groundedproofs/Lax496464Proofs/Ram/T4Final.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 7 of this submission's paper

Description

The greedy of Section 6.1 as a word RAM program: read the word, sort the jobs by start time (O(nlogn)O(n log n)), then consider the jobs in that order, keeping the running jobs in two maximum trees over the job numbers — one keyed by due date (whose root gives the job to drop) and one by BIG−dBIG - d (whose root gives the next job to end) — and counting the members of the set that have already ended. Every step costs O(logn)O(log n), so the whole run is within c⋅sortCostc · sortCost. The statement is exactly the concept's, including its positive-processing-time clause (the paper's standing assumption for Lemma 4).