Proof of `Theorem 5` (4th statement)

groundedproofs/Lax496464Proofs/Ram/F5WFinal.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 endpoint sweep of Section 4 as a word RAM approximation scheme. Read the instance and the accuracy ee (in the place of the threshold), sort the jobs by start time, build the sorted arrays and the due-date order (as in the exact program), zero the weight of every unfit job, take k=max1(wmax′/(en))k = max 1 (w_max' / (e n)), replace every weight w≥1w ≥ 1 by (w−1)/k+1(w - 1)/k + 1, set the threshold W=2en2W = 2 e n², run the exact endpoint sweep (W3Sweep.coreW3Sweep.core, unchanged) on the rescaled weights, scan the finished row TB[0…W]TB[0 … W] for the last finite cell W′W', and write k(W′−n)k (W' - n) if k>1k > 1 and W′W' otherwise (F5Math.fptasOutF5Math.fptasOut). The cost is that of the exact program with threshold 2en22 e n², that is O((n+1)2(e+1)⋅2ω⋅(n+1))O((n+1)² (e+1) · 2^ω · (n+1)), plus the sort; the guarantee is F5Math.fptasvalueF5Math.fptas_value.