Proof of `Theorem 5` (3rd statement)
groundedproofs/Lax496464Proofs/Ram/F5QConclude.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 7 of this submission's paper
Description
The approximation scheme of the fifth theorem from the profile sweep: read the word, zero the weights of the jobs that cannot be preprocessed on their own, choose the rescaling , round the weights up to multiples of , run the profile sweep of the third theorem with the threshold that the rounding leaves, and write , where is the largest weight the rescaled table reaches ( itself when ).