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.

Read the Lean proof on GitHub

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 (O(nlogn)O(n log n)), compute qmaxq_max and a sentinel, then sweep the jobs in that order, carrying for every profile xx (how many selected jobs are due at each of the next qmaxq_max instants, a base m+1m+1 number of qmaxq_max digits) and every weight c≤Wc ≤ W the least preprocessing load of a feasible selection of weight at least cc. One job is one marginalisation pass (the shift of the profile is a division by a power of m+1m+1, the low digits being minimised away) and one take pass, each O(1)O(1) per table cell, so a job costs O((m+1)mqax(W+1))O((m+1)^q_max (W+1)) and the whole run is within c⋅(W+1)⋅(m+1)mqax⋅(n+1)+c⋅sortCostc · (W+1) · (m+1)^q_max · (n+1) + c · sortCost. The answer is read off the profiles at weight WW. The correctness is that of recursion (5) in its repaired form (Q3ModelQ3Model); jobs may tie in start time (δ=0δ = 0), 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.