Proof of `Theorem 5` (1st statement)

groundedproofs/Lax496464Proofs/Section7.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

Chain (8). Rounding up loses less than kk per selected job, so at most k⋅nk·n in all; e⋅k⋅n≤wmaxe·k·n ≤ w_max turns that into wmax/ew_max/e, and wmax≤OPTw_max ≤ OPT — the heaviest job is feasible on its own — turns it into OPT/eOPT/e.