Lemma 3

Lax496464.Lemma3 · concepts/Lax496464/Lemma3.lean · lax-496464

proven

Loading review…

Natural Language Statement

Theorem

Recursion (5) computes the table of due-date profiles.

Stepping to the start time of job $j$ , an entry at $s_j$ is reached either by passing $j$ over, in which case some profile at the previous start time shifts to it, or by selecting $j$ , in which case the profile with $j$ 's own coordinate decremented shifts to it, the weight drops by $w_j$ , and the first-stage machine must be able to finish $j$ by $s_j$ . Past the last start time the table answers the question.

The printed form of the recursion is not correct — its shift leaves coordinates unconstrained that the profile of a selection cannot have — and the counterexamples are small: one job on two machines for the branch that selects, two jobs on one machine for the branch that passes over. The algorithm is nonetheless correct as printed. What it maintains is the weaker invariant that an entry $T_j[\vec{x}, W'] \le P'$ is witnessed by a feasible selection of weight $W'$ and preprocessing cost at most $P'$ whose profile is at most $\vec{x}$ coordinatewise, and it still derives every feasible selection with its exact profile. A vector that overstates the profile only overstates how many machines are busy, so the capacity test rejects more rather than less, and the optimum read off at the end is exact.

Concept map

6 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

In the paper

page 5 of this submission's paper

Lean source view on GitHub

1	import Lax496464.Profile
2
3	/-!
4	---
5	title: Lemma 3
6	type: theorem
7	---
8	Recursion (5) computes the table of due-date profiles.
9
10	Stepping to the start time of job $j$ , an entry at $s_j$ is reached either by passing $j$
11	over, in which case some profile at the previous start time shifts to it, or by selecting
12	$j$ , in which case the profile with $j$ 's own coordinate decremented shifts to it, the
13	weight drops by $w_j$ , and the first-stage machine must be able to finish $j$ by $s_j$ .
14	Past the last start time the table answers the question.
15
16	The printed form of the recursion is not correct — its shift leaves coordinates
17	unconstrained that the profile of a selection cannot have — and the counterexamples are
18	small: one job on two machines for the branch that selects, two jobs on one machine for
19	the branch that passes over. The algorithm is nonetheless correct as printed. What it
20	maintains is the weaker invariant that an entry $T_j[\vec{x}, W'] \le P'$ is witnessed by
21	a feasible selection of weight $W'$ and preprocessing cost at most $P'$ whose profile is
22	at most $\vec{x}$ coordinatewise, and it still derives every feasible selection with its
23	exact profile. A vector that overstates the profile only overstates how many machines are
24	busy, so the capacity test rejects more rather than less, and the optimum read off at the
25	end is exact.
26
27	# Formalization Notes
28
29	Three statements, in order of what they are about.
30
31	The first is the recursion the paper means, with the missing condition supplied by
32	carrying the profile as a function on all coordinates rather than a vector of length
33	$q_{\max}$ : shifting then constrains every coordinate, and there is nothing left free.
34	This is the lemma as it should have been printed.
35
36	The second says the printed recursion is not that lemma: there is an entry it derives
37	that no selection realizes. It quantifies over instances, since a single one suffices,
38	and it is what makes the defect a statement rather than a remark.
39
40	The third is what rescues the algorithm: the value read off after the last job is the
41	largest weight of a feasible set, for the recursion exactly as printed. It carries the
42	paper's standing assumptions — positive processing times, positive weights, processing
43	times bounded by $q_{\max}$ — and the distinctness of start times that Section 4's
44	rescaling provides.
45	-/
46
47	namespace Lax496464.Lemma3
48
49	open Lax496464.FlowShop Lax496464.FlowShop.Instance
50	open Lax496464.Sweep Lax496464.Profile
51
52	variable (I : Instance)
53
54	/-- Lemma 3, repaired. The step to the start time of job `j`. -/
55	axiom reachableProfile_start (hq : ∀ i : I.Job, 0 < I.q i) {qmax : ℕ}
56	(hqmax : ∀ k : I.Job, I.q k ≤ qmax) {t' t : ℤ} {δ : ℕ} {j : I.Job}
57	{x : ℕ → ℕ} {W' : ℕ} {P' : ℤ}
58	(hδ : (δ : ℤ) = t - t') (htt : t' < t) (hsj : s j = t)
59	(hnos : ∀ k : I.Job, k ≠ j → ¬ (t' < s k ∧ s k ≤ t)) :
60	ReachableProfile I t x W' P' ↔
61	(∃ y : ℕ → ℕ, (∀ i, 1 ≤ i → x i = y (δ + i)) ∧ ReachableProfile I t' y W' P') ∨
62	(0 < x (I.q j) ∧ (∑ i ∈ Finset.Icc 1 qmax, x i) ≤ I.machines ∧
63	∃ (W'' : ℕ) (P'' : ℤ) (y : ℕ → ℕ),
64	W'' + I.w j = W' ∧
65	(∀ i, 1 ≤ i → (if i = I.q j then x i - 1 else x i) = y (δ + i)) ∧
66	ReachableProfile I t' y W'' P'' ∧
67	P'' + I.p j ≤ s j ∧ P'' + I.p j ≤ P')
68
69	/-- The read-off, repaired. Past the last start time, a profile of weight `W'` is
70	exactly a feasible set of weight `W'`. -/
71	axiom exists_reachableProfile_iff {t : ℤ} (ht : ∀ k : I.Job, s k ≤ t) (W' : ℕ) :
72	(∃ (x : ℕ → ℕ) (P' : ℤ), ReachableProfile I t x W' P') ↔
73	∃ Z : Finset I.Job, Feasible I Z ∧ weight I Z = W'
74
75	/-- Lemma 3 is false as printed. Some instance, with positive processing times and
76	positive weights, has a stage at which the printed recursion derives a profile that no
77	set of jobs has. -/
78	axiom printed_not_correct :
79	∃ (J : Instance) (qmax : ℕ) (k : J.Job) (x : Fin qmax → ℕ) (W : ℕ) (P : ℤ),
80	(∀ i : J.Job, 0 < J.q i) ∧ (∀ i : J.Job, 0 < J.w i) ∧
81	(∀ i : J.Job, J.q i ≤ qmax) ∧
82	Printed J qmax ((k : ℕ) + 1) x W P ∧
83	∀ Z : Finset J.Job, ∃ c : Fin qmax,
84	dueProfile J Z (s k) ((c : ℕ) + 1) ≠ x c
85
86	/-- The algorithm is correct as printed. For the recursion exactly as the paper
87	prints it, the weights reached after the last job are exactly the weights of feasible
88	sets. -/
89	axiom printed_readoff {qmax : ℕ} (hq : ∀ i : I.Job, 0 < I.q i) (hw : ∀ i : I.Job, 0 < I.w i)
90	(hqmax : ∀ i : I.Job, I.q i ≤ qmax)
91	(hdist : ∀ i j : I.Job, i < j → s i < s j) (W : ℕ) :
92	(∃ (x : Fin qmax → ℕ) (P : ℤ), Printed I qmax I.jobs x W P) ↔
93	∃ Z : Finset I.Job, Feasible I Z ∧ weight I Z = W
94
95	end Lax496464.Lemma3
96

Show ProofShow ProofShow ProofShow Proof

Formalization Notes

Three statements, in order of what they are about.

The first is the recursion the paper means, with the missing condition supplied by carrying the profile as a function on all coordinates rather than a vector of length $q_{\max}$ : shifting then constrains every coordinate, and there is nothing left free. This is the lemma as it should have been printed.

The second says the printed recursion is not that lemma: there is an entry it derives that no selection realizes. It quantifies over instances, since a single one suffices, and it is what makes the defect a statement rather than a remark.

The third is what rescues the algorithm: the value read off after the last job is the largest weight of a feasible set, for the recursion exactly as printed. It carries the paper's standing assumptions — positive processing times, positive weights, processing times bounded by $q_{\max}$ — and the distinctness of start times that Section 4's rescaling provides.

Builds on

Lax496464.Profile

Used by

none

From Mathlib

none

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Lemma 3

Flags

Flag this concept

Natural Language Statement

Theorem

1 `exists_reachableProfile_iff` proven

2 `printed_not_correct` proven

3 `printed_readoff` proven

4 `reachableProfile_start` proven

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments

Lemma 3

Natural Language Statement

Theorem

1 exists_reachableProfile_iff proven

2 printed_not_correct proven

3 printed_readoff proven

4 reachableProfile_start proven

In the paper

Lean source view on GitHub

Discussion

1 `exists_reachableProfile_iff` proven

2 `printed_not_correct` proven

3 `printed_readoff` proven

4 `reachableProfile_start` proven