Corollary 2.6 — for all weights
ProvedSingleMachineSched.LPRelax.corollary_2_6Let jobs have integral processing times , integral release dates and weights , and let the horizon bound the makespan of some feasible nonpreemptive schedule. Then the preemptive time-indexed relaxation (D) with horizon and the mean busy time relaxation (R) have the same optimal value:
Both are lower bounds on the optimum of . The equality means that the pseudopolynomial LP (D) and the exponentially constrained LP (R) give the same bound, and that both are attained by the LP schedule; the approximation results of the paper are measured against this common value.
Formalization Note No ordering of the jobs is assumed: the statement holds for every nonnegative weight vector, and the LP schedule does not appear in it. The paper takes to be an upper bound on the makespan of an optimal schedule; here is only required to bound the makespan of some feasible nonpreemptive schedule (with real start times), which every such does, so the statement covers the paper's. The paper's second sentence, that the common value can be computed in time, is a running-time claim and is not formalized.
import Mathlib import Definitions.Def_SingleMachineSched_Shared_RelaxationR import Definitions.Def_SingleMachineSched_LPRelax_RelaxationD
namespace SingleMachineSched.LPRelax
/-- Corollary 2.6: for any nonnegative weights, the preemptive time-indexed relaxation (D) and
the mean busy time relaxation (R) have the same optimal value, `Z_D = Z_R`. -/
theorem corollary_2_6 {n : ℕ} (p r : Fin n → ℕ) (w : Fin n → ℝ) (T : ℕ)
(hp : ∀ j, 0 < p j) (hw : ∀ j, 0 ≤ w j) (hT : IsMakespanBound p r T) :
zD p r w T = Shared.zR p r w := by sorry
end SingleMachineSched.LPRelax
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.