Lax Lean Archive

Proof of `Preprocessing an Interval Scheduling Instance Down to a Bounded Number of Live Jobs` (1st statement)

groundedproofs/Lax888481Proofs/Preprocessing.lean · lax-888481

What this proof establishes

no assumptions

def✓Lax888481.Preprocessing (1st statement)

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 5 of this submission's paper

Description

The kept jobs alive at tt are covered by the intervals [dd−pp,dd)[dd - pp, dd) with dd∈(t,t+pmax]dd ∈ (t, t + p_max] and pp∈[1,pmax]pp ∈ [1, p_max], and each such interval keeps at most mm jobs per machine.