The OR Formalization Drive

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

Motivation

When a file is transferred over the Internet, no part of the network decides how fast it should go. The machines inside the network forward packets; when a resource is heavily loaded it drops or marks one; the destination reports that to the source; and the source slows down, then gradually speeds up again until the next signal. This end-to-end cycle of increase and decrease is TCP, and it is the mechanism by which the Internet discovers available capacity and divides it among competing flows.

Chapter 7 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) asks what such a scheme converges to. The answer is the chapter's organizing idea: the decentralized dynamics solve a global optimization problem that no participant can see. Each source knows only its own rate and the congestion signals it receives; no machine anywhere holds the link-route incidence matrix; and yet the flow rates converge to the unique maximizer of a concave network utility, and that maximizer is the proportionally fair allocation. This is the same phenomenon as the electrical network of Chapter 4, now with the local rule chosen so that the global objective is the one we want.

Setting

A network has $J$ resources and $R$ routes, with link-route incidence matrix $A$: $A_{jr}=1$ when route $r$ uses resource $j$. Route $r$ carries a time-varying flow rate $x_r(t)>0$, and the load on resource $j$ is $\sum_{s:j\in s}x_s(t)$.

Each resource $j$ generates congestion signals at rate

$$\mu_j(t)=p_j\Bigl(\sum_{s:j\in s}x_s(t)\Bigr),$$

where $p_j$ is non-negative, continuous, increasing and not identically zero — one may read $p_j(y)$ as the probability that a packet is dropped or marked at resource $j$ under load $y$. The primal algorithm is the response of the sources:

$$\frac{d}{dt}x_r(t)=\kappa_r\Bigl(w_r-x_r(t)\sum_{j\in r}\mu_j(t)\Bigr), \qquad r\in\mathcal{R}, \tag{7.5}$$

with $w_r,\kappa_r>0$: a steady increase proportional to the weight $w_r$, and a decrease proportional to the stream of congestion signals received. Both sums are local — over the resources on route $r$, and over the routes through resource $j$ — so nothing in the network needs to know $A$.

The network problem $\mathrm{network}(A,C;w)$ of section 7.1 is to maximize $\sum_r w_r\log x_r$ over $x\ge0$ with $Ax\le C$, and a feasible $x$ is weighted proportionally fair when every feasible $y$ satisfies $\sum_r w_r (y_r-x_r)/x_r\le0$.

Formalization targets

Goal — Theorem 7.6, global stability of the primal algorithm

$$U(x)=\sum_{r}w_r\log x_r-\sum_{j}\int_0^{\sum_{s:j\in s}x_s}p_j(y)\,dy$$

is a Lyapunov function for (7.5): the unique maximizer $\bar x$ of $U$ over the positive orthant is an equilibrium point, and every trajectory of the primal algorithm converges to it.

The goal asserts both halves of the book's last sentence: that $\bar x$ maximizes $U$, and that the trajectory converges to it. It fixes no rate of convergence and no basin restriction beyond starting in the interior, which is what "global" means here.

Supporting levels

Proposition 7.4, that solving $\mathrm{network}(A,C;w)$ and being weighted proportionally fair are the same condition; strict concavity of $U$ on the positive orthant; the partial derivative $\partial U/\partial x_r=w_r/x_r-\sum_{j\in r}p_j(\cdot)$ that identifies the maximizer; the equivalence between a stationary point of $U$ and an equilibrium of (7.5); and the Lyapunov identity (7.7),

$$\frac{d}{dt}U(x(t))=\sum_r\frac{\kappa_r}{x_r(t)}\Bigl(w_r-x_r(t)\sum_{j\in r}p_j(\cdot)\Bigr)^2\ \ge 0 .$$

Significance

The result itself. Theorem 7.6 is the statement that a decentralized rule solves a centralized problem. Its practical content is that the choice of $p_j$ and $w_r$ determines what is optimized, so a protocol designer who wants a particular notion of fairness can get it by choosing the local rule accordingly — the $\alpha$-fair family of Chapter 8 is exactly this dial. Its theoretical content is the identification of the limit: because $U$'s first term is $\sum_r w_r\log x_r$, the limit is the weighted proportionally fair allocation, which by Proposition 7.4 is the solution of the network problem and, by Remark 7.5, also the Nash bargaining solution and a market-clearing equilibrium. Three quite different notions of "the right allocation" coincide, and a simple end-to-end feedback rule finds it.

Formalizing it. Nothing here is open; the model and the theorem are from Kelly, Maulloo and Tan (1998). What the mission produces is a machine-checked congestion-control model — the network problem, proportional fairness, the primal dynamics and the Lyapunov function — and a statement of the convergence result in a form later work can cite. Mathlib has no network utility maximization and no congestion control.

Difficulty

The Lyapunov identity is a chain-rule computation and is not the hard part, and neither is $\frac{d}{dt}U\ge0$. The gap the book flags explicitly is between "$U$ increases along trajectories" and "$x(t)\to\bar x$": a strictly increasing Lyapunov function does not by itself force convergence, because the derivative could decay fast enough for the system to stall short of the maximum. The book closes it with a compactness argument — the trajectory is trapped in $\{x: U(x)\ge U(x(0))\}$, which is compact, and on the complement of an $\epsilon$-ball around $\bar x$ within that set the derivative (7.7) is continuous and therefore bounded away from zero, so only finite time can be spent there. Reproducing that argument is the substance of the goal, and it needs the compactness of the sublevel set, which comes from strict concavity and the growth of $-\int_0^{y}p_j$.

A second difficulty is one of representation rather than mathematics. The primal algorithm is an ODE, and a formal statement must say what a trajectory is. Here a trajectory is given as a differentiable function satisfying (7.5) pointwise, with positivity assumed rather than derived; deriving positivity from the dynamics is a separate (true, and welcome) result.

Formalization scope

Resources and routes are indexed by finite types and the incidence matrix is real-valued with entries constrained to $0$ or $1$, matching the book and the convention of mission IV of this series, whose linkFlow is reused here. Flow vectors live in the positive orthant, stated as ∀ r, 0 < x r: the utility contains $\log x_r$, which has no meaning at $x_r=0$, and the book's own maximum is interior to the positive orthant.

The network problem's objective is maximized over the intersection of the feasible set with the positive orthant rather than over $x\ge0$, since $\log 0$ is not a real number; the fairness condition, by contrast, is quantified over all feasible $y$ including boundary points, exactly as the book states it, and the inequality $\sum_r w_r(y_r-x_r)/x_r\le0$ is meaningful there.

A trajectory is a function of real time satisfying the derivative condition at each $t\ge0$, and staying in the positive orthant is a hypothesis. The equilibrium $\bar x$ is given by its stationarity condition $w_r=\bar x_r\sum_{j\in r}p_j(\cdot)$ rather than by an existence claim, so the goal is about the trajectory rather than about solving the fixed-point equation; that the stationary point is the maximizer is the first conjunct of the conclusion, so nothing is assumed about it that is not also proved.

The goal cannot be satisfied vacuously: the hypotheses are jointly satisfiable — for instance one resource, one route, $p(y)=y$, $w=\kappa=1$, $\bar x=1$ — and the conclusion is a genuine limit.

Contributions welcome beyond the listed items: that the positive orthant is invariant under (7.5); uniqueness and existence of the max-min fair allocation; Theorem 7.2 on problem decomposition into user and network problems; Theorem 7.8, the corresponding global stability result for the TCP-like system of section 7.4; and the dual algorithm of section 7.6.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 7 (pp. 151–185); Proposition 7.4, Theorem 7.6, equations (7.4)–(7.7). DOI 10.1017/cbo9781139565363
• F. P. Kelly, A. K. Maulloo and D. K. H. Tan, Rate control for communication networks: shadow prices, proportional fairness and stability, Journal of the Operational Research Society 49 (1998), 237–252. DOI 10.1057/palgrave.jors.2600523
• F. P. Kelly, Charging and rate control for elastic traffic, European Transactions on Telecommunications 8 (1997), 33–37. DOI 10.1002/ett.4460080106
• J. F. Nash, The bargaining problem, Econometrica 18 (1950), 155–162. DOI 10.2307/1907266
• S. H. Low and D. E. Lapsley, Optimization flow control I: basic algorithm and convergence, IEEE/ACM Transactions on Networking 7 (1999), 861–874. DOI 10.1109/90.811451

Motivation

Chapter 7 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) studies a network with a fixed set of users, and shows that a decentralized rate control converges to a fair allocation. Chapter 8 asks the question one time scale up. Files finish and their flows leave; new files arrive and new flows appear. The number of flows on each route is therefore itself a random process, and the rate allocation — assumed to settle instantly, since rate control runs much faster than files arrive and depart — depends on it.

The question is whether this system is stable: does the number of flows in progress stay bounded, or does it grow without limit? The answer is the best one could hope for. A weighted $\alpha$-fair allocation, the family that contains proportional fairness, TCP fairness, max-min fairness and throughput maximization as special cases, is stable exactly when the offered load at each resource is below that resource's capacity. No more is required — no condition coupling different resources, no dependence on $\alpha$, no dependence on the topology beyond the loads themselves.

Setting

A network has $J$ resources and $R$ routes with incidence matrix $A$. Let $n_r$ be the number of flows active on route $r$ and $x_r$ the rate given to each of them, so route $r$ consumes $n_rx_r$ at each resource it uses. Flows arrive on route $r$ as a Poisson process of rate $\nu_r$ and carry files that are exponentially distributed with parameter $\mu_r$, so

$$n_r\to n_r+1 \text{ at rate } \nu_r, \qquad n_r\to n_r-1 \text{ at rate } \mu_rn_rx_r(n),$$

and $\rho_r=\nu_r/\mu_r$ is the load on route $r$.

Given weights $w_r>0$ and $\alpha\in(0,\infty)$, the weighted $\alpha$-fair allocation is the solution of

$$\text{maximize } \sum_r w_rn_r\frac{x_r^{1-\alpha}}{1-\alpha} \quad\text{subject to } \sum_{r:j\in r}n_rx_r\le C_j,\ x\ge0, \tag{8.1}$$

with $\sum_r w_rn_r\log x_r$ in place of the objective when $\alpha=1$. Written in the aggregate rates $X_r=n_rx_r$ this becomes

$$\text{maximize } G(X)=\sum_r w_rn_r^{\alpha}\frac{X_r^{1-\alpha}}{1-\alpha} \quad\text{subject to } \sum_{r:j\in r}X_r\le C_j,\ X\ge0. \tag{8.4}$$

The family interpolates between the fairness notions of Chapter 7: $\alpha\to0$ with $w\equiv1$ maximizes throughput, $\alpha=1$ is weighted proportional fairness, $\alpha=2$ with $w_r=1/T_r^2$ is TCP fairness, and $\alpha\to\infty$ with $w\equiv1$ approaches max-min fairness.

Formalization targets

Goal — the drift inequality behind Theorem 8.2

Suppose the load respects every capacity, $\sum_{r:j\in r}\rho_r<C_j$ for all $j$. Then there is an $\epsilon>0$, depending only on the loads and capacities, such that for every flow count $n$ and the $\alpha$-fair aggregate rates $X=X(n)$,

$$\sum_r w_r\rho_r^{-\alpha}n_r^{\alpha}\bigl(\rho_r-X_r\bigr) \;\le\;-\epsilon\sum_r w_rn_r^{\alpha}\rho_r^{1-\alpha}.$$

The left-hand side is the drift of the Lyapunov function $L(n)=\sum_r(w_r/\mu_r)\rho_r^{-\alpha}n_r^{\alpha+1}/(\alpha+1)$, by the identity (8.3); the right-hand side is the book's displayed bound. The single $\epsilon$ is uniform in $n$, which is what a Foster–Lyapunov argument needs, and it is the whole deterministic content of Theorem 8.2's sufficiency half.

Supporting levels

The derivative $w_rn_r^{\alpha}X_r^{-\alpha}$ of the objective, in the same form for every $\alpha\in(0,\infty)$ including $\alpha=1$ (Exercise 8.3); strict concavity of the objective; the characterization of the optimum by $x_r=(w_r/\sum_{j\in r}p_j)^{1/\alpha}$ with primal and dual feasibility and complementary slackness (Exercise 8.4); the tangent-plane inequality (8.5) that concavity gives at the optimum; the drift identity (8.3); and that $\alpha=1$ recovers weighted proportional fairness, connecting this chapter to Proposition 7.4 of mission VII.

Significance

The result itself. Theorem 8.2 says the stability region of an $\alpha$-fair network is the largest it could possibly be — the same region a single isolated resource would have — and that it does not shrink as $\alpha$ varies. That is a strong statement about a large design space, and it is not automatic: section 8.4 of the book exhibits rate allocation schemes for which it fails, so the natural condition (8.2) is a property of $\alpha$-fairness and not of rate allocation in general. Since the family covers the fairness notions actually implemented in transport protocols, the theorem is what licenses treating "is the load below capacity?" as the only capacity-planning question at flow level.

Formalizing it. Nothing here is open; the theorem is due to Bonald and Massoulié (2001), with the fluid-limit machinery from Gromoll and Williams and from Massoulié. What the mission produces is a machine-checked $\alpha$-fair allocation — objective, derivative, concavity, KKT conditions — and the exact drift inequality, on top of the congestion-control layer published in mission VII of this series, whose networkFeasible and linkFlow it reuses. Mathlib has no network utility maximization and no fairness criteria.

Difficulty

The proof is short but the step that makes it work is easy to miss. The drift is $\sum_r w_rn_r^{\alpha}\rho_r^{-\alpha}(\rho_r-X_r)$, and there is no reason for this to be negative term by term — some routes are over-served and some under-served. What makes the sum negative is that $\rho$ is itself a feasible point of the same optimization problem (8.4) that $X$ solves, and $G$ is concave, so the tangent plane at $\rho$ lies above $G$:

$$G'(U)\cdot(U-X)\le G(U)-G(X)\le0 \quad\text{for every feasible } U .$$

Since $G'(U)_r=w_rn_r^{\alpha}U_r^{-\alpha}$, taking $U=\rho$ gives the drift $\le0$ immediately. Strict negativity comes from taking $U=(1+\epsilon)\rho$ instead, which is still feasible because (8.2) is a strict inequality, and then dividing through by $(1+\epsilon)^{\alpha}$. The whole argument is one application of concavity at a cleverly chosen point, and the choice of that point is the content.

The scaling that makes it uniform in $n$ is the other thing to notice: $\epsilon$ depends only on how much slack (8.2) leaves, not on $n$, because $n$ enters $G'$ only through the common factor $n_r^{\alpha}$ that appears on both sides.

Formalization scope

Resources and routes are indexed by finite types, the incidence matrix is real-valued with entries $0$ or $1$, and the feasible set is mission VII's networkFeasible, so Chapters 7 and 8 agree on what a feasible flow vector is. The objective is stated in the aggregate variables $X_r=n_rx_r$ of problem (8.4) rather than the per-flow rates of (8.1): they are equivalent, but (8.4) is the form the drift argument uses and the form in which the feasible set does not depend on $n$.

The objective is defined with an explicit case split at $\alpha=1$, exactly as the book defines it, and the derivative milestone asserts that the resulting derivative has the same form $w_rn_r^{\alpha}X_r^{-\alpha}$ in both cases — which is the point of Exercise 8.3. Powers are real exponents, so positivity of the flow counts, weights, loads and rates is hypothesised wherever a power appears.

What is formalized and what is quoted. Theorem 8.2 is a statement about positive recurrence of a Markov process, proved by a Foster–Lyapunov criterion whose remaining hypotheses the book leaves to Exercises 8.6 and D.2. There is no theory of continuous-time Markov chains on a countable state space in Mathlib to state positive recurrence against, so this mission formalizes the deterministic drift inequality that carries the argument and quotes the probabilistic wrapper. The inequality is exactly the one the book displays, including the $\epsilon$, and the necessity half — that the process is unstable when (8.2) fails — is a coupling argument and is quoted too.

The goal is not vacuous: the hypotheses are satisfiable, and for a single resource of capacity $C$ the $\alpha$-fair optimum is $X_r=Cw_r^{1/\alpha}n_r/\sum_sw_s^{1/\alpha}n_s$, for which the inequality holds with $\epsilon=C/\sum_r\rho_r-1$ and strictly positive slack.

Contributions welcome beyond the listed items: the single-resource equilibrium distribution of Exercise 8.1 and the geometric law of the total number of flows; the bounded-drift estimate of Exercise 8.6; the necessity half of Theorem 8.2; the limiting cases $\alpha\to0$ and $\alpha\to\infty$; and the instability examples of section 8.4.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 8 (pp. 186–199); problem (8.1), Theorem 8.2, equations (8.2)–(8.5). DOI 10.1017/cbo9781139565363
• T. Bonald and L. Massoulié, Impact of fairness on Internet performance, ACM SIGMETRICS Performance Evaluation Review 29 (2001), 82–91. DOI 10.1145/384268.378433
• J. Mo and J. Walrand, Fair end-to-end window-based congestion control, IEEE/ACM Transactions on Networking 8 (2000), 556–567. DOI 10.1109/90.879343
• L. Massoulié, Structural properties of proportional fairness: stability and insensitivity, Annals of Applied Probability 17 (2007), 809–839. DOI 10.1214/105051607000000014
• H. C. Gromoll and R. J. Williams, Fluid limits for networks with bandwidth sharing and general document size distributions, Annals of Applied Probability 19 (2009), 243–280. DOI 10.1214/08-AAP541

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

$$Q(x, \xi_k) = \min_{y \ge 0} \{ q_k^\top y \mid W y = h_k - T_k x \},$$

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

$$\min_{x} \ c^\top x + Q(x) \quad \text{s.t.} \quad x \in K_1 \cap K_2, \qquad Q(x) = \sum_{k=1}^K p_k\, Q(x, \xi_k).$$

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)

$$\text{When } \xi \text{ is a finite random variable, the L-shaped algorithm finitely converges to}$$ $$\text{an optimal solution when it exists, or proves } K_1 \cap K_2 = \varnothing.$$

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)

$$\text{If } T \text{ is deterministic, } W \text{ is such that every } t \ge 0 \text{ lies in } \mathrm{pos}\,W,$$ $$\text{and } a = \min_k h_k \text{ (componentwise) is attained by some scenario } h_\ell,$$ $$\text{then } x \in K_2 \iff \exists\, y \ge 0,\ Wy = a - Tx.$$

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

Two-stage stochastic programs with recourse are already hard to optimize when the recourse problem is a linear program: Chapters 4–6 of this series show how the L-shaped method exploits the recourse function's convexity and polyhedrality to converge finitely by cutting planes. Adding integrality restrictions destroys both properties. Birge and Louveaux open Chapter 7 by naming the consequence directly: "properties of stochastic integer programs are scarce," duality is lost, and the recourse value $Q(x)$ for even a single first-stage point $x$ may itself require solving an integer program from scratch, with no warm start available across scenarios (Birge & Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer 2011, p. 290).

Section 7.2 isolates the one structural feature that still buys finite convergence: first-stage variables restricted to $\{0,1\}$. Laporte and Louveaux's Integer L-shaped method (1993) exploits this by combining a branch-and-bound search over the finitely many binary first-stage points with a new family of optimality cuts, valid wherever a finite lower bound on the recourse value is available. This mission formalizes that method's specification and its finite-convergence guarantee, together with the two propositions its proof rests on.

Setting

A stochastic integer program (SIP) extends a two-stage stochastic linear program with fixed recourse (Chapter 3's Recourse.Instance: first-stage data $A, b, c$, fixed recourse matrix $W$, and $K$ scenarios of $(q_k, h_k, T_k)$ with probabilities $p_k$) by two further restrictions:

$$(\mathrm{SIP}) \quad \min_{x \in X} c^{\mathsf T}x + \mathbb E_\xi \min_y \{ q(\omega)^{\mathsf T} y \mid W(\omega)y = h(\omega) - T(\omega)x,\ y \in Y\} \quad \text{s.t. } Ax = b,$$

where $X$ restricts the first stage and $Y$ restricts the recourse variable — typically requiring integrality of $y$. Section 7.2's standing hypothesis narrows $X$ further: every coordinate of $x$ is binary. Write $Q(x)$ for the resulting recourse value (a possibly-infinite expectation, by the same convention as the continuous case) and $C(x)$ for the value of the continuous relaxation, obtained by dropping the restriction $Y$ and keeping only $y \ge 0$ — exactly the recourse value Chapter 3's Recourse.Instance already computes.

The method needs one further hypothesis, Assumption 2: a finite lower bound $L$ with $L \le \min_x \{Q(x) \mid Ax=b,\ x \in X\}$, not required to be tight. For a subset $S$ of the first-stage index set, write $\delta(x,S) = \sum_{i \in S} x_i - \sum_{i \notin S} x_i$, and let $\mathrm{indicator}(S)$ be the binary point with $x_i = 1$ for $i \in S$, $x_i = 0$ otherwise — $\delta(x,S)$ measures how far a binary point $x$ is from matching $S$ exactly, reaching its maximum $|S|$ only at $x = \mathrm{indicator}(S)$.

Formalization targets

Proposition 1 (continuous cuts survive integrality)

$$e - E^{\mathsf T}x \le C(x) \implies e - E^{\mathsf T}x \le Q(x)$$

Any L-shaped optimality cut valid for the continuous relaxation's value remains valid for the true, integrality-restricted recourse value, since $C(x) \le Q(x)$ pointwise.

Proposition 3 (a cut from one binary feasible solution)

$$\theta \ge (q_S - L)\Bigl(\sum_{i \in S} x_i - \sum_{i \notin S} x_i\Bigr) - (q_S-L)(|S|-1) + L$$

is a valid lower bound on $Q(x)$ for every binary first-stage-feasible $x$, given a binary feasible point $\mathrm{indicator}(S)$ with true recourse value $q_S$ and a lower bound $L$ satisfying Assumption 2.

Proposition 4 — the mission's goal

Under Assumption 2, the Integer L-shaped method — the branch-and-bound search over binary first-stage points, tightened at each iteration by a fresh cut of the Proposition 3 form — finitely converges to an optimal solution of an SIP with relatively complete recourse and binary first-stage variables, when one exists. "Finitely" is quantified explicitly: a bound of $2^{n_1}$ on the number of iterations, the number of distinct binary first-stage points.

Significance

Proposition 4 is the chapter's payoff: it turns "solve an SIP with binary first-stage variables" from an open-ended search into a procedure with a certified stopping point, at the cost of one additional hypothesis (a computable lower bound $L$) that is often easy to obtain by relaxing the second-stage integrality restriction, as the book's Example 1 illustrates directly. Propositions 1 and 3 are the two soundness facts the method's cuts rest on: Proposition 1 lets an implementation reuse the continuous L-shaped method's own optimality cuts as valid (if weaker) constraints, and Proposition 3 supplies the chapter's genuinely new cut, tailored to the binary structure and strong enough by itself to guarantee termination.

Formalizing this mission fixes, machine-checkably, the exact hypotheses under which the method is correct — in particular, that "binary" is load-bearing (the finiteness bound is literally $2^{n_1}$) and that "relatively complete recourse" cannot be dropped, since it is what keeps the recourse value from becoming $+\infty$ at a feasible point. No result here has, to the mission's knowledge, been formalized elsewhere; the propositions and the method's specification are drafted fresh.

Difficulty

The recourse function $Q$ is neither convex nor polyhedral once $y$ is integer-restricted, so the argument cannot follow the continuous L-shaped method's proof line for line — that proof leans on $Q$'s convexity to certify a cut from finitely many bases. Proposition 3's cut instead argues purely combinatorially: $\delta(x,S) \le |S|$ for every binary $x$, with equality forcing $x = \mathrm{indicator}(S)$, so the cut's right-hand side collapses to the true value $q_S$ exactly there and falls to at most $L$ everywhere else — a fact about the finitely many binary points of $\{0,1\}^{n_1}$, not about $Q$'s analytic structure. The natural first idea, adapting a continuous L-shaped cut by simply restricting its domain to binary $x$, fails: nothing forces such a cut to be tight at the current iterate, so it need not exclude a revisited point, and finite convergence (the content Proposition 4 actually asserts, not just "an optimum exists") would be lost.

Formalization scope

The mission represents first-stage points as Fin n1 → ℝ with a Binary predicate (∀ i, x i = 0 ∨ x i = 1) rather than a Fin n1 → Bool type, so that the master problem's feasible region and its binary-restricted subset share one ambient space, matching how the book moves between $X$ and its binary points. The second-stage restriction $Y$ is left an arbitrary Set (Fin n2 → ℝ); taking it to be all of $\mathbb R^{n2}$ recovers exactly Chapter 3's continuous recourse value, without a second definition. Flagged (moderator review, 2026-09-19): Proposition 1's own $C(x)$ is the book's $\overline Y$-based continuous/LP-relaxation of $Y$ (Eq. (1.3)-(1.4)), which can retain bounds $Y$ imposes beyond integrality — the book's own worked example on the same page gives binary $Y=\{0,1\}^{m_2}$, so $\overline Y=[0,e]$, not $y\ge0$ alone. This mission's prop1_cuts_valid_for_sip uses the dropped-$Y$ relaxation (only $y \ge 0$) rather than $\overline Y$, which coincides with the book's $C(x)$ only when $Y$ is itself an unbounded integrality restriction; the theorem is a narrower result than the book's Proposition 1 whenever $Y$ carries additional structure, though it remains true as stated because the dropped-$Y$ value is unconditionally $\le$ the book's $\overline Y$-based $C(x)$, which is itself $\le Q(x)$ — see the item's own Formalization Note for the full argument. The existential lower bound $L$ of Assumption 2 is kept a bare existentially-quantified real, never sharpened to a formula, matching the book's own "no requirement is made that the bound $L$ should be tight."

The Integer L-shaped method's branch-and-bound bookkeeping (Steps 0, 1, 3, 4: pendant-node list management, bound-based fathoming, and branching on a violated integrality restriction) is abstracted into a direct optimization over the binary first-stage feasible set at each iteration, since Proposition 3's cut is proved valid there without appeal to any specific branching order — the same level of abstraction the Chapter 5 mission uses for the continuous L-shaped method's own master-problem bookkeeping. What is retained explicitly is the part the finiteness bound actually depends on: Step 5's recourse-value computation and Step 6's binary choice between fathoming and adding a fresh cut, modeled as a state machine whose state is the finite set of binary points already excluded by a cut. A formalization that dropped this state machine — asserting only "if Assumption 2 and relatively complete recourse hold, an optimal solution exists" — would trivialize the proposition's actual content, the finite bound on the number of steps; this mission keeps that bound as an explicit, checkable part of the goal statement.

Definitions reused from earlier missions in this series: StochasticProg.Recourse.Instance (Chapter 3) for the underlying two-stage recourse data and its continuous-relaxation value. Contributions welcome on strengthening Proposition 4's proof to also derive Proposition 3 as a lemma, and on formalizing the improved cuts of Propositions 5–7 (out of scope here, left for a possible follow-up mission).

Selected references

• J.R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer 2011, Chapter 7, §7.2. DOI: 10.1007/978-1-4614-0237-4
• G. Laporte and F. Louveaux, "The integer L-shaped method for stochastic integer programs with complete recourse," Operations Research Letters 13(3), 1993, 133–142.