TightLPT

Graham's family: optimum 3m, LPT makespan 4m − 1.

theorem GrahamLPT.tg_grahamJobs_apply_lt (m : ℕ) (j : Fin (2 * m + 1)) (h : ↑j < 2 * m) : grahamJobs m j = 2 * ↑m - 1 - ↑(↑j / 2)

theorem GrahamLPT.tg_grahamJobs_apply_last (m : ℕ) (j : Fin (2 * m + 1)) (h : 2 * m ≤ ↑j) : grahamJobs m j = ↑m

theorem GrahamLPT.tg_le_grahamJobs (m : ℕ) (j : Fin (2 * m + 1)) : ↑m ≤ grahamJobs m j

theorem GrahamLPT.tg_grahamJobs_nonneg (m : ℕ) (j : Fin (2 * m + 1)) : 0 ≤ grahamJobs m j

theorem GrahamLPT.tg_sum_range_aux (c : ℝ) (k : ℕ) : ∑ j ∈ Finset.range (2 * k), (c - ↑(j / 2)) = 2 * ↑k * c - ↑k * (↑k - 1)

Σ_{j < 2k} (c − ⌊j/2⌋) = 2kc − k(k − 1).

theorem GrahamLPT.tg_grahamJobs_sum (m : ℕ) : ∑ j : Fin (2 * m + 1), grahamJobs m j = 3 * ↑m ^ 2

theorem GrahamLPT.tg_pair (m : ℕ) (j : Fin (2 * m + 1)) (h : ↑j < 2 * m) : grahamJobs m j + grahamJobs m ⟨2 * m - 1 - ↑j, ⋯⟩ = 3 * ↑m - 1

The pairs j, 2m − 1 − j of the first 2m jobs sum to 3m − 1.

theorem GrahamLPT.tg_pair' (m : ℕ) (j : Fin (2 * m + 1)) (h : ↑j < 2 * m - 2) : grahamJobs m j + grahamJobs m ⟨2 * m - 3 - ↑j, ⋯⟩ = 3 * ↑m

The pairs j, 2m − 3 − j of the first 2m − 2 jobs sum to 3m.

theorem GrahamLPT.tg_exists_opt (m : ℕ) [NeZero m] : ∃ (τ : Fin (2 * m + 1) → Fin m), ∀ (i : Fin m), load (grahamJobs m) τ i = 3 * ↑m

The pairing τ₀ (j ↦ min (j, 2m − 3 − j) for j < 2m − 2, the three jobs of length m on the last machine) has every load 3m.

theorem GrahamLPT.tg_le_makespan (m : ℕ) [NeZero m] (τ : Fin (2 * m + 1) → Fin m) : 3 * ↑m ≤ makespan (grahamJobs m) τ

theorem GrahamLPT.tg_exists_prefix_pairing (m : ℕ) [NeZero m] : ∃ (τ : Fin (2 * m + 1) → Fin m), ∀ (i : Fin m), loadBefore (grahamJobs m) τ (2 * m) i = 3 * ↑m - 1

The pairing τ' (j ↦ min (j, 2m − 1 − j)) of the first 2m jobs has every load 3m − 1 before index 2m.

theorem GrahamLPT.grahamJobs_antitone (m : ℕ) : Antitone (grahamJobs m)

Graham's instance is listed in nonincreasing order.

theorem GrahamLPT.tg_loadBefore_two_mul (m : ℕ) [NeZero m] (σ : Fin (2 * m + 1) → Fin m) (hσ : IsListSchedule (grahamJobs m) σ) (i : Fin m) : loadBefore (grahamJobs m) σ (2 * m) i = 3 * ↑m - 1

Every list schedule of Graham's instance in its own order has every load 3m − 1 after the first 2m jobs (the key lemma at T = 3m − 1, then the sum m(3m − 1)).

theorem GrahamLPT.tg_listSchedule_makespan (m : ℕ) [NeZero m] (σ : Fin (2 * m + 1) → Fin m) (hσ : IsListSchedule (grahamJobs m) σ) : makespan (grahamJobs m) σ = 4 * ↑m - 1

Every list schedule of Graham's instance in its own order has makespan 4m − 1.

theorem GrahamLPT.tg_comp_eq (m : ℕ) (π : Equiv.Perm (Fin (2 * m + 1))) (h : Antitone (grahamJobs m ∘ ⇑π)) : grahamJobs m ∘ ⇑π = grahamJobs m

An antitone relabeling of Graham's instance leaves the lengths unchanged (Tuple.unique_antitone).

theorem GrahamLPT.grahamJobs_optMakespan (m : ℕ) [NeZero m] : optMakespan m (grahamJobs m) = 3 * ↑m

Graham's instance has optimal makespan 3m.

theorem GrahamLPT.grahamJobs_lpt_makespan (m : ℕ) [NeZero m] (σ : Fin (2 * m + 1) → Fin m) (hσ : IsLPTSchedule (grahamJobs m) σ) : makespan (grahamJobs m) σ = 4 * ↑m - 1

Every LPT schedule of Graham's instance has makespan 4m − 1: the bound 4/3 − 1/(3m) is attained for every m.