Certificates

The critical job's certificates: the smaller of C(σ) and 3 p_k bounds every comparison schedule, the observed third certifies optimality, equality in Graham's bound forces its proof's inequalities to be equalities, and Della Croce–Scatamacchia's Proposition 4 from Chen's property. Helpers carry the prefix ct_.

theorem GrahamLPT.ct_key_le {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (k : Fin n) (τ : Fin n → Fin m) (h3 : makespan p τ < 3 * p k) : loadBefore p σ (↑k) (σ k) + p k ≤ makespan p τ

The key lemma against the makespan of τ: when C(τ) < 3 p_k, the machine of k ends by C(τ).

theorem GrahamLPT.ct_eq_scalar (m L P S W T : ℝ) (hm : 2 ≤ m) (hT : 0 < T) (h1 : m * L ≤ S) (h2 : S + P ≤ W) (h3 : W ≤ m * T) (hkey : T < 3 * P → L + P ≤ T) (heq : 3 * m * (L + P) = (4 * m - 1) * T) : 3 * P = T ∧ S = m * L ∧ W = S + P ∧ W = m * T

The scalar step of the equality structure for T > 0: L the least load before k, P = p_k, S the length before k, W the total, T = C(τ); the four inequalities of Graham's proof and equality in the bound force 3P = T and the chain mL = S, S + P = W, W = mT.

theorem GrahamLPT.ct_other_scalar (m q s P W T : ℝ) (hq : 0 ≤ q) (hmq : q + 2 ≤ m) (hwork : (m - 1) * s + (q + 1) * P ≤ W) (htotal : W ≤ m * T) (hsize : q * P ≤ T) : q * (m - 1) * (s + P) ≤ ((q + 1) * (m - 1) - 1) * T

The scalar step of Proposition 4: s the least load before the critical job, P its length, s + P the makespan of σ, W the total, T = C(τ); the load count (m − 1) s + (q + 1) P ≤ W ≤ mT and Chen's qP ≤ T give the bound when q + 2 ≤ m.

theorem GrahamLPT.lpt_critical_min_le {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (k : Fin n) (hk : makespan p σ = loadBefore p σ (↑k) (σ k) + p k) (τ : Fin n → Fin m) : min (makespan p σ) (3 * p k) ≤ makespan p τ

The critical job's certificate: in a list schedule of a nonincreasing p, for a job k whose completion time is the makespan, the smaller of C(σ) and 3 p_k is at most C(τ) for every assignment τ (the key lemma read as a lower bound on every comparison schedule).

theorem GrahamLPT.lpt_eq_optMakespan_of_critical_third {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (k : Fin n) (hk : makespan p σ = loadBefore p σ (↑k) (σ k) + p k) (h3 : makespan p σ ≤ 3 * p k) : makespan p σ = optMakespan m p

The observed-third certificate: in a list schedule of a nonincreasing p, when a critical job k is at least a third of the makespan it completes, the schedule is optimal (lpt_eq_optMakespan_of_third_lt asks every job to exceed a third of the unknown optimum).

theorem GrahamLPT.lpt_eq_bound_structure {m n : ℕ} [NeZero m] (hm : 2 ≤ m) (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (k : Fin n) (hk : makespan p σ = loadBefore p σ (↑k) (σ k) + p k) (τ : Fin n → Fin m) (heq : 3 * ↑m * makespan p σ = (4 * ↑m - 1) * makespan p τ) : 3 * p k = makespan p τ ∧ (∀ (i : Fin m), loadBefore p σ (↑k) i = loadBefore p σ (↑k) (σ k)) ∧ (∀ (i : Fin m), load p τ i = makespan p τ) ∧ ∀ (j : Fin n), ↑k < ↑j → p j = 0

In a list schedule σ of a nonincreasing p on m ≥ 2 machines, with k a critical job, equality in Graham's LPT bound against τ forces the four inequalities of its proof to be equalities: 3 p_k = C(τ), every machine of σ carries the least load before k, every machine of τ carries exactly C(τ), and every job after k has length 0.

theorem GrahamLPT.lpt_bound_of_other_card {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (k : Fin n) (hk : makespan p σ = loadBefore p σ (↑k) (σ k) + p k) (i : Fin m) (hi : i ≠ σ k) (q : ℕ) (hq : q ≤ {j : Fin n | ↑j < ↑k ∧ σ j = i}.card) (hqm : q + 2 ≤ m) (τ : Fin n → Fin m) : ↑q * (↑m - 1) * makespan p σ ≤ ((↑q + 1) * (↑m - 1) - 1) * makespan p τ

Della Croce–Scatamacchia's Proposition 4, from Chen's property: in a list schedule σ of a nonincreasing p, if a machine i other than the critical job's holds at least q jobs before the critical job k, and q + 2 ≤ m, then q(m − 1) · C(σ) ≤ ((q + 1)(m − 1) − 1) · C(τ) for every assignment τ.