Proof of `Theorem 3` (1st statement)
groundedproofs/Lax496464Proofs/Ram/Q3Final.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 6 of this submission's paper
Description
The profile sweep of Section 5 as a word RAM program. Read the word, sort the jobs by start time (), compute and a sentinel, then sweep the jobs in that order, carrying for every profile (how many selected jobs are due at each of the next instants, a base number of digits) and every weight the least preprocessing load of a feasible selection of weight at least . One job is one marginalisation pass (the shift of the profile is a division by a power of , the low digits being minimised away) and one take pass, each per table cell, so a job costs and the whole run is within . The answer is read off the profiles at weight . The correctness is that of recursion (5) in its repaired form (); jobs may tie in start time (), no rescaling is needed. The domain restricts to positive processing times, the paper's standing assumption for Lemma 3, exactly as the concept's statement now says.