The OR Formalization Drive

Motivation

Supervisory control theory, introduced by Ramadge and Wonham (SIAM J. Control Optim. 25(1), 1987), models a manufacturing cell, a communication protocol or a resource-sharing system as an automaton whose transitions are events, some of which an external controller may disable. A controller, the supervisor, is itself an automaton that watches the event sequence and, in each of its states, decides which controllable events are currently allowed. The framework is the standard model for logical (untimed) control of discrete event systems and is the subject of textbooks such as Cassandras and Lafortune (Springer, 2008) and Wonham and Cai (Springer, 2019).

A practical concern is supervisor size. The synthesis procedure of the paper (§9) produces a supervisor whose automaton records exactly as much of the past as the desired closed-loop language requires, but there are many other supervisors realising the same behaviour. The paper's second main result, the quotient structure theorem (Theorem 10.1, p. 223), explains how they are related: any supervisor with two natural economy properties is obtained from a canonical one, built on a recognizer of the closed-loop language, by lumping states. This is the structural starting point of the later literature on supervisor reduction.

Setting

A generator is $\mathcal G = (Q, \Sigma, \delta, q_0, Q_m)$: a state set $Q$, a finite alphabet $\Sigma$ of events, a partial transition function $\delta : \Sigma \times Q \to Q$, an initial state $q_0$ and marker states $Q_m \subseteq Q$. Extending $\delta$ to strings gives the generated language $L(\mathcal G)$ (strings along which $\delta$ is defined from $q_0$) and the marked language $L_m(\mathcal G)$ (those that end in $Q_m$). The closure $\bar K$ of a language $K$ is its set of prefixes. Throughout, $\mathcal G$ is trim: $L(\mathcal G) = \bar L_m(\mathcal G)$. A recognizer for a language $K$ is an accessible generator whose marked language is $K$.

A subset $\Sigma_c \subseteq \Sigma$ of events is controllable. A supervisor is $\mathcal S = (S, \phi)$ where $S = (X, \Sigma, \xi, x_0, X_m)$ is an accessible deterministic automaton with possibly infinite state set and $\phi : X \to \{0,1\}^{\Sigma_c}$ is a state feedback map; events outside $\Sigma_c$ are always enabled. The closed loop $\mathcal S/\mathcal G$ runs $S$ and $\mathcal G$ in lockstep and allows $\sigma$ from $(x, q)$ iff $\xi(\sigma, x)$ and $\delta(\sigma, q)$ are defined and $\phi(x)(\sigma) = 1$. Its languages are $L(\mathcal S/\mathcal G)$, $L_m(\mathcal S/\mathcal G)$ (marker set $X_m \times Q_m$) and $L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G) \cap L_m(\mathcal G)$.

$\mathcal S$ is complete if $S$ never refuses an event that the plant can execute and $\phi$ enables: $s \in L(\mathcal S/\mathcal G)$, $s\sigma \in L(\mathcal G)$ and $\phi(\xi(s, x_0))(\sigma) = 1$ imply $s\sigma \in L(\mathcal S/\mathcal G)$. It is proper if it is complete and $\bar L_m(\mathcal S/\mathcal G) = \bar L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G)$.

A projection $\pi : \mathcal S \to \hat{\mathcal S}$ is a surjection $X \to \hat X$ with $\pi(x_0) = \hat x_0$, $X_m = \pi^{-1}(\hat X_m)$, $\hat\xi(\sigma, \pi(x)) = \pi(\xi(\sigma, x))$ wherever $\xi(\sigma, x)$ is defined, and $\hat\phi \circ \pi = \phi$.

For a language $K$, strings $s, s'$ are $\bar K$-equivalent if $st \in \bar K \iff s't \in \bar K$ for all $t$. The automaton $S$ is $\bar K$-reduced if $\bar K$-equivalent strings of $\bar K$ lead to the same state, and $\bar K$-trim if every state is reached by a string of $\bar K$.

Formalization targets

Goal: Theorem 10.1 (quotient structure theorem)

Let $\mathcal S = (S, \phi)$ be complete, $K_1 := L_m(\mathcal S/\mathcal G)$, $K_3 := L(\mathcal S/\mathcal G)$, with $S$ $K_3$-reduced and $K_3$-trim, and let $\hat S^0 = (X^0, \Sigma, \xi^0, x^0_0, X^0)$ be a trim recognizer for $K_3$. Then there are $X^0_m \subseteq X^0$ and $\phi^0$ such that $\mathcal S^0 = ((X^0, \Sigma, \xi^0, x^0_0, X^0_m), \phi^0)$ satisfies

$$\mathcal S^0 \text{ complete},\quad L_m(\mathcal S^0/\mathcal G) = K_1,\quad L(\mathcal S^0/\mathcal G) = K_3,\quad \exists\, \pi : \mathcal S^0 \to \mathcal S,\quad \mathcal S \text{ proper} \Rightarrow \mathcal S^0 \text{ proper}.$$

Milestones

Proposition 8.1 (p. 219): for complete $\mathcal S$ and a projection $\pi : \mathcal S \to \hat{\mathcal S}$, (i) $\pi$ is unique; (ii) $(L_m, L_c, L)(\mathcal S/\mathcal G) = (L_m, L_c, L)(\hat{\mathcal S}/\mathcal G)$; (iii) $\hat{\mathcal S}$ is complete; (iv) nonblocking, nonrejecting and proper transfer in both directions.

The displayed steps of the proof of Theorem 10.1 (pp. 223–224): $\pi(\xi^0(s, x^0_0)) := \xi(s, x_0)$ is well defined on $X^0$; it is a projection once $X^0_m := \pi^{-1}(X_m)$ and $\phi^0 := \phi \circ \pi$; $L(\mathcal S^0/\mathcal G) = K_3$ follows from two enablement conditions; $\mathcal S^0$ is complete; and $L_m(\mathcal S^0/\mathcal G) = K_1$.

Significance

Theorem 10.1 says that the reduction properties the synthesis procedure of §9 guarantees are exactly what makes a supervisor a quotient of the canonical supervisor on a recognizer of $K_3$. Combined with Proposition 8.1, which shows that a projection preserves every closed-loop language, completeness and properness, it identifies supervisors with the same behaviour up to state lumping. This is the basis on which supervisor reduction and the comparison of supervisor realisations rest.

The result is proved in the paper. What this mission produces is a machine-checked version of the model (generators with partial transitions, supervisors with infinite state sets, the closed loop, completeness and properness) and of the two results above. No formalization of Ramadge–Wonham supervisory control was found on Prove2Me at the time of drafting; the definitions of this mission are reusable by any later mission on the theory, including the synthesis results of the first mission of the series.

Difficulty

The mathematics is elementary; the difficulty is bookkeeping with partial functions. Every step compares runs of three automata (the plant, $S$ and the recognizer) that may be undefined at different strings, and a proof must track at each string which of them is defined. The tempting shortcut of treating the projection condition as full commutation, $\hat\xi(\sigma, \pi(x)) = \pi(\xi(\sigma, x))$ for all $\sigma, x$, is not available: the page asks for it only where $\xi(\sigma, x)$ is defined, and Proposition 8.1 (ii) holds only because completeness of $\mathcal S$ compensates for transitions that $\hat\xi$ has and $\xi$ lacks. Likewise, the map $\pi$ of Theorem 10.1 is defined through arbitrary representatives, and its well-definedness uses both that $\hat S^0$ recognizes $K_3$ with all states marked and that $S$ is $K_3$-reduced.

Formalization scope

The alphabet is a Lean type α with [Fintype α] (the page's $\Sigma$, which is Lean syntax); strings are List α, $s\sigma$ is s ++ [σ]. A generator is a structure with its own state type in Type and a partial transition δ : α → Q → Option Q; its extended transition is the left fold. The feedback map has type X → Ec → Bool, and "$\sigma$ enabled at $x$" means $\sigma \notin \Sigma_c$ or $\phi(x)(\sigma) = 1$; the page's $\phi : X \to \{0,1\}^\Sigma$ is the same object under this extension. The closed loop is run from $(x_0, q_0)$ without forming its accessible part, which changes none of its languages. Existential statements over supervisors quantify over state types in Type.

Standing assumptions that are hypotheses of every theorem: $\Sigma$ finite; $\mathcal G$ trim, stated as 𝒢.L = pre 𝒢.Lm; every supervisor automaton accessible. Theorem 10.1 and its proof steps also assume $\mathcal S$ complete, $S$ $K_3$-reduced and $K_3$-trim, and a trim recognizer $R$ for $K_3$ with all states marked, and $\mathcal S^0$ is built on that given $R$ rather than on a recognizer chosen by the prover. The conclusion names $K_1$ and $K_3$ as the languages of $\mathcal S$, not as free variables. A projection predicate that drops $\pi(x_0) = \hat x_0$, surjectivity or the marker equation would make the goal's clause (ii) trivially satisfiable by a constant map; the sanity check shipped with the mission rules this out on the primitive plant of §2.3.

Contributions welcome: proofs of the milestones, lemmas relating the fold-based extended transition to concatenation, and a reusable library for closed-loop runs.

Selected references

• P. J. Ramadge and W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25(1):206–230, 1987. https://doi.org/10.1137/0325013
• C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, 2nd ed., Springer, 2008. https://doi.org/10.1007/978-0-387-68612-7
• W. M. Wonham and K. Cai, Supervisory Control of Discrete-Event Systems, Springer, 2019. https://doi.org/10.1007/978-3-319-77452-7

Motivation

Every financial application in the rest of this book — terminal wealth maximization, portfolio choice with consumption, index tracking, hedging — takes as given that the underlying market admits no risk-free profit: an arbitrage opportunity. Ruling this out is not a modeling nicety but a structural necessity, since a market with arbitrage has no sensible notion of a fair price at all. Bäuerle and Rieder's Chapter 3 fixes the discrete- and continuous-time market vocabulary the rest of the book builds on, and proves the one structural fact about no-arbitrage that the later chapters actually invoke: that the whole-horizon, global absence of arbitrage is equivalent to a much simpler one-period condition, checked separately at each stage. This reduction — not the deeper fundamental theorem of asset pricing (existence of an equivalent martingale measure), which the book does not prove in this section — is what turns a statement about strategies over the whole time horizon into something checkable stage by stage, exactly the form needed to embed a no-arbitrage assumption into a dynamic-programming argument.

Setting

An $N$-period financial market with $d$ risky assets consists of a probability space $(\Omega,\mathcal{F},\mathbb{P})$ with filtration $(\mathcal{F}_n)_{n=0}^N$, $\mathcal{F}_0$ trivial; a riskless bond with deterministic interest rate $i_n$ on $[n-1,n)$ (so $S^0_n = S^0_{n-1}(1+i_n)$); and $d$ risky assets with relative price changes $\tilde R_n = (\tilde R^1_n,\dots,\tilde R^d_n)$, $\mathcal{F}_n$-measurable and a.s. strictly positive ($S^k_n = S^k_{n-1}\tilde R^k_n$). A portfolio (trading strategy) is an $(\mathcal{F}_n)$-adapted process $\varphi = (\varphi^0_n,\varphi_n)$, $\varphi^0_n \in \mathbb{R}$, $\varphi_n \in \mathbb{R}^d$; $\varphi^k_n$ is the money invested in asset $k$ on $[n,n+1)$. Its value before/after trading at time $n$ is $X_n^- := \varphi^0_{n-1}(1+i_n) + \varphi_{n-1}\cdot\tilde R_n$, $X_n^+ := \varphi^0_n + \varphi_n\cdot e$; $\varphi$ is self-financing if $X_n^- = X_n^+$ a.s. for every interior $n$. An arbitrage opportunity is a self-financing $\varphi$ with $X_0^\varphi = 0$, $X_N^\varphi \geq 0$ a.s., $X_N^\varphi > 0$ with positive probability. The relative risk process $R_n^k := \tilde R_n^k/(1+i_n) - 1$ is the excess return of asset $k$ over the riskless rate.

Formalization targets

Goal — Theorem 3.1.5

$$\text{No arbitrage} \iff \forall\, n < N,\ \forall\, \mathcal{F}_n\text{-measurable } \varphi_n \in \mathbb{R}^d: \quad \varphi_n \cdot R_{n+1} \geq 0 \text{ a.s.} \implies \varphi_n \cdot R_{n+1} = 0 \text{ a.s.}$$

This is the weakest stable statement that captures the reduction: it asserts the equivalence of the global, whole-horizon absence of arbitrage strategies with a one-period static condition on the relative risk vector, without asserting the stronger (and here unproved) existence of a martingale measure.

No further milestone is formalized in this mission: this chapter's only other theorem, Theorem 3.3.1 (binomial-tree weak convergence to Black-Scholes), needs the Skorokhod topology on the space of càdlàg paths, absent from Mathlib and out of scope to construct here — see the Formalization scope section and HARD.md.

Significance

Theorem 3.1.5 is the tool that lets every later chapter's "assume the market has no arbitrage" hypothesis be checked and used one period at a time rather than as a global existential statement over an intractably large space of strategies. It is also the precise, minimal claim this section proves: contrasted with the full fundamental theorem of asset pricing (no arbitrage $\iff$ existence of an equivalent martingale measure, due to Harrison–Kreps 1979 and Dalang–Morton–Willinger 1990 in this discrete-time generality), Theorem 3.1.5 is a strictly weaker, purely measure-theoretic reduction that requires no separating-hyperplane or martingale-measure construction to state (only to prove). The definitions this chunk formalizes alongside it — portfolios, self-financing, arbitrage, and utility functions with the Arrow-Pratt risk-aversion coefficient — are the vocabulary every financial mission of this book (Chapters 4, 6, 9, 11) is built from.

Formalizing it contributes the exact discrete-time, filtration-indexed statement of the reduction — a result absent from the platform (searched "arbitrage", "self-financing", "martingale measure", "utility function"; the one related hit, LinearOptimization.no_arbitrage_iff_state_prices, is a static single-period linear-programming duality statement — no-arbitrage iff nonnegative state prices exist for a fixed return matrix — a different equivalence for a different, non-stochastic model, not reused here).

Difficulty

The direction "local no-free-lunch at every stage $\Rightarrow$ no arbitrage" is the easy one: an arbitrage strategy, unwound via the recursive wealth formula, forces a violation of the local condition at some stage by a stopping-time argument on the first period where the wealth increment is a.s. nonnegative and not a.s. zero. The converse, "an arbitrage opportunity forces the local condition to fail somewhere," is the direction that needs the reduction of the whole-horizon problem to a single period: the natural first attempt (induct forward from $n=0$) does not directly work, because whether a strategy is an arbitrage is a statement about the terminal wealth $X_N$, and a violation at an early stage does not obviously propagate; the book's proof instead identifies, from an arbitrage strategy, the last stage at which the one-period condition fails and constructs a genuinely one-period arbitrage there — an argument that needs care with the a.s.-qualifiers at every step (the difference between "$X \geq 0$ a.s." failing to imply "$X < 0$ with positive probability" only up to null sets is exactly where the measure-theoretic bookkeeping matters).

Formalization scope

The market is represented via DiscreteFinancialMarket, bundling the probability space, filtration, and the two primitives ($i$, $\tilde R$) actually used; price processes $S^0, S^k$ are not separately represented, since they would only be running products of these two primitives with no further role once the relative risk process $R$ is derived. Filtration is represented directly as a monotone family of sub-$\sigma$-algebras with a trivial Fam 0, not via Mathlib's Filtration structure, to avoid instance-juggling that would add no content here. Adaptedness/predictability and the a.s. conditions of every definition are exactly the book's own. Definitions 3.2.1-3.2.2 (the continuous-time portfolio and its self-financing condition, needed by chunk 09b's jump-market model) use an abstract StochasticIntegral operator taken as given data, since Mathlib has no general theory of integration against an arbitrary càdlàg semimartingale (only specific constructions such as Itô integration against Brownian motion); this is a deliberate infrastructure gap flagged for whoever eventually needs to instantiate it, not a hidden simplification of the definition's own content, which states the self-financing equation exactly as the book writes it.

Theorem 3.3.1 is not formalized in this mission and is recorded in HARD.md. The theorem asserts weak convergence of the whole path of the binomial-tree price process to the Black-Scholes-Merton stock price on the Skorokhod space $D[0,T]$ of càdlàg functions with the Skorokhod topology — a materially stronger and more setup-heavy claim than finite-dimensional convergence in distribution, and the book explicitly names this topology (it is not left implicit). Mathlib has no formalization of $D[0,T]$ or the Skorokhod topology, and building either from scratch (the space of càdlàg functions, the Skorokhod metric via time-warpings, the tightness criteria needed for Donsker-type invariance principles) is a substantial undertaking outside the scope of a single milestone; weakening the claim to convergence of finite-dimensional distributions, or silently substituting an unnamed alternative topology (e.g. uniform convergence, under which the claim would in fact be false, since the discretized paths have jumps the limit does not), would misstate the theorem rather than state a smaller piece of it faithfully. A general-purpose Skorokhod-space/Skorokhod-topology formalization in Mathlib — reusable well beyond this book — is the prerequisite contribution that would unlock this result.

No trivializing formalization: NoArbitrage quantifies over all self-financing portfolios (Portfolio M, an unrestricted adapted process, not a finite or parametrized family), and the one-period condition of part b) quantifies over all $\mathcal{F}_n$-measurable $\varphi_n \in \mathbb{R}^d$ — narrowing either quantifier (e.g. to strategies with bounded positions) would state a weaker, easier claim than the book's own theorem.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
• J. M. Harrison and D. M. Kreps, "Martingales and arbitrage in multiperiod securities markets", Journal of Economic Theory, 1979 (the discrete-time fundamental theorem of asset pricing this chapter's Theorem 3.1.5 is a structural lemma toward, not itself proved in this section).

Motivation

A multiple objective program asks to maximize $k$ objectives $f_1(x),\dots,f_k(x)$ simultaneously over a feasible set $S$. There is usually no point that is best in every objective, so the object of interest is the set of nondominated criterion vectors: those that cannot be improved in one objective without being worsened in another. Interactive procedures for multiple criteria decision making work by computing nondominated vectors one at a time, by solving a single-objective scalarization, and presenting them to a decision maker.

A scalarization is useful for this purpose only if it is complete (every nondominated vector is the solution of some instance of it) and sound (every solution is nondominated). The weighted-sum scalarization is sound for positive weights but not complete when the feasible region is nonconvex. R. E. Steuer and E.-U. Choo (Math. Programming 26 (1983) 326–344) built their interactive procedure on weighted Tchebycheff distances to an ideal point, following Bowman (1976) and Choo and Atkins (1983). In §3 they treat finite feasible regions with an augmented metric, which requires choosing a small parameter $\rho>0$. In §4 (pp. 334–336) they show that a lexicographic version of the weighted Tchebycheff program is complete and sound for any feasible region, including nonconvex continuous ones, with no parameter to estimate. This mission formalizes that result, Theorems 4.5 and 4.6.

Setting

Let $Z\subseteq\mathbb R^k$, $k\ge1$, be the set of feasible criterion vectors (the image of $S$ under $f=(f_1,\dots,f_k)$). A vector $z$ dominates $\bar z$ if $z_i\ge\bar z_i$ for all $i$ and $z_i>\bar z_i$ for at least one $i$. The nondominated set $N\subseteq Z$ consists of the $\bar z\in Z$ dominated by no $z\in Z$.

An ideal criterion vector is a $z^*\in\mathbb R^k$ with

$$z^*_i=\max\{z_i\mid z\in Z\}+\varepsilon_i,$$

where $\varepsilon_i\ge0$, and $\varepsilon_i>0$ is required whenever (i) more than one nondominated vector maximizes objective $i$, or (ii) the only nondominated vector maximizing objective $i$ also maximizes another objective. So $z^*$ may touch $Z$ in coordinate $i$ only in a controlled way.

The weight set is the simplex $\bar\Lambda=\{\lambda\in\mathbb R^k\mid\lambda_i\ge0,\ \sum_i\lambda_i=1\}$. For $\lambda\in\bar\Lambda$ the weighted Tchebycheff program minimizes $\alpha$ subject to $\alpha\ge\lambda_i(z^*_i-z_i)$ for all $i$ and $z\in Z$; its value at a fixed $z$ is

$$t_\lambda(z)=\max_{1\le i\le k}\lambda_i(z^*_i-z_i).$$

The lexicographic weighted Tchebycheff program first minimizes $t_\lambda$ over $Z$ and then, among the first-stage minimizers, minimizes $e^{\mathsf T}(z^*-z)=\sum_i(z^*_i-z_i)$. The paper writes it as $\min\{P_1\alpha+P_2e^{\mathsf T}(z^*-z)\}$ with pre-emptive priority factors. Finally, for $\bar z\in\mathbb R^k$ the weights $\bar\lambda$ of eq. (4.3) are $\bar\lambda_i\propto1/(z^*_i-\bar z_i)$, normalized to sum to one, when $\bar z_j\ne z^*_j$ for all $j$. When some $\bar z_j=z^*_j$, $\bar\lambda_i$ is $1$ on the coordinates with $\bar z_i=z^*_i$ and $0$ elsewhere.

Formalization targets

Goal: Theorem 4.6 (p. 336)

For compact $Z$, an ideal vector $z^*$ and $\bar z\in Z$,

$$\bar z\in N\iff\exists\,\lambda\in\bar\Lambda\ \text{such that}\ \bar z\ \text{minimizes the lexicographic weighted Tchebycheff program with weights }\lambda .$$

Milestones

1. Proof of Theorem 4.5 (pp. 335–336). For $\bar z\in N$, $\bar\lambda$ as in (4.3) and $\hat\alpha$ the minimal first-stage value,

$$\bar z\in\Phi(\hat\alpha),\qquad N\cap\Phi(\hat\alpha)=\{\bar z\},\qquad \Phi(\hat\alpha)=\{z\mid z_i\ge z^*_i-\hat\alpha/\bar\lambda_i\ \text{when}\ \bar\lambda_i>0\}.$$

2. Theorem 4.5 (p. 335). For $\bar z\in N$: $\bar\lambda\in\bar\Lambda$, and $\bar z$ is the unique minimizer of the lexicographic program with weights $\bar\lambda$.
3. Remark after Theorem 4.6 (p. 336). For every $\lambda\in\bar\Lambda$ the lexicographic program has a minimizer when $Z$ is compact and nonempty, and every minimizer is nondominated.

The goal is the characterization; Theorem 4.5 is the stronger half with uniqueness and an explicit weight.

Significance

Theorem 4.6 says that, as $\lambda$ ranges over the simplex, the lexicographic weighted Tchebycheff program returns exactly the nondominated set, for any feasible region: no convexity, no finiteness, no polyhedral structure. Theorem 4.5 adds that each nondominated vector is the unique output for a weight vector computable from the vector itself, which is what an interactive procedure needs to sample $N$ reliably. The price, as the paper notes, is two optimization stages instead of one; the gain is that no augmentation parameter $\rho$ must be estimated. The result is a standard entry in the textbook treatment of Tchebycheff scalarizations (Steuer, Multiple Criteria Optimization, 1986; Ehrgott, Multicriteria Optimization, 2005).

The result is proved on paper. To our knowledge no machine-checked version exists in Lean or Mathlib, which has no material on Tchebycheff scalarization of multiple objective programs. The formal statements below also pin down two points the printed text leaves loose: the direction of the priority factors, and a closedness assumption that the proof uses without stating it.

Difficulty

The ⇐ direction and the soundness remark are short: a dominating vector is at least as good in the first stage and strictly better in the second. The work is in Theorem 4.5. The obvious argument is that $\bar z$ is the unique minimizer of the first stage with weights $\bar\lambda$; the paper says so. That is true when $\bar z<z^*$ in every coordinate, but false when $\bar z_j=z^*_j$ for some $j$: then $\bar\lambda=e_j$, and every $z\in Z$ with $z_j=z^*_j$ ties with $\bar z$, dominated vectors included. For example, with $Z=\{(5,3),(5,1),(1,10)\}$ and $z^*=(5,10)$, the vectors $(5,3)$ and $(5,1)$ tie. Only the second stage separates them. Showing that it always selects $\bar z$ requires every tied vector to lie below a nondominated vector attaining $z^*_j$, which by the ideal-vector rule must be $\bar z$. That existence step fails for sets that are not closed.

Formalization scope

Criterion vectors are Fin k → ℝ with [NeZero k] ($k\ge1$); objectives are indexed from $0$. $S$, the objectives $f_i$ and the program's variable $\alpha$ are eliminated: $Z$ is a Set (Fin k → ℝ) and the first-stage value is $t_\lambda(z)$ above (the paper's metric uses $|z^*_i-z_i|$, which agrees with $z^*_i-z_i$ on $Z$). $\bar\Lambda$ is Mathlib's stdSimplex ℝ (Fin k). "Minimizes" is global minimization over $Z$; "uniquely minimizes" means every lexicographic minimizer equals $\bar z$ as a criterion vector.

Conventions and added hypotheses:

• The lexicographic program is encoded as the two-stage minimization IsLexMin. The printed "$P_1<<<P_2$" read literally gives the second stage priority; the paper's text on p. 336 and the goal-programming convention it cites give $\alpha$ priority. The two-stage reading is encoded, and the program is not replaced by a weighted sum $P_1\alpha+P_2e^{\mathsf T}(z^*-z)$ with fixed numbers, which would be the augmented program of §3.
• $Z$ compact is an added hypothesis in Theorem 4.5, in the goal, and in the existence half of milestone 3. The paper assumes only that $S$ is bounded, and its "max" in the ideal vector presupposes attainment. Without closedness the weight (4.3) can fail: for $Z=\{(5,3,0),(0,10,0),(0,0,6)\}\cup\{(5,0,4+t):0\le t<1\}$, $z^*=(5,10,6)$ and $\bar z=(5,3,0)\in N$, the program with $\bar\lambda=(1,0,0)$ has no lexicographic minimizer. Closedness is needed by the theorem itself, not only by this proof: adding the points $(5-s^2,\,3+s,\,0)$, $0<s\le1$, to that $Z$ (still bounded, $\varepsilon=0$ still admissible) leaves $\bar z=(5,3,0)\in N$ a lexicographic minimizer for no $\lambda\in\bar\Lambda$, so Theorems 4.5 and 4.6 are false for a bounded, non-closed $Z$. The ⇐ direction, soundness and milestone 1 hold without compactness and are stated without it.
• The ideal vector keeps the paper's $\varepsilon$-rule exactly. Replacing it with a strictly dominating $z^*$ ($\varepsilon>0$ in every coordinate) would remove the case $\bar z_j=z^*_j$ and weaken both theorems; such a formalization does not count.
• In (4.3) and in $\Phi$, division occurs only where the denominator is nonzero. That $\bar\lambda\in\bar\Lambda$ for $\bar z\in N$ is part of Theorem 4.5's conclusion, not an assumption.
• The paper's sentence "the associated weighted Tchebycheff program has a unique solution" (p. 336) is not formalized, since it fails in the tie described above.

Infrastructure needed: dominance and nondominated sets, the ideal vector, the weighted Tchebycheff value, the weights (4.3), and the lexicographic minimizer, all provided as definitions. Proofs will need existence of minimizers of continuous functions on compact sets and a maximal-element argument in the product order on a compact set. Both are reusable for other multiobjective results. Proofs of any item, and faithful statements of Corollaries 4.1 and 4.4 (polyhedral $S$), are welcome.

Selected references

• R. E. Steuer and E.-U. Choo, An interactive weighted Tchebycheff procedure for multiple objective programming, Mathematical Programming 26 (1983) 326–344. https://doi.org/10.1007/BF02591870
• V. J. Bowman, On the relationship of the Tchebycheff norm and the efficient frontier of multiple-criteria objectives, in: Multiple Criteria Decision Making (Jouy-en-Josas 1975), Lecture Notes in Economics and Mathematical Systems 130, Springer, 1976, 76–86. https://doi.org/10.1007/978-3-642-87563-2_5
• E.-U. Choo and D. R. Atkins, Proper efficiency in nonconvex multicriteria programming, Mathematics of Operations Research 8 (1983) 467–470. https://doi.org/10.1287/moor.8.3.467
• A. M. Geoffrion, Proper efficiency and the theory of vector maximization, Journal of Mathematical Analysis and Applications 22 (1968) 618–630. https://doi.org/10.1016/0022-247X(68)90201-1
• M. Ehrgott, Multicriteria Optimization, 2nd ed., Springer, 2005. https://doi.org/10.1007/3-540-27659-9

Motivation

For a convex function on $\mathbb R^n$, a point is a global minimizer as soon as it is a local minimizer — this is one of the earliest and most consequential facts of convex analysis, and it underlies why local-search and gradient methods can certify global optimality in convex programs. The discrete analogue is not automatic: a function on the integer lattice $\mathbb Z^n$ can be "locally optimal" with respect to any fixed finite neighborhood system and still fail to be a global minimizer, unless the function's discrete structure is compatible with that neighborhood in the right way. Identifying exactly which classes of lattice functions admit a local-to-global optimality principle, and with respect to which neighborhood, is one of the organizing questions of discrete convex analysis.

Integrally convex functions, introduced by Favati and Tardella (1990) and developed systematically by Murota, are the most general class of $\mathbb Z^n$-valued functions for which such a principle holds. They are defined purely in terms of the classical convex closure of a real relaxation, which lets one import theorems from ordinary convex analysis, but the resulting notion of local optimality — checking only the $3^n - 1$ neighbors obtained by independently nudging each coordinate by $-1$, $0$, or $+1$ (excluding the trivial no-change case) — is a genuinely discrete, dimension-independent statement about functions whose domain can be arbitrarily large. Almost every discrete convex function class studied later in the book, including M-convex and L-convex functions, is a special case of integral convexity, and this mission's goal theorem is the direct ancestor of the optimality criteria (Theorems 6.26 and 7.14) that drive the algorithms in the rest of the book.

Setting

Let $f : \mathbb Z^n \to \mathbb R \cup \{+\infty\}$ be a function with nonempty effective domain $\operatorname{dom}_{\mathbb Z} f = \{x \in \mathbb Z^n : f(x) \ne +\infty\}$. The convex closure of $f$ is

$$\bar f(x) = \sup_{p \in \mathbb R^n,\, \alpha \in \mathbb R} \{\langle p,x\rangle + \alpha : \langle p,y\rangle + \alpha \le f(y)\ \forall y \in \mathbb Z^n\} \qquad (x \in \mathbb R^n),$$

the pointwise supremum of every affine function minorizing $f$ on all of $\mathbb Z^n$. If $\bar f$ agrees with $f$ on integer points, $f$ is convex extensible. The integral neighborhood of $x \in \mathbb R^n$ is

$$N(x) = \{y \in \mathbb Z^n : \lfloor x_i \rfloor \le y_i \le \lceil x_i \rceil,\ 1 \le i \le n\},$$

and the local convex extension $\tilde f$ relaxes $\bar f$'s definition by requiring the affine minorant condition only on $N(x)$ rather than on all of $\mathbb Z^n$. Always $\tilde f \ge \bar f$ pointwise, and the two agree on $\mathbb Z^n$. A function $f$ is integrally convex if $\tilde f = \bar f$ everywhere on $\mathbb R^n$ — equivalently, if $\tilde f$ is a convex function on all of $\mathbb R^n$ (it is automatically convex on every unit cube $[z, z+1]^n$ with $z \in \mathbb Z^n$, but need not be convex globally without this extra condition).

A discrete set $S \subseteq \mathbb Z^n$ is hole free if $S$ equals the set of integer points in its own real convex hull, and $\arg\min f[-p]$ denotes the minimizer set, over $\mathbb Z^n$, of the linearly perturbed function $f[-p](x) = f(x) - \langle p,x\rangle$.

Formalization targets

Goal: Theorem 3.21 (local optimality characterizes global optimality)

For integrally convex $f$ and $x \in \operatorname{dom}_{\mathbb Z} f$:

$$f(x) \le f(y)\ (\forall y \in \mathbb Z^n) \iff f(x) \le f(x + \chi_Y - \chi_Z)\ (\forall\, Y, Z \subseteq \{1,\dots,n\}),$$

where $\chi_Y \in \{0,1\}^n$ is the indicator vector of $Y$. The right-hand side is a check over at most $3^n - 1$ points (each coordinate independently unchanged, incremented, or decremented), regardless of how large $\operatorname{dom}_{\mathbb Z} f$ is; this uniform, dimension-only bound is the entire content of the theorem, and is the weakest correct formulation — restricting to a single $(Y,Z)$ or letting the right-hand side range over all of $\mathbb Z^n$ would trivialize or falsify the equivalence.

Milestones: Propositions 3.18 and 3.19

Proposition 3.18: $f$ convex extensible $\implies$ $\arg\min f[-p]$ hole free for every $p$ (and conversely, when $\operatorname{dom}_{\mathbb Z} f$ is bounded). Proposition 3.19: $f$ is integrally convex if and only if every restriction $f_{[a,b]}$ to a finite integer interval is integrally convex — integral convexity is detectable by looking at bounded pieces of $f$ one at a time.

Significance

The result itself. Theorem 3.21 is what makes integrally convex functions tractable: without it, verifying global optimality on an infinite or exponentially large integer domain would require checking every point. The theorem reduces this to a check whose size depends only on the dimension $n$, not on the size of the domain, and it does so for the widest class of lattice functions for which such a reduction is possible — the class is defined precisely so that this property holds and no wider natural class enjoys it. Every specialized local-optimality theorem later in the book (for M-convex, M$^\natural$-convex, L-convex, and L$^\natural$-convex functions) restricts this same neighborhood-checking principle to a class where the local check can be made even smaller (a single-element exchange rather than a full sign pattern) precisely because those classes are integrally convex plus more.

Formalizing it. No matching item exists on the platform: a direct search for "integrally convex" returns no results, and the theorem's own proof leans on results (Theorem 1.1's local-to-global principle for ordinary convex functions on $\mathbb R^n$, and an LP-duality-based alternate formula for $\tilde f$) that are either classical convex analysis or belong to a different chapter of this same book. The remaining work is therefore to give a complete, correct account of the definitional chain — convex closure, local convex extension, integral convexity — in a form a solver can build a proof from directly, and to state the finite local-check equivalence itself exactly at the strength the book proves it, not a plausible-looking weakening of it.

Difficulty

The natural first attempt is to try to prove the "$\Leftarrow$" direction of Theorem 3.21 by a direct induction on the $\ell^1$-distance to a global minimizer, moving one coordinate at a time. This fails in general lattice functions (a function that is only "coordinatewise convex" can have strict local minima that are not global), and the theorem's actual proof instead routes through the real relaxation: it shows the neighborhood-check hypothesis forces $x$ to be a local minimizer of the local convex extension $\tilde f$ restricted to the unit ball around $x$, then invokes ordinary convex analysis (local minimality implies global minimality for a convex function on $\mathbb R^n$) to conclude $x$ globally minimizes $\bar f$, and finally uses integral convexity ($\tilde f = \bar f$) to transfer this back to $f$ on $\mathbb Z^n$. The identification of $f$'s local behavior with $\tilde f$'s convexity on a single unit cube — rather than any coordinatewise or separable argument — is the step that makes the class of integrally convex functions exactly the right one for this theorem, and is where a naive combinatorial argument breaks down.

Formalization scope

The ground set is $\mathbb Z^n$, represented as Fin n → ℤ; $f$'s codomain is WithTop ℝ (exactly $\mathbb R \cup \{+\infty\}$), while the convex closure $\bar f$ and local convex extension $\tilde f$ take values in EReal (exactly $\mathbb R \cup \{\pm\infty\}$, a complete lattice, so their defining suprema are total functions with no side conditions). A trivializing formalization of the goal would quantify the right-hand side over a single fixed $(Y,Z)$ pair, or over all of $\mathbb Z^n$ instead of the sign-pattern neighbors; both are excluded by keeping $Y, Z$ universally quantified Finset (Fin n) ranging over the full $3^n$ sign-pattern space (minus the trivial case, which the equivalence still holds through vacuously).

Checked against the platform (GET /theorems?q=integrally convex, 0 hits) and against Mathlib's Analysis/Convex/ for the classical facts this chapter's proof would eventually need (ordinary convex-function local-to-global optimality, LP duality): these are broadly available in Mathlib's convex-analysis library in some form, but none of them is imported here, since none appears in the statement of any item this mission drafts — they belong to a proof this pass does not attempt. Contributions to a shared DiscreteConvex.IntegralConvexity definitions layer are welcome from chunks 06–09, which specialize integral convexity to M-convex and L-convex functions and will need the same convex-closure/local-extension vocabulary.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• P. Favati, F. Tardella, "Convexity in nonlinear integer programming," Ricerca Operativa, 53, 1990, pp. 3–44.

Motivation

The augmented Lagrangian method (method of multipliers) of Hestenes, Powell and Rockafellar solves a constrained nonlinear program by repeatedly minimizing an unconstrained merit function in the primal variables and then updating the multipliers. For inequality constraints, the augmented Lagrangian in the form the paper takes from Rockafellar (Rockafellar 1981) is continuously differentiable but not twice differentiable, even when all problem data are smooth: its Hessian jumps across the surfaces where a constraint switches between the "active" and "inactive" formula. Newton's method for the inner minimization therefore has no classical Hessian to work with on those surfaces.

Qi and Sun (Math. Programming 58, 1993) extended Newton's method to equations $F(x) = 0$ with $F$ locally Lipschitz, replacing the Jacobian by an element of Clarke's generalized Jacobian, and proved local superlinear convergence when $F$ is semismooth. Section 4 of the paper, an example suggested by Rockafellar, shows that the gradient of the augmented Lagrangian of a $C^2$ program is semismooth, so the nonsmooth Newton method applies to the stationarity equation $\nabla L_r = 0$. This mission formalizes that result, Theorem 4.1.

Setting

Let $f_0, f_1, \dots, f_m : \mathbb{R}^n \to \mathbb{R}$ be of class $C^2$ and consider

$$\text{(NLP)}\quad \min f_0(x)\ \text{ s.t. }\ f_i(x) = 0,\ i = 1,\dots,p,\qquad f_i(x) \le 0,\ i = p+1,\dots,m. \tag{4.1}$$

Fix $r > 0$. For a constraint value $a$ and a multiplier $y$ put

$$\phi(r, a, y) = \begin{cases} y a + \tfrac12 r a^2, & y + r a \ge 0,\\ -\tfrac{1}{2r} y^2, & y + r a \le 0,\end{cases}$$

(the two cases agree when $y + ra = 0$). The augmented Lagrangian is the function of $(x, y) \in \mathbb{R}^n \times \mathbb{R}^m$

$$L_r(x, y) = f_0(x) + \sum_{i=1}^{p}\Big(y_i f_i(x) + \tfrac12 r f_i(x)^2\Big) + \sum_{i=p+1}^{m} \phi\big(r, f_i(x), y_i\big).$$

For a locally Lipschitz map $F$ between finite-dimensional spaces, let $D_F$ be the set where $F$ is differentiable. Clarke's generalized Jacobian is $\partial F(x) = \mathrm{co}\{\lim JF(x_i) : x_i \to x,\ x_i \in D_F\}$. $F$ is semismooth at $x$ if it is locally Lipschitz near $x$ and, for every direction $h$, the limit of $V h'$ over $V \in \partial F(x + t h')$, $h' \to h$, $t \downarrow 0$, exists.

For a single constraint function $g$ the proof works with $\eta(x, s) = \phi(r, g(x), s)$ on $\mathbb{R}^n \times \mathbb{R}$, and with the surface $s + r g(x) = 0$ on which the two formulas for $\phi$ meet.

Formalization targets

Goal: Theorem 4.1

For $r > 0$ and $f_0, \dots, f_m \in C^2$:

$$L_r \in C^1, \qquad \nabla L_r \text{ semismooth at } (x,y) \text{ whenever } \exists\, i > p:\ y_i + r f_i(x) = 0,$$ $$\nabla L_r \in C^1 \text{ near } (x, y) \text{ whenever } y_i + r f_i(x) \neq 0 \text{ for all } i > p.$$

All three clauses are the theorem; the last two together cover every point.

Milestones

1. $\eta \in C^1$, with $\nabla\eta(x,s) = \big((s + r g(x))\nabla g(x),\ g(x)\big)$ if $s + r g(x) \ge 0$ and $(0, -s/r)$ if $s + r g(x) \le 0$, and $\nabla \eta$ is locally Lipschitz.
2. Eq. (4.2): the Hessian of $\eta$ on each side of the surface, and $\nabla\eta \in C^1$ near every point off it.
3. Eq. (4.7): if $\bar s + r g(\bar x) = 0$ and $\bar s + t_j\alpha_j + r g(\bar x + t_j h_j) = 0$ with $h_j \to h$, $\alpha_j \to \alpha$, $t_j \downarrow 0$, then $\alpha + r\nabla g(\bar x)^{\mathsf T} h = 0$.
4. $\nabla\eta$ is semismooth, jointly in $(x, s)$, at every point of the surface.

Significance

The result places the inner problem of the augmented Lagrangian method inside the scope of the paper's convergence theory: with $F = \nabla L_r$, the generalized-Jacobian Newton iteration converges locally superlinearly at a root where every element of $\partial F$ is nonsingular. Its practical content is that second-order methods can be run on $L_r$ even though $L_r$ is only $C^{1}$, with the elements of $\partial \nabla L_r$ playing the role of Hessians. The same pattern (a $C^1$ merit function with semismooth gradient) recurs in extended linear-quadratic programming and in semismooth Newton methods for complementarity problems.

The theorem is proved in the paper by direct computation. As far as a search of the platform showed, none of the objects involved (Clarke's generalized Jacobian, semismoothness, Rockafellar's augmented Lagrangian) has a published formalization there, and Mathlib has none of them. The mission produces a machine-checked version of the computation and, as a by-product, reusable statements about $C^1$ functions obtained by gluing two $C^2$ pieces along a hypersurface.

Difficulty

Clauses 1 and 3 are calculus with a case split: one has to check that the two formulas for $\phi$ and for its gradient match on the surface. Clause 2 is where the argument is not routine. On the surface, $\nabla\eta$ is not differentiable, and the generalized Jacobian $\partial\nabla\eta$ there contains convex combinations of the two one-sided Hessians of (4.2). Semismoothness asks that $V(h', \alpha')$ have a single limit over all such $V$, for all approaches $(h', \alpha') \to (h, \alpha)$, $t \downarrow 0$, including approaches that cross the surface infinitely often. The two one-sided Hessians are different matrices, so no single derivative describes $\nabla\eta$ near the surface, and the existence of the limit must be shown for approaches that alternate between the two sides and for the convex combinations that $\partial\nabla\eta$ contains on the surface itself. General theorems that piecewise-smooth maps are semismooth appear in later literature but are not available in Mathlib, so they cannot be invoked as a shortcut. A second obstacle is infrastructure: Mathlib has no generalized Jacobian, so every fact about $\partial\nabla\eta$ (which limits of derivatives occur near the surface) must be derived from the definition.

Formalization scope

• $\mathbb{R}^n$ and $\mathbb{R}^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); $L_r$ is a function on their product, and $\eta$ on EuclideanSpace ℝ (Fin n) × ℝ.
• The constraint index $i \in \{1,\dots,m\}$ is i : Fin m with paper index i.val + 1; equality constraints are i.val < p, inequality constraints p ≤ i.val. The paper's implicit $p \le m$ is not assumed (for $p > m$ there are no inequality constraints).
• The paper's first sum prints $h(r_i, f_i(x), y_i)$; the single $r$ is used, as in the paper's definition of $h$.
• $\phi$ uses the first branch when $y + ra \ge 0$; the branches agree on the boundary. Every statement assumes $r > 0$.
• $C^2$ is ContDiff ℝ 2 on all of $\mathbb{R}^n$; "smooth" is the paper's continuously differentiable, ContDiffAt ℝ 1 of the gradient at the point.
• $\nabla L_r$ and $\nabla\eta$ are Fréchet derivatives, valued in continuous linear functionals; semismoothness is invariant under the Riesz isometry to gradient vectors and under equivalent norms on the domain (Mathlib's product has the sup norm).
• The Jacobian in Clarke's definition is fderiv, limits are along sequences, and no closure is taken in the convex hull. Semismoothness is the explicit $\varepsilon$–$\delta$ form of the paper's limit, uniform over $V \in \partial F(x + th')$.
• Hessians in (4.2) are stated as the Fréchet derivative of the gradient map applied to a direction.

A formalization that states only $L_r \in C^1$, or only the semismoothness of one term $\eta$, is not Theorem 4.1; the goal contains all three clauses for the full $L_r$. The combination step from the terms $\eta$ to $L_r$ uses that sums of semismooth maps and $C^1$ maps with locally Lipschitz derivative are semismooth; the paper cites this without proof, and a solver will need to prove it.

Contributions welcome: the lemmas above; general facts about clarkeJac (it contains fderiv at points of strict differentiability; it is a singleton for $C^1$ maps; behaviour under sums and linear maps); and the semismoothness of sums.

Selected references

• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
• R. T. Rockafellar, Proximal subgradients, marginal values, and augmented Lagrangians in nonconvex optimization, Mathematics of Operations Research 6 (1981) 427–437. https://doi.org/10.1287/moor.6.3.427
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983 (reprinted SIAM Classics in Applied Mathematics 5, 1990). https://doi.org/10.1137/1.9781611971309
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15 (1977) 959–972. https://doi.org/10.1137/0315061

Motivation

A firm that sells several products must decide, before demand is known, how much production capacity to build and of what kind. Dedicated capacity makes one product; flexible capacity makes any of them. The classic argument for flexibility is demand pooling: capacity that can follow demand to whichever product needs it wastes less than capacity locked to one product (Fine and Freund 1990; Van Mieghem 1998).

When capacity itself is unreliable, as with a supplier that may fail to deliver, a plant that may be disrupted, or a batch that may be rejected, flexibility has a second face. A single flexible resource concentrates the firm's supply in one place, so one failure removes all of it, whereas several dedicated resources rarely fail together. This resource-aggregation effect works against flexibility. Tomlin and Wang (2005) set up a newsvendor network in which both effects are present and ask when a firm should pay more for flexible capacity than for dedicated capacity. Their first answer (Proposition 1) is that a risk-neutral firm facing equal reliabilities and costs never loses by choosing flexibility, whatever the joint distribution of demand. This mission formalizes that answer.

Setting

There are $N$ products with a common unit contribution margin $p>0$. The demand vector $\tilde X=(\tilde X_1,\dots,\tilde X_N)$ is random, nonnegative and integrable; its total is $\tilde X_{N+1}=\tilde X_1+\dots+\tilde X_N$.

Two networks are compared. In the dedicated network SD, resource $n\in\{1,\dots,N\}$ makes only product $n$ and has marginal total cost $c>0$. In the flexible network SF, a single resource, labelled $N+1$, makes every product and has marginal total cost $c_{N+1}$.

Every resource $j$ is unreliable with a Bernoulli yield $\tilde Y_j\in\{0,1\}$, $\mathbb P(\tilde Y_j=1)=\theta$. The common reliability is $\theta\in[0,1]$, the yields are mutually independent, and they are independent of demand. Investing $K_j\ge 0$ in resource $j$ delivers capacity $\tilde Y_jK_j$ and costs $(\lambda+(1-\lambda)\tilde Y_j)c_jK_j$: the firm pays the committed cost $\lambda c_j$ per unit ordered and a further $(1-\lambda)c_j$ per unit delivered, with $\lambda\in[0,1]$.

The realized profits are

$$W^{SD}(K)=\sum_{n=1}^N\Big(-(\lambda+(1-\lambda)\tilde Y_n)cK_n+p\min\{\tilde X_n,\tilde Y_nK_n\}\Big),$$ $$W^{SF}(K_{N+1})=-(\lambda+(1-\lambda)\tilde Y_{N+1})c_{N+1}K_{N+1}+p\min\{\tilde X_{N+1},\tilde Y_{N+1}K_{N+1}\},$$

and a risk-neutral firm maximizes the expected profit $V^{SD}_{RN}(K)=\mathbb E[W^{SD}(K)]$ or $V^{SF}_{RN}(K_{N+1})=\mathbb E[W^{SF}(K_{N+1})]$ over nonnegative investments. Let $V^{SD,*}$ and $V^{SF,*}$ be the optimal values. SF is (weakly) preferred if $V^{SF,*}\ge V^{SD,*}$.

The indifference cost $c^I_{N+1}$ is a value of $c_{N+1}$ at which $V^{SF,*}=V^{SD,*}$, and the flexibility premium is $\Delta=(c^I_{N+1}-c)/c$. The firm prefers SF as long as $c_{N+1}\le(1+\Delta)c$.

The $\alpha$-expected shortfall of a random variable $Z$ is, for $\alpha\in(0,1)$ and the lower quantile $x_{(\alpha)}=\inf\{x:\mathbb P(Z\le x)\ge\alpha\}$,

$$ES_\alpha(Z)=-\frac1\alpha\Big(\mathbb E\big[Z\mathbf 1\{Z\le x_{(\alpha)}\}\big]+x_{(\alpha)}\big(\alpha-\mathbb P(Z\le x_{(\alpha)})\big)\Big).$$

Formalization targets

Goal: Proposition 1

For any demand random vector $\tilde X$:

1. $\Delta_{RN}\ge 0$ for all $0\le\theta\le 1$, that is, SF is preferred whenever $c_{N+1}\le c$;

$$0\le\theta\le\frac{\lambda c}{p-(1-\lambda)c}\ \Longrightarrow\ \Delta_{RN}=0;$$

3. $\Delta_{RN}=0$ if $\rho_X=\mathbf 1$, i.e. all pairwise demand correlations equal $1$.

No distributional form of demand is fixed and no constant is hard-coded beyond the paper's threshold.

Milestones

• (9): the closed form of $V^{SF}_{RN}$.
• (10)–(11), (12)–(13): the optimal investments are critical fractiles

$$F_{X_{N+1}}(K^*_{N+1})=1-\frac{(\lambda+(1-\lambda)\theta)c_{N+1}}{\theta p},\qquad F_{X_n}(K^*_n)=1-\frac{(\lambda+(1-\lambda)\theta)c}{\theta p},$$

and the optimal values are $\theta p$ times partial expectations of demand.

• (A-1) in expected-shortfall form: with $\alpha=1-(\lambda+(1-\lambda)\theta)c/(\theta p)\in(0,1)$,

$$V^{SF,*}\ge V^{SD,*}\ \text{at}\ c_{N+1}=c\iff \alpha\Big(\sum_n ES_\alpha(\tilde X_n)-ES_\alpha\Big(\sum_n\tilde X_n\Big)\Big)\ge 0 .$$

• Subadditivity of $ES_\alpha$ (Acerbi and Tasche 2002).
• The positivity threshold of part 2: investing is worthwhile iff $\theta>\lambda c/(p-(1-\lambda)c)$.
• Correlation $1$ implies $\tilde X_n=a\tilde X_1+b$ with $a>0$, and $ES_\alpha(aX+b)=aES_\alpha(X)-b$.

Significance

Proposition 1 separates the two effects of flexibility under unreliable supply. It shows that for a risk-neutral firm the demand-pooling benefit together with an upside effect of aggregation (one flexible resource succeeds more often than all dedicated ones together) always outweighs the downside aggregation risk. Even with no pooling benefit at all (perfectly correlated demand) the firm is indifferent, not averse. The later results of the paper (loss aversion, CVaR, dual sourcing) are measured against this baseline: a negative premium can appear only once the firm is risk-averse. The expected-shortfall form links newsvendor optimal values to a coherent risk measure, a connection that recurs in inventory risk analysis.

The result is proved in the paper, with a proof that cites Acerbi and Tasche (2002) for two properties of expected shortfall. No machine-checked version exists. A formalization adds three things: a proof for general demand distributions (the paper assumes a joint density and uses the continuous form of expected shortfall); a Lean development of Acerbi–Tasche expected shortfall for general integrable random variables, including subadditivity and affine equivariance; and a reusable model of newsvendor networks with Bernoulli yields and committed costs.

Difficulty

The newsvendor steps (9)–(13) are single-variable concave optimization, but they must be done without a density: the distribution function of total demand may have atoms and flat pieces, so the critical fractile need not be attained or may be attained on an interval, and optimal values must be expressed through lower quantiles. Subadditivity of expected shortfall is the heart of part 1 and is not elementary in the general (atomic) case, which is exactly why the correction term $x_{(\alpha)}(\alpha-\mathbb P(Z\le x_{(\alpha)}))$ appears. Part 3 requires identifying correlation $1$ with almost-sure positive affine dependence, which rests on the equality case of the Cauchy–Schwarz inequality in $L^2$, and then handling nonnegativity constraints on the investments that the affine change of variables may violate. The obvious shortcut of computing everything from densities is not available, because the goal is stated for every demand vector and part 3 is incompatible with a joint density when $N\ge 2$.

Formalization scope

Randomness lives on one probability space $(\Omega,\mu)$; demand is X : Ω → Fin N → ℝ and yields are Y : Ω → Fin (N + 1) → ℝ, where dedicated resource $n$ is Fin.castSucc n and the flexible resource $N+1$ is Fin.last N. Expectations are Bochner integrals and probabilities are μ.real. The standing assumptions are: $p>0$, $c>0$, $\lambda,\theta\in[0,1]$; demands measurable, almost surely nonnegative and integrable (integrability is needed for expected shortfall and makes every profit integrable); yields measurable, $\{0,1\}$-valued almost surely with $\mathbb P(\tilde Y_j=1)=\theta$, mutually independent, and independent of demand (the paper states the last in Appendix E). The paper's joint density of demand is deliberately not assumed.

The premium $\Delta$ and the indifference cost are not defined as real numbers, because Definition 1's indifference cost need not exist or be unique (for $\theta$ below the threshold both optimal values are $0$ for every $c_{N+1}$ near $c$). "$\Delta\ge 0$" is encoded as "SF is weakly preferred for every $c_{N+1}\le c$", and "$\Delta=0$" as "SF and SD are each weakly preferred to the other at $c_{N+1}=c$". Weak preference $V^{SF,*}\ge V^{SD,*}$ is stated as: every nonnegative SD investment is matched by some nonnegative SF investment; no real supremum is taken. Quantiles $F^{-1}$ in (10) and (12) appear only as parameters with the hypothesis $F(K^*)=$ fractile. Part 3 adds square integrability and positive variances, the conditions under which correlation coefficients exist; the threshold milestone adds almost surely positive demand and $N\ge 1$ for its "if" direction. When $p\le(1-\lambda)c$ the Lean value of the threshold is $\le 0$, so part 2 then covers only $\theta=0$, where it is true.

A formalization that assumed a joint density, took $\Delta$ as a free real satisfying Definition 1, or defined optimal values as real suprema over all of $\mathbb R^N$ would make parts of the goal vacuous or trivial; each is ruled out above.

Needed infrastructure: single-variable newsvendor optimality for general distributions; the Acerbi–Tasche expected shortfall with subadditivity and affine equivariance; the equality case of Cauchy–Schwarz for correlation. The expected-shortfall and correlation lemmas are reusable well beyond this mission, and contributions of them are especially welcome. Out of scope: the loss-averse and CVaR analyses (Propositions 2–3, §3.2–3.3), the perfect-reliability result (Proposition 4, a separate mission), the dual-sourcing networks (§4) and all numerical results.

Selected references

• B. Tomlin and Y. Wang, On the value of mix flexibility and dual sourcing in unreliable newsvendor networks, Manufacturing & Service Operations Management 7(1):37–57, 2005. https://doi.org/10.1287/msom.1040.0063
• C. Acerbi and D. Tasche, On the coherence of expected shortfall, Journal of Banking & Finance 26(7):1487–1503, 2002. https://doi.org/10.1016/S0378-4266(02)00283-2
• C. H. Fine and R. M. Freund, Optimal investment in product-flexible manufacturing capacity, Management Science 36(4):449–466, 1990. https://doi.org/10.1287/mnsc.36.4.449
• J. A. Van Mieghem, Investment strategies for flexible resources, Management Science 44(8):1071–1078, 1998. https://doi.org/10.1287/mnsc.44.8.1071

Motivation

The traveling salesman problem (TSP) asks for a shortest closed route through a finite set of points. It is NP-hard, and in practice tours are built by fast constructive heuristics whose output is then improved or used as is. A central question in the analysis of algorithms, raised in this form by Rosenkrantz, Stearns and Lewis in 1977, is how far such a heuristic can be from optimal in the worst case, as a function of the number of points $n$, when the distances satisfy the triangle inequality.

The paper (SIAM J. Comput. 6(3), 1977) answers this for several heuristics. For the general class of insertion methods it proves a logarithmic bound (Theorem 3); for two specific rules, nearest insertion and cheapest insertion, it proves a bound that does not grow with $n$: the tour is less than twice the optimal (Theorem 4), and more precisely at most $2(1-1/n)$ times the optimal (Corollary, eq. (4.12)). Theorem 5 of the same paper shows the constant $2(1-1/n)$ is attained, so this is the exact worst case of both rules. These results, with Christofides' 3/2 bound of 1976, are the classical reference points for approximation ratios of TSP construction heuristics and appear in standard OR and approximation-algorithm texts.

Setting

A traveling salesman graph $(N,d)$ has a finite node set $N$ with $|N| = n$ and a distance $d : N\times N\to\mathbb R$ that is symmetric, nonnegative and satisfies the triangle inequality $d(i,k)\le d(i,j)+d(j,k)$. A tour is a circuit visiting every node exactly once; its length is the sum of its edge lengths, and OPTIMAL is the least tour length.

A subtour $T$ is a tour on a subset of $N$ (a one-node subtour has no edges). For $k\notin T$, $\mathrm{TOUR}(T,k)$ inserts $k$ into $T$ where it is cheapest: if $T$ has at least two nodes, choose an edge $(x,y)$ of $T$ minimizing $d(x,k)+d(k,y)-d(x,y)$ and replace it by $(x,k),(k,y)$; if $T=\{i\}$, form the two-node tour on $i,k$. $\mathrm{COST}(T,k)$ is the length of $\mathrm{TOUR}(T,k)$ minus the length of $T$.

An insertion method builds subtours $T_1,\dots,T_n$ with $T_1=\{a_0\}$ and $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$ for some $a_i\notin T_i$, $1\le i<n$; INSERT is the length of $T_n$. With $d(T,p)=\min_{x\in T}d(x,p)$:

• nearest insertion chooses each $a_i$ with $d(T_i,a_i)=\min\{d(T_i,x): x\in N-T_i\}$;
• cheapest insertion chooses each $a_i$ with $\mathrm{COST}(T_i,a_i)=\min\{\mathrm{COST}(T_i,x): x\in N-T_i\}$.

The start node $a_0$ and every tie (between candidate nodes, and between candidate edges) are arbitrary. TREE denotes the length of a minimal spanning tree of $(N,d)$.

Formalization targets

Goal: Corollary to Theorem 4, eq. (4.12)

For every traveling salesman graph on $n\ge1$ nodes and every run of nearest insertion or of cheapest insertion,

$$\mathrm{INSERT}\;\le\;2\Bigl(1-\frac1n\Bigr)\cdot\mathrm{OPTIMAL}.$$

Milestones

1. Lemma 2, (3.3): $\mathrm{COST}(T,k)\le 2\,d(k,j)$ for $k\notin T$, $j\in T$.
2. Eq. (3.7): for every insertion method, $\mathrm{INSERT}=\sum_{i=1}^{n-1}\mathrm{COST}(T_i,a_i)$.
3. Eqs. (4.9)–(4.10): nearest insertion satisfies $\mathrm{COST}(T_i,a_i)\le 2\,d(p,q)$ for all $p\in T_i$, $q\notin T_i$ (4.5).
4. Proof of Theorem 4: cheapest insertion satisfies (4.5) as well.
5. Lemma 3: every insertion run satisfying (4.5) has $\mathrm{INSERT}\le 2\cdot\mathrm{TREE}$ (4.6).
6. Eq. (4.11): $\mathrm{TREE}\le(1-1/n)\cdot\mathrm{OPTIMAL}$.

Theorem 4 itself, $\mathrm{INSERT}<2\cdot\mathrm{OPTIMAL}$ when $d$ is not identically zero, is included as a companion statement.

Significance

The bound says that two simple $O(n^2)$ and $O(n^2\log n)$ construction rules are never worse than a factor $2(1-1/n)$ from optimal on any metric instance, a guarantee independent of $n$, in contrast with nearest neighbor and with arbitrary insertion orders, whose ratios the same paper shows can grow logarithmically. Lemma 3 is reusable on its own: any insertion rule satisfying the local inequality (4.5) inherits the bound $2\cdot\mathrm{TREE}$, and the paper notes that similar arguments apply to nearest addition and nearest merger.

The result has been proved since 1977. The Prove2Me library has a machine-checked proof of the weaker statement for nearest insertion only with constant $2$ (SupplyChainTheory.nearest_insertion_bound, from Snyder–Shen, Theorem 10.7) and of $\mathrm{TREE}\le\mathrm{OPTIMAL}$ (SupplyChainTheory.mst_lower_bound). This mission asks for the paper's full statement: both rules, the exact constant $2(1-1/n)$, and the general Lemma 3 via its correspondence between insertion steps and spanning-tree edges. Paired with the tightness result of the companion mission (Theorem 5), it would give a formally verified exact worst-case ratio for both heuristics.

Difficulty

Lemma 2 and inequality (4.5) are local consequences of the triangle inequality; the difficulty is global. The obvious attempt at Lemma 3 charges step $i$ to the tree edge joining $a_i$ to its nearest node of $T_i$, but distinct steps can then be charged to the same tree edge, and the sum of the charges no longer bounds $2\cdot\mathrm{TREE}$. Any correct argument must control how the insertion order interacts with the structure of an arbitrary spanning tree, which in Lean means reasoning about paths in SimpleGraph together with the evolving subtours. For cheapest insertion the chosen node need not be a nearest node, so (4.5) is not immediate from the rule. Finally, the goal's constant $2(1-1/n)$ is sharper than the bound $2\cdot\mathrm{OPTIMAL}$ obtained from $\mathrm{TREE}\le\mathrm{OPTIMAL}$, so the weaker spanning-tree bound already in the library does not suffice.

Formalization scope

Nodes are Fin n with $n\ge1$ (the paper's nodes $1,\dots,n$ shifted to $0,\dots,n-1$). The distance satisfies the paper's three axioms plus the normalization $d(i,i)=0$, which never affects a tour, subtour or tree length. Tours are permutations; OPTIMAL is a minimum over all of them (Finset.inf'). Subtours are lists of distinct nodes with closed length. $\mathrm{TOUR}(T,k)$ is encoded as insertion of $k$ at a list position whose resulting length is minimal over all $|T|+1$ positions, which is the minimization of (3.1) over the edges of $T$; COST is the corresponding minimum increase. The subtour index is 1-based as printed ($T_1=\{a_0\}$, $T_n$ final). The distance $d(T,p)$ is taken in $\mathbb R\cup\{+\infty\}$, so no default value enters the nearest rule. Spanning trees are SimpleGraph (Fin n) with IsTree; statements about TREE are phrased over every spanning tree (upper bounds) or some spanning tree (bounds on TREE), which is equivalent. Ratios are multiplied out, so the goal needs no nontriviality hypothesis; Theorem 4's strict form carries the paper's exclusion of the identically zero distance (p. 564).

A formalization in which TOUR inserts at an arbitrary rather than a cheapest position, or in which the run fixes the start node or the tie-breaking, would state a different (and, for arbitrary positions, false) theorem; the statements here quantify over every run.

A complete development needs subtour-length lemmas for List.insertIdx, the telescoping identity (3.7), and a spanning-tree edge-assignment argument on Mathlib's SimpleGraph paths; the last two are reusable for other insertion rules and for the companion missions of this series. Proofs of any milestone are welcome independently.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM Journal on Computing 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• N. Christofides, Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, Report 388, GSIA, Carnegie Mellon University, 1976. https://doi.org/10.1007/s43069-021-00101-z (reprint in Operations Research Forum 3, 2022)
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 10 (Theorem 10.7). https://doi.org/10.1002/9781119584445