The OR Formalization Drive

Motivation

Two-stage stochastic programs with recourse require evaluating $Q(x) = \mathbb E_\xi[Q(x,\xi)]$, the expected value of a recourse function, at every candidate first-stage decision $x$. When $\xi$ is high-dimensional or continuously distributed, this expectation is a multivariate integral of a piecewise-linear, generally nondifferentiable integrand, and classical quadrature rules — built for smooth integrands in low dimension — do not apply (Birge & Louveaux, §8.1). What does apply is convexity: $Q(x,\cdot)$ is convex whenever the recourse problem is a linear program in $\xi$, and convexity alone is enough to sandwich $\mathbb E_\xi[Q(x,\xi)]$ between two computable discrete approximations. This chapter develops that sandwich, and it is the standard device used throughout the stochastic-programming literature to bound and iteratively refine the recourse function: the lower bound goes back to Jensen [1906]; the upper bound is due to Edmundson [1956] and Madansky [1959], with the mean-consistent LP refinement due to Madansky [1960] and Gassmann & Ziemba [1986]. Refinements of both bounds appear in Huang, Ziemba & Ben-Tal [1977], Kall & Stoyan [1982] and Frauendorfer [1988].

Setting

Fix a probability space $(\Omega, \mathcal F, P)$ and an integrand $g : D \times \Xi \to \mathbb R$, where $\Xi \subseteq E$ is the (convex, closed) support of a random vector $\xi : \Omega \to \Xi$ and $E$ is a real vector space (in the recourse application, $g(x,\cdot) = Q(x,\cdot)$ and $D$ is the first-stage feasible region). Write $\mathbb E(g(x)) = \mathbb E_\xi[g(x,\xi)] = \int_\Xi g(x,\xi)\, P(d\xi)$.

A partition of $\Xi$ into $\nu$ measurable blocks $S^\nu = \{S_1,\dots,S_\nu\}$ determines, for each block, its probability $p_l = P[\xi \in S_l]$ and its conditional mean $\xi^l = \mathbb E[\xi \mid S_l]$. Equivalently — and this is the convention this mission's Lean development uses — the blocks may be taken directly on the sample space as the pulled-back sets $S_l = \xi^{-1}(\text{region}_l) \subseteq \Omega$, with $p_l = P(S_l)$ and $\xi^l = p_l^{-1}\int_{S_l}\xi\,dP$ the Bochner integral average of $\xi$ over the block; the two descriptions coincide.

Formalization targets

Goal — Chapter 8, Theorem 1 (Jensen lower bound), p. 346

$$g(x,\cdot) \text{ convex on } \Xi \ \Longrightarrow\ \mathbb E(g(x)) \ \ge\ \sum_{l=1}^{\nu} p_l\, g(x,\xi^l).$$

This is the sharpest statement the chapter proves for the lower bound: it holds for every finite measurable partition, with no assumption beyond convexity of $g(x,\cdot)$ and integrability.

Chapter 8, Theorem 2 (Edmundson-Madansky upper bound), pp. 347-348

For $\Xi$ compact, let $\mathrm{ext}\,\Xi$ be the extreme points of $\mathrm{co}\,\Xi$, carrying the Borel field of all its subsets. If, for every $\xi \in \Xi$, $\varphi(\xi,\cdot)$ is a probability measure on $\mathrm{ext}\,\Xi$ with barycenter $\xi$ (i.e. $\int_{\mathrm{ext}\,\Xi} e\,\varphi(\xi,de) = \xi$) and $\omega \mapsto \varphi(\xi(\omega), A)$ is measurable for every $A$, then

$$\mathbb E(g(x)) \ \le\ \int_{\mathrm{ext}\,\Xi} g(x,e)\, \lambda(de), \qquad \lambda(A) = \int_\Omega \varphi(\xi(\omega), A)\, P(d\omega).$$

Together the two targets give the chapter's headline sandwich: for convex $g(x,\cdot)$, the finite-partition Jensen value and the Edmundson-Madansky value bracket the true expectation, and refining the partition (resp. the disintegration) tightens both sides toward it.

Significance

The Jensen bound is the workhorse of discrete-distribution approximation in stochastic programming: it is what makes $Q^\nu(x) = \sum_l p_l Q(x,\xi^l)$ a valid, refinable lower-approximation of the true recourse function, and it underlies the partition-refinement schemes (§8.2, following Birge & Wets [1986] and Frauendorfer & Kall [1988]) used inside the $L$-shaped method and separable-programming solvers described later in the chapter (§8.3). The Edmundson-Madansky bound is its indispensable upper counterpart: without it there is no certificate of how far a lower approximation can be from the truth, and the mean-consistent LP refinement (eq. 2.9, not part of this mission) reduces to a moment-problem computation over $\lambda$. Both bounds are, to date, unformalized: the platform holds no theorem matching either a finite-partition conditional-Jensen inequality or an extreme-point disintegration bound (searched GET /theorems?q=... for "Jensen", "conditional expectation", "Edmundson Madansky", "partition convex" — no relevant hits), so this mission is a first formalization of both, not a reformulation of existing platform content. Mathlib supplies the raw convexity substrate this mission is built from — finite Jensen (Analysis/Convex/Jensen.lean) and, critically, the set-average integral Jensen inequality (ConvexOn.map_set_average_le in Analysis/Convex/Integral.lean), exactly the per-block step the book's proof of Theorem 1 performs — but no existing lemma assembles these into the partitioned, conditional-mean statement the book actually states.

Difficulty

The obvious shortcut is to prove "convex functions lie above their tangent line" and stop — this captures no partition structure at all and is not the theorem the book states (the theorem is about $\Sigma_l p_l g(x,\xi^l)$, a sum over blocks, not a single linearization). The real content is bookkeeping across the partition: writing $\mathbb E(g(x))$ as $\sum_l P(S_l)\,\mathbb E[g(x,\xi)\mid S_l]$ (an exact identity, no convexity needed), then applying ordinary Jensen inside each block to replace $\mathbb E[g(x,\xi)\mid S_l]$ by $g(x,\xi^l)$ from below — the inequality only enters at the second step, once per block. Proving this in Lean means correctly discharging, for every block, the side conditions Mathlib's integral-Jensen lemma needs (closedness of $\Xi$, continuity of $g(x,\cdot)$ on $\Xi$, integrability on the block) and then summing the $\nu$ per-block inequalities against weights $p_l$ that themselves depend on the partition — an easy step to get wrong by, e.g., letting $\xi^l$ be an arbitrary point of $S_l$ rather than exactly its conditional mean, which understates what Jensen actually forces. Theorem 2 additionally requires setting up the disintegration $\lambda$ correctly: $\lambda$ is a probability measure defined as an integral of the kernel-like family $\varphi$ against $P\circ\xi^{-1}$, and both the barycenter condition on $\varphi$ and the measurability of $\omega \mapsto \varphi(\xi(\omega),A)$ are load-bearing — dropping either makes $\lambda$ ill-defined or the bound's proof inapplicable.

Formalization scope

$\Xi \subseteq E$ for $E$ a complete real normed vector space (NormedAddCommGroup E, NormedSpace ℝ E, CompleteSpace E); no finite-dimensionality is assumed since neither theorem's proof needs it. The parameter $x$ ranges over an arbitrary type $\alpha$ with $D \subseteq \alpha$, and $g$ is left as a bare function α → E → ℝ, matching the book's level of abstraction (the recourse LP's own data $A,b,c,q,W,T,h$ is never used in either proof).

The partition is formalized directly on the sample space $\Omega$ (a Partition structure: pairwise-disjoint measurable blocks covering $\Omega$, each of positive measure) rather than on $\Xi$, per the equivalence noted under Setting; $\xi^l$ is defined as the Bochner-integral average $p_l^{-1}\int_{S_l}\xi\,dP$, so it is forced to be the conditional mean and cannot be weakened to an arbitrary sample point of the block — the change the chunk brief flags as the main faithfulness trap for this chapter.

Two explicit hypotheses are added beyond the book's own statement of Theorem 1, both needed by Mathlib's integral-Jensen lemma rather than narrowings of the mathematical content: ContinuousOn (g x) Ξ (finite-dimensional convex functions are automatically continuous on the interior of their domain, which is what the book implicitly relies on; stated explicitly since $E$ is not assumed finite-dimensional) and integrability of $\xi$ and of $g(x,\xi(\cdot))$ (needed for $\mathbb E(g(x))$ and each $\xi^l$ to be well-defined). For Theorem 2, the disintegrating family $\varphi$ is E → Measure Ext for an abstract type Ext (standing for $\mathrm{ext}\,\Xi$) with the discrete MeasurableSpace (every subset measurable, matching the book's "Borel field ... the collection of all subsets"), mapped into $E$ by an embedding toE whose range is exactly (convexHull ℝ Ξ).extremePoints ℝ; the measure $\lambda$ (named μExt in the Lean code, since λ is a reserved keyword) is a hypothesis satisfying its defining equation (2.6) rather than constructed, since constructing a measure from a set function is a separate, book-external piece of measure theory the chapter's own proof does not perform either — it simply asserts $\lambda$ is the probability measure with that value on every set.

A trivializing formalization is ruled out explicitly: a version that lets $\xi^l$ range over an arbitrary point of $S_l$, or that proves only the ordinary (unconditional) Jensen inequality without ever introducing the partition, states something strictly weaker than the book and is not what is formalized here.

Both draft theorems end in := by sorry; a full Lean proof of Theorem 1 combines Mathlib's ConvexOn.map_set_average_le applied per block with the exact decomposition of $\int_\Omega$ into $\sum_l \int_{S_l}$ over the partition's disjoint, covering blocks. Reusable beyond this mission: the Partition structure and its weight/condMean accessors generalize to any chapter needing a finite measurable partition with conditional means (this book's later approximation schemes, §8.2-8.5 and Chapter 10, all build on the same device). Contributions solving either theorem, or formalizing the partition-refinement monotonicity $\mathbb E(g(x)) \ge \mathbb E^{\nu+1}(g(x)) \ge \mathbb E^\nu(g(x))$ (eq. 2.3, not part of this mission's milestone list since it is not itself a numbered theorem) as a follow-up, are welcome.

Selected references

• J.R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• J.L.W.V. Jensen, Sur les fonctions convexes et les inégalités entre les valeurs moyennes, Acta Mathematica 30 (1906), 175-193. https://doi.org/10.1007/BF02418571
• H.P. Edmundson, Bounds on the expectation of a convex function of a random variable, The RAND Corporation, Paper 982, 1956.
• A. Madansky, Bounds on the expectation of a convex function of a multivariate random variable, Annals of Mathematical Statistics 30 (1959), 743-746. https://doi.org/10.1214/aoms/1177706207
• A. Madansky, Inequalities for stochastic linear programming problems, Management Science 6 (1960), 197-204. https://doi.org/10.1287/mnsc.6.2.197
• H.I. Gassmann, W.T. Ziemba, A tight upper bound for the expectation of a convex function of a multivariate random variable, Mathematical Programming Study 27 (1986), 39-53. https://doi.org/10.1007/BFb0121114
• J.R. Birge, R.J-B. Wets, Designing approximation schemes for stochastic optimization problems, in particular for stochastic programs with recourse, Mathematical Programming Study 27 (1986), 54-102. https://doi.org/10.1007/BFb0121122

Motivation

Many results in economics and operations research reduce to a single question: does a system of interacting, mutually reinforcing choices settle at an equilibrium? A firm choosing input levels that are complements, a Cournot duopoly whose best responses move together, a matching market where agents' preferences reinforce assortative pairings — each is a fixed-point problem, but classical fixed-point theory (Brouwer, Kakutani) asks for convexity and continuity that these problems rarely have. Tarski's fixed point theorem [1955] showed that order, not topology, suffices: every increasing (monotone) self-map of a nonempty complete lattice has a fixed point, and the fixed points themselves form a nonempty complete lattice, with no continuity or convexity assumed at all. Zhou [1994] extended this from single-valued functions to set-valued correspondences, which is what is needed once "best response" becomes "the (possibly non-unique) set of optimizers." This mission formalizes Zhou's theorem (Topkis's Theorem 2.5.1) together with its parametric extension (Theorem 2.5.2), the two capstones of the lattice-theoretic toolkit that the rest of Topkis's monograph — and, within this series, its mission on supermodular games (Supermodularity and Complementarity V) — builds on directly.

Setting

A lattice $(X, \preceq)$ is a partially ordered set in which every pair of elements $x, y$ has a join $x \vee y$ (least upper bound) and a meet $x \wedge y$ (greatest lower bound). $X$ is a complete lattice if every subset (not just every pair) has a supremum and an infimum in $X$; a nonempty complete lattice always has a greatest element $\top$ and a least element $\bot$.

To compare sets of points — not just points — Topkis defines the induced set ordering $\sqsubseteq$: for $A, B \subseteq X$, $A \sqsubseteq B$ holds when every $a \in A$ and $b \in B$ satisfy $a \wedge b \in A$ and $a \vee b \in B$. Restricted to singletons, $\{a\} \sqsubseteq \{b\}$ says exactly $a \preceq b$, so $\sqsubseteq$ is the natural extension of $\preceq$ from points to sets, and it is the order with respect to which set-valued maps (correspondences) $Y : X \to \mathcal{P}(X)$ are called increasing: $x \preceq x'$ implies $Y(x) \sqsubseteq Y(x')$.

A subset $S \subseteq X$ is a sublattice if it is closed under the binary join and meet of $X$. $S$ is subcomplete if, more strongly, the supremum and infimum in $X$ of every nonempty subset of $S$ exist and lie in $S$ — so a subcomplete sublattice is itself a complete lattice under the order it inherits. A point $x \in X$ is a fixed point of a correspondence $Y$ if $x \in Y(x)$.

Formalization targets

Goal — Theorem 2.5.1 (Zhou's fixed point theorem)

Let $X$ be a nonempty complete lattice and $Y : X \to \mathcal{P}(X)$ an increasing correspondence with $Y(x)$ subcomplete for every $x$. Then:

$$x^\* = \sup\{x \in X : Y(x) \cap [x,\infty) \neq \emptyset\} \quad\text{is the greatest fixed point of } Y,$$ $$x_\* = \inf\{x \in X : Y(x) \cap (-\infty,x] \neq \emptyset\} \quad\text{is the least fixed point of } Y,$$

and the set of fixed points of $Y$, under its inherited order, is itself a nonempty complete lattice.

Theorem 2.5.2 (the parametric extension)

Let $T$ be a partially ordered set and $Y(x,t)$ a jointly increasing, subcomplete-valued correspondence on $X \times T$. Then for each $t$ the greatest and least fixed points $g(t)$, $l(t)$ of $Y(\cdot, t)$ exist and are increasing functions of $t$; under the further hypothesis that $\sup Y(x',t') \prec \inf Y(x',t'')$ whenever $t' \prec t''$, both become strictly increasing in $t$. This is the theorem that gives comparative statics their bite: it says an equilibrium moves monotonically — even strictly — as a parameter of the underlying system changes.

Two supporting results are formalized as milestones because Theorem 2.5.1's own proof invokes them directly: Lemma 2.4.2 (supremum and infimum are monotone under $\sqsubseteq$, whenever they exist) and Theorem 2.4.2 (an intersection of increasing correspondences, if it stays nonempty, is itself increasing).

Significance

The result itself. Tarski–Zhou is the order-theoretic alternative to Brouwer–Kakutani: where the latter needs a convex, compact strategy space and a continuous map, Tarski–Zhou needs only a lattice order and monotonicity, and it delivers something Brouwer–Kakutani does not — a greatest and a least fixed point, with an explicit order-theoretic formula for each, and the guarantee that the whole fixed-point set is a complete lattice in its own right. This is exactly the machinery behind existence proofs for supermodular games (Topkis's own Theorem 4.2.1, where the fixed points of the best-response correspondence are the pure-strategy Nash equilibria) and behind monotone comparative statics more broadly (Milgrom–Roberts [1994], of which Theorem 2.5.2 is a strict generalization to correspondences).

Formalizing it. Mathlib already has Tarski's theorem for single-valued monotone functions (OrderHom.lfp/gfp, fixedPoints.completeLattice, Knaster–Tarski). Nothing in Mathlib currently proves it for set-valued correspondences: this mission is a genuine strengthening of existing formalized mathematics, not a restatement of it, and it introduces the induced set ordering and subcompleteness — reused throughout the rest of this book's mission series — for the first time.

Difficulty

The natural first idea — "apply Knaster–Tarski to some selection function built from $Y$" — fails because there is no canonical way to select a single point from each $Y(x)$ that remains monotone without already knowing the theorem: an arbitrary selection from an increasing correspondence need not itself be increasing (this is exactly the subtlety Topkis's Theorem 2.4.3 addresses only for correspondences with a greatest/least element). The real argument instead builds the candidate fixed point directly as a supremum over an auxiliary set $\{x : Y(x) \cap [x,\infty) \neq \emptyset\}$ and establishes it is a fixed point using the monotonicity lemma (Lemma 2.4.2) at each step — no selection is ever made. A second subtlety is that the fixed-point set is not, in general, a sublattice of $X$: Topkis's Example 2.5.1 exhibits an increasing self-map of $[0,3]^2 \subset \mathbb{R}^2$ whose four fixed points are not closed under $\vee$/$\wedge$. Part (b)'s claim that the fixed points form their own complete lattice must therefore be proved without ever assuming, or implying, that ambient joins and meets of fixed points are again fixed points.

Formalization scope

$X$ is formalized as an abstract CompleteLattice, not ℝⁿ — the theorem is genuinely about order, and specializing to $ℝⁿ$ would hide exactly the generality Zhou's result adds over finite-dimensional fixed-point theorems. The induced set ordering InducedSetOrder and the predicate Subcomplete are defined once in this mission and reused by every later mission in the series that reasons about correspondences ordered by $\sqsubseteq$. A formalization that replaced the correspondence $Y$ by a single-valued function would trivialize the mission into a restatement of Mathlib's existing Knaster–Tarski theorem; the set-valued, subcomplete-ranged correspondence is not an optional generality but the entire content being added. Part (b) of Theorem 2.5.1 is formalized as a completeness statement about the induced order on the fixed-point set itself — not as a claim that the fixed-point set is closed under $X$'s ambient join and meet, which Example 2.5.1 refutes. "Partially ordered set" throughout is Lean's PartialOrder, matching the book's own usage in Chapter 2.

Selected references

• Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5(2), 1955, pp. 285–309. https://doi.org/10.2140/pjm.1955.5.285
• Zhou, L., The set of Nash equilibria of a supermodular game is a complete lattice, Games and Economic Behavior 7(2), 1994, pp. 295–300. https://doi.org/10.1006/game.1994.1051
• Milgrom, P. and Roberts, J., Comparing equilibria, American Economic Review 84(3), 1994, pp. 441–459. https://www.jstor.org/stable/2118061
• Topkis, D. M., Supermodularity and Complementarity, Princeton University Press, 2011 (DOI 10.1515/9781400822539), Chapter 2, §2.2–2.5.

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

$$t \;\longmapsto\; \operatorname{argmax}_{x \in S_t} f(x, t)$$

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

Existence of equilibrium is the first question any model of strategic interaction must answer, and the classical answer — Nash's theorem via Kakutani's fixed point theorem — asks for a convex, compact strategy space and continuous payoffs. Many of the models economists actually use do not have that: a firm's technology set can be discrete or irregular, and a payoff need only be upper semicontinuous, not continuous. Topkis [1979] showed that when a game's structure is instead order-theoretic — each player's strategies form a lattice, and the players' incentives reinforce each other in a precise sense — an equilibrium exists without any convexity or continuity assumption at all, and the proof method delivers something Kakutani's theorem cannot: a greatest and a least equilibrium point, with the whole equilibrium set forming a complete lattice. Zhou [1994] later showed the completeness of the equilibrium lattice in full generality; this mission formalizes the resulting theorem (Topkis's Theorem 4.2.1) together with its parametric extension (Theorem 4.2.2, established independently by Milgrom and Roberts [1990a] and Sobel [1988]), which shows how the greatest and least equilibria move as a parameter of the game — its technology, its cost structure — changes. This machinery underlies monotone comparative statics for games throughout economics: oligopoly models with strategic complements, coordination games, and search and matching models with increasing returns.

Setting

A noncooperative game $(N, S, \{f_i : i \in N\})$ consists of a finite player set $N$, a set $S \subseteq \mathbb{R}^m$ of feasible joint strategies $x = (x_i)_{i \in N}$ (allowing the set of strategies feasible for one player to depend on the others' choices, so $S$ need not be a product set), and a payoff function $f_i$ for each player $i$. Write $x_{-i}$ for the strategies of every player but $i$, $S_i(x_{-i})$ for the section of $S$ at $x_{-i}$ — player $i$'s feasible strategies given the others' choice — and $Y_i(x_{-i}) = \operatorname{argmax}_{y_i \in S_i(x_{-i})} f_i(y_i, x_{-i})$ for player $i$'s best-response set. The best joint response correspondence is $Y(x) = \prod_{i \in N} Y_i(x_{-i})$. A feasible $x'$ is an equilibrium point if $f_i(y_i, x'_{-i}) \le f_i(x')$ for every player $i$ and every feasible deviation $y_i \in S_i(x'_{-i})$ — no player can unilaterally improve.

A lattice is a partially ordered set in which every pair of elements has a join $\vee$ and a meet $\wedge$. A function $g$ is supermodular on a subset if $g(x) + g(y) \le g(x \vee y) + g(x \wedge y)$ for all $x, y$ in it, and has increasing differences in two of its arguments $(y,t)$ if $y \mapsto g(y, t'') - g(y, t')$ is monotone whenever $t' \prec t''$. A game $(N, S, \{f_i\})$ is a supermodular game if $S$ is a sublattice, $f_i(y_i, x_{-i})$ is supermodular in $y_i$ for every fixed $x_{-i}$ and every $i$, and $f_i(y_i, x_{-i})$ has increasing differences in $(y_i, x_{-i})$ for every $i$ — jointly, the conditions under which each player's own strategy components are complements and complementary to the other players' strategies (Theorem 2.6.1 of chunk 01-lattices/02-monotonicity's book).

Formalization targets

Goal — Theorem 4.2.1

If $(N, S, \{f_i\})$ is a supermodular game, $S$ is nonempty and compact, and each $f_i(y_i, x_{-i})$ is upper semicontinuous in $y_i$ on $S_i(x_{-i})$ for every $x_{-i}$ and every $i$, then

$$\{\text{equilibrium points of } (N, S, \{f_i\})\}$$

is nonempty, has a greatest and a least element, and, under the order it inherits from $\mathbb{R}^m$, is itself a nonempty complete lattice.

Theorem 4.2.2 (the parametric extension)

Let $T$ be a partially ordered set and, for each $t \in T$, $(N, S^t, \{f_i^t\})$ a supermodular game with $S^t$ nonempty, compact, and increasing in $t$; suppose each $f_i^t(y_i, x_{-i})$ is upper semicontinuous in $y_i$ and has increasing differences in $(y_i, t)$. Then for every $t$ there exist a greatest and a least equilibrium point of game $t$, and both are increasing functions of $t$ on $T$ — the equilibrium set moves monotonically as the parameter increases.

Two supporting results are formalized as milestones because Theorem 4.2.1's own proof uses them directly: Lemma 4.2.1 (equilibrium points are exactly the fixed points of the best joint response correspondence) and Lemma 4.2.2, parts (b) and (f) (the best joint response set is a nonempty compact sublattice for every feasible $x$, and the correspondence is increasing in $x$).

Significance

The result itself. Theorem 4.2.1 is the lattice-theoretic alternative to Nash/Kakutani existence: it needs no convexity of $S$ and no continuity of $f_i$ (upper semicontinuity suffices), and in exchange it delivers a greatest and a least equilibrium — with an explicit order-theoretic characterization via Theorem 2.5.1 of chunk 01-lattices — and the guarantee that the entire equilibrium set is a complete lattice, not merely nonempty. Theorem 4.2.2 gives this existence result teeth for applied comparative statics: it says that if a firm's cost structure, a market's demand parameter, or any other feature of the game increases (in the sense of the induced set order on $S^t$ and increasing differences in the payoffs), the extremal equilibria increase too — the qualitative content behind results such as "more competition leads to lower prices" in supermodular oligopoly models.

Formalizing it. The platform's existing Nash-equilibrium theorem (AGT.nash_existence, Theorem 1.8 of Algorithmic Game Theory) is a Brouwer/Kakutani argument for finite games with mixed strategies: it needs finiteness of every player's strategy set (so that mixed strategies form a compact convex simplex) and gives no lattice structure on the equilibrium set at all. Theorem 4.2.1 is a different technique entirely — it needs no finiteness, no mixing, and no convexity, and its conclusion (a complete lattice of equilibria) is exactly the content Brouwer/Kakutani cannot give. This mission is therefore not a restatement of Nash's theorem in different notation, but a second, independent existence technique with a strictly different structural payoff, formalized here for the first time on the platform. It builds directly on chunk 01-lattices's Theorem 2.5.1 (Zhou's fixed point theorem for increasing correspondences) and chunk 02-monotonicity's supermodularity/increasing differences definitions, both formalized earlier in this series.

Difficulty

The natural first idea for existence — "the best joint response correspondence has a fixed point by some general fixed-point theorem for correspondences" — needs the correspondence to be convex-valued and upper hemicontinuous for a Kakutani argument, neither of which supermodularity or upper semicontinuity alone supply: a best-response set under only upper semicontinuity can be a disconnected, non-convex set (e.g. the maximizers of a supermodular but non-quasiconcave function). The actual route goes through order instead of topology: Lemma 4.2.2 shows the best joint response set is a compact sublattice (hence subcomplete, by Theorem 2.3.1) and that the correspondence is increasing under the induced set order, which is exactly the hypothesis Theorem 2.5.1's non-constructive supremum/infimum construction needs — no convexity anywhere. A second subtlety, which the mission is careful not to elide: the equilibrium set of a supermodular game need be neither compact nor a sublattice of $\mathbb{R}^m$ when there are more than one player (Topkis's Examples 4.2.1 and 4.2.2 exhibit both failures); only the weaker claim — a complete lattice under the inherited order — is true in general, and that is what Theorem 2.5.1(b) supplies.

Formalization scope

A joint strategy is represented as a dependent function ∀ i, Fin (m i) → ℝ over a finite player type ι, with a player's own strategy accessed and overwritten via Function.update, so that $x_{-i}$ is never reified as a separate object — every statement about $f_i(y_i, x_{-i})$ or membership in $S_i(x_{-i})$ substitutes y for x's own i-th coordinate directly. IsSupermodularGame reuses chunk 02-monotonicity's SupermodularOn and IncreasingDifferencesOn verbatim, applied to each player's own payoff, rather than restating the supermodularity/increasing- differences conditions from scratch — a formalization that inlined a weaker, ad hoc notion here (e.g. supermodularity of the joint payoff vector rather than each player's own payoff in their own strategy) would trivialize the connection to chunk 02-monotonicity's theorems that the book's own proof relies on. Theorem 4.2.1's "nonempty complete lattice" conclusion is formalized, as in chunk 01-lattices, via IsLUB/IsGLB on the subtype of equilibrium points — never as membership of the ambient $\mathbb{R}^m$ supremum/infimum in the equilibrium set, which the book's own Examples 4.2.1–4.2.2 refute; a solution that instead proved the equilibrium set compact or a sublattice of $\mathbb{R}^m$ would be proving a strictly stronger and false claim. Only parts (b) and (f) of Lemma 4.2.2 are formalized, since those are the only two of its eight parts the proof of Theorem 4.2.1 uses; a complete development still needs chunk 01-lattices's Theorem 2.3.1 (subcomplete iff compact) and Theorem 2.5.1/2.5.2, and chunk 02-monotonicity's Theorem 2.8.1 and Corollary 2.7.1, none of which are restated here.

Selected references

• Topkis, D. M., Equilibrium points in nonzero-sum n-person submodular games, SIAM Journal on Control and Optimization 17(6), 1979, pp. 773–787. https://doi.org/10.1137/0317054
• Zhou, L., The set of Nash equilibria of a supermodular game is a complete lattice, Games and Economic Behavior 7(2), 1994, pp. 295–300. https://doi.org/10.1006/game.1994.1051
• 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
• Sobel, M. J., Isotone comparative statics for supermodular games, unpublished manuscript, 1988 (cited by Topkis [2011], Theorem 4.2.2).
• Topkis, D. M., Supermodularity and Complementarity, Princeton University Press, 2011 (DOI 10.1515/9781400822539), Chapter 4, §4.1–4.2.

Motivation

In the early twentieth century Agner Krarup Erlang worked for the Copenhagen Telephone Company and faced a sizing question that every shared-resource operator still faces: how many parallel circuits must a telephone link carry so that an arriving call is almost never turned away? The answer he published — the Erlang loss formula — is still the standard dimensioning tool for circuit-switched links, call centres, hospital beds, rental fleets, and any system in which a customer who finds every server occupied leaves rather than waits.

The formula is the first capstone of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), where it closes Chapter 1 and supplies the building block for the loss networks of Chapter 3. It is also the cleanest possible demonstration of the book's method: write down the transition rates of a Markov process, guess that the process is reversible, solve the detailed balance equations, and read the answer off the normalizing constant. This mission formalizes that chapter: the reversibility apparatus, the birth-and-death chain of the loss link, and Erlang's formula itself.

Setting

A link carries $C$ parallel circuits. Calls arrive as a Poisson process of rate $\lambda$ and each call, while it lasts, occupies one circuit for an exponentially distributed holding time of parameter $\mu$; holding times are independent of one another and of the arrival times. A call that arrives to find all $C$ circuits busy is lost — it does not queue.

Let $X(t)\in\{0,1,\dots,C\}$ be the number of busy circuits. Then $X$ is a Markov process with transition rates

$$q(j,j+1)=\lambda \quad (j=0,\dots,C-1), \qquad q(j,j-1)=j\mu \quad (j=1,\dots,C),$$

and $q(j,k)=0$ otherwise. A collection of numbers $\pi=(\pi(j))$ is in detailed balance with rates $q$ when

$$\pi(j)\,q(j,k)=\pi(k)\,q(k,j)\qquad\text{for all }j,k,$$

and satisfies the equilibrium (full balance) equations when

$$\pi(j)\sum_k q(j,k)=\sum_k \pi(k)\,q(k,j)\qquad\text{for all }j .$$

Detailed balance is the statement that, in equilibrium, transitions from $j$ to $k$ occur as frequently as transitions from $k$ to $j$. Writing $\nu=\lambda/\mu$ for the traffic intensity, Erlang's formula is

$$E(\nu,C)=\frac{\nu^{C}/C!}{\sum_{j=0}^{C}\nu^{j}/j!}.$$

Formalization targets

Goal — Erlang's formula

$$\pi \text{ in detailed balance with } q, \ \sum_{j=0}^{C}\pi(j)=1 \quad\Longrightarrow\quad \pi(C)=E\!\left(\tfrac{\lambda}{\mu},C\right).$$

The goal fixes no numerical constant: it says that whatever probability vector solves the detailed balance equations of the loss link assigns exactly $E(\nu,C)$ to the blocking state. The hypothesis is detailed balance rather than full balance, which is what the book's derivation actually uses and is the stronger assumption to discharge.

Supporting levels

$$\pi(j)=\frac{\nu^{j}}{j!}\,\pi(0), \qquad \sum_{j=0}^{C} j\,\pi(j)=\nu\bigl(1-E(\nu,C)\bigr), \qquad \frac{d}{d\nu}E(\nu,C)=-\bigl(1-E(\nu,C)\bigr)\bigl(E(\nu,C)-E(\nu,C-1)\bigr),$$

together with the reversibility results that justify the method: detailed balance implies full balance, the reversed process of Proposition 1.1 has rates $q'(j,k)=\pi(k)q(k,j)/\pi(j)$ and retains $\pi$ as an equilibrium distribution, and $q'=q$ holds exactly when $\pi$ and $q$ are in detailed balance.

Significance

The result itself. $E(\nu,C)$ is the blocking probability of the link, so it converts a traffic measurement $\nu$ and a target grade of service into a circuit count. It is insensitive: the same formula holds for any holding-time distribution with mean $1/\mu$, which is why it survives as an engineering tool far outside the exponential model that produces it here. Chapter 3 of the book builds loss networks on top of it, and the Erlang fixed point that approximates a whole network is a system of coupled copies of this one formula. The derivative identity is the ingredient that makes $E(\nu,C)$ tractable in optimization: it shows $E$ is increasing in $\nu$, and the recursion it encodes is how the formula is evaluated numerically without overflow.

Formalizing it. Nothing here is open mathematics; the value of the mission is a machine-checked statement of the loss model and a reusable reversibility layer. Mathlib has no theory of detailed balance or of reversible Markov processes over a countable state space, so this mission contributes the first: the predicates DetailedBalance and FullBalance, the reversed rate matrix, and the three structural facts relating them. Those are shared by every later mission in this series — the migration processes of Chapter 2 and the loss networks of Chapter 3 are all proved reversible or quasi-reversible by exactly these means.

Difficulty

The obvious route to $\pi(C)$ is to solve the equilibrium equations directly, and for a birth-and-death chain that is a three-term recursion whose general solution needs two boundary conditions. Detailed balance replaces it with a two-term recursion and one boundary condition, and the whole content of the reversibility section is that the substitution is legitimate. The remaining work is bookkeeping that Lean makes less forgiving than the page does: the detailed balance equations must be indexed so that the $j=0$ and $j=C$ boundaries are not silently assumed away, the normalizing sum must be shown positive before it can be inverted, and the induction that produces $\nu^{j}/j!$ has to carry the Fin (C+1) index through Nat.factorial. For the derivative identity, the naive differentiation of a quotient gives $\left(\sum_{j\le C-1}\nu^{j}/j!\right)$ in the numerator, and recognizing it as $\bigl(1-E(\nu,C)\bigr)$ times the denominator is the step that produces the stated form.

Formalization scope

The state space is Fin (C + 1), so the link with $C$ circuits has $C+1$ states and finiteness is built in; $\pi$ is a plain function Fin (C + 1) → ℝ constrained by hypotheses rather than a PMF, so that the normalization $\sum_j \pi(j) = 1$ appears explicitly wherever it is used. FullBalance is written with unconditional sums (tsum) over an arbitrary state space, so the same predicate serves the countable chains of later chapters; over a Fintype it is the finite sum. Rates are real-valued and q j j = 0 by construction, matching the book's convention that a Markov process must change state when it jumps.

The rates carry $\lambda,\mu>0$ as hypotheses. This rules out the degenerate reading in which $\mu = 0$ makes every downward rate vanish: with $\mu=0$ the detailed balance equations force $\pi(j)\lambda = 0$ for $j<C$, so the only normalized solution is the point mass at $C$, and $\pi(C)=1$ while Lean evaluates $E(\lambda/0,C)=E(0,C)=0$ for $C\ge1$; the goal would be false. Erlang's formula is stated for the last state Fin.last C, not for an unconstrained index, so it cannot be satisfied by a degenerate reindexing.

Contributions welcome beyond the listed items: the insensitivity of $E(\nu,C)$ to the holding time distribution, the recursion $E(\nu,C)=\nu E(\nu,C-1)/(C+\nu E(\nu,C-1))$, the finite-source variant $\pi_M(j)\propto\binom{M}{j}(\eta/\mu)^{j}$ and the PASTA statement that an arriving call in that model sees $\pi_{M-1}$, and the parking-space identity $\sum_{C\ge 0}E(\nu,C)$ of Exercise 1.9.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 1 (pp. 13–21), equations (1.2), (1.4), (1.5), Proposition 1.1, Exercises 1.7 and 1.8. DOI 10.1017/cbo9781139565363
• A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektrotkeknikeren 13 (1917), 5–13.
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapter 1.
• J. R. Norris, Markov Chains, Cambridge University Press, 1998. DOI 10.1017/CBO9780511810633

Motivation

A queueing network is a collection of service stations through which customers — jobs, packets, telephone calls, patients — move one at a time. The state of such a network is a vector of occupancy counts, one per station, and the number of states grows exponentially in the number of stations, so solving the equilibrium equations directly is hopeless for any network worth modelling. The product form is what rescues the subject: for a large and identifiable class of networks the equilibrium distribution factorizes into one term per station, as if the stations were independent, and a network of $J$ stations costs $J$ one-dimensional calculations instead of one exponentially large one.

Chapter 2 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) establishes this for migration processes, the Markov model in which individuals move between colonies one at a time at a rate that factorizes as $\lambda_{jk}\varphi_j(n_j)$: a part depending only on the two colonies and a part depending only on the occupancy of the source. The class covers single-server and $s$-server queues, infinite-server queues, and networks of them, open or closed.

Setting

There are $J$ colonies, and a state is a vector $n = (n_1,\dots,n_J)$ of non-negative integers, $n_j$ being the number of individuals in colony $j$. Three operators move one individual:

$$T^{jk}n \ \text{ moves one from } j \text{ to } k, \qquad T^{j\to}n \ \text{ removes one from } j, \qquad T^{\to k}n \ \text{ adds one to } k .$$

An open migration process is the Markov process on $\mathbb{Z}_+^J$ with transition rates

$$q(n, T^{jk}n)=\lambda_{jk}\varphi_j(n_j), \qquad q(n, T^{j\to}n)=\mu_j\varphi_j(n_j), \qquad q(n, T^{\to k}n)=\nu_k ,$$

where $\varphi_j(0)=0$: nothing leaves an empty colony. Immigration into colony $k$ is Poisson of rate $\nu_k$. Taking $\mu\equiv 0$ and $\nu\equiv 0$ and restricting to states of a fixed total $\sum_j n_j = N$ gives a closed migration process. Setting $\varphi_j(n)=\min(n,s)$ models an $s$-server queue at colony $j$; $\varphi_j(n)=n$ models individuals moving independently.

The traffic equations define $(\alpha_j)$ from the rates. In the open case they are

$$\alpha_j\Bigl(\mu_j+\sum_k \lambda_{jk}\Bigr) \;=\; \nu_j+\sum_k \alpha_k\lambda_{kj}, \qquad j = 1,\dots,J,$$

and in the closed case $\alpha_j\sum_k \lambda_{jk}=\sum_k \alpha_k\lambda_{kj}$ with $\alpha_j>0$ and $\sum_j\alpha_j=1$. Finally set

$$g_j=\sum_{n=0}^{\infty}\frac{\alpha_j^{\,n}}{\prod_{r=1}^{n}\varphi_j(r)} .$$

Formalization targets

Goal — Theorem 2.8, the product form of an open migration process

If $g_1,\dots,g_J<\infty$ then

$$\pi(n)=\prod_{j=1}^{J}\pi_j(n_j), \qquad \pi_j(m)=g_j^{-1}\,\frac{\alpha_j^{\,m}}{\prod_{r=1}^{m}\varphi_j(r)}$$

is an equilibrium distribution: it satisfies the equilibrium equations for the open migration rates, and it sums to one over $\mathbb{Z}_+^J$. Both halves are asserted, because the first alone is satisfied by every positive multiple of $\pi$ and the second is what makes the convergence hypothesis $g_j<\infty$ do work.

Supporting levels

The closed-network product form of Theorem 2.4; the two families of partial balance equations (2.3) and (2.4) that the proof reduces to; Theorem 2.9, that the time reversal of a stationary open migration process is again an open migration process with rates $\lambda'_{jk}=\alpha_k\lambda_{kj}/\alpha_j$, $\mu'_j=\nu_j/\alpha_j$ and $\nu'_k=\alpha_k\mu_k$; the single M/M/1 queue that the chapter starts from; the cycle identity (2.6) behind Little's law; and the traffic equations of Kendall's family-size process, an open migration process with infinitely many colonies.

Significance

The result itself. Theorem 2.8 says that at a fixed time the occupancies $n_1,\dots,n_J$ of an open migration network are independent, each distributed as if its colony were fed by a Poisson stream of rate $\alpha_j\lambda_j$ — even though the actual arrival stream into a colony is in general not Poisson, and the occupancies are emphatically not independent as processes. That gap between the one-time-marginal and the process is the reason the theorem is useful and the reason it is easy to misapply. Everything downstream in the book rests on it: the loss networks of Chapter 3 are the truncation of a product-form process to a capacity set, and the flow-level models of Chapter 8 ask when a product form survives a bandwidth-sharing policy. Theorem 2.9 supplies the reversibility argument from which Burke's theorem and the Poisson character of the exit streams follow.

Formalizing it. The mathematics is classical — Jackson (1957), Whittle (1968), Kelly (1979) — and none of it is open. What the mission produces is a machine-checked model of a queueing network: the migration operators, the rate matrix, the traffic equations and the product form, in a form later missions in this series import rather than restate. Mathlib has no queueing theory and no theory of continuous-time Markov chains on a countable state space, so this is the first such development. It builds on the DetailedBalance / FullBalance layer published in mission I.

Difficulty

An open migration process is not reversible — the detailed balance equations fail, as Figure 2.5 of the book shows with an arrival stream of geometrically sized bursts — so the method of Chapter 1 does not apply and the equilibrium equations must be met head on. The content of the proof is that they split: a separate balance holds for each colony $j$ (rate of individuals leaving colony $j$ equals rate arriving into it) and one more across the boundary with the outside world, and each of those is equivalent to a traffic equation. Finding that split is the step, and it is why the partial balance equations are milestones in their own right.

The formal obstacle is different and worth naming. The equilibrium equation at a state $n$ sums over the states that can jump into $n$, and the naive transcription $\sum_{j,k}\pi(T^{jk}n)q(T^{jk}n,n)$ silently assumes $T^{jk}n$ is a state, which fails when $n_j=0$. Over $\mathbb{Z}_+^J$ such a term must be dropped, and a formalization that keeps it — with $n_j-1$ read as truncated subtraction — states something false.

Formalization scope

The state space is Fin J → ℕ, a function from a finite index type of colonies to occupancy counts, with J finite; no irreducibility is assumed, since none of the statements below need it. Rates are real-valued and the whole rate matrix is a single function of two states, assembled as a sum of indicator terms over the possible transitions, so the equilibrium equations can be stated as the FullBalance predicate of mission I, with unconditional sums over the countable state space. This is what avoids the trap above: a sum over actual states never includes a would-be-negative one, and any spurious coincidence of operators at a boundary carries a $\varphi_j(0)=0$ factor and contributes nothing.

Conventions the development commits to: $\lambda_{jj}=0$, so a transfer is always between distinct colonies; $\varphi_j(0)=0$ and $\varphi_j(r)>0$ for $r\ge 1$; $\alpha_j>0$; and $g_j$ is asserted via HasSum, which states convergence and the value at once, rather than as an extended real that might be infinite. Occupancy vectors use truncated natural subtraction, so the partial balance and reversed-rate statements carry an explicit $n_j\ge 1$ where the book's state space carries it implicitly; the goal itself does not need such a guard.

A trivializing formalization is ruled out by the second conjunct of the goal: the equilibrium equations alone are a homogeneous linear condition satisfied by $\pi\equiv 0$, whereas the requirement that $\pi$ sum to $1$ forces the constants $g_j$ to be exactly the ones stated.

Contributions welcome beyond the listed items: Burke's theorem (2.1) and the Poisson character of the exit streams, Corollary 2.10, the closed-form of the telephone banking example (Exercise 2.6), the Chinese restaurant process of Exercise 2.13, and Bartlett's theorem (2.17) on linear migration processes over a general space.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 2 (pp. 22–48); Theorems 2.4, 2.8, 2.9, 2.13, equations (2.1)–(2.6). DOI 10.1017/cbo9781139565363
• James R. Jackson, Networks of waiting lines, Operations Research 5 (1957), 518–521. DOI 10.1287/opre.5.4.518
• P. Whittle, Equilibrium distributions for an open migration process, Journal of Applied Probability 5 (1968), 567–571. DOI 10.2307/3211921
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapters 2 and 3.
• David G. Kendall, Some problems in mathematical genealogy, in Perspectives in Probability and Statistics (J. Gani, ed.), Academic Press, 1975, 325–345.
• John D. C. Little, A proof for the queuing formula: $L = \lambda W$, Operations Research 9 (1961), 383–387. DOI 10.1287/opre.9.3.383

Motivation

Erlang's formula, the subject of mission I of this series, sizes a single telephone link. Real networks are not single links: a call occupies a circuit on every link of its route simultaneously, and it is lost unless every one of those links has a free circuit. That is the loss network, the model of Chapter 3 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), and it describes not only circuit-switched telephony but any system in which a request must acquire several resources at once or be refused: wavelength assignment in optical networks, radio channel allocation under interference constraints, slot booking, and admission control generally. The term used in those application areas is circuit-switched: before a request is accepted it is checked that enough resource is available for each stage of it.

The exact equilibrium distribution of a loss network is known and has product form. It is also useless for computation — its normalizing constant is a sum over the feasible states, and for a general resource matrix computing it is NP-hard. What practitioners use instead is the Erlang fixed point: pretend the links block independently, so that the traffic offered to link $j$ is the traffic on the routes through it thinned by the blocking probability of every other link on each route, and then apply Erlang's formula link by link. The result is a system of coupled copies of Erlang's formula. The chapter's aim, in its own words, is to give insight into why that approximation works as well as it does; the first step is to show that it is well posed at all.

Setting

The links are $\mathcal{J} = \{1,\dots,J\}$, link $j$ carrying $C_j$ circuits. A route $r$ belongs to a set $\mathcal{R}$ of $R$ routes, and the link-route incidence matrix $A$ records how much of each link a route needs: a call on route $r$ requires $A_{jr}$ circuits from link $j$ and is lost if any link has fewer than $A_{jr}$ free. (The classical case is $A$ a $0$–$1$ matrix and $A_{jr}=1$ exactly when $j\in r$; from section 3.3 the book allows any non-negative integers.)

Calls requesting route $r$ arrive as a Poisson process of rate $\nu_r$, independently across routes, and hold their circuits for an exponentially distributed time of unit mean. Writing $n_r$ for the number of calls in progress on route $r$, the process $n=(n_r)$ is Markov on

$$S(C)=\{n\in\mathbb{Z}_+^{R} : An\le C\},$$

and is called a loss network with fixed routing.

Write $E(\nu,C)$ for Erlang's formula, $E(\nu,C)=\dfrac{\nu^{C}/C!}{\sum_{j=0}^{C}\nu^{j}/j!}$, published in mission I of this series. The Erlang fixed point equations are

$$E_j \;=\; E\!\left((1-E_j)^{-1}\sum_r A_{jr}\,\nu_r\prod_i (1-E_i)^{A_{ir}},\; C_j\right), \qquad j=1,\dots,J. \tag{3.7}$$

The factor $(1-E_j)^{-1}$ removes link $j$'s own thinning from the product, so in the $0$–$1$ case the argument is $\sum_{r\ni j}\nu_r\prod_{i\in r\setminus\{j\}}(1-E_i)$, the reduced load offered to link $j$.

Formalization targets

Goal — Theorem 3.20, existence and uniqueness of the Erlang fixed point

$$\exists!\,(E_1,\dots,E_J)\in[0,1]^J \text{ satisfying } (3.7).$$

The goal fixes no formula for $E$ and no rate of convergence: it asserts only that the approximation the field has used since the 1960s names a single, well-defined object. Existence alone is a short argument from Brouwer's theorem, since (3.7) defines a continuous self-map of the compact convex cube $[0,1]^J$; uniqueness is the substance.

Supporting levels

The exact theory that the fixed point approximates: Lemma 3.4 on truncating a reversible process; the uncapacitated network as an instance of the open migration product form of mission II; equation (3.3), the exact equilibrium distribution $\pi(n)=G(C)\prod_r \nu_r^{n_r}/n_r!$ on $S(C)$; and the acceptance probability $1-L_r=G(C)/G(C-Ae_r)$. Then the optimization side: that $E(\nu,C)$ and the utilization $\nu(1-E(\nu,C))$ are strictly increasing in $\nu$, which is what makes the revised dual objective strictly convex; and Theorem 3.10, that a minimizer of the Dual problem (3.5) over the positive orthant satisfies the conditions on $B$, equation (3.6).

Significance

The result itself. Without Theorem 3.20 the phrase "the Erlang fixed point" is not well formed, and neither is any engineering procedure that computes one — repeated substitution converges to a solution, and damped iteration is guaranteed to converge to one, but "the blocking probabilities predicted by the reduced-load approximation" names a unique vector only because of this theorem. The proof is also the interesting part: the fixed point equations are re-read as the stationary conditions of a strictly convex minimization, the revised dual (3.8), which is the Dual problem (3.5) of the maximum-probability analysis with its linear term replaced by $\int_0^{y_j}U(z,C_j)\,dz$. That connection is what later lets the book prove the approximation asymptotically exact in a limiting regime: Corollary 3.22 says the Erlang fixed point converges to the vector $B$ coming from the maximum-probability problem.

Formalizing it. Nothing here is open. What the mission produces is the loss network model in Lean — state space, truncated rates, normalizing constant, incidence matrix — and a machine-checked statement of the object the reduced-load approximation computes. It is also where this series' earlier missions pay off: the uncapacitated network is literally the open migration process of mission II with $\lambda\equiv 0$, $\mu\equiv 1$, $\varphi_j(n)=n$, and the exact distribution (3.3) is its truncation by Lemma 3.4 to the feasible set, using the DetailedBalance layer of mission I. Mathlib has no loss network theory and no Erlang formula beyond what mission I published.

Difficulty

Existence of a fixed point is easy and is not where the difficulty lies. Uniqueness resists every direct attack: the map defined by (3.7) is not a contraction in any obvious metric, its monotonicity structure is not the kind that forces a unique fixed point, and iterating it undamped can cycle. The book's route is indirect — exhibit a strictly convex function whose stationary conditions are exactly (3.7) — and finding that function is the whole content. Its strict convexity comes from a monotonicity fact about Erlang's formula, that the utilization $\nu\bigl(1-E(\nu,C)\bigr)$ is strictly increasing in $\nu$, which is itself a milestone here.

A second, formal difficulty: the equations involve $(1-E_j)^{-1}$, so a solution with $E_j=1$ would be meaningless. It is worth checking before starting that no such solution exists for $C_j\ge 1$, rather than assuming it.

Formalization scope

Routes and links are indexed by finite types, the incidence matrix has natural-number entries (the general case of section 3.3, not only $0$–$1$), capacities are natural numbers, and arrival rates are positive reals. The feasible set $S(C)$ is a subset of the state space, and a truncated process is the rate matrix restricted to that subset — which is exactly the book's truncation, since a transition leaving the set simply has no target.

Conventions: holding times have unit mean throughout, matching the book, so the departure rate from route $r$ is $n_r$ and no separate service-rate parameter appears. Normalizing constants are introduced through summability hypotheses that assert convergence and the value together, rather than as possibly-infinite quantities; $G(C)$ is the reciprocal of the sum in the book's notation. Capacities are assumed at least $1$ in the goal: a link with no circuits blocks everything, $E(\nu,0)=1$ identically, and the factor $(1-E_j)^{-1}$ would then be undefined rather than merely large.

The goal cannot be satisfied trivially: it is a uniqueness statement, so a vacuous or degenerate reading would have to produce no solution, and existence is half of what is asserted.

Contributions welcome beyond the listed items: the Brouwer argument for existence of a solution to the $0$–$1$ equations (3.1) of section 3.2; the utilization function $U(y,C)$ and the revised dual (3.8); the central limit theorem 3.14 and Corollary 3.17; Lemma 3.21 and Corollary 3.22 on the limiting regime; and the diverse-routing models of section 3.7.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 3 (pp. 49–82); Lemma 3.4, equation (3.3), Theorems 3.10 and 3.20, equations (3.1), (3.5)–(3.9). DOI 10.1017/cbo9781139565363
• F. P. Kelly, Loss networks, Annals of Applied Probability 1 (1991), 319–378. DOI 10.1214/aoap/1177005872
• F. P. Kelly, Blocking probabilities in large circuit-switched networks, Advances in Applied Probability 18 (1986), 473–505. DOI 10.2307/1427303
• R. B. Cooper and S. Katz, Analysis of alternate routing networks with account taken of the nonrandomness of overflow traffic, Bell Telephone Laboratories memorandum, 1964.
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapter 1 on truncation.

Motivation

A network of resistors solves an optimization problem. Nobody tells the electrons what to do; each one moves under a purely local rule, and the current distribution that emerges minimizes energy dissipation over all distributions satisfying Kirchhoff's node law. Add a wire and the network can only become easier to traverse. This is the encouraging case, and Chapter 4 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) opens with it.

Road traffic is the discouraging case. Drivers also follow a local rule — take the fastest route — and the pattern that emerges is again characterized by an optimization problem, but not the one anyone wants solved. Braess's paradox is the sharp form of the discrepancy: in a small road network carrying six cars per unit time, every route takes 83 time units at equilibrium; open an extra road, and at the new equilibrium every route takes 92. Building road capacity made everyone slower. The difference from the electrical case is that a driver's choice imposes a delay on everyone else sharing the road and the driver does not pay for it, and correcting that — pricing the externality — is how a decentralized rule can be made to produce good global behaviour. That idea recurs in Chapters 7 and 8 of the book as the basis of Internet congestion control.

Setting

The network is a set $\mathcal{J}$ of $J$ directed links. A route $r$ is a subset of links, and $\mathcal{R}$ is the set of $R$ routes under consideration — not necessarily all physically possible ones. The link-route incidence matrix $A$ has $A_{jr}=1$ when $j \in r$ and $A_{jr}=0$ otherwise. Writing $x_r$ for the flow on route $r$, the flow on link $j$ is

$$y_j=\sum_{r}A_{jr}x_r, \qquad\text{that is } y = Ax.$$

Each link has a delay function $D_j(y_j)$, continuous and increasing in the flow on that link, and the delay along a route is the sum of the delays of its links, $\sum_j D_j(y_j)A_{jr}$. Drivers care only about getting from origin to destination: $\mathcal{S}$ is the set of source–destination pairs, each route $r$ serves exactly one of them, written $s(r)$, and the flow requirement between pair $\sigma$ is $f_\sigma$.

A routing pattern is stable when no driver has an incentive to switch. Definition 4.2 makes this precise: a Wardrop equilibrium is a feasible vector of route flows $x$ such that

$$x_r>0 \;\Longrightarrow\; \sum_{j}D_j(y_j)A_{jr}=\min_{r'\in s(r)}\sum_{j}D_j(y_j)A_{jr'}, \qquad y = Ax .$$

Every route actually carrying traffic is a shortest route, in delay, for the traffic it carries.

Formalization targets

Goal — Theorem 4.3, a Wardrop equilibrium exists

$$\exists\, x \ge 0 \ \text{ with } Hx=f \ \text{ such that } x \text{ is a Wardrop equilibrium.}$$

The goal asserts existence only, for an arbitrary network, arbitrary route set and arbitrary continuous increasing delay functions. It fixes no uniqueness claim, because the equilibrium flows need not be unique even though the link loads are, and no efficiency claim, because Braess's paradox is precisely the statement that the equilibrium is not efficient.

Supporting levels

Kirchhoff's node law as the equations satisfied by the expected reward in the random-walk game of section 4.1; the two Braess networks of Figures 4.4a and 4.4b, with their equilibrium delays $83$ and $92$; convexity of $\int_0^{y}D(u)\,du$ for increasing $D$; the optimization characterization that makes the goal reachable — a minimizer of $\sum_j\int_0^{y_j}D_j(u)\,du$ over the feasible flows is a Wardrop equilibrium; and the exact externality decomposition of the queueing network of section 4.3.1.

Significance

The result itself. Theorem 4.3 is what makes the Wardrop equilibrium a usable object: a traffic model that could fail to have an equilibrium would be describing nothing. Its proof does more than establish existence — it identifies the equilibrium as the solution of a specific convex program, minimizing $\sum_j\int_0^{y_j}D_j(u)\,du$. That function is not the total delay $\sum_j y_jD_j(y_j)$, and the gap between the two is exactly Braess's paradox: selfish routing optimizes the wrong objective. Once the two objectives are written side by side, the fix is readable off them, and it is the fix used in practice — a toll on link $j$ equal to $y_jD_j'(y_j)$, the marginal delay a driver imposes on everyone else, makes the selfish objective coincide with the social one. Section 4.3 then carries the same accounting into queueing and loss networks, where the derivative of the mean cost splits into a term for the delay a customer suffers and a term for the knock-on cost it inflicts.

Formalizing it. Nothing here is open; Wardrop stated the principle in 1952 and Beckmann, McGuire and Winsten gave the optimization formulation in 1956. What the mission produces is a machine-checked model of selfish routing — incidence matrix, link flows, delay functions, the equilibrium condition — and a formal record of Braess's paradox as a concrete pair of networks rather than a story. Mathlib has no traffic or congestion-game theory.

Difficulty

Existence is not a fixed-point argument in the obvious variable: the best-response map of the routing game is not continuous, since a small change in flows can flip which route is shortest and move all the traffic. The book's route is to replace the equilibrium condition by the stationarity conditions of a convex program on a compact feasible set, where existence is routine and the content is the translation. The translation is where the care is needed, and it is stated here as a separate milestone: the first-order conditions say the Lagrange multiplier $\lambda_{s(r)}$ equals the route delay on routes carrying traffic and is a lower bound on the others, which is Definition 4.2 restated.

The subtlety worth naming in advance is that "increasing" is doing real work in two different places. It makes $\int_0^{y}D(u)\,du$ convex, which is what makes the program tractable; and it is what makes each $D_j(y_j)$ interpretable as a price. Neither convexity of $D_j$ itself nor strict monotonicity is needed, and assuming them would be assuming more than the book does.

Formalization scope

Links, routes and source–destination pairs are indexed by finite types. The incidence matrix is real-valued with entries constrained to be $0$ or $1$, matching the book's definition in this chapter (unlike Chapter 3, which allows general non-negative integers). The map from routes to source–destination pairs is given as a function $s$ rather than as the matrix $H$, which is exactly the book's statement that each column of $H$ sums to $1$.

Delay functions are total functions $\mathbb{R}\to\mathbb{R}$, continuous and monotone. This excludes the vertical asymptote that Figure 4.5 permits — a link with a finite capacity at which delay blows up — and that restriction is recorded here rather than left implicit. The equilibrium condition is stated as the inequality "$\text{delay on } r \le \text{delay on } r'$ for every $r'$ serving the same pair", which is Definition 4.2 with the minimum written out; the two are equivalent because $r$ itself serves $s(r)$, and the inequality form avoids having to produce a minimum over a possibly empty set.

The goal is not vacuous: the feasibility hypotheses ($f_\sigma\ge0$, and each source–destination pair served by at least one route) are exactly what makes the feasible set non-empty, and without them the existence claim would be false rather than trivial.

Contributions welcome beyond the listed items: uniqueness of the equilibrium link loads $y$; the marginal-cost toll that aligns the selfish and social optima; Rayleigh monotonicity (Exercise 4.3, that effective resistance does not decrease when a resistance is increased); the price of anarchy for affine delays; and Theorem 4.6 on the derivatives of the loss-network rate of return with respect to offered traffic and capacity.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 4 (pp. 85–107); Definition 4.2, Theorem 4.3, sections 4.1–4.3. DOI 10.1017/cbo9781139565363
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1 (1952), 325–362. DOI 10.1680/ipeds.1952.11259
• M. Beckmann, C. B. McGuire and C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956.
• D. Braess, Über ein Paradoxon aus der Verkehrsplanung, Unternehmensforschung 12 (1968), 258–268. DOI 10.1007/BF01918335
• Peter Doyle and J. Laurie Snell, Random Walks and Electric Networks, Mathematical Association of America, 1984. arXiv:math/0001057
• R. G. Gallager, A minimum delay routing algorithm using distributed computation, IEEE Transactions on Communications 25 (1977), 73–85. DOI 10.1109/TCOM.1977.1093711

Motivation

When many stations share one broadcast channel, something has to decide who transmits. A token passed around the stations works when there are few of them and none is silent for long, but it scales badly and breaks if the token is lost. The alternative is to let stations transmit whenever they like and use randomness to recover from the resulting collisions. That is the design of ALOHA, built in the 1970s to connect terminals across the Hawaiian islands, and of Ethernet, and of essentially every contention-based access protocol since.

Chapter 5 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) asks what such protocols can achieve, and the answers are largely negative. ALOHA with a fixed retransmission probability jams: with probability one there is a finite random time after which every slot contains a collision and no packet ever succeeds again, for every positive arrival rate. Ethernet's binary exponential backoff does better, but only just: it has a positive critical arrival rate, above which only finitely many packets are ever transmitted, and it is still not positive recurrent at rates where it does transmit infinitely many. The chapter's general statement is the one this mission targets: any backoff slower than exponential jams at every positive arrival rate.

Setting

Time is slotted, and a transmission attempt occupies exactly one slot. New packets arrive in a Poisson stream of rate $\nu$, so the number arriving in a slot is Poisson with mean $\nu$. A slot in which exactly one station transmits carries its packet successfully; a slot in which two or more transmit is a collision and carries nothing.

In an acknowledgement-based scheme a station learns nothing about the channel except whether its own transmissions succeeded. A packet arriving in slot $t$ attempts transmission in slots $t+x_0, t+x_1, \dots$ with $1 = x_0 < x_1 < \cdots$, the sequence chosen independently for each packet, and

$$h(x) = \mathbb{P}(x \in X), \qquad h(1) = 1$$

is the retransmission function. For ALOHA, $h(x) = f$ for every $x > 1$; for Ethernet's binary exponential backoff, $\sum_{r \le t} h(r) \sim \log_2 t$.

Now imagine the channel externally jammed from time $0$, so that every retransmission actually occurs. The attempts in slot $t$ are then Poisson with mean $\nu\sum_{r=1}^{t}h(r)$, and the probability that fewer than two attempts are made in slot $t$ is

$$P_t=\Bigl(1+\nu\sum_{r=1}^{t}h(r)\Bigr)\exp\Bigl(-\nu\sum_{r=1}^{t}h(r)\Bigr).$$

The expected number of such slots is $H(\nu)=\sum_{t\ge1}P_t$, which is decreasing in $\nu$, and the critical rate is

$$\nu_c=\inf\{\nu : H(\nu)<\infty\}.$$

Theorem 5.11 of the book says $\nu_c$ deserves its name: below it infinitely many packets are transmitted with probability one, above it only finitely many.

Formalization targets

Goal — condition (5.7): slower-than-exponential backoff has $\nu_c=0$

$$\frac{1}{\log t}\sum_{x=1}^{t}h(x)\longrightarrow\infty \quad\Longrightarrow\quad H(\nu)=\sum_{t\ge1}P_t<\infty \ \text{ for every } \nu>0 .$$

Since $H(\nu)<\infty$ for every positive $\nu$, the critical rate is $\nu_c=0$, and by Theorem 5.11 the expected number of successful transmissions is finite at every positive arrival rate. The goal fixes no constant and no rate: it says only that the dividing line between "jams always" and "has a positive capacity" sits at logarithmic growth of $\sum_{x\le t}h(x)$, which is exponential growth of the backoff.

Supporting levels

The ALOHA drift calculation of section 5.1 and its consequence that the drift is positive once the backlog is large enough; the summability $\sum_n p(n)<\infty$ that combines with Borel–Cantelli to give Proposition 5.3; the monotonicity of $P_t$ in $\nu$; the opposite extreme, that a scheme with $\sum_x h(x)<\infty$ — one that gives up on a packet after finitely many attempts — has $\nu_c=\infty$; that ALOHA's own retransmission function satisfies condition (5.7); and the bound of Remark 5.14, that a positive recurrent acknowledgement-based scheme needs $\nu\le e^{-\nu}$ and hence $\nu<0.5672$, which is strictly below Ethernet's $\nu_c=\log 2$.

Significance

The result itself. Condition (5.7) is the chapter's structural statement about random access, and it is a sharp one. Any retransmission rule under which a packet keeps trying at a rate that does not decay fast enough — a fixed probability, a polynomially growing backoff, anything short of exponential — has critical rate zero: the channel jams at every positive load. Exponential backoff is not a tuning choice, it is the minimum that makes the protocol work at all, and the $\log b$ formula for a backoff by factor $b$ (Exercise 5.7) then says how much capacity each choice of $b$ buys. The gap recorded in Remark 5.14 is the other half of the picture: even above the threshold, "infinitely many packets get through" is much weaker than "the backlog is stable", and between $0.567$ and $\log 2 \approx 0.693$ Ethernet does the first and provably not the second.

Formalizing it. None of this is open; the analysis is due to Kelly and MacPhee (1987) and Aldous (1987). What the mission contributes is a machine-checked account of the analytic core: the definitions of $P_t$, $H(\nu)$ and $\nu_c$, the two extremes of the classification, and the ALOHA calculations. Mathlib has no protocol analysis and nothing about random access channels.

Difficulty

The obstacle is a modelling one and it is worth stating plainly rather than discovering halfway through. The chapter's headline results — Proposition 5.3 that ALOHA jams almost surely, Theorem 5.11 that $\nu_c$ is the critical rate, Theorem 5.15 that geometric Ethernet is transient — are statements about sample paths of a Markov chain built on a Poisson arrival stream, and their proofs are coupling arguments comparing a system started empty with one started with a backlog. Nothing in Mathlib supports that construction, and building it is a research-scale project rather than a chapter. This mission therefore formalizes the analytic half and quotes the probabilistic half, which is the same division the book itself makes when it computes $\nu_c$ for a scheme: Theorem 5.11 is proved once, and every subsequent statement about a protocol is a convergence question about $\sum_t P_t$.

Within that analytic half the difficulty is real but ordinary. The summand $P_t$ is a product of a factor growing with $\sum_{r\le t}h(r)$ and one decaying exponentially in it, so the growth hypothesis has to be turned into a summable bound without assuming any regularity of $h$ beyond non-negativity — in particular $\sum_{r\le t}h(r)$ need not be eventually monotone in any useful quantitative sense, only divergent faster than $\log t$.

Formalization scope

The retransmission function is any non-negative real sequence; the normalization $h(1)=1$ is not imposed, since none of the statements need it and imposing it would exclude the comparison schemes. $P_t$ and the partial sums are real-valued, and "$H(\nu)<\infty$" is stated as summability of the sequence rather than as a bound on an extended-real sum, so convergence is asserted rather than assumed. The goal is stated for each fixed $\nu>0$ separately, which is what makes $\nu_c=0$; it is not stated as a claim about the infimum, because the infimum of the set $\{\nu : H(\nu)<\infty\}$ adds nothing once the set is known to be all of $(0,\infty)$.

The growth hypothesis is the book's condition (5.7) verbatim: $\bigl(\log t\bigr)^{-1}\sum_{x\le t}h(x)\to\infty$. Note that at $t=0$ and $t=1$ the quotient involves $\log t \le 0$ and is not meaningful; divergence to infinity is an eventual statement, so this costs nothing, but it is why the hypothesis is a limit rather than a pointwise bound.

The mission is not vacuous in either direction: the ALOHA milestone exhibits a retransmission function satisfying the hypothesis, and the $\sum_x h(x)<\infty$ milestone exhibits one that fails it as strongly as possible, with $H(\nu)=\infty$ for every $\nu$.

Contributions welcome beyond the listed items: Ethernet's $\sum_{r\le t}h(r)\sim\log_2 t$ and the resulting $\nu_c=\log 2$; the generalization $\nu_c=\log b$ of Exercise 5.7; the scheme $h(x)=1/(x\log x)$ with $\nu_c=\infty$; the continuous-time halving $\nu_c=\frac12\log b$ of Kelly and MacPhee; and, for anyone willing to build the probabilistic layer, Proposition 5.3 and Theorem 5.11 themselves.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 5 (pp. 108–132); Definition 5.1, Proposition 5.3, Theorems 5.11 and 5.15, condition (5.7), Examples 5.8, 5.12 and 5.13, Remark 5.14. DOI 10.1017/cbo9781139565363
• N. Abramson, The ALOHA system — another alternative for computer communications, AFIPS Conference Proceedings 37 (1970), 281–285. DOI 10.1145/1478462.1478502
• F. P. Kelly and I. M. MacPhee, The number of packets transmitted by collision detect random access schemes, Annals of Probability 15 (1987), 1557–1568. DOI 10.1214/aop/1176991992
• D. J. Aldous, Ultimate instability of exponential back-off protocol for acknowledgement-based transmission control of random access communication channels, IEEE Transactions on Information Theory 33 (1987), 219–223. DOI 10.1109/TIT.1987.1057295
• R. M. Metcalfe and D. R. Boggs, Ethernet: distributed packet switching for local computer networks, Communications of the ACM 19 (1976), 395–404. DOI 10.1145/360248.360253