p. 66 — total idle time of machine 3 is
ProvedJohnsonFlowShop.ThreeStage.makespan_asap_eqLet , let , and let be any ordering of the items. With and the quantities of (positions in the paper's indexing), the total elapsed time of the as-soon-as-possible three-machine schedule of is
Equivalently, since machine 3 is busy for and idle for , the total idle time of machine 3 is , the display of p. 66. On p. 68 Johnson restates it: "is the maximum sum of elements passed through on all 'walks' in the time matrix from the upper left-hand corner to the lower right-hand corner, taking steps to the right or downward. The problem is to find a scheduling of items which minimizes this maximum walk."
This turns the three-stage problem into the minimization of an explicit function of the ordering.
Formalization Note The statement is in elapsed-time form. The maximum over pairs is written as over 0-based positions. It holds for every ordering; the special-case hypothesis is not assumed.
import Mathlib import Definitions.Def_JohnsonFlowShop_Shared_makespan import Definitions.Def_JohnsonFlowShop_ThreeStage_asapSchedule import Definitions.Def_JohnsonFlowShop_Shared_K import Definitions.Def_JohnsonFlowShop_ThreeStage_H
namespace JohnsonFlowShop.ThreeStage
/-- p. 66 (closed form of the total idle time of machine 3, `Σ Y_i = max_{u ≤ v} (H_v + K_u)`),
in elapsed-time form (p. 68): for positive processing times, `n ≥ 1` and every order `σ`, the
total elapsed time of the as-soon-as-possible schedule of `σ` equals
`∑_i C_i + max_{u ≤ v} (K_u + H_v)`, the maximum over pairs of positions `u ≤ v`. -/
theorem makespan_asap_eq {n : ℕ} [NeZero n] (A B C : Fin n → ℝ)
(hA : ∀ i, 0 < A i) (hB : ∀ i, 0 < B i) (hC : ∀ i, 0 < C i)
(σ : Equiv.Perm (Fin n)) :
Shared.makespan C (asapStart3 A B C σ) =
∑ i, C i + Finset.univ.sup' Finset.univ_nonempty (fun v : Fin n =>
(Finset.Iic v).sup' Finset.nonempty_Iic (fun u => Shared.K A B σ u + H B C σ v)) := by sorry
end JohnsonFlowShop.ThreeStage
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.