Optimization

Motivation

Von Neumann's minimax theorem (Chapter VIII) settles two-player zero-sum games with scalar payoffs. In 1956, Blackwell asked the natural generalization: what can a player guarantee in a repeated game with vector-valued payoffs, where "winning" means driving the average payoff into a target set rather than above a target value? For decades the resulting theory — approachability — and the regret-minimization theory this book develops were believed to be different, with approachability seen as the stronger notion. Chapter 13 closes that gap: approachability and online convex optimization are shown to be algorithmically equivalent, each reducible to the other with no loss of efficiency, and along the way this equivalence yields a constructive, rate-quantified proof of Blackwell's own theorem.

Setting

A generalized vector game (Definition 13.2) is given by bounded convex closed decision sets $K_1,K_2$ and a vector payoff $u:K_1\times K_2\to\mathbb R^d$. A set $S$ is approachable (Definition 13.3) if some non-anticipating algorithm, playing in $K_1$ against any sequence $y_1,y_2,\dots\in K_2$, drives the average payoff's distance to $S$ to zero. Blackwell's theorem (13.4) characterizes exactly which $S$ are approachable via a purely geometric condition: every column-player strategy $y$ admits a row-player best response $x$ landing the payoff in $S$.

Section 13.2 constructs an explicit approachability algorithm from any OCO algorithm: given a best-response oracle realizing Blackwell's condition, Algorithm 37 runs the OCO algorithm on the proxy losses $f_t(w) = w^\top u_{t-1} - h_S(w)$ (the support function $h_S(w)=\max_{x\in S}\{w^\top x\}$ letting distance-to-$S$ be written, via Lemma 13.5's minimax duality, as a convex optimization problem over the unit ball), queries the oracle at the OCO algorithm's play $w_t$, and averages the resulting rewards.

Formalization targets

Theorem 13.7 (OCO-to-approachability rate, milestone)

Theorem 13.4 — the mission's goal (sufficiency direction only)

Significance

This chapter's headline claim — approachability and OCO are equivalent — is proved in two directions in the book (§13.2 and §13.3); this mission drafts the direction the book itself foregrounds as "the more interesting implication" and constructively proves: any sublinear-regret OCO algorithm converts directly into an explicit approachability algorithm with an explicit convergence rate, giving a self-contained, algorithmic proof of a 1956 game-theory theorem using 1990s–2000s online-learning machinery. Historically, this equivalence resolved a standing misconception (approachability believed strictly stronger) and reframes Blackwell's theorem as a special case of regret minimization rather than a separate theory requiring its own toolkit. No prior art was found on the platform for Blackwell approachability (planning search: q=Blackwell — the one hit, PRNGCompression.prng_no_free_lunch's cousin, an unrelated Rao-Blackwellization result, is not a substitute); this mission drafts both items fresh.

Difficulty

Theorem 13.4's statement is a clean geometric implication, but the book is explicit that its proof is entirely carried by Theorem 13.7 plus an unstated "explicit conclusion" left as an exercise (the passage from a finite-horizon rate bound to the asymptotic Dist → 0 claim, using any of the book's own sublinear-regret OCO algorithms as a witness). Theorem 13.7's own proof combines three nontrivial facts: Lemma 13.5's minimax-duality rewriting of $\mathrm{Dist}(\cdot, S)$ as a linear optimization over the unit ball (itself proved via Sion's minimax theorem, not excerpted here), the best-response oracle's defining inequality (13.2) applied pointwise at each round's $w_t$, and the OCO algorithm's own regret guarantee applied to the specific proxy-loss sequence $f_t$ built from the realized game trajectory — a genuine composition of three separate pieces of machinery from earlier in the book (Chapters III–VIII), not a routine substitution.

Formalization scope

IsApproachable is declared as its own definition (per BRIEF.md's explicit instruction, since Theorem 13.4 depends on it), with the non-anticipation clause made explicit (matching the series' IsOnlineAlgorithm convention from Chunk 03) even though the book's own Definition 13.3 states it only informally ("x_t ← A(y_1,\dots,y_{t-1})"). SupportFunction is h_S exactly as displayed, as a real supremum (a genuine maximum given the chapter's standing "closed, bounded" hypothesis on S). $\mathrm{Dist}(\cdot,S)$ throughout is Euclidean distance, rendered as Mathlib's Metric.infDist — confirmed the chapter uses no other distance notion (checked §13.1-13.3 directly, per the pitfall BRIEF.md flags). Theorem 13.7 transcribes Algorithm 37's $f_t(w)=w^\top u_{t-1}-h_S(w)$ construction faithfully, including its one-round offset (using the previous round's realized reward to build the current round's proxy loss, while the conclusion averages the current round's rewards) — exactly as the book's own pseudocode has it, not smoothed over.

Scope decision on Theorem 13.4's biconditional. The book states Theorem 13.4 as an ↔ but proves, and explicitly flags as proved, only the sufficiency direction (←): "The necessity of this condition is left as an exercise... Our reductions henceforth give an explicit proof of Blackwell's theorem [meaning: of the sufficiency direction]." Per CAPTAIN_BRIEF.md rule 6 and BRIEF.md's explicit instruction, this mission drafts only that direction, named as such in the goal item's own docstring; see STATUS.md.

Not formalized (out of scope for this mission, given the remaining budget and the explicit "exercise" status of several results on these pages): the necessity direction of Theorem 13.4; Lemma 13.5 (minimax duality for Dist, itself relying on Sion's theorem, not separately formalized here); Lemma 13.6 (the equivalent best-response-oracle condition); §13.3's entire approachability-to-OCO direction (Theorem 13.9, Lemma 13.8, the cone/polar-cone machinery of §13.3.1) and §13.3.3 (existence of a best-response oracle for the constructed set); the "explicit conclusion" of Blackwell's theorem from Theorem 13.7, left as an exercise by the book itself.

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 13.
• D. Blackwell, "An analog of the minimax theorem for vector payoffs," Pacific Journal of Mathematics 6(1), 1956, 1-8.
• N. Abernethy, P. Bartlett, E. Hazan, "Blackwell approachability and no-regret learning are equivalent," COLT 2011.

Motivation

Online convex optimization (OCO) asks a learner to repeatedly pick a point in a convex set $K$, pay a cost that an adversary reveals only after the choice is made, and be judged against the best fixed point in hindsight. Chapter III of this series formalized the simplest general-purpose answer, online gradient descent (OGD): take a gradient step, project back onto $K$. OGD's analysis, however, is tied to the Euclidean geometry of the projection step — it treats every coordinate of $K$ alike, and its regret bound degrades badly when $K$'s natural geometry is not Euclidean (the probability simplex under the $\ell_1$ norm is the standard example, where a Euclidean-projection algorithm's regret scales with $\sqrt{n}$ in the dimension $n$, while an algorithm that exploits the simplex's own geometry attains regret scaling only with $\sqrt{\log n}$).

Regularized Follow the Leader (RFTL) is the meta-algorithm this chapter introduces to fix this: rather than fixing a specific geometry, RFTL is parameterized by an arbitrary regularization function $R$, and its regret bound depends on $R$ only through two scalar quantities the mission makes explicit — the range of $R$ over $K$, and a $R$-dependent "local norm" of the gradients. Choosing $R$ to match $K$'s geometry (entropy regularization on the simplex, for instance) recovers the sharp bounds that plain OGD cannot. RFTL and its close relative Online Mirror Descent (OMD), also introduced here, are the ancestors of essentially every regularization-based online learning algorithm in use today, including the multiplicative-weights/Hedge algorithm of Chapter I as a special case (entropy regularization on the simplex) and the exponentiated-gradient algorithm this book's own Chapter VIII reuses (Corollary 5.7, a further specialization of Theorem 5.2 this mission's Theorem 5.2 underlies). The naive "Follow the Leader" strategy this chapter opens by refuting — always play the empirically best point so far — is a natural first idea and provably fails: the book gives an explicit two-point cost sequence on which it incurs regret linear in the horizon. Regularization is the fix, and quantifying exactly how much it costs and buys is this chapter's content.

Setting

Fix a convex, nonempty decision set $K$ in a real inner product space $E$ and a sequence of convex cost functions $f_1, f_2, \dots : K \to \mathbb{R}$. As in Chapter III, regret after $T$ rounds is

A regularization function $R : K \to \mathbb{R}$ is a strongly convex, smooth, twice differentiable function with a positive-definite Hessian on the interior of $K$. Its Bregman divergence measures the gap between $R$ and its own first-order Taylor approximation:

By the mean value theorem, $B_R(x\|y) = \tfrac12\|x-y\|_z^2$ for some point $z$ on the segment $[x,y]$, where $\|\cdot\|_z$ is the norm induced by the Hessian $\nabla^2 R(z)$; its dual norm, denoted $\|\cdot\|_z^*$, is the local norm at $z$. Writing $\|\cdot\|_t$ for the local norm between consecutive iterates $x_t, x_{t+1}$, the $R$-diameter of $K$ is $D_R^2 = \max_{x,y\in K}(R(x)-R(y))$.

The RFTL algorithm (Algorithm 13), with step size $\eta > 0$, plays $x_1 = \arg\min_{x\in K} R(x)$, then at every round updates

The agile Online Mirror Descent algorithm (Algorithm 14, agile version) instead maintains a dual point $y_t$ with $\nabla R(y_1) = 0$, updates it by $\nabla R(y_{t+1}) = \nabla R(x_t) - \eta \nabla_t$, and projects via the Bregman divergence, $x_{t+1} = \arg\min_{x\in K} B_R(x\|y_{t+1})$ (with $x_1$ defined the same way from $y_1$). RFTL and the lazy variant of OMD coincide for linear costs (Lemma 5.5, not formalized here — it is not used by either target); the agile variant's analysis is genuinely different and is the mission's second target.

Formalization targets

Target (Theorem 5.2 — RFTL's regret bound)

This is the mission's goal: RFTL, run with any admissible regularizer, attains a regret bound governed only by the cumulative squared local norm of the gradients and $R$'s range over $K$. The bound is proved via two milestones: Lemma 5.3 (regret controlled by the total "prediction drift" $\sum_t \nabla_t^\top(x_t - x_{t+1})$ plus $D_R^2/\eta$), which in turn rests on Lemma 5.4 (a "follow-the-leader beats be-the-leader" comparison inequality, proved by induction on the horizon).

Further target (Theorem 5.6 — agile OMD's regret bound)

A structurally similar bound for the agile variant, included as its own goal-level item since — as the book states explicitly — its proof technique is unrelated to RFTL's, not a corollary of it.

Both targets are the book's own tightest, non-asymptotic statements: neither is weakened to an $O(\cdot)$ form, and the book's own further (unnumbered) corollary specializing Theorem 5.2 to a uniform local-norm bound $\|\nabla_t\|_t^* \le G_R$ is left out, matching this series' convention of formalizing only the numbered results.

Significance

The results themselves. Theorem 5.2 is the general regret theorem behind every regularization scheme in online learning: instantiating $R$ recovers the projected-gradient bound of Chapter III (Euclidean $R$), the multiplicative-weights bound of Chapter I (entropy $R$ on the simplex), and — through the exponentiated-gradient specialization (Corollary 5.7, not itself a target here) — the row-player regret bound this book's own Chapter VIII cites as "Eq. (8.1)" in its reduction of zero-sum games to regret minimization. Theorem 5.6 gives the same guarantee for an algorithm (agile OMD) that, unlike RFTL, maintains a feasible point at every round, which the book notes is preferable in the adaptive-regret setting of Chapter X.

Formalizing it. Both theorems have complete, elementary proofs in the source (no gaps, no "with high probability", no hidden regularity conditions); the mission's work is converting the analytic argument — the Bregman-divergence identity, the generalized Cauchy-Schwarz inequality bounding the drift term by the local norm, and the two induction arguments underlying Lemma 5.4 — into machine-checked statements. No formalization of RFTL, OMD, or the local-norm machinery exists on the platform (checked below); the closest Formalpedia entries state a related but distinctly narrower result.

Difficulty

The central obstacle is that the regularizer $R$ is a hypothesis, not a fixed function: the theorem must hold for every admissible $R$ simultaneously, so nothing about $R$ beyond its stated properties (strong convexity, smoothness, twice differentiability) may be used. A newcomer's first instinct — bound the local norm $\|\nabla_t\|_t^*$ by a fixed multiple of the Euclidean dual norm $\|\nabla_t\|_2$ — fails in general and is exactly the bound RFTL is designed to avoid needing; the whole point of the local-norm formulation is that it can be tight for regularizers (like entropy) whose Hessian is very far from a multiple of the identity. A second obstacle is Lemma 5.4's induction, which compares $x_{t+1}$ (a minimizer over $t+1$ terms) against $u$ using the minimality of $x_{t+1}$ at exactly the right instantiation — an argument that looks almost circular until the induction hypothesis is applied at $u = x_{t+2}$, not at the theorem's free variable.

Formalization scope

$K$ ranges over an arbitrary real, complete inner product space (a real Hilbert space), matching Chapters III and IV, not a fixed $\mathbb{R}^n$. The RFTL and agile-OMD update rules are represented relationally (IsArgMinOn), since Mathlib has no canonical argmin operator for a general convex set — mirroring IsMetricProjection's precedent from Chapter III. The Hessian at the mean-value-theorem's intermediate point is represented via the second Fréchet derivative of $R$'s gradient map (HasFDerivAt), since Mathlib has no dedicated Hessian type; the local dual norm is then any value satisfying the resulting existential characterization (IsLocalDualNormSq), stated once and shared by both targets. A boundedness hypothesis on $R$ over $K$ is added to Lemma 5.3's statement to keep the $R$-diameter $D_R^2$ from collapsing to Mathlib's junk value for an unbounded supremum — a condition every regularizer the book actually uses (strongly convex and smooth over a bounded $K$) already satisfies, so it narrows nothing.

Trivializing formalization ruled out. A regret bound stated for an "algorithm" defined loosely enough to include the after-the-fact optimal choice would be vacuous; IsRFTLRun and IsOMDAgileRun instead pin down the exact history-dependent update rule of Algorithms 13 and 14 (the current gradient sequence, the current regularizer, and nothing else) as a hypothesis, so a proof must genuinely use the specific update. Theorem 5.2 and Theorem 5.6 are kept as two separate items rather than one theorem parameterized by an algorithm choice, since — per the chapter's own remark that their analyses are unrelated — a merged statement would either need to branch internally on the algorithm or silently identify two genuinely different update rules.

Reuse and prior art. OnlineConvexOpt.FirstOrder.RegretT (Chapter III, published) is imported and reused verbatim, keeping the regret functional identical across the whole book. Definitions specific to Chapter IV (OnlineConvexOpt.SecondOrder, not yet published) are not imported per this series' convention that a draft cannot import another draft; quadForm is redeclared locally instead. On the platform, BanditAlgorithm.ftrl_regret_bound, BanditAlgorithm.mirror_descent_regret_bound, and BanditAlgorithm.ftrl_simplex_exp_weights_regret (the Bandit Algorithms series, Chapter XII) state regret bounds for FTRL and Mirror Descent in the linear-cost, bandit-idiom setting (a fixed linear loss $\langle a, y_t\rangle$ at each round, regret compared via a Bregman-divergence potential at fixed points). Hazan's Theorem 5.2 and 5.6 are for general convex $f_t$ and use the book's own local-norm object, which has no counterpart in those statements; they are read in full and are not faithful substitutes (different hypothesis class), so this mission drafts its own, independent items rather than reusing them.

Selected references

• Hazan, Introduction to Online Convex Optimization, 2nd ed., Chapter 5. arXiv:1909.05207v3
• Shalev-Shwartz, Online Learning and Online Convex Optimization, Foundations and Trends in Machine Learning, 2012 (surveys RFTL/Mirror Descent under the name "Online Mirror Descent"). https://doi.org/10.1561/2200000018
• Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003 (the Euclidean special case this chapter generalizes). https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf

Motivation

Online convex optimization measures a decision maker against the best fixed decision in hindsight, and the standard guarantee — achieved, for instance, by online gradient descent — is regret growing like $O(\sqrt T)$ over $T$ rounds. This rate is unimprovable for general convex losses: an adversary can always force $\Omega(\sqrt T)$ regret against any algorithm. But many losses that arise in practice are not merely convex — they carry extra curvature that a first-order method cannot exploit. The paradigm case is online portfolio selection: a trader repeatedly rebalances wealth across $n$ assets, observes the market's return vector, and is scored by the logarithm of her wealth growth. Thomas Cover's 1991 universal portfolio theory showed that a decision maker with vanishing average regret against this log-wealth objective grows her wealth, asymptotically, at the same rate as the best fixed (constantly rebalanced) portfolio in hindsight — without any statistical assumption on how the market behaves, in sharp contrast to the Geometric Brownian Motion model of mainstream finance (Cover, Universal Portfolios, Mathematical Finance 1991). Cover's own algorithm, and the class of losses his analysis needs, turned out to generalize far beyond portfolio selection: the same curvature condition governs online square-loss regression (Azoury–Warmuth 2001) and other exp-concave learning problems. This chapter isolates that condition — exp-concavity — and shows it buys a logarithmic-in-$T$ regret bound via a second-order algorithm, online Newton step, introduced by Hazan, Agarwal and Kale (Logarithmic Regret Algorithms for Online Convex Optimization, Machine Learning 2007), building on the polynomial-time randomization of Cover's algorithm due to Kalai and Vempala (Efficient Algorithms for Universal Portfolios, Journal of Machine Learning Research 2003) and on the multiplicative-weights algorithm EWOO, which Hazan, Kalai, Kale and Agarwal extended to general exp-concave losses (2006).

Setting

Fix a real inner-product space $E$ (in the goal theorem, $E = \mathbb{R}^n$) and a convex, bounded decision set $K \subseteq E$. As in Chapters I and III, an online convex optimization protocol runs for $T$ rounds: at round $t$ the player picks $x_t \in K$, an adversary reveals a convex cost $f_t : E \to \mathbb{R}$, the player incurs $f_t(x_t)$, and regret is

exactly Eq. (1.2) of Chapter I (OnlineConvexOpt.FirstOrder.RegretT, reused unchanged here). The costs are assumed $G$-gradient-bounded ($\|\nabla f_t(x)\| \le G$ on $K$) and $K$ has diameter $D$ ($\mathrm{dist}(x,y) \le D$ for $x,y \in K$), the same standing hypotheses as Chapters II–III.

A convex $f : E \to \mathbb{R}$ is $\alpha$-exp-concave over $K$ (Definition 4.1) if $g(x) = e^{-\alpha f(x)}$ is concave on $K$. This is strictly weaker than $\alpha$-strong convexity (Chapter III), yet Lemma 4.2 shows it is exactly a directional strong-convexity condition: a twice-differentiable $f$ is $\alpha$-exp-concave at $x$ iff its Hessian dominates $\alpha \nabla f(x)\nabla f(x)^\top$ — strong curvature only along the gradient direction, not in every direction, which is what lets loss functions like $-\log(r^\top x)$ (rank-one Hessian, far from strongly convex) qualify. Lemma 4.3 turns this into the quadratic lower bound the whole chapter runs on: for $\gamma \le \tfrac12\min\{1/(GD), \alpha\}$ and $x, y \in K$,

Two algorithms are formalized. The Exponentially Weighted Online Optimizer (Algorithm 11, EWOO) plays the $w_t$-weighted centroid of $K$, $x_t = \bigl(\int_K w_t\bigr)^{-1}\int_K x\, w_t(x)\,dx$ with $w_t(x) = e^{-\alpha\sum_{\tau<t} f_\tau(x)}$; it needs no Lipschitz or diameter bound but is only quasi-polynomial-time in general. Online Newton step (Algorithm 12, ONS) instead maintains a running second-moment matrix $A_t = A_{t-1} + \nabla_t\nabla_t^\top$ ($A_0 = \varepsilon I$) and moves by $y_{t+1} = x_t - \gamma^{-1}A_t^{-1}\nabla_t$, projecting back onto $K$ in the norm $\|\cdot\|_{A_t}$ induced by $A_t$ rather than the Euclidean norm. The formalization represents $A_t$ not as a matrix but as an operator $E \to_L E$, with $A_t = A_{t-1} + \nabla_t\nabla_t^\top$ rendered as Mathlib's rank-one operator InnerProductSpace.rankOne ℝ ∇_t ∇_t, $A_t^{-1}$ as ContinuousLinearMap.inverse, and the generalized projection as minimizing $\langle y - x, A_t(y-x)\rangle$ over $K$ (quadForm/IsGeneralizedProjection in Def_..._OnlineNewtonStep).

Formalization targets

Goal — Theorem 4.5

This is the chapter's capstone: logarithmic regret in $T$, at the price of a factor of the ambient dimension $n$ — a genuine trade-off against the dimension-free $O(\sqrt T)$ of Chapter III, stated as such rather than hidden inside an $O(\cdot)$.

Comparator — Theorem 4.4

Also logarithmic and, unlike Theorem 4.5, independent of $G$ and $D$ — the price is EWOO's running time, not its regret, so this is not a weaker version of the same target but an incomparable algorithm formalized for contrast.

Significance

Exp-concavity is the precise dividing line between $\Theta(\sqrt T)$-regret losses and losses that admit $O(\log T)$ regret via a tractable algorithm — narrower than convexity, broader than strong convexity, and satisfied by the log-loss of universal portfolio selection, the square loss of online regression, and (Chapter IX onward) losses arising from PAC learning reductions. The dimension dependence in Theorem 4.5 is not an artifact of a loose proof: it is inherent to the second-moment-matrix approach and is the reason later work (self-concordant barriers, sketching) is needed to remove it in special cases. Both regret bounds have long been proved on paper; formalizing them contributes machine-checked statements of the exp-concavity characterization, the quadratic lower bound it yields, and both algorithms' regret guarantees — none of which currently exist on the platform in any form (a search for "exp-concave", "online Newton step", "second-order online" and "universal portfolio" returned no hits).

Difficulty

The natural first idea for bounding $\mathrm{Regret}_T(\mathrm{ONS})$ is to bound each round's progress the way online gradient descent's analysis does: a generalized-Pythagorean argument (Lemma 4.6) reduces the regret to $\bigl(\tfrac1\alpha + GD\bigr)\bigl(\sum_t \nabla_t^\top A_t^{-1}\nabla_t + 1\bigr)$ — this much follows the OGD template with the Euclidean norm replaced by the $A_t$-norm. The obstruction is bounding $\sum_t \nabla_t^\top A_t^{-1}\nabla_t$ itself: term-by-term it need not be summable, since $\nabla_t^\top A_t^{-1}\nabla_t$ does not shrink with $t$ on its own. The book's proof instead recognizes $\nabla_t^\top A_t^{-1}\nabla_t = A_t^{-1}\bullet(A_t - A_{t-1})$ as a discrete log-determinant increment and telescopes it against $\log|A_T|/|A_0|$, using a matrix generalization of the scalar inequality $a^{-1}(a-b) \le \log(a/b)$. This determinant argument (the book's Lemma 4.7) is not itself formalized as a milestone here — see Formalization scope — so a solver of Theorem 4.5 must reconstruct or restate it.

Formalization scope

$K$, $D$, $G$ and $\alpha$ are the chapter's standing hypotheses, stated explicitly on every theorem rather than left as ambient unused variables, exactly as in Chapters II–III; $\gamma$ and $\varepsilon$ are pinned to the theorem's own formulas via explicit hypotheses (hγ, hε) rather than left as free existentials — Rule 7 of the captain brief. The running matrix $A_t$ is formalized as a continuous linear operator on $E$, not as a Matrix (Fin n) (Fin n) ℝ: the rank-one update uses InnerProductSpace.rankOne, and $A_t^{-1}$ uses ContinuousLinearMap.inverse, which is total (it returns the zero map when $A_t$ is not invertible, a convention that never bites here since every $A_t$ is positive definite by construction — $A_0 = \varepsilon I \succ 0$ and each update only adds a positive semidefinite rank-one term, so .inverse always agrees with the genuine inverse). IsOnlineNewtonStep and IsGeneralizedProjection are dimension-free, stated for a general real inner-product space; only the goal theorem and Theorem 4.4 fix $E = \mathbb{R}^n$, since only their bounds mention the dimension $n$ explicitly. RegretT is imported unchanged from OnlineConvexOpt.FirstOrder.Protocol (kind: reference), keeping the regret notation identical across the whole book series. A trivializing formalization is ruled out by requiring $0 < \alpha$, $0 < G$, $0 < D$ and $K$ nonempty throughout: dropping any of these would let $\gamma$, $\varepsilon$, or the bound itself degenerate (e.g. $\gamma \le 0$ would make the projection's norm ill-behaved), producing a statement that is vacuously true rather than the book's actual claim. Lemma 4.7 (the log-determinant inequality) and the exercises are not formalized: the former is a general fact about positive definite operators disconnected from the OCO-specific definitions this mission introduces, and the latter are pedagogical, not numbered results the chapter's own proofs depend on. Reusable beyond this mission: the exp-concavity definitions (IsExpConcaveOn, IsExpConcaveAt) for any later chapter's exp-concave losses (the series plan flags Chapters V and X), and the generalized-projection machinery for any future second-order OCO algorithm.

Selected references

• T. M. Cover, Universal Portfolios, Mathematical Finance 1(1), 1991. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
• E. Hazan, A. Agarwal, S. Kale, Logarithmic Regret Algorithms for Online Convex Optimization, Machine Learning 69(2–3), 2007. https://doi.org/10.1007/s10994-007-5016-8
• A. Kalai, S. Vempala, Efficient Algorithms for Universal Portfolios, Journal of Machine Learning Research 3, 2003. https://www.jmlr.org/papers/v3/kalai02a.html
• K. Azoury, M. Warmuth, Relative Loss Bounds for On-Line Density Estimation with the Exponential Family of Distributions, Machine Learning 43, 2001. https://doi.org/10.1023/A:1010896012157
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 4. https://arxiv.org/abs/1909.05207

Motivation

A multistage stochastic program's exact deterministic equivalent grows exponentially with the number of periods, even when each period's random data takes only a handful of values (Chapter 9's concern was the growth in the number of realizations; Chapter 10 adds growth in the number of periods). One remedy, generalizing Chapter 8's single-period Jensen bound, is to replace the exact per-period random data by a coarser, aggregated version — conditional expectations over a partition of the history space at each stage — and solve the resulting smaller deterministic equivalent instead. This is only useful if the aggregated problem's optimal value is provably a bound (here, a lower bound) on the exact problem's, and Birge & Louveaux's Chapter 10, §10.1, Theorem 1 is exactly the statement that makes this legitimate, together with a genuinely necessary extra condition the book states explicitly two paragraphs before the theorem: "if not [i.e. if the extra condition fails], then the conditional expectation form ... may not actually achieve a bound." This mission formalizes that theorem.

Setting

The book's exact multistage stochastic linear program (Eq. 1.1, p. 418) is

min c¹x¹ + E_Ω[c²x² + ⋯ + cᴴxᴴ]
s.t. W¹x¹ = h¹,  Tᵗ⁻¹xᵗ⁻¹ + Wᵗxᵗ = hᵗ (t=2,…,H, a.s.),  xᵗ ≥ 0 a.s., xᵗ nonanticipative (Σᵗ-measurable),

over the exact event space Ω = Ω₁ × ⋯ × Ω_H. Given a consistent nested partition of each Ωᵗ = Ω₁ × ⋯ × Ωₜ into finitely many blocks Sᵗ₁, …, Sᵗ_νₜ, and aggregated data (h̄ᵗᵢ, T̄ᵗᵢ) = E^{Sᵗᵢ}[(hᵗ,Tᵗ)] (the conditional expectation of the true random data over block i), the aggregated problem (Eq. 1.2, p. 419) replaces the exact recursion by a finite tree of blocks, one decision per block, linked to its parent block's decision. Both (1.1) and (1.2) are, structurally, the same kind of object — a finite-tree deterministic-equivalent recourse LP — differing only in which tree and which node data they use; this mission formalizes that shared shape once (Tree, Instance, Feasible, obj) and instantiates it twice.

Formalized as: a shared Tree H structure (a finite node type, per-node stage, anc, and a root), the same representation Chunk 06's Multistage.Tree uses for the exact scenario tree of its own (different) chapter, restated here rather than imported (a draft cannot import another chunk's draft). An Instance H n m T bundles a tree's node-varying LP data (c, W, Tmat, h, p); Feasible/obj give its feasible set and objective. The exact problem (1.1) is Instance H n m TFine for a fine/exact tree TFine; the aggregated problem (1.2) is Instance H n m TCoarse for a coarser tree TCoarse, connected to TFine by an aggregation map agg : TFine.Node → TCoarse.Node.

Formalization targets

Goal — Chapter 10, Theorem 1 (p. 419)

agg respects the tree structure (root, stage, ancestor);
W, c agree between the fine and coarse instances (up to agg);
coarse.h, coarse.Tmat are the p-weighted conditional expectations of fine.h, fine.Tmat over
  each aggregation fiber;
∀ coarse nodes i,i' at the same stage sharing a "current-period outcome",
  coarse.h i = coarse.h i' ∧ coarse.Tmat i = coarse.Tmat i'
  ⟹ zCoarse ≤ zFine

This is the mission's only formalization target: BRIEF.md records that no separately numbered lemma precedes Theorem 1's proof in this section to serve as an independent milestone (the proof is a direct LP-duality argument against the theorem's own hypotheses), and that Chapter 8's Theorem 1 — the two-period case this theorem generalizes — is a cross-chapter dependency belonging to Chunk 08's own mission, not a milestone here. milestones.yaml is accordingly empty; see STATUS.md for the explicit accounting of what else in this chapter was considered and left out (Theorem 3, the aggregation error bound of §10.2, an unrelated and substantially heavier result).

Significance

Theorem 1 is what licenses every aggregation-based approximation scheme the rest of the book's multistage material builds on: it says precisely when replacing a multistage recourse problem's random data by within-period conditional expectations preserves a valid lower bound, and precisely identifies the condition (aggregated nodes sharing a current-period outcome must carry identical aggregated data) whose failure breaks the bound — a condition the book states is not decorative ("if not, then the conditional expectation form ... may not actually achieve a bound," p. 418). Formalizing it gives Prove2Me a first structural result connecting Chapter 8's single-period Jensen bound (Chunk 08) to genuinely multistage approximation, using the same finite-scenario-tree deterministic-equivalent representation Chunk 06 uses for the exact nested Benders decomposition — the two missions' shared representation choice (documented in both STATUS.md files) means a future mission relating them formally (e.g. instantiating Chunk 06's exact tree as this mission's TFine) has a compatible object to work with, even though neither imports the other's draft.

Difficulty

The theorem's proof (p. 419-420) is a direct LP weak-duality argument: given an optimal dual solution to the aggregated problem, the book constructs a dual-feasible solution to the exact problem attaining the same value, using precisely the "common outcome ⟹ equal aggregated data" hypothesis to make the constructed dual solution well-defined across the exact tree's finer structure. This is a real argument, not a citation, but it is left as sorry: formalizing the proof would need the multistage LP duality machinery (the "multistage version of Theorem 3.13" the book's own proof invokes, itself left as Exercise 1) that no chunk of this series has built. The value of this mission is the faithful statement of the bound and its exact hypotheses.

Formalization scope

• The book's own printed typo, resolved and documented. Theorem 1's hypothesis clause reads, as printed, "such that (ωt−1,ωt) ∈ Stj if and only if there exist some (ω̂t−1,ωt) ∈ Stj" — S^t_j appears on both sides of the "if and only if," where the sentence's own subject ("S^t_i and S^t_j that have a common outcome") requires the left side to range over S^t_i. Confirmed against a direct render of PDF page 436 (uv run --with pymupdf python), not assumed from OCR: the PDF's own typesetting has this repetition, not an artefact of text extraction. This formalization reads the corrected clause as "S^t_i and S^t_j project onto the same set of period-t outcomes" and states it via an explicit label type Θ and curOutcome : TCoarse.Node → Θ, since the aggregated tree alone does not carry a literal per-period outcome space to project onto (see Setting above — Tree records only history-node structure, not the underlying product space Ω = Ω₁ × ⋯ × Ω_H).
• W, c shared exactly, not aggregated, matching the book's explicit assumption that the recourse matrix and per-stage cost are deterministic and identical across (1.1) and (1.2) ("Wt known and not random," "ct = ct," p. 418) — formalized as direct equality hypotheses (hW_agree, hc_agree) rather than folding W/c into the conditional-expectation machinery that h/Tmat go through.
• zFine/zCoarse are hypothesis-characterized, not sInf-defined, avoiding the real infimum's junk value 0 on an unbounded-below or empty feasible set (reference/FAITHFULNESS_TRAPS.md trap 5) — neither tree-LP's feasible set is shown bounded or nonempty by the hypotheses alone.
• The conditional-expectation defining equations are weighted, p·h/p·Tmat, not h/Tmat alone, matching the book's own E^{Sti}[·] = (h̄ti,T̄ti) read as "the fiber-sum of p·(h,T) equals p_i·(h̄ti,T̄ti)" — the standard definition of a conditional expectation against counting measure on a finite partition. Instance's own hp_pos (every node's probability is strictly positive) rules out the degenerate case a bare unweighted equation would need to guard separately (a coarse node of probability 0, which cannot occur, is what the read-back of this theorem flags as the one case where the weighted equation would not pin down h_coarse/ Tmat_coarse themselves — moot here since hp_pos excludes it).
• Trivialization risk (this chapter's own). A formalization that let coarse.h/coarse.Tmat be arbitrary constants unrelated to fine.h/fine.Tmat (dropping the conditional-expectation defining equations) would still typecheck a "lower bound" conclusion but assert nothing about aggregation — exactly the risk BRIEF.md flags: "a formalization that treats (h̄ti,T̄ti) as arbitrary constants rather than as conditional expectations over a partition of the scenario space at time t loses the theorem's actual content." Both hCoarse_h/hCoarse_T (the defining equations) and hCommonOutcome (the theorem's own extra hypothesis) are load-bearing and present.

Selected references

• Birge, J.R., Louveaux, F. Introduction to Stochastic Programming, 2nd ed., Springer 2011, Chapter 10, §10.1 (pp. 417-420), Theorem 1 (p. 419).
• Birge, J.R. "Decomposition and partitioning methods for multistage stochastic linear programs." Operations Research 33 (1985), 989-1007 — the source Chapter 10's aggregation bounds draw on (cited in §10.2, the neighboring section this mission does not formalize).

Motivation

Two-stage stochastic programs with recourse — choose a first-stage decision $x$ now, observe a random outcome $\xi$, then choose a second-stage recourse decision $y(\xi)$ to repair whatever $x$ left infeasible or suboptimal — are the workhorse model of the field, used for capacity planning, inventory and financial portfolio problems since the 1950s (Dantzig 1955; Beale 1955). When $\xi$ ranges over a finite set of scenarios, the recourse function $Q$ that averages the second-stage cost over scenarios is piecewise linear and convex in $x$, so the overall problem is itself a large linear program — but one whose constraint matrix has a scenario for every column block and can be far too large to hand to a general-purpose LP solver directly. Van Slyke and Wets' L-shaped method (1969), the subject of this mission, is the algorithm that made two-stage recourse problems with finite scenario sets practically solvable: it is Benders decomposition specialized to this block structure, alternating between a small master program over $x$ (and a scalar $\theta$ approximating the recourse cost) and, at each candidate $x$, a batch of second-stage linear programs that either certify $x$'s second-stage feasibility or supply a linear underestimate — a cut — of $Q$ around $x$. Birge & Louveaux's Introduction to Stochastic Programming (2nd ed., Springer 2011), Chapter 5 §5.1, gives the algorithm and proves its two central guarantees: a shortcut feasibility test for a special case (Theorem 1) and the algorithm's finite convergence in general (Theorem 2), which is this mission's goal.

Setting

A two-stage recourse instance consists of a first-stage feasible region $K_1 = \{x \mid Ax = b,\ x \ge 0\}$ for $x \in \mathbb{R}^{n_1}$, and, for each of $K$ finite scenarios $k = 1, \dots, K$ (occurring with probability $p_k$), second-stage data $(q_k, h_k, T_k)$ defining the recourse subproblem

where the recourse matrix $W$ is fixed — the same across every scenario, the case this chapter treats. $K_2 = \{x \mid Q(x,\xi_k) < \infty \text{ for all } k\}$ is the set of $x$ for which every scenario's subproblem is feasible, and the two-stage problem is

A basis of the recourse subproblem is an injective choice of $m_2$ of $W$'s columns (where $m_2$ is $W$'s row count); each basis $b$ determines a simplex multiplier $\pi = (W_b^\top)^{-1} q_b$, and when $b$ attains the true optimum of $Q(x,\xi_k)$, LP duality gives $Q(x,\xi_k) = \pi^\top(h_k - T_k x)$ — the mechanism that turns a batch of second-stage LP solves into linear cuts on $x$.

Formalization targets

The L-shaped algorithm proceeds in three steps, repeated until neither applies:

• Step 1 solves the current master program (the $K_1$-feasible $x$, plus $\theta$ once at least one optimality cut exists, minimizing $c^\top x + \theta$ subject to every cut recorded so far — or just $c^\top x$ over $K_1$ before the first optimality cut, matching the book's convention that $\theta$ "is set equal to $-\infty$ and is not considered" until then).
• Step 2 tests each scenario's second-stage feasibility at the Step-1 optimum via an auxiliary LP; if some scenario fails (the LP's optimal value is positive), its optimal basis yields a feasibility cut and the algorithm returns to Step 1.
• Step 3, once every scenario is feasible, checks whether $\theta$ already dominates the true recourse cost at $x$ (using each scenario's optimal basis via LP duality); if not, an optimality cut is added and the algorithm returns to Step 1; if so, $x$ is optimal and the algorithm stops.

Goal — Chapter 5, Theorem 2 (p. 198)

Formalized as: starting from the empty cut set, there is a finite-length run of the algorithm's Step-1/2/3 transition relation, of length bounded by the total number of distinct feasibility- and optimality-cut witnesses available, ending at a state admitting no further step — at which point either the master program has become infeasible (certifying $K_1 \cap K_2 = \varnothing$) or its optimum is second-stage feasible, passes every fresh Step-3 test, and is optimal for the two-stage problem.

Milestone — Chapter 5, Theorem 1 (p. 194)

A shortcut avoiding $K$ separate feasibility LPs at Step 2: under these structural assumptions on $W$, checking feasibility at the single componentwise-worst right-hand side certifies feasibility at every scenario simultaneously.

Significance

Van Slyke and Wets' method (and Benders decomposition more generally, of which it is the recourse-problem specialization) underlies essentially every large-scale two-stage stochastic program solved in practice, and its finite-convergence guarantee — not merely that an optimum exists, but that this specific cutting-plane procedure reaches it in finitely many outer iterations — is what makes the method a decision procedure rather than a heuristic. The proof's content is an explicit finiteness argument (the number of distinct simplex bases of the recourse subproblem and the feasibility-test LP is finite, so the algorithm cannot generate infinitely many distinct cuts before either exhausting the feasible region or converging), not a general compactness or fixed-point argument; formalizing it means formalizing the cutting-plane mechanism itself as a transition system and proving termination combinatorially, over the finite type of available bases, rather than proving only that some optimal $x$ exists.

Difficulty

The natural shortcut — state only "an optimal $x$ exists, or $K_1 \cap K_2 = \varnothing$" — is not Theorem 2's actual content and is not what this mission targets: that weaker claim would already follow from $K_1 \cap K_2$ being a nonempty polyhedron (or empty), with no reference to the algorithm at all, and would not require the finiteness-of-bases argument the book's proof turns on. The genuine difficulty is representing Steps 1-3 faithfully as a relation on accumulating cut sets, and pinning the termination bound to the actual combinatorial object the book cites (the finite set of bases of the two LPs the algorithm solves at each iteration) rather than to a numeral or an abstract compactness bound. A second, quieter difficulty is Step 1's own optimum: once optimality cuts exist, the master program optimizes $c^\top x + \theta$ jointly, but before the first one it optimizes $c^\top x$ alone; conflating the two (e.g. always requiring $\theta$ to be part of the optimum) does not match Step 1 as the book states it.

Formalization scope

First-stage and second-stage vectors are Fin n1 → ℝ / Fin n2 → ℝ; the finite scenario set is Fin K with probability vector p. A basis is {b : Fin m2 → Fin n2 // Function.Injective b} (m2 = the recourse matrix's row count), matching "an injective choice of $m_2$ columns of $W$"; its finiteness is definitional, from Fin m2 → Fin n2 being finite. Simplex multipliers use Matrix.inv, whose junk value 0 on a singular matrix is never reachable in a proof because multipliers are only ever used through an IsOptimalAt/IsFeasBasisOptimalAt hypothesis that pins the basis to one genuinely attaining the LP's true optimum. The recourse value $Q(x,\xi_k)$ is EReal-valued (reusing this series' Instance/QVal convention from Chunk 03), so an optimality-cut witness's claimed value is compared to it by an explicit EReal cast, never by EReal arithmetic. The algorithm's state is a pair of finite sets of witnesses recorded so far (Finset (Fin K × FeasBasis n2 m2) × Finset (Fin K → Basis n2 m2)); Step is an inductive relation with one constructor per Step-2 and Step-3 branch, each requiring its witness not already recorded, and the goal states a bounded-length Step-path from the empty state to a state admitting no further Step. This mission does not restate Chapter 3's polyhedrality fact about $K_2$ as a separate lemma: the finiteness fact it is invoked for is already exposed directly and structurally by the finite Fintype bound on the number of bases, so no additional axiom stands in for it (see MODERATION_NOTES.md). Lemmas 3-9 and Theorem 10 of §5.2 (Regularized Decomposition, a different algorithm) are out of scope. The trivializing formalization this mission rules out is exactly the one named under Difficulty above: a bare existence-of-optimal-or- infeasible-$x$ statement with no reference to Steps 1-3 or to a finite bound on the number of iterations — such a statement would be true of any nonempty polyhedron and would not be Theorem 2.

Selected references

• R. Van Slyke and R. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM Journal on Applied Mathematics, 17(4), 1969, pp. 638-663. https://doi.org/10.1137/0117061
• J. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 5. https://doi.org/10.1007/978-1-4614-0237-4
• G. Dantzig, Linear Programming under Uncertainty, Management Science, 1(3-4), 1955, pp. 197-206. https://doi.org/10.1287/mnsc.1.3-4.197

Motivation

Every regret guarantee through Chapter IX compares the algorithm to the single best fixed decision in hindsight. That comparison is meaningless when the environment itself changes: a commuter's best route differs on weekdays versus weekends, an investor's best portfolio differs in a bull versus a bear market. A standard sublinear-regret algorithm, competing against one static comparator, will converge to some average compromise between regimes — exactly the wrong behavior when the regimes are genuinely different. Chapter 10 develops adaptive regret, a strictly stronger performance metric that demands low regret on every contiguous sub-interval of time simultaneously, and an efficient algorithm (Simple-FLH) that attains it for any base OCO algorithm at only a logarithmic additive cost.

Setting

For a comparator sequence $u_1,\dots,u_T$ with path length $P(u_1,\dots,u_T) = \sum_{t=1}^{T-1}\|u_t-u_{t+1}\|+1$, the dynamic regret $\mathrm{DynamicRegret}_T(A,u) = \sum_t f_t(x_t) - \sum_t f_t(u_t)$ measures performance against a moving target (§10.1). The chapter's central object, adaptive regret (Definition 10.2), instead takes the supremum of ordinary regret over every contiguous sub-interval $[r,s]\subseteq[T]$:

An algorithm is strongly adaptive if its adaptive regret matches its ordinary regret up to logarithmic factors in $T$ (§10.2.1).

The chapter builds toward this via the Fixed-Share algorithm (§10.3, Algorithm 30) — a variant of Hedge for the discrete expert-tracking problem, adding a uniform exploration term to each round's multiplicative update so that no expert's weight can vanish entirely — and then lifts it (§10.4) to the continuous OCO setting via Simple-FLH (Algorithm 32): run one fresh copy of a base OCO algorithm $A$ per starting time $1,\dots,T$, and apply Fixed-Share to this set of $T$ "experts."

Formalization targets

Theorem 10.1 (dynamic regret, milestone)

Online gradient descent with constant step size $\eta > 0$ satisfies, for every comparator sequence $u \in K$,

Theorem 10.3 (Fixed-Share tracking regret, milestone)

Given $\alpha$-exp-concave losses, Fixed-Share with $\delta=1/(2T)$ guarantees, for every interval $[r,s]$ and every expert $i$,

Theorem 10.6 — the mission's goal

Simple-FLH guarantees

Significance

Theorem 10.6 answers §10.2.1's own question — are there algorithms simultaneously optimal in ordinary regret and adaptive regret? — affirmatively and constructively: Simple-FLH pays only an additive $O(\frac1\alpha\log T)$ over whatever regret its base algorithm $A$ already achieves, for any $\alpha$-exp-concave-loss algorithm $A$ (in particular, taking $A$ to be the Online Newton Step algorithm of Chapter IV gives an adaptive-regret algorithm with no asymptotic cost at all). This is the chapter's capstone reduction, structurally similar to Chapter IX's OCO-to-PAC reduction: a generic wrapper around any algorithm in a broad class, converting one guarantee into a strictly stronger one. No prior art was found on the platform for adaptive regret, dynamic regret, or Fixed-Share (planning search: q=adaptive+regret, q=dynamic+regret, q=tracking+regret — no hits); this mission drafts all three results fresh.

Difficulty

Theorem 10.1's proof adapts Theorem 3.1's telescoping-sum argument to a moving comparator, picking up an extra term $\sum_t x_t^\top(u_{t-1}-u_t)$ that Cauchy–Schwarz and the diameter bound convert into the path length $P(u)$ — a genuinely different quantity from $\sqrt T$ regret, not a trivial corollary. Theorem 10.3's proof (Lemma 10.4, an exp-concavity-driven potential argument structurally parallel to Hedge's own analysis in Chapter I) tracks how the fixed-share exploration term $\delta/N$ prevents any expert's weight from decaying below a usable floor, so that even an expert active only over a short sub-interval $[r,s]$ still has enough accumulated weight at time $r$ for the argument to close — the sup-over-all-intervals form of the guarantee is exactly what this floor buys. Theorem 10.6's own proof is comparatively short (a direct application of Theorem 10.3 to Simple-FLH's experts, instantiated at the expert matching the interval's own start point), but depends on both of the preceding results' analyses for its correctness.

Formalization scope

AdaptiveRegretT is stated as a genuine supremum over a finite index set (subintervals of [0,T-1]), so it is a maximum, never a real-suprema-of-an-unbounded-set junk value — the chapter brief's own flagged pitfall (do not state it as a sum or average). ExpConcave is redeclared locally (Chapter IV's own exp-concavity is not yet a published series definition; see MODERATION_NOTES.md). IsFixedShareRun gives expert decisions xi as external data (matching the book's own treatment, where "an expert i suggests decision x^i_t" is not itself part of Fixed-Share's specification) — Theorem 10.3 is drafted at this level of generality, applying to Fixed-Share on any experts, matching how the book itself proves it once and reuses it for Simple-FLH. The goal (Theorem 10.6) connects Simple-FLH's experts to the base algorithm A via the one property the book's own proof actually uses — each expert's interval-regret bound inherited from A — rather than mechanizing Algorithm 32's exact re-indexing formula for starting a fresh copy of A at each round, which never enters the numerical bound; see MODERATION_NOTES.md. Three of this chapter's headline results (Theorems 10.1, 10.3, 10.6) are stated in the book with a bare O(·); per CAPTAIN_BRIEF.md rule 7 and BRIEF.md's explicit guidance, this mission uses the explicit constant each proof actually derives instead (Theorem 10.1's own η-parametrized inequality before the unstated optimal choice of η; Theorems 10.3 and 10.6's own final displayed bounds before they are folded into O(·) notation).

Not formalized: Definition 10.2's own generalization to $k$-shifting comparators (a remark, not a numbered theorem), §10.2.1's tightness/lower-bound claims (left as exercises in the book, no proof given), Lemma 10.4 (an intermediate step whose content is folded directly into Theorem 10.3's own explicit bound), and §10.5's starred FLH2 (Theorem 10.7, poly-logarithmic running time) — an advanced, optional stretch goal per BRIEF.md, not attempted given the chapter's non-starred primary goal (Theorem 10.6) was reachable within budget.

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 10.
• M. Herbster, M. Warmuth, "Tracking the best expert," Machine Learning 32(2), 1998, 151-178 (the Fixed-Share algorithm).
• A. Daniely, A. Gonen, S. Shalev-Shwartz, "Strongly adaptive online learning," ICML 2015 (FLH/Simple-FLH).

Motivation

A recurring question in economics and operations research is: when a decision problem depends on a parameter, does the optimal decision move monotonically as the parameter changes? A firm's optimal input mix as a price rises, a consumer's optimal consumption bundle as income grows, a Cournot firm's optimal output as a rival's output changes — in each case one wants "more of the parameter implies (weakly) more of the optimum" without assuming convexity, differentiability, or a unique optimizer. The classical tool for such comparative statics questions is the implicit function theorem, which needs smoothness and a nondegenerate Hessian and breaks down the moment the optimum is not unique or the objective is not differentiable. Topkis [1978] showed that a purely order-theoretic condition — supermodularity of the objective jointly in the decision variable and the parameter — is sufficient on its own, with no smoothness, uniqueness, or convexity assumed at all, and Milgrom and Roberts [1990a, 1994] later showed this lattice-theoretic approach subsumes and strengthens the classical monotone-comparative-statics results in economics. This mission formalizes the two central results this book calls "Topkis's theorem" (Theorem 2.8.1 and Theorem 2.8.2), together with the structural fact about maximizers of a supermodular function (Theorem 2.7.1) that both rest on, and the strengthening to strictly ordered optimal selections (Theorem 2.8.4).

Setting

Let $X$ be a lattice: a partially ordered set $(X, \preceq)$ in which every pair $x, x'$ has a join $x \vee x'$ and a meet $x \wedge x'$. A real-valued function $f : X \to \mathbb{R}$ is supermodular on $X$ if $f(x') + f(x'') \le f(x' \vee x'') + f(x' \wedge x'')$ for all $x', x'' \in X$; this is the same relativized notion (SupermodularOn) used, with $S = X$, throughout chunk I of this series.

Now let $T$ also be a partially ordered set (the parameter set), and let $f : X \times T \to \mathbb{R}$ be a real-valued function of the pair $(x, t)$. $f$ has increasing differences in $(x, t)$ if, for every $t' \prec t''$ in $T$, the map $x \mapsto f(x, t'') - f(x, t')$ is monotone (order-preserving) in $x$; equivalently, the marginal gain from raising $t$ is itself increasing in $x$. Replacing "monotone" with "strictly monotone" gives strictly increasing differences. To compare the resulting sets of optimizers rather than single points, this mission reuses the induced set ordering $\sqsubseteq$ from chunk I: for $A, B \subseteq X$, $A \sqsubseteq B$ holds when $a \wedge b \in A$ and $a \vee b \in B$ for all $a \in A$, $b \in B$.

Formalization targets

Goal — Theorem 2.8.2 (Topkis's theorem)

Let $X$ and $T$ be lattices, let $S$ be a sublattice of the product lattice $X \times T$, and let $S_t = \{x \in X : (x, t) \in S\}$ be the section of $S$ at $t \in T$. If $f : X \times T \to \mathbb{R}$ is supermodular on $S$ (jointly in the pair $(x, t)$), then

is increasing in $t$, with respect to $\sqsubseteq$, on $\{t \in T : \operatorname{argmax}_{x \in S_t} f(x, t) \neq \emptyset\}$.

Theorem 2.8.1 (the underlying, more elementary sufficient condition)

With $S_t \subseteq X$ increasing in $t$ (with respect to $\sqsubseteq$), $f(x,t)$ supermodular in $x$ for each fixed $t$, and $f(x,t)$ having increasing differences in $(x,t)$ on $X \times T$, the same conclusion — $t \mapsto \operatorname{argmax}_{x \in S_t} f(x,t)$ increasing in $\sqsubseteq$ — holds. Theorem 2.8.2's joint-supermodularity hypothesis on a sublattice of $X \times T$ automatically forces both of Theorem 2.8.1's hypotheses, so 2.8.1 is the logically weaker, more elementary statement from which 2.8.2's proof proceeds.

Theorem 2.8.4 (strict strengthening)

Under the hypotheses of Theorem 2.8.1 but with strictly increasing differences, every individual optimal solution at a larger parameter value dominates every individual optimal solution at a smaller one: $t' \prec t''$, $x' \in \operatorname{argmax}_{x \in S_{t'}} f(x,t')$, and $x'' \in \operatorname{argmax}_{x \in S_{t''}} f(x,t'')$ together force $x' \preceq x''$ — a genuinely stronger conclusion than $\sqsubseteq$ alone gives.

A supporting result is formalized as a milestone because both goals' proofs use it directly: Theorem 2.7.1, that $\operatorname{argmax}_{x \in X} f(x)$ is a sublattice of $X$ whenever $f$ is supermodular on $X$ — the structural fact that makes it meaningful to compare optimal-solution sets with $\sqsubseteq$ in the first place.

Significance

The result itself. Theorem 2.8.2 is the book's own headline theorem, cited throughout the rest of the monograph: it underlies the assortative-matching existence theorem (Chapter 3), monotone optimal policies in Markov decision processes (Chapter 3), and equilibrium comparative statics in supermodular games (Chapter 4) — each a later mission in this series. Its distinguishing feature relative to the implicit function theorem is that it needs no differentiability, no uniqueness of the optimizer, and no interiority: it applies equally to discrete decision problems (integer programming, combinatorial selection) and continuous ones.

Formalizing it. Nothing in Mathlib currently states a parametric monotone-comparative- statics result of this shape: the closest neighboring material (order-preserving maps, MonotoneOn, lattice structures) supplies only the vocabulary, not the theorem. This mission is the first formalization of Topkis's theorem on this platform and introduces the increasing-differences vocabulary (IncreasingDifferencesOn, StrictlyIncreasingDifferencesOn) that later missions in this series (matching, MDPs, supermodular games) reuse directly.

Difficulty

The natural first idea — differentiate $f$ in $x$, set the gradient to zero, and use the implicit function theorem on the resulting first-order condition — fails immediately because nothing here is assumed differentiable, and $\operatorname{argmax}_{x \in S_t} f(x,t)$ need not be a single point. The correct argument instead compares two arbitrary elements $x' \in S_{t'}$, $x'' \in S_{t''}$ directly through the supermodularity inequality applied to the pair $(x', t')$ against $(x' \vee x'', t')$ (a chain of inequalities Topkis calls "Lemma 2.8.1"), using increasing differences only to move the parameter from $t'$ to $t''$ inside that chain — at no point is a derivative, a selection function, or an interior point used. A second subtlety is that "increasing" in the conclusion is with respect to the induced set order $\sqsubseteq$, not a claim that some selection $t \mapsto x(t)$ is monotone: proving the stronger, pointwise-ordered conclusion (Theorem 2.8.4) genuinely needs the strict form of increasing differences, not merely increasing differences plus an extra hypothesis.

Formalization scope

$X$ and $T$ are kept as abstract Lattice/PartialOrder types throughout, matching the book's own generality — Theorem 2.8.1's and 2.8.2's $\mathbb{R}^n$/$\mathbb{R}^m$ corollary via second partial derivatives (discussed in the book's prose immediately after Theorem 2.8.2, p. 77) is not itself a numbered theorem and is not formalized here. Supermodularity, increasing differences, and strictly increasing differences are each formalized as a single relativized definition (SupermodularOn f S, IncreasingDifferencesOn f S, StrictlyIncreasingDifferencesOn f S) so the same declaration expresses both "supermodular on the whole lattice $X$" (used by Theorem 2.7.1 and Theorem 2.8.1's per-$t$ hypothesis) and "jointly supermodular on a sublattice $S$ of $X \times T$" (Theorem 2.8.2) — a formalization that instead only ever supermodularized $f(\cdot, t)$ for fixed $t$ would collapse Theorem 2.8.2's genuinely joint hypothesis into a restatement of Theorem 2.8.1, which is exactly the trivialization this mission's chunk brief warns against. $\operatorname{argmax}_{x \in S_t} f(x,t)$ is written out as the set of $x \in S_t$ that dominate every other element of $S_t$ under $f(\cdot, t)$, and every conclusion is stated only for pairs $t \preceq t'$ at which both argmax sets are assumed nonempty — matching the book's own restriction to $\{t \in T : \operatorname{argmax}_{x \in S_t} f(x,t) \neq \emptyset\}$, since $\sqsubseteq$ holds vacuously whenever either side is empty. This mission depends on chunk I's InducedSetOrder; it introduces no reusable infrastructure beyond its own three definitions, which later missions in the series (matching, MDPs, supermodular games) are expected to import directly rather than redefine.

Selected references

• Topkis, D. M., Minimizing a submodular function on a lattice, Operations Research 26(2), 1978, pp. 305–321. https://doi.org/10.1287/opre.26.2.305
• Topkis, D. M., Supermodularity and Complementarity, Princeton University Press, 2011 (DOI 10.1515/9781400822539), Chapter 2, §2.6–2.8.
• Milgrom, P. and Shannon, C., Monotone comparative statics, Econometrica 62(1), 1994, pp. 157–180. https://doi.org/10.2307/2951479
• Milgrom, P. and Roberts, J., Rationalizability, learning, and equilibrium in games with strategic complementarities, Econometrica 58(6), 1990, pp. 1255–1277. https://doi.org/10.2307/2938316

Motivation

Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality — stochastic shortest path (SSP) problems first (Prop. 7.2.1–7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1–7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.

Setting

States $1, \dots, n$ plus an implicit cost-free absorbing termination state $t$; finite nonempty control sets $U(i)$; costs $g(i,u)$; sub-stochastic transitions $p_{ij}(u) \ge 0$, $\sum_j p_{ij}(u) \le 1$, the deficit being the termination probability (BertsekasSSPModel). Operators

(BertsekasSSPPolicyOp, BertsekasSSPBellmanOp), $N$-stage costs by backward recursion with policy shift (BertsekasSSPNCost), and the survival mass $P\{x_m \ne t\}$ (BertsekasSSPSurvival). Assumption 7.2.1: for some $m > 0$, every admissible policy has survival mass $< 1$ from every state after $m$ stages. The discounted setting reuses the same model with stochastic rows and $0 < \alpha < 1$ (BertsekasDiscounted*); the average-cost setting adds a designated state $s$ with the avoidance probability of Assumption 7.4.1 (BertsekasSSPAvoidProb).

Target

Under Assumption 7.2.1, there is a vector $J^*$ with

and a stationary policy attaining $J^*$ — BertsekasDP.ssp_main_theorem (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.

Significance

These are the convergence guarantees behind value iteration and policy iteration — the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly $T$). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability $1 - \alpha$ per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, $m$-stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.

Difficulty

$T$ is not a one-stage contraction in the sup-norm under Assumption 7.2.1 — only an $m$-stage contraction, uniformly over the finitely many $m$-stage policy prefixes; extracting the uniform contraction factor $\rho < 1$ (via finiteness of the policy space) is the crux of the whole chapter. The limit of $N$-stage costs for nonstationary policies must be established, not assumed (tail-sum estimate $\rho^{\lfloor N/m \rfloor}$). For the average-cost results the associated-SSP construction (stop on reaching $s$) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the Cesàro limit need not exist.

Formalization scope

Finite states Fin n, finite control type, constraint sets as Finsets with attained minima; no termination state in the carrier — termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is Tendsto in the product topology (equivalently sup-norm, $n$ finite). Average cost uses real liminf and division with the $N = 0$ term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)–(e) in one statement mirroring Prop. 7.3.1.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§7.1–7.4.) http://www.athenasc.com/dpbook.html
• D. P. Bertsekas, J. N. Tsitsiklis, An analysis of stochastic shortest path problems, Math. Oper. Res. 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580
• M. L. Puterman, Markov Decision Processes, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Linear approximation is only one instance of distance minimization. Feasible sets in optimization are typically convex rather than subspaces, so a useful certificate must compare a target point with an entire convex set and must allow an affine offset. Chapter 5 of Luenberger's Optimization by Vector Space Methods builds this certificate through geometric forms of the Hahn--Banach theorem, supporting hyperplanes, and separation of convex sets. The resulting minimum-distance theorem expresses the distance from a point to a convex set as an optimal gap measured by a norm-bounded continuous linear functional (Luenberger, §§5.12--5.13, pp. 130--137).

This mission advances the series from subspace annihilators to affine separation. It formalizes the Minkowski gauge used by the chapter, three progressively stronger separation statements, and a capstone distance-duality certificate. These results are standard infrastructure for constrained optimization: they turn a geometric exclusion or distance into a scalar inequality that can later become a multiplier or a dual bound.

Setting

Let $X$ be a real normed space and $K\subseteq X$ a nonempty convex set. Convexity is represented by Convex ℝ K, and topological interior, closure, and infimum distance use Mathlib's interior, closure, and Metric.infDist. A continuous affine separator is described by a continuous linear functional $f:X\toL[\mathbb R]\mathbb R$ and a scalar level $c$. The inequality $f(k)\le c$ for all $k\in K$ places $K$ in one closed half-space.

When a convex set contains zero in its interior, its Minkowski gauge is the functional gauge K. The source characterizes it by nonnegativity, positive homogeneity, subadditivity, continuity, and the level sets

These properties are bundled into the first milestone, following Lemma 1 of §5.12 (pp. 131--132).

For two convex sets $K_1,K_2$, Eidelheit separation means finding nonzero $f$ and $c$ with $f(x)\le c\le f(y)$ for $x\in K_1$ and $y\in K_2$. The source assumes that $K_1$ has nonempty interior and that its interior does not meet $K_2$. The Lean statement records the nonemptiness of $K_2$ explicitly, since otherwise nonzero separation is not forced.

Formalization targets

Gauge and geometric Hahn--Banach milestones

Formalize the six gauge properties above. Then, for a convex $K$ with nonempty interior and an affine subspace $V$ disjoint from that interior, produce $f\ne0$ and $c$ such that

This is Mazur's geometric Hahn--Banach theorem as stated in §5.12, Theorem 1 (p. 133).

Supporting hyperplanes and convex-set separation

For $x\notin\operatorname{int}K$, formalize a nonzero functional satisfying $f(k)\le f(x)$ for all $k\in K$. Next formalize Eidelheit separation:

These are Theorems 2 and 3 of §5.12 (pp. 133--134).

Convex minimum-distance duality

Let $x_1$ have positive distance $d$ from $K$. Produce $f$ and a real upper-bound level $c$ with $\|f\|\le1$, $f(k)\le c$ on $K$, and

Every other feasible pair $(g,b)$ must satisfy $g(x_1)-b\le d$. If $x_0\in K$ realizes the distance, require $-f$ to align with $x_0-x_1$. This is the finite real certificate form of §5.13, Theorem 1 (pp. 136--137).

Significance

The capstone is an exact strong-duality statement for distance to a convex set. A feasible pair $(g,b)$ yields a certified lower bound on the distance, and the distinguished pair reaches the primal value. Unlike a nearest-point characterization, it remains meaningful when $K$ is not closed and no minimizing point exists. The conditional alignment clause identifies the equality case when attainment is available.

Formalizing the chapter's progression creates more than one isolated equality. The gauge package links convex geometry to sublinear analysis; Mazur separation handles affine constraints; the supporting-hyperplane and Eidelheit statements provide reusable interfaces for later multiplier rules. The results are known and proved in the 1969 text; the mission's contribution is a coherent machine-checked Lean layer that preserves the source hypotheses and can support later chapters on duality and optimization.

Difficulty

A direct reuse of subspace distance duality is insufficient because a general convex set is neither closed under subtraction nor described by an annihilator. An affine level $c$ is unavoidable. The common shorthand $\sup_{k\in K} f(k)$ introduces a second problem: $K$ need not be bounded, so a real-valued supremum is not available for an arbitrary functional. The capstone therefore quantifies over a real upper bound $c$ and asserts its optimality through a universal inequality; this records the same finite support value without imposing boundedness absent from the source.

Topological hypotheses also differ across the milestones. Separation uses nonempty interior, whereas the final distance theorem only assumes convexity, nonemptiness, and positive distance. Replacing positive distance by mere exclusion $x_1\notin K$ would be invalid for a nonclosed set. Similarly, requiring closure or compactness would make formalization easier but would lose the theorem's intended infinite-dimensional scope.

Formalization scope

The mission is restricted to real normed spaces. Sets use Set X; affine varieties use AffineSubspace ℝ X; separators use ContinuousLinearMap. The gauge is Mathlib's existing gauge, so no competing definition is introduced. The bundled gauge milestone deliberately includes both level-set identities as well as continuity, positive homogeneity for positive real scalars, subadditivity, and nonnegativity.

The Eidelheit theorem includes K₂.Nonempty, an assumption used implicitly by the source's separating conclusion. The capstone includes K.Nonempty and 0 < Metric.infDist x₁ K; it does not assume closedness, boundedness, compactness, or attainment. Its pair $(f,c)$ represents a finite support level, and the universal comparison over all feasible $(g,b)$ rules out a weakened statement in which an arbitrarily loose upper bound could trivialize existence. The optional nearest-point clause uses the exact equality $\|x_0-x_1\|=d$ and fixes the sign of alignment. Contributions may add reusable lemmas on gauges, interiors, affine subspaces, or support bounds, but the public results should remain independent of finite-dimensionality and completeness.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 5, §§5.11--5.13, pp. 127--137. Public scan.

Every full-dimensional convex body is sandwiched between an ellipsoid and its $n$-fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid $\mathcal{E}$ about its centre $x_0$ by the factor $1/n$ lands inside the body,

and the factor $n$ is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes $C = \operatorname{conv}\{x_1,\dots,x_m\}$, exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum ($\sum_i \lambda_i x_i x_i^{T} = I$, $\sum_i \lambda_i x_i = 0$, $\sum_i \lambda_i = n$), the convex-combination step that produces the $1/n$ ball, and affine invariance.

Interior point methods solve linear programs by moving through the interior of the feasible set instead of along its edges — the approach that turned Karmarkar's 1984 breakthrough into today's practical large-scale solvers. This mission formalizes the primal path following algorithm of Chapter 9 of Bertsimas–Tsitsiklis. For $\mu > 0$ the logarithmic barrier

replaces the constraint $\mathbf{x} \ge \mathbf{0}$; the minimizers $\mathbf{x}(\mu)$ of $B_\mu$ over $\{A\mathbf{x} = \mathbf{b}\}$ trace the central path, characterized by the KKT conditions (9.17): $A\mathbf{x} = \mathbf{b}$, $\mathbf{x} \ge \mathbf{0}$, $A'\mathbf{p} + \mathbf{s} = \mathbf{c}$, $\mathbf{s} \ge \mathbf{0}$, $XS\mathbf{e} = \mu\mathbf{e}$ (Lemma 9.5). The algorithm follows the path with one Newton step of the barrier problem per shrink $\mu^{k+1} = \alpha\mu^k$, maintaining the proximity invariant

. The goal theorem is Theorem 9.7: with $\alpha = 1 - \frac{\sqrt{\beta}-\beta}{\sqrt{\beta}+\sqrt{n}}$ and a $\beta$-close start, after $K = \Big\lceil \frac{\sqrt{\beta}+\sqrt{n}}{\sqrt{\beta}-\beta}\,\log\frac{(\mathbf{s}^0)'\mathbf{x}^0(1+\beta)}{\varepsilon(1-\beta)} \Big\rceil$ iterations the algorithm reaches primal and dual feasible solutions with duality gap $(\mathbf{s}^K)'\mathbf{x}^K \le \varepsilon$ — the explicit form of the celebrated $O(\sqrt{n}\log(1/\varepsilon))$ iteration bound. Alongside it we formalize the generic potential-reduction scheme (Theorem 9.4): any algorithm cutting $G(\mathbf{x},\mathbf{s}) = q\log\mathbf{s}'\mathbf{x} - \sum_j \log x_j - \sum_j \log s_j$ by $\delta$ per step reaches gap $\varepsilon$ within an explicit $K$.

Can the feasibility of a system of linear inequalities be decided in a provably small number of iterations? The ellipsoid method — the algorithm with which Khachiyan showed in 1979 that linear programming is polynomially solvable — answers this with pure convex geometry. This mission formalizes Chapter 8 of Bertsimas–Tsitsiklis. An ellipsoid is

with $D$ symmetric positive definite. The geometric engine is Theorem 8.1: the half-ellipsoid $E \cap \{\mathbf{x} \mid \mathbf{a}'\mathbf{x} \ge \mathbf{a}'\mathbf{z}\}$ is contained in the explicitly constructed ellipsoid $E' = E(\bar{\mathbf{z}}, \bar{D})$,

and the volume contracts:

. Two integer-data estimates make the contraction decisive: every extreme point of $P = \{\mathbf{x} \mid A\mathbf{x} \ge \mathbf{b}\}$ with entries bounded by $U$ has coordinates in $[-(nU)^n, (nU)^n]$ (Lemma 8.2), and a full-dimensional bounded such polyhedron has $\mathrm{Vol}(P) > n^{-n}(nU)^{-n^2(n+1)}$ (Lemma 8.4). The goal theorem is Theorem 8.2: started on a ball $E(\mathbf{x}_0, r^2 I)$ of volume at most $V$ containing $P$, with $v$ a lower bound on $\mathrm{Vol}(P)$ when $P$ is nonempty, the ellipsoid method correctly decides whether $P$ is empty within $t^* = \lceil 2(n+1)\log(V/v) \rceil$ iterations — the explicit iteration count behind the polynomial-time headline.

Why do network linear programs return integer answers for free? This mission formalizes the structural theory of the minimum cost network flow problem of Chapter 7 of Bertsimas & Tsitsiklis: a directed graph $G=(\mathcal{N},\mathcal{A})$ with external supplies $b_i$, arc costs $c_{ij}$, and the node-arc incidence matrix $\mathbf{A}$ — an $n\times m$ matrix in which every column has exactly one $+1$ (start node) and one $-1$ (end node) — so that flow conservation reads $\mathbf{A}\mathbf{f}=\mathbf{b}$, forcing the standing assumption $\sum_{i\in\mathcal{N}} b_i=0$. Because the rows of $\mathbf{A}$ sum to zero, the book works with the truncated matrix $\tilde{\mathbf{A}}$ of the first $n-1$ rows. The combinatorial heart is the correspondence between algebra and graph structure: a set $T$ of $n-1$ arcs forming a tree determines a unique tree solution of $\tilde{\mathbf{A}}\mathbf{f}=\tilde{\mathbf{b}}$, $f_{ij}=0$ off $T$ (Theorem 7.3); connectedness makes $\tilde{\mathbf{A}}$ full-rank (Corollary 7.1); and a flow vector is a basic solution if and only if it is a tree solution (Theorem 7.4). The goal theorem is the integrality theorem (Theorem 7.5): for the uncapacitated problem on a connected graph, every basis matrix $\mathbf{B}$ has an integer inverse $\mathbf{B}^{-1}$ (its determinant is $\pm 1$ by the tree/lower-triangular argument), integer supplies make every basic solution integer, and integer costs make every dual basic solution integer — whence integer optimal primal and dual solutions exist whenever the optimal cost is finite (Corollary 7.2). This is the fountainhead of combinatorial integrality in linear optimization, feeding the max-flow min-cut mission that follows.