Proof of `Theorem 5` (2nd statement)

groundedproofs/Lax496464Proofs/Ram/F5MFinal.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 table of Section 3 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 (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 table program of Theorem 2 (D2Core.core2D2Core.core2, unchanged) on the rescaled weights, scan the finished column of the first mm indices for the last non-zero cell W′W' (for no job or no machine, W′=0W' = 0), 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)(n+1)m)O((n+1)² (e+1) (n+1)^m), plus the sort; the guarantee is F5Math.fptasvalueF5Math.fptas_value.