Proof of `Corollary 3`
groundedproofs/Lax496464Proofs/Ram/D5Final.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
Corollary 3 as a word RAM program: the dual table of Section 3 for equal preprocessing times. Read the word, sort the jobs by start time, and fill the table over sets of thresholds written as base- numbers exactly as for Theorem 2, but with rows the instants (the instant a partial solution has spent after selecting jobs) instead of the weights: the cell for the instant is , the second term present when . The guard is tested as , where is computed once per job by a division, so the machine never forms the product (only the entries of the word are bounded by the word length). The table has entries, filled from the largest number down, and the answer is one entry. The domain restricts to positive processing times, the paper's standing assumption for Lemma 1's recursion.