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.

Read the Lean proof on GitHub

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-(n+1)(n+1) numbers exactly as for Theorem 2, but with rows the n+1n + 1 instants u⋅pu · p (the instant a partial solution has spent after selecting uu jobs) instead of the W+1W + 1 weights: the cell for the instant u⋅pu · p is max(T[X1,u])(minW(wj+T[X2,u+1]))max (T[X₁, u]) (min W (w_j + T[X₂, u + 1])), the second term present when (u+1)p+qj≤dj(u+1) p + q_j ≤ d_j. The guard is tested as u<limju < lim_j, where limjlim_j is computed once per job by a division, so the machine never forms the product u⋅pu · p (only the entries of the word are bounded by the word length). The table has (n+1)m⋅(n+1)(n+1)^m · (n+1) 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.