The Due-Date Profile of Section 5, and Recursion (5)

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

definition

Loading review…

Natural Language Statement

Definition

The algorithm behind the second half of the third theorem. It sweeps the start times in order, and at the start time of job $j$ it carries, instead of the set of selected jobs alive then, only their profile: the vector $\vec{x}$ whose $i$ -th coordinate counts the selected jobs due at $s_j + i$ . Since a job's second operation is at most $q_{\max}$ long, only the coordinates $1, \dots, q_{\max}$ can be nonzero, and each is at most $m$ ; the table therefore has $m^{q_{\max}}$ columns.

Stepping from the previous start time to $s_j$ moves the reference point by $\delta_j = s_j - s_{j-1}$ , so a profile at $s_{j-1}$ becomes a profile at $s_j$ shifted down by $\delta_j$ . The paper writes $\vec{x}[\delta]$ for the vectors that shift to $\vec{x}$ , and recursion (5) has the two branches of every such sweep: job $j$ is passed over, or job $j$ is selected, in which case its own coordinate $q_j$ drops by one.

Concept map

5 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 5 of this submission's paper

Lean source view on GitHub

1	import Lax496464.Sweep
2	import Mathlib.Algebra.BigOperators.Fin
3	import Mathlib.Order.Interval.Finset.Nat
4
5	/-!
6	---
7	title: The Due-Date Profile of Section 5, and Recursion (5)
8	type: definition
9	---
10	The algorithm behind the second half of the third theorem. It sweeps the start times in
11	order, and at the start time of job $j$ it carries, instead of the set of selected jobs
12	alive then, only their profile: the vector $\vec{x}$ whose $i$ -th coordinate counts the
13	selected jobs due at $s_j + i$ . Since a job's second operation is at most $q_{\max}$ long,
14	only the coordinates $1, \dots, q_{\max}$ can be nonzero, and each is at most $m$ ; the
15	table therefore has $m^{q_{\max}}$ columns.
16
17	Stepping from the previous start time to $s_j$ moves the reference point by
18	$\delta_j = s_j - s_{j-1}$ , so a profile at $s_{j-1}$ becomes a profile at $s_j$ shifted
19	down by $\delta_j$ . The paper writes $\vec{x}[\delta]$ for the vectors that shift to
20	$\vec{x}$ , and recursion (5) has the two branches of every such sweep: job $j$ is passed
21	over, or job $j$ is selected, in which case its own coordinate $q_j$ drops by one.
22
23	# Formalization Notes
24
25	The profile is carried as a function on all $i \ge 1$ rather than as a vector of length
26	$q_{\max}$ . This is deliberate. The coordinates beyond $q_{\max}$ are not free: the jobs
27	counted by the profile at $s_j$ all have due dates in $(s_j, s_j + q_{\max}]$ , so those
28	coordinates are zero, and a formulation that leaves them out has to say so separately —
29	which is exactly what the printed recursion fails to do.
30
31	The printed recursion is stated here as well, unchanged. The paper writes
32	$\vec{x}[\delta] = \{\vec{y} \in \{0,\dots,m\}^{q_{\max}} : y_i = x_{i-\delta} \text{ for all } i \in \{\delta+1, \dots, q_{\max}\}\},$
33
34	which pins $\vec{y}$ on the coordinates above $\delta$ and leaves the last $\delta$
35	coordinates of the shifted vector unconstrained. They are not free, for the reason just
36	given, and leaving them so lets the recursion reach entries that no selection realizes —
37	in both of its branches. The consequence for the algorithm is nothing at all, which is
38	the content of the third theorem's second half: a reachable entry is still witnessed by a
39	feasible selection, only with a profile no larger than the one recorded, and since the
40	capacity test $\sum_i x_i \le m$ is then applied to the larger vector it can only reject
41	more. The optimum read off at the end is exact.
42
43	Both versions are therefore defined: the one with the missing condition supplied, whose
44	correctness is the lemma the paper states, and the printed one, whose correctness is the
45	weaker invariant the algorithm actually maintains. Keeping them apart is what lets both
46	be stated.
47
48	The printed recursion is given as an inductively defined relation — the entries it
49	derives — rather than as a table of values, since that is what "the recursion reaches
50	this entry" means and it needs no order of evaluation. Its coordinates are numbered from
51	zero, so coordinate $c$ counts the jobs due at $s_j + c + 1$ .
52	-/
53
54	namespace Lax496464.Profile
55
56	open Lax496464.FlowShop Lax496464.FlowShop.Instance Lax496464.Sweep
57
58	variable (I : Instance)
59
60	/-- The due-date profile of `Z` at `t`: the number of jobs of `Z` due at `t + i`. -/
61	def dueProfile (Z : Finset I.Job) (t : ℤ) (i : ℕ) : ℕ :=
62	(Z.filter fun k => (I.d k : ℤ) = t + i).card
63
64	/-- The repaired table: a feasible set of weight `W'`, all of whose jobs have started by
65	`t`, has profile exactly `x` at `t` and costs at most `P'` to preprocess. -/
66	def ReachableProfile (t : ℤ) (x : ℕ → ℕ) (W' : ℕ) (P' : ℤ) : Prop :=
67	∃ Z : Finset I.Job, Feasible I Z ∧ (∀ k ∈ Z, s k ≤ t) ∧
68	(∀ i, 1 ≤ i → dueProfile I Z t i = x i) ∧ weight I Z = W' ∧ pload I Z ≤ P'
69
70	/-- The start time of the job before `k`, and `0` before the first job. -/
71	def sBefore (k : I.Job) : ℤ :=
72	if h : (k : ℕ) = 0 then 0 else s (⟨(k : ℕ) - 1, by omega⟩ : I.Job)
73
74	/-- The paper's `δⱼ`: how far the reference point moves at job `k`. -/
75	def delta (k : I.Job) : ℕ := (s k - sBefore I k).toNat
76
77	variable {I}
78
79	/-- The paper's `x⃗^{(q)}`: the vector `x` with coordinate `c` decremented. -/
80	def decAt {qmax : ℕ} (x : Fin qmax → ℕ) (c : Fin qmax) : Fin qmax → ℕ :=
81	Function.update x c (x c - 1)
82
83	variable (I)
84
85	/-- Recursion (5), exactly as printed. The entries it derives: the base
86	`T₀[0⃗, 0] = 0`, the convention `Tⱼ[0⃗, 0] = 0`, the capacity test `∑ xᵢ ≤ m` and `W' > 0`
87	on every other entry, and the two branches, each through the printed shift — which
88	constrains the earlier vector only on the coordinates at or above `δ`. -/
89	inductive Printed (qmax : ℕ) : ℕ → (Fin qmax → ℕ) → ℕ → ℤ → Prop
90	/-- Before the first job, the empty selection. -/
91	\| init : Printed qmax 0 0 0 0
92	/-- At any stage, the empty selection. -/
93	\| zero (t : ℕ) : Printed qmax t 0 0 0
94	/-- Job `k` is passed over. -/
95	\| skip {k : I.Job} {x y : Fin qmax → ℕ} {W : ℕ} {P : ℤ}
96	(hcap : ∑ i, x i ≤ I.machines) (hW : 0 < W)
97	(hshift : ∀ i : Fin qmax, ∀ hi : delta I k ≤ (i : ℕ),
98	y i = x ⟨(i : ℕ) - delta I k, by have := i.isLt; omega⟩)
99	(h : Printed qmax (k : ℕ) y W P) : Printed qmax ((k : ℕ) + 1) x W P
100	/-- Job `k` is selected. -/
101	\| take {k : I.Job} {x y : Fin qmax → ℕ} {W : ℕ} {P : ℤ} (c : Fin qmax)
102	(hc : (c : ℕ) + 1 = I.q k) (hxc : 1 ≤ x c)
103	(hcap : ∑ i, x i ≤ I.machines) (hW : 0 < W) (hwW : I.w k ≤ W)
104	(hshift : ∀ i : Fin qmax, ∀ hi : delta I k ≤ (i : ℕ),
105	y i = decAt x c ⟨(i : ℕ) - delta I k, by have := i.isLt; omega⟩)
106	(h : Printed qmax (k : ℕ) y (W - I.w k) P) (hfit : P + I.p k ≤ s k) :
107	Printed qmax ((k : ℕ) + 1) x W (P + I.p k)
108
109	end Lax496464.Profile
110

Formalization Notes

The profile is carried as a function on all $i \ge 1$ rather than as a vector of length $q_{\max}$ . This is deliberate. The coordinates beyond $q_{\max}$ are not free: the jobs counted by the profile at $s_j$ all have due dates in $(s_j, s_j + q_{\max}]$ , so those coordinates are zero, and a formulation that leaves them out has to say so separately — which is exactly what the printed recursion fails to do.

The printed recursion is stated here as well, unchanged. The paper writes

\vec{x}[\delta] = \{\vec{y} \in \{0,\dots,m\}^{q_{\max}} : y_i = x_{i-\delta} \text{ for all } i \in \{\delta+1, \dots, q_{\max}\}\},

which pins $\vec{y}$ on the coordinates above $\delta$ and leaves the last $\delta$ coordinates of the shifted vector unconstrained. They are not free, for the reason just given, and leaving them so lets the recursion reach entries that no selection realizes — in both of its branches. The consequence for the algorithm is nothing at all, which is the content of the third theorem's second half: a reachable entry is still witnessed by a feasible selection, only with a profile no larger than the one recorded, and since the capacity test $\sum_i x_i \le m$ is then applied to the larger vector it can only reject more. The optimum read off at the end is exact.

Both versions are therefore defined: the one with the missing condition supplied, whose correctness is the lemma the paper states, and the printed one, whose correctness is the weaker invariant the algorithm actually maintains. Keeping them apart is what lets both be stated.

The printed recursion is given as an inductively defined relation — the entries it derives — rather than as a table of values, since that is what "the recursion reaches this entry" means and it needs no order of evaluation. Its coordinates are numbered from zero, so coordinate $c$ counts the jobs due at $s_j + c + 1$ .

Builds on

Lax496464.Sweep

Used by

Lax496464.Lemma3

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

The Due-Date Profile of Section 5, and Recursion (5)

Flags

Flag this concept

Natural Language Statement

Definition

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments