Equality

The necessity half of Dósa's theorem, sorted form: equality forces n = 2m + 1 and Graham's instance up to a positive scale, by counting the jobs of each length on each machine of the two schedules. Helpers carry the prefix eq_.

Counting helpers

theorem GrahamLPT.eq_card_filter_pair {n : ℕ} (p : Fin n → ℝ) (S : Finset (Fin n)) (s x : ℝ) (hS : S.card = 2) (hsum : ∑ j ∈ S, p j = s) : {j ∈ S | p j = x}.card = {j ∈ S | p j = s - x}.card

On a two-element set whose values sum to s, the fibers at x and at s − x have the same size.

theorem GrahamLPT.eq_card_filter_const {n : ℕ} (p : Fin n → ℝ) (S : Finset (Fin n)) (t x : ℝ) (hS : ∀ j ∈ S, p j = t) (hx : x ≠ t) : {j ∈ S | p j = x}.card = 0

On a set of constant value t, the fiber at x ≠ t is empty.

theorem GrahamLPT.eq_card_lt {n : ℕ} (k : Fin n) : {j : Fin n | ↑j < ↑k}.card = ↑k

The jobs of index below k number k.

theorem GrahamLPT.eq_n_eq {n : ℕ} (k : Fin n) (hlast : ∀ (j : Fin n), ↑j ≤ ↑k) : n = ↑k + 1

No job after the critical job: n = k + 1.

Step 3: two jobs on every machine before the critical job

theorem GrahamLPT.eq_card_le_two {n : ℕ} (p : Fin n → ℝ) (hanti : Antitone p) (k : Fin n) (t δ : ℝ) (ht : 0 < t) (hδ : 0 < δ) (hpk : p k = t) (S : Finset (Fin n)) (hS : ∀ j ∈ S, ↑j < ↑k + 1) (hsum : ∑ j ∈ S, p j = 3 * t - δ) : S.card ≤ 2

A set of jobs of index ≤ k with sum 3t − δ (0 < δ, 0 < t = p k) has at most two jobs.

theorem GrahamLPT.eq_card_pos {n : ℕ} (p : Fin n → ℝ) (t δ : ℝ) (hδt : δ < t) (ht : 0 < t) (S : Finset (Fin n)) (hsum : ∑ j ∈ S, p j = 3 * t - δ) : 1 ≤ S.card

A set with sum 3t − δ > 0 is nonempty.

theorem GrahamLPT.eq_card_ne_one {m n : ℕ} (p : Fin n → ℝ) (t δ : ℝ) (ht : 0 < t) (hδ : 0 < δ) (hδt : δ < t) (hpt : ∀ (j : Fin n), t ≤ p j) (τ : Fin n → Fin m) (hG : ∀ (i : Fin m), ∑ j : Fin n with τ j = i, p j = 3 * t) (S : Finset (Fin n)) (hsum : ∑ j ∈ S, p j = 3 * t - δ) : S.card ≠ 1

A set with sum 3t − δ is not a single job: that job, of length 3t − δ, would be alone on its τ-machine (every other job is ≥ t > δ), whose load 3t − δ is not 3t.

theorem GrahamLPT.eq_card_fiber_two {m n : ℕ} (p : Fin n → ℝ) (hanti : Antitone p) (k : Fin n) (t δ : ℝ) (ht : 0 < t) (hδ : 0 < δ) (hδt : δ < t) (hpk : p k = t) (hpt : ∀ (j : Fin n), t ≤ p j) (σ : Fin n → Fin m) (hF : ∀ (i : Fin m), loadBefore p σ (↑k) i = 3 * t - δ) (τ : Fin n → Fin m) (hG : ∀ (i : Fin m), ∑ j : Fin n with τ j = i, p j = 3 * t) (i : Fin m) : {j : Fin n | ↑j < ↑k ∧ σ j = i}.card = 2

Step 3: every machine holds exactly two jobs before the critical job.

theorem GrahamLPT.eq_val_eq_two_mul {m n : ℕ} (σ : Fin n → Fin m) (k : Fin n) (hF2 : ∀ (i : Fin m), {j : Fin n | ↑j < ↑k ∧ σ j = i}.card = 2) : ↑k = 2 * m

Step 3: with two jobs on every machine before it, the critical job has index 2m.

Step 4: every job is at most 2t − δ

theorem GrahamLPT.eq_le_two_t {m n : ℕ} (p : Fin n → ℝ) (hanti : Antitone p) (k : Fin n) (t δ : ℝ) (hδt : δ ≤ t) (hpk : p k = t) (hlast : ∀ (j : Fin n), ↑j ≤ ↑k) (σ : Fin n → Fin m) (hF : ∀ (i : Fin m), loadBefore p σ (↑k) i = 3 * t - δ) (hF2 : ∀ (i : Fin m), {j : Fin n | ↑j < ↑k ∧ σ j = i}.card = 2) (j : Fin n) : p j ≤ 2 * t - δ

Step 5: the machines of τ

theorem GrahamLPT.eq_tau_cases {n : ℕ} (p : Fin n → ℝ) (hanti : Antitone p) (k : Fin n) (t δ : ℝ) (ht : 0 < t) (hδ : 0 < δ) (hδt : δ ≤ t) (hpk : p k = t) (hlast : ∀ (j : Fin n), ↑j ≤ ↑k) (hpt : ∀ (j : Fin n), t ≤ p j) (hle : ∀ (j : Fin n), p j ≤ 2 * t - δ) (S : Finset (Fin n)) (hsum : ∑ j ∈ S, p j = 3 * t) : S.card = 2 ∨ S.card = 3 ∧ ∀ j ∈ S, p j = t

A set of jobs with sum 3t, every job in [t, 2t − δ], holds two jobs, or three jobs of length t.

theorem GrahamLPT.eq_exists_three {m n : ℕ} (τ : Fin n → Fin m) (hn : n = 2 * m + 1) (hle : ∀ (i : Fin m), {j : Fin n | τ j = i}.card ≤ 3) : ∃ (i : Fin m), {j : Fin n | τ j = i}.card = 3

2m + 1 jobs on m machines, at most three each: some machine holds three.

Step 6: the counts

theorem GrahamLPT.eq_count_split {n : ℕ} (p : Fin n → ℝ) (k : Fin n) (hlast : ∀ (j : Fin n), ↑j ≤ ↑k) (x : ℝ) : {j : Fin n | p j = x}.card = {j ∈ {j : Fin n | ↑j < ↑k} | p j = x}.card + if p k = x then 1 else 0

The jobs of length x: those before k, plus k itself when p k = x.

theorem GrahamLPT.eq_count_sigma {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (k : Fin n) (A : ℝ) (hF : ∀ (i : Fin m), ∑ j : Fin n with ↑j < ↑k ∧ σ j = i, p j = A) (hF2 : ∀ (i : Fin m), {j : Fin n | ↑j < ↑k ∧ σ j = i}.card = 2) (x : ℝ) : {j ∈ {j : Fin n | ↑j < ↑k} | p j = x}.card = {j ∈ {j : Fin n | ↑j < ↑k} | p j = A - x}.card

The first count symmetry: summed over the machines of σ, each holding two jobs of total A before k, the jobs before k of length x and of length A − x are equally many.

theorem GrahamLPT.eq_count_tau {m n : ℕ} (p : Fin n → ℝ) (τ : Fin n → Fin m) (t : ℝ) (hG : ∀ (i : Fin m), ∑ j : Fin n with τ j = i, p j = 3 * t) (hGc : ∀ (i : Fin m), {j : Fin n | τ j = i}.card = 2 ∨ ∀ j ∈ {j : Fin n | τ j = i}, p j = t) (x : ℝ) (hx : x ≠ t) (hx2 : x ≠ 2 * t) : {j : Fin n | p j = x}.card = {j : Fin n | p j = 3 * t - x}.card

The second count symmetry: summed over the machines of τ, each holding two jobs of total 3t or three jobs of length t, the jobs of length x and of length 3t − x are equally many when x ≠ t, 2t.

theorem GrahamLPT.eq_chain_step {m n : ℕ} (p : Fin n → ℝ) (σ τ : Fin n → Fin m) (k : Fin n) (t δ : ℝ) (hδ : 0 < δ) (hmδ : ↑m * δ = t) (hpk : p k = t) (hlast : ∀ (j : Fin n), ↑j ≤ ↑k) (hF : ∀ (i : Fin m), ∑ j : Fin n with ↑j < ↑k ∧ σ j = i, p j = 3 * t - δ) (hF2 : ∀ (i : Fin m), {j : Fin n | ↑j < ↑k ∧ σ j = i}.card = 2) (hG : ∀ (i : Fin m), ∑ j : Fin n with τ j = i, p j = 3 * t) (hGc : ∀ (i : Fin m), {j : Fin n | τ j = i}.card = 2 ∨ ∀ j ∈ {j : Fin n | τ j = i}, p j = t) (i : ℕ) (hi : i + 1 < m) : {j ∈ {j : Fin n | ↑j < ↑k} | p j = t + (↑i + 1) * δ}.card = {j ∈ {j : Fin n | ↑j < ↑k} | p j = t + ↑i * δ}.card

One step of the chain: the two symmetries carry the count at t + (i + 1)δ to the count at `t

• iδ`.

theorem GrahamLPT.eq_chain {m n : ℕ} (p : Fin n → ℝ) (σ τ : Fin n → Fin m) (k : Fin n) (t δ : ℝ) (hδ : 0 < δ) (hmδ : ↑m * δ = t) (hpk : p k = t) (hlast : ∀ (j : Fin n), ↑j ≤ ↑k) (hF : ∀ (i : Fin m), ∑ j : Fin n with ↑j < ↑k ∧ σ j = i, p j = 3 * t - δ) (hF2 : ∀ (i : Fin m), {j : Fin n | ↑j < ↑k ∧ σ j = i}.card = 2) (hG : ∀ (i : Fin m), ∑ j : Fin n with τ j = i, p j = 3 * t) (hGc : ∀ (i : Fin m), {j : Fin n | τ j = i}.card = 2 ∨ ∀ j ∈ {j : Fin n | τ j = i}, p j = t) (i : ℕ) (hi : i < m) : {j ∈ {j : Fin n | ↑j < ↑k} | p j = t + ↑i * δ}.card = {j ∈ {j : Fin n | ↑j < ↑k} | p j = t}.card

The chain: every count c'(t + iδ), i < m, equals c'(t).

theorem GrahamLPT.eq_card_biUnion {n : ℕ} (p : Fin n → ℝ) (J : Finset (Fin n)) (m : ℕ) (t δ : ℝ) (hδ : 0 < δ) : ((Finset.range m).biUnion fun (i : ℕ) => {j ∈ J | p j = t + ↑i * δ}).card = ∑ i ∈ Finset.range m, {j ∈ J | p j = t + ↑i * δ}.card

The fibers at t + iδ, i < m, are disjoint: their union has the summed size.

theorem GrahamLPT.eq_step6 {n : ℕ} (p : Fin n → ℝ) (k : Fin n) (m : ℕ) (hm : 0 < m) (t δ : ℝ) (hδ : 0 < δ) (hk : ↑k = 2 * m) (hpk : p k = t) (hlast : ∀ (j : Fin n), ↑j ≤ ↑k) (hchain : ∀ i < m, {j ∈ {j : Fin n | ↑j < ↑k} | p j = t + ↑i * δ}.card = {j ∈ {j : Fin n | ↑j < ↑k} | p j = t}.card) (h3 : 3 ≤ {j : Fin n | p j = t}.card) : (∀ i < m, {j ∈ {j : Fin n | ↑j < ↑k} | p j = t + ↑i * δ}.card = 2) ∧ ∀ (j : Fin n), ↑j < ↑k → ∃ i < m, p j = t + ↑i * δ

Step 6: every fiber at t + iδ, i < m, has two jobs, and they exhaust the jobs before k.

Step 7: the function

theorem GrahamLPT.eq_antitone_eq_of_count {N : ℕ} (f g : Fin N → ℝ) (hf : Antitone f) (hg : Antitone g) (h : ∀ (x : ℝ), {j : Fin N | f j = x}.card = {j : Fin N | g j = x}.card) : f = g

Two antitone functions on Fin N with the same fiber sizes are equal: their value lists are sorted and are permutations of each other.

theorem GrahamLPT.eq_cast_iff (m q i : ℕ) : 2 * ↑m - 1 - ↑q = ↑m + ↑i ↔ q + 1 + i = m

theorem GrahamLPT.eq_cast_iff' (m i : ℕ) : ↑m = ↑m + ↑i ↔ i = 0

theorem GrahamLPT.eq_grahamJobs_fiber (m i : ℕ) (hi : i < m) : {j : Fin (2 * m + 1) | grahamJobs m j = ↑m + ↑i}.card = if i = 0 then 3 else 2

Graham's instance takes the value m + i, i < m, three times for i = 0 and twice otherwise.

theorem GrahamLPT.eq_grahamJobs_lattice (m : ℕ) (hm : 1 ≤ m) (j : Fin (2 * m + 1)) : ∃ i < m, grahamJobs m j = ↑m + ↑i

Every value of Graham's instance is m + i for some i < m.

theorem GrahamLPT.eq_count_eq {m : ℕ} (hm : 0 < m) (p : Fin (2 * m + 1) → ℝ) (k : Fin (2 * m + 1)) (t δ : ℝ) (hδ : 0 < δ) (hmδ : ↑m * δ = t) (hpk : p k = t) (hlast : ∀ (j : Fin (2 * m + 1)), ↑j ≤ ↑k) (hfib : ∀ i < m, {j ∈ {j : Fin (2 * m + 1) | ↑j < ↑k} | p j = t + ↑i * δ}.card = 2) (hlat : ∀ (j : Fin (2 * m + 1)), ↑j < ↑k → ∃ i < m, p j = t + ↑i * δ) (x : ℝ) : {j : Fin (2 * m + 1) | p j = x}.card = {j : Fin (2 * m + 1) | δ * grahamJobs m j = x}.card

The fiber sizes of p and of δ · grahamJobs m agree at every real x.

theorem GrahamLPT.graham_of_listSchedule_eq_bound {m n : ℕ} [NeZero m] (hm : 2 ≤ m) (hn : 0 < n) (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 < p j) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (heq : 3 * ↑m * makespan p σ = (4 * ↑m - 1) * optMakespan m p) : ∃ (a : ℝ) (h : n = 2 * m + 1), 0 < a ∧ ∀ (j : Fin n), p j = a * grahamJobs m (Fin.cast h j)

Dósa's theorem (2004), the sorted form: a list schedule of a nonempty nonincreasing positive p on m ≥ 2 machines attains Graham's bound against the optimum only for Graham's instance: then n = 2m + 1 and p is a positive multiple of grahamJobs m.