All missions

Motivation

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) is one of the founding papers of the theory of approximation algorithms. It asks, for optimization problems whose decision versions Karp had just shown to be polynomial complete, how close a fast heuristic can be guaranteed to come to the optimum in the worst case, and it measures this with a worst-case performance ratio that is still the standard yardstick.

Its first example is SUBSET-SUM, the simplest form of the knapsack problem: pack items of given sizes into a knapsack of capacity $b$ so as to fill it as much as possible. For this problem the paper gives a family of algorithms $A_k$, one for each $k \ge 1$, whose guaranteed ratio $(k+1)/k$ tends to $1$. It is one of the first examples of what is now called a polynomial-time approximation scheme: for every $\epsilon > 0$ there is a polynomial-time algorithm within a factor $1 + \epsilon$ of optimal. Sahni (1975) extended the idea to the knapsack problem with utilities, and Ibarra and Kim (1975) later obtained fully polynomial schemes for knapsack and subset-sum.

This mission formalizes Theorem 1 of the paper, the performance guarantee of $A_k$ together with its tightness.

Setting

An input $\langle T, s, b\rangle$ of SUBSET-SUM is a finite set $T$, a positive rational size $s(x)$ for every $x \in T$, and a positive rational bound $b$. An approximate solution is a subset $T' \subseteq T$ with $m(T') \le b$, where the measure is $m(T') = \sum_{x \in T'} s(x)$. The problem is a maximization problem with optimal measure

$$\langle T, s, b\rangle^* = \max\{\, m(T') : T' \subseteq T,\ m(T') \le b \,\}.$$

Fix $k \ge 1$ and call $x$ big if $s(x) > b/(k+1)$ and small otherwise. Algorithm $A_k$ keeps a set $\mathrm{SUB}$, its measure $\mathrm{SUM}$, and the remaining elements $\mathrm{LEFT}$:

1. $\mathrm{SUB}$ is a subset of the big elements whose measure is as large as possible without exceeding $b$; $\mathrm{SUM} = m(\mathrm{SUB})$ and $\mathrm{LEFT} = T \setminus \mathrm{SUB}$.
2. If $s(x) + \mathrm{SUM} > b$ for every $x \in \mathrm{LEFT}$, return $\mathrm{SUB}$.
3. Otherwise pick $y \in \mathrm{LEFT}$ with $s(y) + \mathrm{SUM}$ as large as possible without exceeding $b$, move it from $\mathrm{LEFT}$ to $\mathrm{SUB}$, add $s(y)$ to $\mathrm{SUM}$, and return to step 2.

Steps 1 and 3 may have ties. Following the paper, a set $T_1$ is choosable by $A_k$ if some resolution of all ties produces it, and the performance $A_k(u)$ on input $u$ is the smallest measure of a choosable output. The ratio is $r(A_k, u) = u^*/A_k(u) \ge 1$, and $R[A_k](n)$ is its maximum over inputs of size at most $n$.

Formalization targets

Goal: Theorem 1 (p. 260)

For $k \ge 1$ and $n > 0$,

$$R[A_k](n) \le \frac{k+1}{k}, \qquad \lim_{n \to \infty} R[A_k](n) = \frac{k+1}{k}.$$

Formally, for every $k \ge 1$: every choosable output $T_1$ of every input satisfies $k\,\langle T,s,b\rangle^* \le (k+1)\,m(T_1)$; and for every $\delta > 0$ some input has a choosable output $T_1$ with $m(T_1) > 0$ and $\langle T,s,b\rangle^* > \big(\tfrac{k+1}{k} - \delta\big)\,m(T_1)$.

Milestones

1. For $T_1$ choosable and $T_0$ any approximate solution, $m(T_1^{\mathrm{BIG}}) \ge m(T_0^{\mathrm{BIG}})$ (p. 260).
2. If a small $x \in T$ is not in a choosable $T_1$, then $s(x) + m(T_1) > b$, hence $m(T_1) > kb/(k+1) \ge \tfrac{k}{k+1}\langle T,s,b\rangle^*$ (p. 261).
3. The stronger dichotomy: $m(T_1) = \langle T,s,b\rangle^*$ or $m(T_1) \ge \tfrac{k}{k+1}\,b$ (p. 260).
4. The lower-bound input $T = \{a_1,\dots,a_{k+2}\}$, $s(a_1) = 1+\varepsilon$, $s(a_i) = 1$ otherwise, $b = k+1$: its optimum is $k+1$, some output is choosable, and every choosable output has measure $k + \varepsilon$ (p. 261).

Significance

Theorem 1 shows that SUBSET-SUM admits polynomial-time algorithms with any worst-case ratio above $1$, in contrast with the other problems of the paper (set covering, graph colouring, maximum clique), whose best known ratios grow with the input. The algorithms $A_k$ are an early instance of the partial-enumeration schemes later used for knapsack-type problems. The tightness half shows that the analysis of $A_k$ itself cannot be sharpened.

The theorem has a short published proof, but no machine-checked version is known; there is no subset-sum or knapsack approximation result on the platform. The mission produces a reusable model of SUBSET-SUM, a model of nondeterministic algorithms through a run relation that captures every tie-break, and a checked proof that the worst case is exactly $(k+1)/k$. The same modelling pattern (choosable outputs, worst-case ratio taken over them) is used in the sibling missions of this series for MAX-SAT, set covering and exact covering.

Difficulty

The arithmetic of the upper bound is short; the difficulty is in reasoning about the algorithm as a nondeterministic process. The natural first attempt, implementing $A_k$ as a function with a fixed tie-breaking rule, proves a weaker statement: the guarantee must hold for every output the algorithm may return, including adversarial ties in step 1 (several maximum-measure sets of big elements) and step 3. Facts that are obvious for a single run, such as $\mathrm{SUM}$ always equalling $m(\mathrm{SUB})$ or which elements can enter $\mathrm{SUB}$ after step 1, have to be established for the run relation as a whole. The lower bound requires tracing the run on the explicit input for general $k$: exactly $k-1$ unit elements are added after $a_1$, and this must be shown for every choosable run, not only for one.

Formalization scope

• Numbers. Sizes and the bound are rationals (ℚ), as in the paper; sizes are required to be positive on $T$ and $b > 0$. The index $k$ is a natural number with $1 \le k$ as a hypothesis; $b/(k+1)$ is rational division, and "big" is the strict inequality $s(x) > b/(k+1)$.
• Optimum. opt u is Finset.sup' of the measure over the finite set of approximate solutions, which always contains $\emptyset$; it is $0$ when no element fits.
• Run relation. Choosable k u T₁ states that some admissible step 1 choice, followed by a finite chain of admissible iterations (Relation.ReflTransGen), reaches a halting state returning $T_1$. Every "closest to, without exceeding" is an existential choice among all maximizers.
• Size-free restatement. The paper's input size $|u|$ ("in some standard notation") is never fixed, so the goal quantifies over all inputs instead of over sizes. The upper bound for all choosable outputs is equivalent to $R[A_k](n) \le (k+1)/k$ for all $n$; since $R[A_k]$ is nondecreasing, the limit claim is equivalent to the supremum of the ratio over all inputs being $(k+1)/k$, which is the second part.
• Multiplicative ratios. No ratio is written as a division, so an output of measure $0$ cannot satisfy a bound vacuously; the lower-bound part requires $m(T_1) > 0$. The value $(k+1)/k$ is not claimed to be attained: the paper's family has ratio $(k+1)/(k+\varepsilon)$.
• Lower-bound input. A def on Fin (k + 2) exactly as on the page, with $0 < \varepsilon < 1$ (the page leaves the range implicit; $\varepsilon < 1$ keeps $a_1$ the only big element that fits when $k = 1$).
• Ruled out. A formalization with a deterministic tie-break, with a bound of the form $\mathrm{opt}/m \le c$ in a field where $x/0 = 0$, or with tightness for a single fixed $k$ would be trivial or weaker; none of these is the target.

Contributions welcome: proofs of the milestones and the goal, invariant lemmas for the run relation, and further sanity checks on small inputs. The running-time remark ($O(n^k)$ for step 1) and Sahni's knapsack extension are not part of the mission.

Selected references

• D. S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974) 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• S. Sahni, Approximate algorithms for the 0/1 knapsack problem, Journal of the ACM 22 (1975) 115–124. https://doi.org/10.1145/321864.321873
• O. H. Ibarra, C. E. Kim, Fast approximation algorithms for the knapsack and sum of subset problems, Journal of the ACM 22 (1975) 463–468. https://doi.org/10.1145/321906.321909
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum (1972) 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

A single machine must process a set of jobs, each with a processing time and a due-date, and a job that finishes after its due-date is late. Counting late jobs is the natural objective when a late order is simply lost, whatever its lateness. In the three-field notation of scheduling theory this is the problem $1\,\|\,\sum U_j$, and it is one of the few single-machine problems with a due-date objective that a simple greedy rule solves exactly.

J. Michael Moore gave that rule in 1968 (Management Science 15(1):102–109). The only exact method previously available was the Held–Karp dynamic program, which is exponential in the number of jobs. Moore's algorithm is two sorts plus at most $n(n+1)/2$ additions and comparisons. The rule, and the variant from the paper's Author's Supplement (credited to T. J. Hodgson and today called the Moore–Hodgson algorithm), is in every scheduling textbook, for example Brucker, Scheduling Algorithms, Ch. 4, and is the base case of later work on weighted and release-date variants.

Timeline:

• 1955: J. R. Jackson shows that a job set can be scheduled with no late job if and only if the earliest-due-date order has none (Management Science Research Project report 43, UCLA).
• 1968: Moore publishes the algorithm and its proof of optimality, with Hodgson's variant stated without proof.
• 1970s onward: the weighted version $1\,\|\,\sum w_jU_j$ is shown NP-hard (Karp 1972, via knapsack), and $1\,|\,r_j\,|\,\sum U_j$ likewise (Lenstra, Rinnooy Kan and Brucker 1977), so Moore's greedy rule does not extend to them.

Setting

A finite set $J$ of jobs is given. Job $j$ has a processing time $t_j \ge 0$ and a due-date $D_j$, and the paper assumes $t_j \le D_j$ for every job (a job that cannot finish on time even if started at time $0$ is removed beforehand). The machine starts at time $0$ and processes the jobs one after another, without idle time or preemption.

A schedule $S$ of $J$ is an ordering $(J_{i_1},\dots,J_{i_n})$ of all jobs of $J$. The job in position $k$ completes at $C_{i_k} = t_{i_1} + \dots + t_{i_k}$. The late set is $L = \{J_i : C_i > D_i\}$ and the early set is $E = \{J_i : C_i \le D_i\}$. A schedule is optimal if no schedule of $J$ has fewer late jobs. $A$ and $R$ denote the early and late jobs of $S$, each kept in their order in $S$.

Moore's algorithm works on a current sequence and a list of rejected jobs.

• Step 1: order the jobs by non-decreasing processing time (the shortest processing time rule).
• Step 2: find the first late job $J_{i_q}$ of the current sequence. If there is none, stop.
• Step 3: re-order $J_{i_1},\dots,J_{i_q}$ by non-decreasing due-date. If all of them are then early, keep the re-ordered sequence. Otherwise reject $J_{i_q}$ and remove it. Return to Step 2.

The output is the final current sequence sorted by due-dates, followed by the rejected jobs in any order.

In Lean, a schedule is IsSchedule J l, the late set is lateSet t D l, optimality is IsOptimal t D J l, $A$ and $R$ are earlyPart/latePart, and one pass of Steps 2–3 is the relation MooreStep t D, all in the namespace MooreLateJobs.NumLate.

Formalization targets

Goal: Moore's algorithm is optimal (The Algorithm, Step 2, p. 103)

Let $l_0$ be a shortest-processing-time schedule of $J$, and let a run of MooreStep from $(l_0,[\,])$ reach a state $(\mathrm{cur},\mathrm{rej})$ in which $\mathrm{cur}$ has no late job. Then for every due-date ordering $A_D$ of $\mathrm{cur}$ and every ordering $P$ of $\mathrm{rej}$,

$$(A_D,\,P)\ \text{is an optimal schedule for } J.$$

All tie-breaks in both sorts are covered.

Milestones

In attack order:

1. Lemma 1 (p. 105): every optimal schedule has the same number of late jobs as $(A,R)$ and as every $(A,P)$.
2. Jackson's lemma (p. 105).
3. Lemma 2 (p. 105): re-ordering $A$ by due-dates keeps an optimal $(A,R)$ schedule optimal.
4. Lemma 3 (p. 105): a job that is late in some optimal schedule can be removed and appended.
5. The repeated-elimination claim (p. 106): after removing jobs late in successive optimal schedules until the rest is feasible, $(A_D,P)$ is optimal.
6. Cases 2) and 3) of the Selection Algorithm (p. 107): in either case the job $J_q$ is late in some optimal schedule.
7. Progress and termination of the algorithm (p. 108).

A companion item states the p. 104 remark that the final current sequence need not be re-sorted: $(\mathrm{cur},P)$ is already optimal.

Significance

The theorem shows that the minimum number of late jobs on one machine can be found in $O(n\log n)$ time, by a rule that also produces an optimal schedule of a very particular shape: due-date ordered early jobs first, then the late jobs in any order. Lemma 3's decomposition, that jobs late in some optimal schedule may be discarded one at a time, is the template reused for many related greedy results in scheduling.

The result is classical and fully proved on paper. To our knowledge no machine-checked proof of Moore's algorithm, of the Moore–Hodgson variant, or of Jackson's rule exists in Mathlib. This mission produces a checked proof of the algorithm as stated in the paper, with every tie-break allowed, together with reusable single-machine objects (schedules as lists, completion times, late sets) and Jackson's earliest-due-date feasibility lemma.

Difficulty

Neither ordering rule works alone. Sorting by due-dates alone gives a schedule with no late job whenever one exists, but it can make many jobs late once any must be. Keeping the shortest jobs first does not respect the due-dates at all. The step that fails in a direct greedy argument is the claim that the specific job $J_{i_q}$, the one just found late, belongs to the late set of some optimal schedule. That job is not in general the longest job of the prefix, and the paper has to treat separately the two cases in which it is rejected. On top of this, the algorithm re-sorts prefixes on the fly, so the claim has to be tied to the invariants of the run: the prefix is early and due-date sorted, and the jobs after it are at least as long as $J_{i_q}$.

Formalization scope

• Jobs and times. Jobs form a type ι with decidable equality; $J$ is a Finset ι; $t, D : ι \to \mathbb{R}$.
• Standing hypotheses. Every statement that involves schedules assumes $t_j \ge 0$ and $t_j \le D_j$ on $J$. The first is added: processing times are durations, and Jackson's lemma fails for negative times. The second is the paper's assumption on p. 102.
• Schedules and completion times. A schedule is a duplicate-free list with exactly the jobs of $J$. Positions are 0-based, and the job in position $k$ completes at the sum of the first $k+1$ processing times. Lateness is strict ($C_j > D_j$).
• Optimality compares against every schedule of the same job set.
• Ties. Orderings "by due-dates" and "by processing times" are List.Pairwise with ≤. Ties are arbitrary, and every statement quantifies over all such orderings.
• The algorithm. Steps 2–3 are the relation MooreStep. The re-ordered prefix is any due-date sorted permutation of the first $q+1$ jobs, and case 2) rejects the first late job $J_{i_q}$ itself, not the longest job of the prefix (that is Hodgson's variant). A run is Relation.ReflTransGen.

The goal must concern runs of this step relation from a shortest-processing-time schedule of $J$. Replacing the run by an arbitrary set of rejected jobs satisfying invariants would state a different theorem. The goal is not vacuous: the progress and termination milestones show that a terminal state is always reached.

Contributions are welcome at every level. Useful ones include general lemmas on completion times under permutation and filtering of lists, a proof of Jackson's lemma, proofs of the Selection Algorithm cases, and a proof of Hodgson's variant.

Selected references

• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• M. Held and R. M. Karp, A Dynamic Programming Approach to Sequencing Problems, J. SIAM 10(1):196–210, 1962. https://doi.org/10.1137/0110015
• R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9
• J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1:343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• P. Brucker, Scheduling Algorithms, 5th ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69516-5

Let $u_1, \dots, u_n$ be unit vectors in a Euclidean space such that among any three of them some two are orthogonal. How large can $\|u_1 + \dots + u_n\|$ be?

The answer is $\Theta(n^{2/3})$.

Attribution, which is commonly given wrong in both halves

Lovasz posed the question, as Problem 11.8 of Combinatorial Problems and Exercises (North Holland, 1979). Konyagin proved the $O(n^{2/3})$ upper bound in Systems of vectors in Euclidean space and an extremal problem for polynomials, Mat. Zametki 29 (1981) 63-74, doi:10.1007/BF01142512. Alon gave a matching lower bound in Explicit Ramsey graphs and orthonormal labelings, Electron. J. Combin. 1 (1994) R12, doi:10.37236/1192. The two together pin the exponent exactly.

Where the proof comes from

The hypothesis is a graph condition in disguise. Join $i$ to $j$ when $\langle u_i, u_j \rangle \ne 0$; then "among any three some two are orthogonal" says that graph is triangle-free.

The proof does not run through Ramsey counting, which is the natural first guess and does not reach the right exponent. It runs through the Lovasz theta function. Kashin and Konyagin bound $\theta = O(n^{1/3})$ for graphs of independence number less than 3, that is for complements of triangle-free graphs, and Cauchy-Schwarz turns that into the bound on the norm of the sum. The orthonormal labeling of a graph by unit vectors is not a coincidence of notation: it is the definition of $\theta$ that the argument uses.

What this mission will cost

State this honestly rather than discover it later. The Lovasz theta function, orthonormal graph labeling, and Shannon capacity are all absent from Mathlib. So the milestone chain that the upper bound needs cannot be written yet, and this proposal ships with exactly one milestone, which is Alon's lower bound.

google-deepmind/formal-conjectures contains an SDP-form definition of the theta function, with basic bounds such as lovaszThetaFunction_le_card since PR #6100 of 2026-09-18. The proof here needs the orthonormal-labeling form instead, so that file is a starting point rather than a foundation. Building the theta function, proving that the two forms agree, and getting the Kashin-Konyagin bound is the real content of this mission and is larger than the statement of the goal suggests.

The lower bound is the tractable half. It needs explicit Ramsey graphs and an orthonormal labeling of one, and it does not need $\theta$ at all.

Notes on the formalization

Both items are stated in Mathlib primitives alone, so the mission omits definition items. The triangle-free hypothesis is written as a condition on triples of indices rather than through SimpleGraph.CliqueFree 3, so that a reader auditing the statement does not have to unfold a graph construction to see what is assumed. Anyone proving it is free to build the graph and use the Mathlib predicate.

Motivation

A processor, a machine shop or a single server must work through a set of jobs one at a time, and each job is costly when it is late. Deciding the order is the single-machine sequencing problem, the simplest and most studied model of scheduling theory. Robert McNaughton's 1959 article Scheduling with Deadlines and Loss Functions (Management Science 6(1):1–12) treats it for a computer that must run several tasks, each with a deadline and a loss that grows linearly with the lateness. Its §2 gives the first sufficient condition under which a simple ratio rule is optimal in the presence of deadlines, and shows that interrupting and resuming tasks ("splitting", now called preemption) never helps on one processor.

Timeline.

• 1956: W. E. Smith, Various optimizers for single-stage production (Naval Research Logistics Quarterly 3), proves that sequencing jobs by non-increasing weight-to-processing-time ratio minimizes the total weighted completion time over non-preemptive sequences.
• 1959: McNaughton, §2 of the present paper, proves independently that the same ratio order is optimal against all schedules, split or not and with idle time (Theorem 2.3), and extends it to deadlines when no task finishes early in that order (Theorem 2.4). §3 of the same paper gives the "wrap-around" rule for preemptive makespan on identical processors, and §4 the non-preemptive optimality for weighted completion time on several processors.
• 1977: J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker show that minimizing total weighted tardiness on one machine, the general problem of §2, is strongly NP-hard (Annals of Discrete Mathematics 1); this is why §2 gives a sufficient condition and not an algorithm.

Setting

There are $m$ tasks $(1),\dots,(m)$ for a single processor, and the present is time $0$. Task $(i)$ takes $a_i > 0$ units of processing time, has a deadline $d_i$ and a penalty rate $p_i \ge 0$. If $(i)$ is finished at time $C_i \le d_i$ there is no loss; otherwise the loss on $(i)$ is $p_i x$, where $x = C_i - d_i$ is the time from the deadline to the completion. Thus the loss on a task completed at time $t$ is

$$\ell_i(t) = p_i \max(0,\ t - d_i).$$

The ratio of task $(i)$ is $r_i = p_i / a_i$.

A task may be split: part of it may run between times 4 and 6 and the remainder between times 8 and 11, and similarly in any finite number of parts. A schedule $S$ is therefore a finite list of pieces, each a task together with a start and a stop time. It is feasible when every piece lies in $[0,\infty)$ with start $\le$ stop, no two pieces overlap in time, and the pieces of each task $(i)$ have total length exactly $a_i$. The completion time $C_i(S)$ is the latest stop time of a piece of $(i)$, and the total loss is

$$c(S) = \sum_{i=1}^{m} \ell_i\bigl(C_i(S)\bigr).$$

For an order $\sigma$ of the tasks ($\sigma(k)$ in position $k$), the sequenced schedule $S_\sigma$ runs the tasks without splits and without unused time: $\sigma(k)$ occupies $\bigl[\sum_{l<k} a_{\sigma(l)},\ \sum_{l\le k} a_{\sigma(l)}\bigr]$. The order is in decreasing $r_i$ when $k \le l$ implies $r_{\sigma(l)} \le r_{\sigma(k)}$. Finally $c^*(S)$ denotes the total loss of $S$ computed as if $d_1 = \dots = d_m = 0$.

Formalization targets

Goal: Theorem 2.4 (p. 5)

If $\sigma$ is in decreasing $r_i$ and no task finishes before its deadline in $S_\sigma$, i.e. $d_i \le C_i(S_\sigma)$ for every $i$, then $S_\sigma$ is feasible and

$$c(S_\sigma) \le c(S') \qquad \text{for every feasible schedule } S'.$$

The competitors $S'$ may split tasks and leave the processor idle. The condition is sufficient but not necessary.

Milestones, in attack order

1. Theorem 2.1 (p. 4): if both $(i)$ and $(j)$ run in the $a_i + a_j$ consecutive units of time after a time $t$ past both deadlines and $r_i > r_j$, their joint loss is strictly smaller when $(i)$ goes first:

$$\ell_i(t+a_i) + \ell_j(t+a_i+a_j) < \ell_j(t+a_j) + \ell_i(t+a_j+a_i).$$

2. The reduction in the proof of Theorem 2.2 (pp. 4–5): a feasible schedule with more than $m$ pieces can be replaced by a feasible one with fewer pieces and no greater loss.
3. Theorem 2.2 (p. 4): some optimal schedule, optimal among all feasible schedules, splits no task.
4. Theorem 2.3 (p. 5): if $d_1 = \dots = d_m = 0$, the sequenced schedule in decreasing $r_i$ minimizes the total loss over all feasible schedules.
5. The display of the proof of Theorem 2.4 (p. 6): if no task finishes early in $S = S_\sigma$, then for every feasible $S'$,

$$c(S') - c(S) \ge c^*(S') - c^*(S).$$

Significance

The result. Theorem 2.3 is the ratio rule for total weighted completion time, in its strongest single-machine form: it holds against preemptive schedules and schedules with idle time, not only against permutations. Theorem 2.4 carries the rule over to deadlines and linear tardiness penalties under a checkable condition on one schedule. Since weighted tardiness is strongly NP-hard in general, a condition of this kind is what one can hope for, and the paper's two-step heuristic for general deadlines (p. 6) is built on it. Theorem 2.2, as the paper remarks (p. 6), "does not depend on the linear loss function": it makes non-preemptive scheduling without loss of generality for single-machine objectives of this kind.

Formalizing it. All results of §2 are proved in the paper and are textbook material; none has a machine-checked proof on the platform. The platform's Scheduling Algorithms V mission formalizes the multi-processor results of §§3–4 (via Brucker's textbook), and nothing there states a single-processor ratio rule with deadlines. This mission supplies a single-processor schedule model with splitting, the interchange lemma, the non-preemption theorem and the ratio rule, each over all feasible schedules.

Difficulty

The interchange argument of Theorem 2.1 compares only two schedules that differ in the order of two adjacent tasks. Turning it into optimality against every feasible schedule requires two further steps, and each fails if done naively. First, a competitor may split tasks and leave gaps; the interchange argument does not apply to such schedules, so a separate argument must remove splits without raising any completion time. Second, with deadlines the loss $\max(0, t - d_i)$ is not linear in the completion time, so the ratio order is in general not optimal; the obvious attempt to repeat the interchange argument fails as soon as a task can finish before its deadline, since moving such a task later costs nothing. This is why Theorem 2.4 needs its hypothesis that no task finishes early, and why the paper leaves the general case to a heuristic.

Formalization scope

Tasks and positions are the zero-based indices of Fin m; times, lengths, deadlines and penalties are real numbers. A schedule is a List of pieces (task, start, stop), mirroring the public definition SchedulingAlgorithms_ParallelMachines with one processor. Feasibility requires $0 \le$ start $\le$ stop, pairwise disjoint pieces, and exact total length $a_i$ per task; zero-length pieces and unsorted lists are allowed. The completion time is the maximum stop time of the task's pieces ($0$ for a task with no pieces, which feasibility excludes). "No split" means exactly one piece per task, so two abutting pieces count as a split. "Decreasing $r_i$" is non-increasing, with ties in any order. "Minimal" and "optimal" are stated as $\le$ against every feasible schedule, never as an infimum.

Standing assumptions, stated in every item: $a_i > 0$ (tasks take time, and $r_i = p_i/a_i$ needs $a_i \ne 0$), and $p_i \ge 0$ for Theorems 2.2–2.4 and the proof steps (penalties are non-negative; with a negative penalty and idle time allowed the loss is unbounded below). Theorem 2.1 carries no sign condition. No condition is placed on the deadlines.

A formalization that restricts the competitors of Theorems 2.2–2.4 to unsplit schedules, or to sequenced schedules of other orders, states a weaker theorem and is ruled out: every statement quantifies over all feasible schedules.

A complete development needs: sums over sublists of pieces, rearrangements of pieces of a schedule and their effect on completion times, and optimality over permutations of a finite set of tasks. The schedule model and the non-preemption argument are reusable for any single-machine regular objective. Contributions of intermediate lemmas on these points are welcome.

Selected references

• R. McNaughton, Scheduling with Deadlines and Loss Functions, Management Science 6(1):1–12, 1959. https://doi.org/10.1287/mnsc.6.1.1
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3(1–2):59–66, 1956. https://doi.org/10.1002/nav.3800030106
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Annals of Discrete Mathematics 1:343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• P. Brucker, Scheduling Algorithms, 5th ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69516-5

Motivation

The nearest common ancestor problem asks, for a rooted tree and two of its vertices $v$ and $w$, for the deepest vertex that is an ancestor of both, written $\operatorname{nca}(v,w)$. It is a subroutine in string and graph algorithms.

Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) preprocess a static tree of $n$ vertices in linear time on a random-access machine so that each query takes constant time. For a complete binary tree the queries reduce to bit arithmetic on vertex numbers (§3). An arbitrary tree is first reduced, in §4, to a compressed tree $C$ whose sizes double along every edge, and $C$ is cut by rank into three plies. Lemma 9 bounds the size of each ply, and those bounds are what make the tables of the method fit in linear space. This mission formalizes the structural lemmas of §4 about $C$ and Lemma 9.

Timeline.

• 1976: Aho, Hopcroft and Ullman give an $O(\log\log n)$-per-query random-access algorithm for static trees.
• 1979: Tarjan (Applications of path compression on balanced trees, J. ACM 26) uses the decomposition of a tree by the doubling rule on subtree sizes to compute functions on paths; Lemmas 5–7 of Harel–Tarjan are cited from there without proof.
• 1983: Sleator and Tarjan (A data structure for dynamic trees, J. Comput. System Sci. 26) use the same heavy/light split of edges for dynamic trees.
• 1984: Harel and Tarjan give the $O(n)$-preprocessing, $O(1)$-query algorithm, with the compressed tree and its plies (§4).

Setting

A rooted tree $T$ (Appendix, p. 354) consists of a finite vertex set $V$ with $n = |V|$, a root $r \in V$ and a parent map $p_T$, defined for $v \ne r$, such that every vertex reaches $r$ by iterating $p_T$. The edges of $T$ are the pairs $v \to p_T(v)$ for $v \ne r$. If $p_T^i(v) = w$ for some $i \ge 0$, then $v$ is a descendant of $w$ and $w$ an ancestor of $v$. Every vertex is its own ancestor and descendant. The depth of $v$ is the number of edges from $v$ to $r$. $\mathrm{size}_T(v)$ is the number of descendants of $v$, including $v$.

An edge $v \to p_T(v)$ is light if $2\cdot\mathrm{size}_T(v) \le \mathrm{size}_T(p_T(v))$ and heavy otherwise. At most one heavy edge enters each vertex, so the heavy edges partition $V$ into heavy paths. A vertex with no heavy edge entering or leaving it forms a heavy path by itself. The apex of a heavy path is its vertex of smallest depth, and $\mathrm{apex}(v)$ denotes the apex of the heavy path containing $v$.

The compressed tree $C$ has the same vertices and root as $T$, and its edges are

$$\{\, v \to \mathrm{apex}(p_T(v)) : v \ne r \,\}.$$

Write $p_C(v) = \mathrm{apex}(p_T(v))$, and let $\mathrm{size}_C(v)$ be the number of descendants of $v$ in $C$. The rank of $v$ is $\mathrm{rank}(v) = \lfloor \lg \mathrm{size}_C(v)\rfloor$, where $\lg = \log_2$. Let $\lg^{(i)}$ denote the $i$-fold iterate of $\lg$. Ply three is the set of vertices of rank at least $\lfloor\lg^{(2)} n\rfloor$. Ply two is the set of vertices whose rank lies between $\lfloor\lg^{(3)} n\rfloor$ and $\lfloor\lg^{(2)} n\rfloor - 1$, inclusive. Ply one is the set of vertices of rank below $\lfloor\lg^{(3)} n\rfloor$.

Formalization targets

Goal: Lemma 9 in the explicit form of its proof

For every rooted tree on $n \ge 4$ vertices:

$$|\text{ply three}| \le \frac{4n}{\lg n}, \qquad |\text{ply two}| \le \frac{4n}{\lg^{(2)} n},$$

and for every vertex $v$ in ply one, every $C$-descendant of $v$ lies in ply one and $\mathrm{size}_C(v) \le \lg^{(2)} n$.

The paper states the first two bounds as $O(n/\log n)$ and $O(n/\log^{(2)} n)$. The constants $4$ and $4$ are the ones its proof on p. 345 establishes. The third clause is the paper's "each connected component of ply one is a subtree of $C$ containing at most $\log^{(2)} n$ vertices", read vertex by vertex. Ply one is closed under $C$-descendants, so the component of a ply-one vertex is the $C$-subtree of its shallowest ply-one ancestor.

Milestones

1. Lemma 5 (p. 344): $\mathrm{size}_C(v) = \mathrm{size}_T(v)$ if $v$ is an apex, and $\mathrm{size}_C(v) = 1$ otherwise.
2. Lemma 6 (p. 344): $2\cdot\mathrm{size}_C(v) \le \mathrm{size}_C(p_C(v))$ for every $v \ne r$.
3. Lemma 8 (p. 344): for every $i$, at most $n/2^i$ vertices have rank $i$.
4. Proof of Lemma 9, first sentence (p. 345): at most $n/2^{k-1}$ vertices have rank $k$ or greater.

A further item states Lemma 7 (p. 344): $C$ has depth at most $\lfloor\lg n\rfloor$. The paper uses it to bound the tables of ply three, not in the proof of Lemma 9.

Significance

Lemma 9 is the counting step of the linear-time preprocessing. Ply three has $O(n/\log n)$ vertices, each with $O(\log n)$ ancestors in $C$ by Lemma 7, so storing every vertex's ply-three ancestors takes $O(n)$ space. Ply two has $O(n/\log^{(2)} n)$ vertices, each with $O(\log^{(2)} n)$ ply-two ancestors, which again gives $O(n)$. Ply one splits into subtrees of at most $\lg^{(2)} n$ vertices, and these are small enough to be embedded in complete binary trees and answered by the bit arithmetic of §3.

Lemmas 5–8 and the proof of Lemma 9 are proved or cited in the paper, and none of them is open. As far as a search of the platform shows, none has a machine-checked proof, and Mathlib has no parent-map rooted trees, subtree sizes or heavy-path decompositions. The mission produces a reusable formal account of heavy paths and of the size-doubling compressed tree, with the paper's explicit constants.

Difficulty

The paper states Lemmas 5–7 without proof, citing Tarjan (1979). Lemma 5 requires identifying the $C$-descendants of an apex with its $T$-descendants. That identification needs a clean description of heavy paths: at most one heavy edge enters each vertex, a vertex's heavy path runs up to its apex, and the heavy paths do not overlap. Lemma 8 needs the observation that two vertices of equal rank are unrelated in $C$, so that their descendant sets are disjoint and the sizes add up to at most $n$. Lemma 9 turns floors of iterated real logarithms into bounds on powers of two. The step $2^{\lfloor \lg^{(2)} n\rfloor} > \tfrac12 \lg n$ loses a factor $2$, and this is where the constant $4$ comes from; a proof that expects the constant $2$ fails at this step.

Formalization scope

• Trees. A rooted tree is a structure over a Fintype vertex type $V$ with a root, a total parent map and the axiom that every vertex reaches the root. The paper's partial map is made total by $p_T(r) = r$. Every statement about an edge $v \to p(v)$ assumes $v \ne r$, since for $v = r$ Lemma 6 would read $2n \le n$. The Appendix's printed "$p^0(v) = 0$" is read as $p^0(v) = v$.
• Heavy edges and apex. A heavy edge is $v \ne r$ with $\mathrm{size}_T(p_T(v)) < 2\,\mathrm{size}_T(v)$, the strict negation of light. $\mathrm{apex}(v)$ is computed by climbing heavy edges from $v$ until the first edge that is not heavy, which is the apex of the heavy path containing $v$. The root is always an apex.
• Compressed tree. $p_C(v) = \mathrm{apex}(p_T(v))$ for $v \ne r$ and $p_C(r) = r$. Ancestors and sizes in $C$ are defined through iterates of $p_C$.
• Logarithms. The rank is Nat.log 2 of $\mathrm{size}_C$, which is exactly $\lfloor\lg\mathrm{size}_C\rfloor$. The ply thresholds are iterated Nat.log 2, which equal the real floors $\lfloor\lg^{(2)} n\rfloor$ and $\lfloor\lg^{(3)} n\rfloor$ for $n \ge 4$. The bounds of the goal use Real.logb 2.
• Added hypothesis $n \ge 4$ in the goal. It makes $\lg n \ge 2$ and $\lg^{(2)} n \ge 1$, so the divisions are honest (Lean's $x/0 = 0$), and it makes $\lg^{(3)} n \ge 0$. On the page it is hidden in the $O(\cdot)$.
• Division-free milestones. Lemma 8 is stated as $\#\{\mathrm{rank} = i\}\cdot 2^i \le n$, and the rank-$\ge k$ count as $\#\{\mathrm{rank} \ge k\}\cdot 2^k \le 2n$.
• Ruled out. The goal is not an $\exists C$ statement. Replacing the paper's $4$ by an existential constant, or bounding ply three by $n$, would discard the content of the lemma.
• Welcome contributions. A library of facts about heavy paths is welcome: uniqueness of the entering heavy edge, apex characterizations, and the descendants of an apex in $C$. So are proofs of Lemmas 5–8 and proofs that the iterated Nat.log thresholds agree with the real ones. It is reusable for heavy-light decompositions generally.

Selected references

• D. Harel, R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2):338–355, 1984. https://doi.org/10.1137/0213024
• R. E. Tarjan, Applications of path compression on balanced trees, J. ACM 26(4):690–715, 1979. https://doi.org/10.1145/322154.322161
• A. V. Aho, J. E. Hopcroft, J. D. Ullman, On finding lowest common ancestors in trees, SIAM J. Comput. 5(1):115–132, 1976. https://doi.org/10.1137/0205011
• D. D. Sleator, R. E. Tarjan, A data structure for dynamic trees, J. Comput. System Sci. 26(3):362–391, 1983. https://doi.org/10.1016/0022-0000(83)90006-5

Motivation

Small and medium-sized suppliers that sell to large retailers typically ship first and are paid weeks or months later. Until the invoice is paid, the supplier's cash is trapped in accounts receivable, while production has to be financed up front. Factoring (selling or pledging the receivable to a financial intermediary for immediate cash) and reverse factoring (a buyer-initiated program in which the retailer approves the invoice and the supplier is paid early by the retailer's bank) are the standard remedies, and reverse factoring programs of large buyers are often coupled with an extension of payment terms. Which of these instruments a supplier should use, and how the answer depends on the credit ratings of the two firms, is the question addressed by Kouvelis and Xu, "A Supply Chain Theory of Factoring and Reverse Factoring", Management Science 67(10):6071–6088, 2021 (doi:10.1287/mnsc.2020.3788). The paper embeds each financing scheme in the pull wholesale-price game of Cachon (2004) and compares the resulting equilibria.

Setting

A retailer (the Stackelberg leader) offers a wholesale price $w$ to a capital-constrained supplier (the follower), who then chooses a production quantity $q \ge 0$ and carries the inventory; the retail price $p$ is fixed, and $0 < c < p$ is the unit production cost. Demand $D \ge 0$ has density $f$, complementary distribution function $\bar F$, finite mean, $f > 0$ on $[0, \mathbb Z]$ ($\mathbb Z \le +\infty$), and a strictly increasing failure rate $z = f/\bar F$ (strict IFR). Expected sales are $S(q) = \int_0^q \bar F(\xi)\,d\xi$, and $k(q) = S(q)/\bar F(q)$.

Each firm $j \in \{s, r\}$ has a credit rating $C_j \in (C_{\min}, C_{\max})$. The default probability $\rho_j = \rho(C_j) \in [0,1]$ is strictly decreasing in the rating, and the interest-rate premium $\eta_j = \eta(C_j) > 0$ is decreasing. Production takes a lead time $t_1$, payment follows after a term $t_2$, and the supplier faces a Poisson liquidity shock of rate $\lambda_s$ during production (the retailer, rate $\lambda_r$). Under a scheme $i \in \{\mathcal F, \mathcal N, \mathcal R\}$ (recourse, non-recourse, reverse factoring, the last with a payment extension $\tau \ge 0$), the supplier's expected profit is

$$\pi_i(q; w) = (1-\rho_s)\big(\Lambda_i e^{-\lambda_s t_1} w S(q) - c q e^{\eta_s t_1}\big),$$

with coefficients $\Lambda_{\mathcal F} = (1-\rho_r) + (1-\rho_s) - e^{\eta_s t_2}$, $\Lambda_{\mathcal N} = e^{-\eta_r t_2}(1-\rho_r)$, $\Lambda_{\mathcal R} = e^{-\eta_r(t_2+\tau)}$, and effective unit cost $c_i = c\,e^{(\eta_s+\lambda_s)t_1}/\Lambda_i$. The retailer's profit is $e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and carries the extra factor $2 - e^{-\lambda_r \tau}$ under reverse factoring.

Formalization targets

Goal: Proposition 5

For a given $\tau \ge 0$, let $\mathbb C_3$ be the unique supplier rating with $\Lambda_{\mathcal F} = \Lambda_{\mathcal R}$, $\mathbb C_1$ the one with $\Lambda_{\mathcal F} = \Lambda_{\mathcal N}$, and $\mathbb C_{\mathcal F}, \mathbb C_{\mathcal N}, \mathbb C_{\mathcal R}$ the feasibility thresholds ($c_i = p$). With all three schemes available,

$$e^{-\eta_r\tau} < 1-\rho_r:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_1,\qquad \mathcal N \text{ adopted} \iff \mathbb C_{\mathcal N} < C_s \le \mathbb C_1;$$ $$1-\rho_r \le e^{-\eta_r\tau}:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_3,\qquad \mathcal R \text{ adopted} \iff \mathbb C_{\mathcal R} < C_s \le \mathbb C_3.$$

Milestones

1. Proposition 2 (p. 6078): recourse factoring is feasible iff $C_s > \mathbb C_{\mathcal F}$, and then the unique equilibrium solves $p\bar F(q) = c_{\mathcal F}[1+z(q)k(q)]$, $w = c_{\mathcal F}/\bar F(q)$.
2. Proposition 3 (p. 6079): the same for non-recourse factoring with $c_{\mathcal N}$.
3. §5.2 (p. 6082, Proposition EC.2): the same for reverse factoring with $c_{\mathcal R}(\tau)$.
4. §4.4 (p. 6080, Lemma EC.2): between feasible schemes, the supplier's equilibrium profits are ordered as the $\Lambda_i$.
5. Proposition 4 (p. 6080): the choice between $\mathcal F$ and $\mathcal N$ alone.

A follow-on item states Corollary 1(i) (p. 6081): when the retailer's rating is at least the supplier's, non-recourse factoring strictly dominates recourse factoring whenever the latter is feasible.

Significance

Proposition 5 is the paper's main prediction: non-recourse factoring is the choice of medium-rated suppliers, recourse factoring of highly rated ones, and reverse factoring with a fixed payment extension is chosen only by low-to-medium-rated suppliers and only if the retailer's rating is not too high relative to the extension. The paper uses it to explain the documented reluctance of suppliers to join reverse-factoring programs that come with extended payment terms (Wuttke, Rosenzweig and Heese 2019; Corsten 2010, a teaching case), and it is the starting point of the paper's Proposition 6 on the retailer's optimal payment extension, which is the subject of the second mission of this series.

The results are proved in the paper's Online Appendix B. To the best of available knowledge none of them, and no model of supply chain finance, has a machine-checked proof. A formal development would also supply a reusable treatment of the pull wholesale-price game under a strictly IFR demand with an arbitrary effective unit cost, of which Propositions 2, 3 and EC.2 are three instances.

Difficulty

The case analysis of Proposition 5 is short once the milestones are available; the substance lies in them. Proposition 2 requires solving a bilevel problem: the follower's best response has to be identified for every wholesale price, including prices at which the supplier produces nothing, and the leader's objective has to be shown to have a single maximizer. The natural route through the first-order condition needs the IFR property to exclude multiple stationary points, and it has to cope with a support end $\mathbb Z$ that may be finite (where $\bar F$ vanishes and $k$, $z$ lose meaning) or infinite. Lemma EC.2 requires the equilibrium supplier profit as an explicit function of the effective cost and a monotonicity argument for it; comparing the $\Lambda_i$ directly, without the equilibrium, does not prove it. The proofs themselves are not in the main text.

Formalization scope

Demand is a probability measure μ on ℝ with a density f, the support end Z : EReal, and the complementary distribution function Fbar μ x = μ((x, ∞)). The model data, the coefficients coef, the effective costs cF, cN, cR, the two profit functions, best responses, equilibria, feasibility and adoption are definitions; all theorems are for arbitrary data satisfying Params.Valid and DemandModel. Readings fixed by the formalization:

• "Feasible": some wholesale price $w \ge 0$ with a supplier best response gives the retailer strictly positive profit. It is not defined as $c_i < p$, which is what Propositions 2 and 3 prove.
• "Adopted" / "should be adopted": the scheme is feasible and its equilibrium supplier profit is best among the feasible available schemes, with ties resolved $\mathcal R \succ \mathcal N \succ \mathcal F$, the order forced by the paper's boundaries ($C_s = \mathbb C_1$, $C_s = \mathbb C_3$, $C_r = \mathbb C_2$). Profits are compared, not the $\Lambda_i$.
• "The unique value of $C_s$ that satisfies …": a point of $(C_{\min}, C_{\max})$ satisfying the equation and the only such point. The equation $c_{\mathcal F} = p$ is cross-multiplied, $c\,e^{(\eta_s+\lambda_s)t_1} = p\Lambda_{\mathcal F}$, since $\Lambda_{\mathcal F}$ may be $\le 0$.
• "$C_r > \mathbb C_2$" is read through the paper's equivalence $\tau > -\eta_r^{-1}\ln(1-\rho_r)$, i.e. $e^{-\eta_r\tau} < 1-\rho_r$: the stated assumptions give no single crossing in $C_r$.
• "The unique equilibrium can be derived from …": the equilibrium exists and is unique, and it is exactly the solution of the system with $q \in (0, \mathbb Z)$; this part is stated under feasibility.
• "Increasing/decreasing" is weak unless stated (p. 6075); $\rho$ is strictly decreasing, $\eta$ weakly.
• Continuity of $f$ is read on $[0,\mathbb Z]$, and $\mathbb Z$ as the upper end of the support.
• Additions: wholesale prices are nonnegative; the retailer's reverse-factoring profit is the last line of the p. 6082 display (the middle line has a stray factor $w$).
• Corollary 1(i): "higher credit rating" is read as $C_r \ge C_s$, "dominates" as a strictly larger equilibrium supplier profit whenever recourse is feasible.

A formalization in which feasibility or adoption is defined by the inequalities being proved ($c_i < p$, largest $\Lambda_i$) makes the propositions trivial and is ruled out by the definitions above. The profit functions (7), (10) and the p. 6082 display are taken as the model; the derivation from bank and factor pricing (Eqs. (1), (5), (6), Lemma 1) is not formalized, and the unstated assumptions of Table EC.2 are not included. Contributions of reusable lemmas on $S$, $k$ and $z$ under strict IFR are welcome.

Selected references

• P. Kouvelis and F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0189
• D. A. Wuttke, E. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019.
• P. Kouvelis and W. Zhao, Who Should Finance the Supply Chain? Impact of Credit Ratings on Supply Chain Decisions, Manufacturing & Service Operations Management 20(1):19–35, 2018.

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality $F(x) = F_0 + \sum_{i=1}^m x_i F_i \succeq 0$. In engineering applications the coefficient matrices are rarely known exactly: they come from measurements, from a model of a physical plant, or from a finite-precision implementation. El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for solutions that remain feasible for every admissible value of the uncertain data, and showed how to compute such robust solutions by semidefinite programming. The paper appeared alongside Ben-Tal and Nemirovski's robust convex programming (Math. Oper. Res. 23(4), 1998) and is one of the two founding treatments of robust SDP.

When the uncertainty has structure (a block-diagonal perturbation, repeated scalar parameters, a symmetric matrix), the exact robust problem is NP-hard (El Ghaoui and Lebret, SIAM J. Matrix Anal. Appl. 18, 1997). This is the same obstacle that robust control meets in computing the structured singular value, and the remedy the paper uses, scaling matrices that commute with the perturbation structure, goes back to that literature (Doyle, IEE Proc. D 129, 1982; Fan, Tits and Doyle, IEEE Trans. Automat. Control 36, 1991). This mission formalizes the resulting tractable conservative approximation, Theorem 3.2 of the paper, together with the lemma it rests on and an application to integer feasibility problems.

Setting

Fix natural numbers $m, n, p, q$. The decision variable is $x \in \mathbb{R}^m$. The nominal data are affine maps

$$F(x) = F_0 + \sum_{i=1}^m x_i F_i \in \mathbb{R}^{n\times n}, \qquad R(x) = R_0 + \sum_{i=1}^m x_i R_i \in \mathbb{R}^{q\times n},$$

with every $F_i$ symmetric, and fixed matrices $L \in \mathbb{R}^{n\times p}$, $D \in \mathbb{R}^{q\times p}$. A perturbation is a matrix $\Delta \in \mathbb{R}^{p\times q}$, and the perturbed constraint matrix is the linear-fractional representation (LFR)

$$\mathbf{F}(x,\Delta) = F(x) + L\Delta(I - D\Delta)^{-1}R(x) + R(x)^T(I - \Delta^TD^T)^{-1}\Delta^TL^T,$$

which is defined when $\det(I - D\Delta) \neq 0$. The perturbation ranges over a linear subspace $\mathcal{D} \subseteq \mathbb{R}^{p\times q}$, which encodes the structure, and is bounded by a level $\rho > 0$ in the spectral norm $\|\Delta\|$ (the largest singular value). The robust feasible set is

$$\mathcal{X}_\rho = \{x : \text{for every } \Delta \in \mathcal{D} \text{ with } \|\Delta\| \le \rho,\ \det(I - D\Delta) \neq 0 \text{ and } \mathbf{F}(x,\Delta) \succeq 0\},$$

and the robust SDP (RSDP) is to minimize $c^Tx$ over $\mathcal{X}_\rho$.

The scaling set of $\mathcal{D}$ is the linear subspace

$$\mathcal{B} = \{(S,T,G) \in \mathbb{R}^{p\times p}\times\mathbb{R}^{q\times q}\times\mathbb{R}^{p\times q} : S\Delta = \Delta T,\ G\Delta^T = -\Delta G^T \text{ for every } \Delta \in \mathcal{D}\}.$$

Formalization targets

Goal: Theorem 3.2 (p. 37), as an inclusion of feasible sets

For every $x$: if some $(S,T,G) \in \mathcal{B}$ has $S \succ 0$, $T \succ 0$ and

$$\begin{bmatrix} F(x) - LSL^T & R(x)^T - LSD^T + LG \\ R(x) - DSL^T + G^TL^T & \rho^{-2}T - DSD^T + DG + G^TD^T\end{bmatrix} \succ 0,$$

then $x \in \mathcal{X}_\rho$, and in fact $\mathbf{F}(x,\Delta) \succ 0$ for every $\Delta \in \mathcal{D}$ with $\|\Delta\| \le \rho$. A companion item states the consequence for optimal values: the SDP value is an upper bound on the RSDP value, with both infima taken in the extended reals.

Milestones

1. Lemma 3.2 (p. 37): the same implication for constant $F$, $R$ and $\rho = 1$, with the matrix (13).
2. The full-perturbation case (p. 37): for $\mathcal{D} = \mathbb{R}^{p\times q}$ and $p, q \ge 1$, $\mathcal{B}$ consists exactly of the triples $(\tau I_p, \tau I_q, 0)$, with $\tau \ge 0$ when $S \succeq 0$.
3. Theorem 5.6 (p. 48): if $F_i = 2L_iR_i$ with $r_i = \operatorname{rank} F_i$, and $x_{\mathrm{feas}}$ satisfies, for some $\lambda \ge 0$ and block-diagonal $S = S^T$, $G = -G^T$,

$$\begin{bmatrix} F(x_{\mathrm{feas}}) - \lambda I - LSL^T & \tfrac12R^T + LG \\ \tfrac12R - GL^T & S\end{bmatrix} \succ 0,$$

then every integer vector closest to $x_{\mathrm{feas}}$ in the maximum norm satisfies $F(z) \succeq 0$.

Significance

The result. Theorem 3.2 replaces an NP-hard semi-infinite constraint, one matrix inequality for each admissible perturbation, by a single linear matrix inequality in the enlarged variable $(x, S, T, G)$. Every point it certifies is robustly feasible, so its optimal value is a certified upper bound on the robust optimum and its optimizer is a usable robust solution. In the full case the scalings collapse to one multiplier $\tau$ (milestone 2), which connects the bound to the exact reformulation of Section 3.1 of the paper. Theorem 5.6 shows the same machinery at work on a combinatorial problem: robustness against perturbations of size $1/2$ in each coordinate of $x$ turns an SDP-feasible point into an integer solution by rounding.

Formalizing it. The results are proved in the paper (Lemma 3.2 with the proof deferred to [16]); none of them has a machine-checked proof that this mission is aware of, and the platform has no linear-fractional or structured-perturbation results. The formalization also settles the exact form of the certificate: as printed, the matrix (13) and the LMI of Theorem 3.2 contain products that are dimensionally undefined, and this mission states the condition the proof actually yields (see the scope section).

Difficulty

The inequality to be proved is a statement about infinitely many perturbations, and $\mathbf{F}(x,\Delta)$ depends on $\Delta$ through a matrix inverse. The natural first step, eliminating $\Delta$ by an exact S-procedure as in the full case, is not available: with a structured $\mathcal{D}$ the set of pairs of vectors linked by some $\Delta \in \mathcal{D}$ is not described by one quadratic inequality, and losslessness fails. The scalings in $\mathcal{B}$ give several valid quadratic inequalities instead, and one must show that their combination controls every $\Delta$ in the norm ball, including the well-posedness claim $\det(I - D\Delta) \neq 0$, which is part of the conclusion rather than an assumption. The commutation condition $S\Delta = \Delta T$ must be turned into an inequality for $\|\Delta\| \le 1$, which requires more than the definition of the spectral norm. For Theorem 5.6 the block-diagonal perturbation family and the rescaling between $\rho = 1/2$ and the stated matrix must be matched to the general lemma.

Formalization scope

Matrices are Matrix (Fin a) (Fin b) ℝ; $\succ 0$ and $\succeq 0$ are Matrix.PosDef and Matrix.PosSemidef (both include symmetry); block matrices are Matrix.fromBlocks on Fin n ⊕ Fin q. The norm of a perturbation is the $\ell^2$ operator norm (open scoped Matrix.Norms.L2Operator), i.e. the largest singular value; the maximum norm in Theorem 5.6 is Mathlib's sup norm on Fin m → ℝ. $\mathcal{D}$ is a Submodule. Affine maps are given by coefficient families indexed by Fin (m+1). Mathlib's matrix inverse is $0$ at a singular matrix, so every statement pairs the LFR with $\det(I - D\Delta) \neq 0$. The standing assumption $\rho > 0$ of Section 3 is a hypothesis.

Readings and corrections of the printed statements:

• (13) as printed is dimensionally inconsistent; we state the condition the proof yields, which coincides with the printed one when $G$ is square and skew-symmetric and $\mathcal{D}$ consists of symmetric matrices. Concretely, (11) prints $G \in \mathbb{R}^{q\times p}$ with $G\Delta = -\Delta^TG^T$ and (13) prints the blocks $R - DSL - GL^T$ and $T - GD^T + DG - DSD^T$; the mission uses $G \in \mathbb{R}^{p\times q}$ with $G\Delta^T = -\Delta G^T$ and the blocks $R - DSL^T + G^TL^T$ and $T - DSD^T + DG + G^TD^T$. The same correction applies to the LMI of Theorem 3.2 (with $\rho^{-2}T$). Theorem 5.6 is stated as printed.
• "An upper bound on the RSDP (4) and a corresponding solution $x$ can be computed by solving the SDP" is read as the inclusion of the SDP's feasible projection in $\mathcal{X}_\rho$, for every $x$; the goal states it with the strict conclusion $\mathbf{F}(x,\Delta) \succ 0$ as well. The value form is a separate item.
• In the full-perturbation remark, "for some $\tau \ge 0$" is stated under $S \succeq 0$, and "We then recover the exact results of section 3.1" is not formalized.
• In Theorem 5.6, $\mathcal{S}$'s index range "$i = 1,\dots,n$" is read as $i = 1,\dots,m$; the hypothesis $r_i = \operatorname{rank}F_i$ is kept.

Trivializing formalizations are ruled out: $(0,0,0) \in \mathcal{B}$ always, so the hypotheses $S \succ 0$ and $T \succ 0$ are kept outside $\mathcal{B}$; $\mathcal{D}$ is a subspace, not an arbitrary set; and the norm is the spectral norm, not Mathlib's default entrywise norm.

A complete development needs the square root of a positive definite matrix and its commutation with $S$ and $T$, the spectral-norm characterization $\Delta\Delta^T \preceq \|\Delta\|^2 I$, Schur-complement and congruence facts for block matrices, and a linear-fractional identity relating $(I - D\Delta)^{-1}$ to an auxiliary vector. These are reusable well beyond this mission; contributions of any of them, and of the value and rounding corollaries, are welcome.

Selected references

• L. El Ghaoui, F. Oustry, H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1):33–52, 1998. https://doi.org/10.1137/S1052623496305717
• L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18:1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• M. K. H. Fan, A. L. Tits, J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36:25–38, 1991. https://doi.org/10.1109/9.62265
• J. C. Doyle, Analysis of feedback systems with structured uncertainties, IEE Proc. D 129(6):242–250, 1982. https://doi.org/10.1049/ip-d.1982.0053
• A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777

Motivation

Many firms learn about demand before it has to be served: customers place orders days or weeks ahead of the date they want delivery. Gallego and Özer (Management Science 47(10), 2001) model this advance demand information in a periodic-review inventory system and ask how the optimal replenishment policy should use it. Classical inventory theory (Arrow, Harris and Marschak 1951; Scarf 1959; Veinott 1965, 1966; Iglehart 1963) assumes that nothing about future demand is known when an order is placed. With advance orders the state of the system is no longer a single number, and it is not a priori clear whether the familiar policy structures survive.

This mission covers the paper's zero set-up cost case (Section 5). The companion mission Integrating Replenishment Decisions with Advance Demand Information I covers the positive set-up cost case and its $(s, S)$ policies.

Setting

Time is divided into periods $t = 1, \dots, T$. The supply lead time is an integer $L \ge 0$, and the information horizon is $N$. In period $t$ customers place orders $D_t = (D_{t,t}, \dots, D_{t,t+N})$, where $D_{t,s} \ge 0$ is demand placed in period $t$ for delivery in period $s$. Throughout, $N > L + 1$; write $M = N - L - 1 \ge 1$.

At the start of period $t$ the decision maker knows two things. The first is the modified inventory position $x_t$: on-hand stock plus outstanding orders minus backorders, net of the demand already observed for the protection period $t, \dots, t+L$. The second is the vector

$$o_t = (o_{t,t+L+1}, \dots, o_{t,t+N-1}) \in \mathbb{R}^M$$

of demands already observed for periods beyond the protection period. The decision maker raises the position to $y \ge x_t$ at zero fixed cost, the demand vector $D_t$ is realised, and the state moves to

$$x_{t+1} = y - \sum_{k=0}^{L+1} D_{t,t+k} - o_{t,t+L+1}, \qquad o_{t+1,s} = o_{t,s} + D_{t,s}\ (s = t+L+2, \dots, t+N),$$

with $o_{t,t+N} = 0$.

Costs enter through a single-period cost $G_t : \mathbb{R} \to \mathbb{R}$ (holding, backorder and linear ordering cost, charged against the demand over the protection period) and one-period discount factors $\alpha_{t+1} > 0$. The optimal cost-to-go $J_t$ and the cost $V_t$ of ordering up to $y$ satisfy

$$J_t(x, o) = \min_{y \ge x} V_t(y, o), \qquad V_t(y, o) = G_t(y) + \alpha_{t+1}\,\mathbb{E}\,J_{t+1}(x_{t+1}, o_{t+1}), \qquad J_{T+1} \equiv 0,$$

where the expectation is over $D_t$. The base-stock level in period $t$ is the smallest minimizer

$$y_t(o) = \min\{y : V_t(y, o) = \min_x V_t(x, o)\},$$

and the myopic level is the smallest minimizer of the single-period cost,

$$y^m_t = \min\{y : G_t(y) = \min_x G_t(x)\}.$$

A function $f(x, \theta)$ has decreasing differences if $f(x_1, \theta) - f(x_2, \theta) \le f(x_1, \theta') - f(x_2, \theta')$ whenever $x_1 \ge x_2$ and $\theta \ge \theta'$ componentwise.

Formalization targets

Goal: Theorem 5 (p. 1352)

If $t \mapsto y^m_t$ is nondecreasing on $\{1, \dots, T\}$, then for every period $t$ and every observed-demand vector $o \ge 0$,

$$y_t(o) = y^m_t .$$

The optimal order-up-to level then ignores all advance information beyond the protection period. A second item states the paper's stationary special case: if $G_t = G$ for all $t$, the smallest minimizer $y^m$ of $G$ is the optimal base-stock level in every period.

Milestones: Theorem 4 (p. 1351)

For every period $t$ and every fixed $o_t$:

1. $V_t(\cdot, o_t)$ is convex and $V_t(x, o_t) \to \infty$ as $|x| \to \infty$;
2. $y_t(o_t)$ exists and $J_t(x, o_t) = V_t(\max(y_t(o_t), x), o_t)$: a state-dependent base-stock policy is optimal;
3. $J_t(\cdot, o_t)$ is nondecreasing and convex;
4. $V_t(x, o)$ has decreasing differences in $(x, o)$;
5. $J_t(x, o)$ has decreasing differences in $(x, o)$;
6. $y_t(o)$ is nondecreasing in $o$.

Parts 1–3 are what the goal's proof uses. Parts 4–6 are the paper's second zero set-up result, monotonicity of the base-stock level in observed demand.

Significance

The theorem identifies when advance demand information beyond the protection period can be ignored. When the myopic levels do not decrease over time, which includes stationary costs and ramping-up demand, the $(1 + M)$-dimensional dynamic program collapses to a sequence of one-dimensional newsvendor-type problems. That is both a computational simplification and a managerial statement: information about demand after the protection period does not change the order. Theorem 4, Part 5 gives the complementary monotone comparative statics. When the myopic condition fails, more observed demand never lowers the order-up-to level.

The results are proved in the paper, with the proofs in Appendix B. No machine-checked version exists. This mission produces a formal account of the finite-horizon recursion with a multi-dimensional information state, and checks the base-stock and myopic-optimality arguments against it.

Difficulty

The obvious induction carries convexity of $J_{t+1}$ backward, but here the future cost is evaluated at a random next state $(x_{t+1}, o_{t+1})$ whose first coordinate depends on the current observed demand $o_{t,t+L+1}$. Showing that the base-stock level does not depend on $o_t$ therefore needs more than convexity. It needs to know where $J_{t+1}(\cdot, o_{t+1})$ is flat, uniformly in the random $o_{t+1}$, and that the next position cannot exceed the current order-up-to level. The latter holds only on the reachable states, where observed demands are nonnegative. For a sufficiently negative $o_{t,t+L+1}$ the next period starts above its myopic level whatever is ordered now, and the conclusion fails. On the analytic side, every infimum and expectation in the recursion must be shown to be finite and attained before the order-theoretic argument can start.

Formalization scope

The model is parametrised by $L$ and $M \ge 1$, with $N = L + M + 1$. The demand vector is a function on $\{0, \dots, N\}$ and $o$ a function on $\{0, \dots, M-1\}$, ordered componentwise. $J_t$ is defined by backward recursion with $J_t \equiv 0$ for $t > T$. The minimum over $y \ge x$ is a real infimum and the expectation a Bochner integral against the law $\mu_t$ of $D_t$. Attainment and finiteness are consequences proved in the theorems, not assumptions. Base-stock and myopic levels are characterised as smallest minimizers (IsLeast), never through sInf.

The single-period cost $G_t$ is a primitive rather than being assembled from $c_t$, $g_t$ and the lead-time demand; the paper's $G_t$ has the assumed properties, so the theorems cover the paper's model. Hypotheses the paper uses without stating, all placed on primitives and labelled in the statements:

• nonnegative demands, $D_{t,s} \ge 0$ almost surely;
• coercivity of $G_t$ (the paper states it for $\tilde G_t$ only);
• $\alpha_{t+1} > 0$;
• finiteness of the expectation in (9), guaranteed by linear growth of $G_t$ and finite first moments of $D_t$. This covers piecewise-linear holding and backorder costs with any finite-mean demand (including the paper's Poisson example), but excludes superlinear costs;
• in the goal, $o \ge 0$, the set of reachable states.

The goal cannot be trivialised: the hypotheses are satisfied by concrete instances (for example $G_t(y) = |y|$ with any finite-mean nonnegative demand), and the conclusion identifies the base-stock level exactly rather than asserting that some minimizer exists.

Out of scope: the reduction of the control problem to the functional equation (Appendix A, Özer 2000), the infinite-horizon Theorem 6, and Lemma 5, whose proof argues on the integers and whose real-valued form with a unit forward difference is unverified. Contributions of general lemmas are welcome: convexity and attainment for $\inf_{y \ge x}$ of a convex coercive function, and preservation of convexity and decreasing differences under expectation. All of them are reusable in other inventory models.

Selected references

• G. Gallego, Ö. Özer, Integrating Replenishment Decisions with Advance Demand Information, Management Science 47(10):1344–1360, 2001. https://doi.org/10.1287/mnsc.47.10.1344.10261
• A. F. Veinott, Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539