All missions

Pooling as a design principle

A firm that holds inventory in five warehouses needs more safety stock than one that holds the same inventory in one warehouse, because the demands of five regions do not all run high at once. Eppen (1979) made this precise for a multi-location newsvendor and gave it its name, the risk-pooling effect. Chapter 7 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) follows the same idea through three settings in which pooling happens without physical consolidation: two retailers who ship stock to each other after seeing demand (transshipments, after Tagaras 1989), and plants that can each make more than one product (process flexibility, after Jordan and Graves 1995). The chapter's capstone is the theorem of Simchi-Levi and Wei (2012) that, among designs in which every plant makes two products and every product is made at two plants, a single long chain through all of them is best. This mission formalizes the chapter's numbered results, with that theorem as its goal.

Setting

Risk pooling. $N$ distribution centers face normally distributed per-period demands $D_i \sim N(\mu_i, \sigma_i^2)$ with correlation coefficients $\rho_{ij}$, and each runs a base-stock policy with holding cost $h$ and backorder cost $p$ per unit per period, so its optimal expected cost is the optimal newsvendor cost optNvCost h p D, the infimum over base-stock levels $S$ of $\mathbb{E}[h(S - D)^+ + p(D - S)^+]$. Merging the centers gives one facing the total demand, normal with mean $\sum_i \mu_i$ and variance $\sigma_0^2 = \sum_i \sum_j \sigma_i \sigma_j \rho_{ij}$ (pooledVariance).

Transshipments. Two retailers $i, j$ with base-stock levels $S_i, S_j$ face independent demands. After demand is observed, under complete pooling the retailer with a surplus sends the retailer with a shortage $Y_{ji} = \min\{S_j - D_j,\ D_i - S_i\}$ units (transship), and nothing moves otherwise. The type-1 service level is the probability of no stockout, $\alpha^0_i = \Pr[D_i \le S_i]$ without and $\alpha_i = \Pr[D_i - S_i \le Y_{ji}]$ with transshipments; the type-2 service level is the fill rate, one minus expected unmet demand over expected demand, $\beta^0_i$ and $\beta_i$ likewise.

Process flexibility. A flexibility design on $n$ products and $n$ plants is a set $E$ of (product, plant) pairs, an edge $(i, j)$ meaning plant $j$ can make product $i$. Given a demand realization $d$ and a common plant capacity $C$, the performance $P(d, E)$ (perf) is the maximum sales obtainable by assigning production along the edges of $E$ without exceeding any capacity or demand, the linear program (7.22) to (7.26). A balanced system (BalancedSystem) has equal capacities and an exchangeable demand vector, one whose joint law is invariant under permutations of the products, and $[E] = \mathbb{E}[P(D, E)]$ is the expected performance (expPerf). The named designs are the dedicated design $D_n = \{(i, i)\}$, the long chain $C_n$ in which plant $j$ also makes product $j + 1$ (and plant $n$ makes product $1$), the open chain $L_k$ obtained from $C_k$ by deleting the edge $(1, k)$, and $L^n_k$, the open chain on the first $k$ pairs together with the dedicated edges of the rest. A 2-flexibility design (TwoFlex) is one in which every product has exactly two plants and every plant exactly two products; $C_n$ is one, and so is any union of disjoint shorter chains.

Formalization targets

Goal: Theorem 7.9

For a balanced system of size $n \ge 2$ with exchangeable demand,

$$C_n \in \arg\max_{A \in \mathcal{F}_2} [A],$$

that is, $C_n$ is a 2-flexibility design and $[A] \le [C_n]$ for every 2-flexibility design $A$. This is long_chain_optimal.

Supporting targets

The chapter's route to the goal: Lemma 7.5, supermodularity of sales in the flexible edges of the long chain for every realization, $P(d, E) + P(d, E \setminus \{\alpha, \beta\}) \ge P(d, E \setminus \{\alpha\}) + P(d, E \setminus \{\beta\})$ for $E \subseteq C_n$; Corollary 7.6, the same in expectation; Lemma 7.7, the increments $[L^n_{k+1}] - [L^n_k]$ are nondecreasing in $k$, ending with $[C_n] - [L^n_n]$; and Lemma 7.8, $[C_n] = n([L_n] - [L_{n-1}])$.

Risk pooling, Theorem 7.1: $g^*_C \le g^*_D$, the optimal cost of the merged center is at most the sum of the optimal costs of the separate ones, with the covariance inequality $\sqrt{\sum_i\sum_j \sigma_i\sigma_j\rho_{ij}} \le \sum_i \sigma_i$ as a separate lemma.

Transshipments, Theorems 7.2 to 7.4: $\alpha_i = \alpha^0_i + |\partial\mathbb{E}[Y_{ji}]/\partial S_i|$, $\beta_i = \beta^0_i + \mathbb{E}[Y_{ji}]/\mathbb{E}[D_i]$, and all four post-transshipment service levels are nondecreasing in $S_i$.

Significance

Theorem 7.9 is the analytical answer to a question that had been settled only by simulation: Jordan and Graves reported that one chain through all plants achieves nearly twice the sales benefit of three short chains with the same number of edges, and Simchi-Levi and Wei proved that no arrangement of the same edge budget does better. It is the justification for the chaining guideline used in automotive and semiconductor capacity planning, and Lemma 7.8, which expresses the long chain through open chains, is what makes the long chain's performance computable by a greedy pass. Theorem 7.1 is the quantitative basis for consolidation decisions and for postponement, since a generic product is pooled inventory. Theorems 7.2 to 7.4 quantify what transshipments buy in service, which is the argument for allowing them despite their cost.

None of these results has a machine-checked proof. The book proves Lemma 7.7, Lemma 7.8 and Theorem 7.9 in full given Lemma 7.5, which it cites to Simchi-Levi and Wei, and omits the proofs of Theorems 7.3 and 7.4 and the identity (7.30) behind Lemma 7.8. Formalizing Lemma 7.5 and (7.30) means formalizing the structure of maximum flows on a cycle, which is reusable for the later results of Simchi-Levi and Wei on the long chain's performance relative to full flexibility and for the multi-echelon flexibility models the chapter cites.

Difficulty

The obvious approach to Theorem 7.9 is to compare $C_n$ with an arbitrary 2-flexibility design directly. Nothing in the definitions supports that: the two designs share no structure beyond their degree sequences. The book's argument instead routes everything through the long chain's own edges. Lemma 7.5 gives supermodularity only for subsets of $C_n$, and the decomposition of an arbitrary 2-flexibility design into disjoint cycles, each a relabeled long chain on a subsystem, is what allows the comparison. A solver must therefore prove that a 2-regular bipartite graph is a disjoint union of even cycles, that exchangeability makes every relabeling of a cycle worth the same as $C_{n_j}$ on its subsystem, and that the performance of a disjoint union is the sum of the performances of its parts.

Lemma 7.5 itself is where the combinatorics lives. It says that on the cycle $C_n$ the maximum flow is supermodular in the flexible edges, and the proof in Simchi-Levi and Wei goes through the structure of augmenting paths on a cycle. The natural first idea, that supermodularity follows from some general property of maximum flows, is false: maximum flow is not supermodular in arbitrary edge sets, and the lemma is specific to subsets of a single cycle.

Lemma 7.7 is where exchangeability is used, and it is used in a way that is easy to state and tedious to formalize: removing the edge $(2, 1)$ from $L^n_{k+1}$ leaves a design that is $L^n_k$ only after the pair $1$ is moved to the end, so the argument needs the invariance of $[E]$ under relabeling the products and plants by a common permutation. The book notes that Lemma 7.7, unlike Lemma 7.5, is false realization by realization.

For the transshipment theorems, the book differentiates a density formula by Leibniz's rule. Under the weaker hypothesis stated here, laws without atoms and with finite means, the derivative of $\mathbb{E}[Y_{ji}]$ in $S_i$ has to be obtained by dominated convergence from the pointwise derivative of a piecewise-linear function whose kinks lie on null sets.

Formalization scope

perf is a supremum over a set of reals, nonempty because $y = 0$ is feasible when $d \ge 0$ and $C \ge 0$, and bounded by $\sum_i d_i$; the demand is nonnegative for every outcome and the capacity nonnegative in BalancedSystem, and Lemma 7.5 carries these as hypotheses. The supremum is attained, but the definition does not assert it. Expected performance is a Lebesgue integral; the demand is integrable by assumption and $P(d, E)$ is $1$-Lipschitz in $d$, so the integrand is integrable, and a solver must prove this measurability rather than assume it.

Exchangeability is the equality of the laws of $(D_{\sigma(i)})_i$ and $(D_i)_i$ for every permutation $\sigma$. Designs are finite sets of pairs of Fin n; the chains are defined with finRotate, so indices wrap modulo $n$ and the closing edge of $C_n$ is $(1, n)$ in the book's numbering, which is the edge its proofs and Figure 7.3(c) use. Lemma 7.8 involves open chains on subsystems of sizes $n$ and $n - 1$; these are designs on Fin k evaluated on the first $k$ coordinates of the demand (subDemand, subPerf).

Theorem 7.1 states the optimal costs as infima of the newsvendor cost over all base-stock levels, on Mathlib's gaussianReal; a nonpositive pooled variance gives a degenerate law, for which the inequality still holds, so the statement is not trivialized by that convention. The transshipment theorems take the two demand laws as probability measures on $\mathbb{R}$ with no atoms (Theorem 7.2) and finite, positive means; the quantity $Y_{ji}$ is defined for all outcomes and the service levels are probabilities and expectations under the product law.

The definition module is shared by all eleven items. Beyond the milestones, formalizing the identity (7.30) as its own lemma and the disjoint-union additivity of perf would be natural contributions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 7. https://doi.org/10.1002/9781119584445
• G. D. Eppen, Effects of centralization on expected costs in a multi-location newsboy problem, Management Science 25(5), 1979. https://doi.org/10.1287/mnsc.25.5.498
• G. Tagaras, Effects of pooling on the optimization and service levels of two-location inventory systems, IIE Transactions 21(3), 1989. https://doi.org/10.1080/07408178908966208
• W. C. Jordan and S. C. Graves, Principles on the benefits of manufacturing process flexibility, Management Science 41(4), 1995. https://doi.org/10.1287/mnsc.41.4.577
• D. Simchi-Levi and Y. Wei, Understanding the performance of the long chain and sparse designs in process flexibility, Operations Research 60(5), 2012. https://doi.org/10.1287/opre.1120.1082

Why orders swing more than sales

Procter & Gamble observed in the 1990s that the orders its distributors placed for diapers were far more variable than the retail sales of diapers, and that its own orders to suppliers were more variable still, although the end demand for diapers is about as stable as demand gets. The phenomenon, a growing amplification of variability as one moves upstream in a supply chain, is the bullwhip effect. Lee, Padmanabhan and Whang (1997) argued that it is not a symptom of irrational behaviour: four rational responses of an inventory manager to their own environment each produce it. Chapter 13 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) makes three of the four quantitative, following Chen, Drezner, Ryan and Simchi-Levi (2000) for demand signal processing, Lee et al. for the rationing game, and Cachon (1999) for order batching. This mission formalizes those three models and the theorems the chapter proves about them.

Setting

Demand signal processing. A retailer faces a demand process $D_t$, $t \in \mathbb{Z}$, that follows the stationary first-order autoregressive model

$$D_t = d + \rho D_{t-1} + \epsilon_t,$$

with a constant $d \ge 0$, a correlation constant $-1 < \rho < 1$, and errors $\epsilon_t$ that are independent $N(0, \sigma^2)$ variables, each independent of the demands before period $t$. In steady state every $D_t$ has the law $N\big(d/(1-\rho),\ \sigma^2/(1-\rho^2)\big)$. The retailer replenishes with a lead time of $L$ periods under a base-stock policy but does not know the demand parameters, so it estimates the lead-time demand from a moving average of the previous $m \ge 1$ demands:

$$\hat\mu^L_t = \frac{L}{m}\sum_{i=1}^m D_{t-i}, \qquad \hat\sigma^L_{et} = C\sqrt{\frac{1}{m}\sum_{i=1}^m e_{t-i}^2}, \qquad e_t = D_t - \hat\mu^1_t,$$

and sets the base-stock level $S_t = \hat\mu^L_t + z_\alpha \hat\sigma^L_{et}$, where $z_\alpha$ is a safety factor. The book writes the constant in $\hat\sigma^L_{et}$ as $C_{L\rho}$ and does not give its form; here it is a free parameter $C$. Each period the retailer orders $Q_t = S_t - S_{t-1} + D_{t-1}$, which may be negative. In Lean the process is the structure AR1Demand, whose fields are the parameters, the errors, the demands, the recursion, the independence properties and the stationary law; muHat, err, sigmaHat, baseStock and order are the five quantities above.

Order batching. $N$ retailers face independent $N(\mu, \sigma^2)$ demands in every period and each orders once every $R \ge 1$ periods, the order being its demand over the previous $R$ periods. The supplier's order in a given period is the total ordered by the retailers whose ordering day falls in that period. Three patterns are compared: random ordering, in which each retailer's day is uniform over the $R$ days, so the number $X$ of retailers ordering on a given day is binomial$(N, 1/R)$; positively correlated ordering, in which all retailers order on the same day, so $X = N$ with probability $1/R$ and $0$ otherwise; and balanced ordering, in which the retailers are spread as evenly as possible, so with $N = MR + k$, $0 \le k < R$, $X$ is $M+1$ with probability $k/R$ and $M$ otherwise. The structure BatchOrders P N R mu sigma carries the demands, the ordering count $X$ independent of them, and supplierOrder, the sum of the last $R$ demands of retailers $1, \dots, X$; each pattern enters a theorem as a hypothesis on the law of $X$.

Rationing game. Two identical retailers face single-period demand with distribution function $F$, holding cost $h$ and stockout penalty $p$, so the newsvendor quantity $Q^*$ satisfies $F(Q^*) = p/(h+p)$. With probability $r$ the supplier can deliver only $A_1 < 2Q^*$ units in total and allocates them pro rata to the orders, retailer 1 receiving $A_1 Q_1/(Q_1 + Q_2)$; with probability $1 - r$ supply is unlimited. Retailer 1's expected cost when the retailers order $Q_1$ and $Q_2$ is

$$g_1(Q_1) = (1-r)\,\mathrm{nv}(Q_1) + r\,\mathrm{nv}\!\Big(\frac{A_1 Q_1}{Q_1 + Q_2}\Big),$$

with $\mathrm{nv}$ the newsvendor cost; this is rationingCost.

Formalization targets

Goal: Theorem 13.2, demand signal processing

$$\frac{\mathrm{Var}[Q_t]}{\mathrm{Var}[D_t]} \;\ge\; 1 + \Big(\frac{2L}{m} + \frac{2L^2}{m^2}\Big)(1 - \rho^m),$$

with equality when $z_\alpha = 0$. This is bullwhip_signal_processing. The bound exceeds $1$ whenever $L > 0$, whatever the value of $\rho$: a lead time and a moving-average forecast are enough to produce the effect.

Supporting targets

The chapter's own route to the goal, each a milestone: the steady-state moments (13.2) to (13.4), $\mathbb{E}[D_t] = d/(1-\rho)$, $\mathrm{Var}[D_t] = \sigma^2/(1-\rho^2)$ and $\mathrm{Cov}[D_t, D_{t-k}] = \rho^k \mathrm{Var}[D_t]$; the identity $Q_t = (1 + L/m) D_{t-1} - (L/m) D_{t-m-1} + z_\alpha(\hat\sigma^L_{et} - \hat\sigma^L_{e,t-1})$; Lemma 13.1, $\mathrm{Cov}[D_{t-i}, \hat\sigma^L_{et}] = 0$ for $1 \le i \le m$; the vanishing of the cross term (13.12); and the variance of the demand part, $\big(1 + (2L/m + 2L^2/m^2)(1 - \rho^m)\big)\mathrm{Var}[D_t]$.

Order batching, Theorem 13.4: under the three patterns the supplier's order has mean $N\mu$ and

$$\mathrm{Var}[Q^c_t] \ge \mathrm{Var}[Q^r_t] \ge \mathrm{Var}[Q^b_t] \ge N\sigma^2,$$

through the three variance formulas $N\sigma^2 + \mu^2 N(R-1)$, $N\sigma^2 + \mu^2 N^2 (R-1)$ and $N\sigma^2 + \mu^2 k(R-k)$.

The rationing game, Theorem 13.3: if $Q > 0$ is a symmetric Nash equilibrium, that is, $Q$ minimizes $g_1$ over positive order quantities when the other retailer orders $Q$, then $Q > Q^*$.

Significance

The three theorems are the quantitative core of the chapter. Theorem 13.2 is the single-stage building block that Theorems 13.6 and 13.7 later iterate along a serial chain, giving the product-form and the exponential lower bounds on the amplification at stage $k$; its comparative statics, the bound decreasing in $m$ and increasing in $L$, are the basis of the remedies the chapter recommends (shorter lead times, smoother forecasts, sharing point-of-sale data). Theorem 13.4 ranks the ordering patterns and justifies the advice to balance ordering days when batching cannot be avoided. Theorem 13.3 shows that pro-rata rationing alone inflates orders; the book is careful to note that inflated orders are not by themselves inflated variances, and that the variance statement for this model is due to Rong, Shen and Snyder (2017).

None of these results has a machine-checked proof. The book's proofs of Theorems 13.2 and 13.4 are complete but informal, and the proof of Lemma 13.1 is omitted with a citation to Ryan's 1997 thesis; formalizing it requires a self-contained argument. The variance decomposition of $Q_t$ and the conditioning argument for Theorem 13.4 are reusable for the multistage results of Sect. 13.2.5, which are natural follow-up missions on the same definitions.

Difficulty

The obvious computation of $\mathrm{Var}[Q_t]$ expands the order into its demand part and its safety-stock part and hopes the cross term disappears. It does, but not for a reason visible in the formulas: $\hat\sigma^L_{et}$ is a square root of a sum of squares of forecast errors, a nonlinear function of $m + m$ demands, and its covariance with a single demand is zero only because the errors are jointly Gaussian with mean zero and $\hat\sigma$ is an even function of them, so the covariance is the expectation of an odd function of a centred Gaussian vector. That is Lemma 13.1, and the vanishing of the cross term needs two further covariances, $\mathrm{Cov}[D_{t-1}, \hat\sigma^L_{e,t-1}]$ and $\mathrm{Cov}[D_{t-m-1}, \hat\sigma^L_{et}]$, which the book reduces to the lemma through the recursion (the second reduction divides by $\rho$) but which hold for every $\rho$ by the same symmetry. A solver must set up the joint Gaussian structure of the demand vector and prove the odd-function argument; nothing in Mathlib does this directly.

The second obstacle is that the moments (13.2) to (13.4) are not assumed but derived: the structure carries the stationary law of each $D_t$ and the independence of $\epsilon_t$ from the past, and the autocovariance $\rho^k \mathrm{Var}[D_t]$ has to be obtained from the recursion by induction on the lag, with integrability supplied by the Gaussian laws.

For Theorem 13.4 the work is the conditioning on $X$: given $X = x$ the supplier's order is a sum of $xR$ independent normals, so its conditional mean is $xR\mu$ and conditional variance $xR\sigma^2$, and the total variance is $\mathbb{E}[\mathrm{Var}[Q \mid X]] + \mathrm{Var}[\mathbb{E}[Q \mid X]]$. The order is defined by a sum over retailers $i < X$, so the independence of $X$ from the demands has to be used through the indicator structure rather than through a conditional-expectation library result.

For Theorem 13.3 the argument is a first-order condition. It requires that the newsvendor cost be differentiable with derivative $(h+p)F(y) - p$, which holds when $F$ is continuous, and that the symmetric equilibrium be an interior minimizer, which is why $Q > 0$ and the minimization over $Q_1 > 0$ are hypotheses.

Formalization scope

Time is indexed by $\mathbb{Z}$ so that $D_{t-m-1}$ exists for every $t$. AR1Demand asserts the recursion for every outcome, the independence of the whole error family, the independence of $\epsilon_t$ from $(D_s)_{s < t}$, and the stationary law of every $D_t$; these are the "steady-state" assumptions the book makes in words. The structure is satisfiable: the stationary Gaussian AR(1) process on a full-measure set of error sequences has all these properties. The constant $C_{L\rho}$ is a free real parameter $C$; no theorem depends on its value.

The goal divides by $\mathrm{Var}[D_t]$, which is $\sigma^2/(1-\rho^2) > 0$ under the structure's hypotheses $\sigma > 0$ and $|\rho| < 1$, so the ratio is a genuine quotient. Mathlib's ProbabilityTheory.variance and covariance are used; both are the ordinary real quantities for square-integrable variables, which every variable here is, $\hat\sigma^L_{et}$ included.

In BatchOrders the demands are indexed by Fin N × Fin R, the count $X$ is a natural-valued random variable bounded by $N$ and independent of the demand family, and supplierOrder sums the $R$ demands of retailers $1, \dots, X$, the book's "without loss of generality" choice. The laws of $X$ are hypotheses on point probabilities P.real {ω | X ω = j}; with $R \ge 1$ each of the three families of hypotheses is satisfiable by a structure with the corresponding law. The subtractions $R - 1$ and $R - k$ are real.

In the rationing game the demand law is a probability measure on $\mathbb{R}$ whose distribution function is continuous and strictly increasing on $[0, \infty)$; the newsvendor loss is assumed integrable at every order quantity. The pro-rata allocation uses Lean's total division, which is never at $0$ in the theorem since $Q_1 + Q_2 > 0$.

Beyond the ten milestones, the multistage Theorems 13.6 and 13.7 and the centralized-information bound of Theorem 13.5 are welcome as extensions on the same AR1Demand.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 13. https://doi.org/10.1002/9781119584445
• H. L. Lee, V. Padmanabhan and S. Whang, Information distortion in a supply chain: the bullwhip effect, Management Science 43(4), 1997. https://doi.org/10.1287/mnsc.43.4.546
• F. Chen, Z. Drezner, J. K. Ryan and D. Simchi-Levi, Quantifying the bullwhip effect in a simple supply chain: the impact of forecasting, lead times, and information, Management Science 46(3), 2000. https://doi.org/10.1287/mnsc.46.3.436.12069
• G. P. Cachon, Managing supply chain demand variability with scheduled ordering policies, Management Science 45(6), 1999. https://doi.org/10.1287/mnsc.45.6.843
• Y. Rong, Z.-J. M. Shen and L. V. Snyder, The impact of ordering behavior on order-quantity variability: a study of forward and reverse bullwhip effects, Naval Research Logistics 64(1), 2017. https://doi.org/10.1002/nav.21757

Motivation

When a system is controlled indefinitely and decisions are frequent — a router admitting packets, a queue accepting jobs, a machine being maintained — discounting future rewards is often unjustified, and what matters is the long-run average reward per period. Puterman's Chapter 8 (doi:10.1002/9780470316887) develops the theory of this criterion, and its central object is a single equation, the average reward optimality equation $0=\max_{a\in A_s}\{r(s,a)-g+\sum_jp(j\mid s,a)h(j)-h(s)\}$, whose unknowns are a scalar gain $g$ and a bias function $h$. For unichain models, in which every stationary policy generates a Markov chain with one recurrent class, this equation determines the optimal gain and an optimal stationary policy. The results go back to Howard (Dynamic Programming and Markov Processes, MIT Press, 1960) for the recurrent case and to Blackwell (Discrete dynamic programming, Annals of Mathematical Statistics 33, 1962, doi:10.1214/aoms/1177704593) and Derman for the general finite case; Puterman's Section 8.4 proves them through the discounted theory of mission II, by letting the discount factor tend to one.

Setting

The model is stationary (Assumption 8.0.1): a finite set $S$ of states, for each $s$ a finite nonempty set $A_s$ of actions, a reward $r(s,a)$ and transition probabilities $p(j\mid s,a)$, none depending on the decision epoch. A policy $\pi\in\Pi^{HR}$ may randomize and may depend on the whole history; the deterministic stationary policy $d^\infty$ applies the decision rule $d:S\to A$ at every epoch. Its transition matrix is $P_d(i,j)=p(j\mid i,d(i))$.

For a policy $\pi$, $v^\pi_{N+1}(s)=\mathbb E^\pi_s[\sum_{t=1}^Nr(X_t,Y_t)]$ is the expected reward over $N$ epochs. Since the limit of $N^{-1}v^\pi_{N+1}(s)$ need not exist (Example 8.1.1), the chapter works with the lim sup and lim inf average rewards $g^\pi_+(s)$ and $g^\pi_-(s)$, and with $g^*_\pm(s)=\sup_{\pi}g^\pi_\pm(s)$. A policy $\pi^*$ is average optimal when $g^{\pi^*}_-(s)\ge g^\pi_+(s)$ for all $s$ and $\pi$, the strongest of the three criteria of Section 8.1.2.

The optimality residual is $B(g,h)(s)=\max_{a\in A_s}\{r(s,a)-g+\sum_jp(j\mid s,a)h(j)-h(s)\}$, and the optimality equation is $B(g,h)=0$. A decision rule is $h$-improving when it attains $\max_{a\in A_s}\{r(s,a)+\sum_jp(j\mid s,a)h(j)\}$ at every state. A transition matrix is unichain when it consists of a single recurrent class plus a possibly empty set of transient states, and the MDP is unichain when $P_d$ is unichain for every deterministic decision rule.

Formalization targets

Goal — Theorem 8.4.5 (printed p. 361)

For a finite unichain model: (a) some deterministic stationary policy is average optimal; (b) the optimality equation $B(g^*,h^*)=0$ has a solution, and (d) its scalar satisfies $g^*_+(s)=g^*_-(s)=g^*$ for every $s$; (c) for every solution, every $h^*$-improving decision rule gives an average optimal stationary policy.

Theorem 8.4.1 (printed p. 356)

If $B(g,h)\le 0$ then $g\ge g^*_+$; if $B(g,h)\ge 0$ then $g\le\sup_{d}g^{d^\infty}_-\le g^*_-$; if $B(g,h)=0$ then $g^*_+=g^*_-=g$.

Theorem 8.4.3 (printed p. 358)

In a finite unichain model $B(g,h)=0$ has a solution, and every solution has the same $g$.

Theorem 8.4.4 (printed p. 361)

If $B(g^*,h^*)=0$ and $d^*$ is $h^*$-improving, then $(d^*)^\infty$ is average optimal.

Significance

Theorem 8.4.1(c) is what the source calls "one of the most important results for average reward models": a solution of the optimality equation with constant $g$ pins down the optimal gain under every criterion at once, so that in finite unichain models the three optimality criteria of Section 8.1.2 coincide. Theorem 8.4.3 guarantees such a solution exists, and Theorem 8.4.4 reads an optimal policy off it. Together, Theorem 8.4.5 reduces the infinite-horizon average reward problem over all history-dependent randomized policies to a finite system of equations in $(g,h)$, which is what policy iteration, value iteration and linear programming solve in Sections 8.5 to 8.8.

The results are classical and proved. Formalizing them fixes the chain-structure hypothesis in a checkable form and pins down which criterion "average optimal" means, two places where the literature is loose. The platform's MarkovDecisionProcesses series has the finite-horizon (mission I) and discounted (mission II) models; this mission adds the undiscounted stationary model, the gains, and the unichain classification, on which Chapter 9's multichain optimality equations and Chapter 10's sensitive discount optimality can be built.

Difficulty

The obvious argument for Theorem 8.4.3 is to take the discounted optimal value $v^*_\lambda$ of mission II and let $\lambda\uparrow 1$. It fails as stated because $v^*_\lambda$ blows up like $(1-\lambda)^{-1}$; what converges is the Laurent expansion $v^{d^\infty}_\lambda=(1-\lambda)^{-1}ge+h+o(1)$ of the value of a fixed stationary policy, Corollary 8.2.4, and that expansion needs the limiting matrix $P_d^*$ and the deviation matrix $H_{P_d}$ of a unichain chain. So the proof must first develop the Markov chain theory of Section 8.2 and Appendix A, choose a subsequence of discount factors along which one policy is discount optimal (possible because $D^{MD}$ is finite), and only then pass to the limit in the discounted optimality equation.

Theorem 8.4.1 looks elementary and hides the analytic step: iterating $ge\ge r_d+(P_d-I)h$ along an arbitrary history-dependent policy and dividing by $N$ requires the telescoping term $N^{-1}(P^\pi_N-I)h$ to vanish, which uses boundedness of $h$, and requires the reduction from history-dependent randomized to Markov randomized policies (Theorem 8.1.2). For Theorem 8.4.4 the step is Corollary 8.2.7, that $r_d-ge+(P_d-I)h=0$ forces the gain of $d^\infty$ to be $g$, which is the multiplication by $P_d^*$ that annihilates $(P_d-I)$.

The traps are in the definitions. Recurrence and the unichain property must be stated so that the source's Example 8.4.3 comes out as the book says — the policy using $a_{1,1}$ has the absorbing state $s_2$ as its single recurrent class — and the optimality residual must use the lim sup / lim inf gains, since a definition through a limit that need not exist would be a junk value on the policies of Example 8.1.1.

Formalization scope

State and action spaces are Fintypes and admissible actions are nonempty Finsets, as in missions I and II; the stationary model is a new structure because mission II's DiscountedMDP bundles a discount factor, and carries the same data otherwise. Policies are history-dependent and randomized, so "average optimal" has its full strength; a stationary policy is the deterministic one built from a decision rule. Expected total reward is defined by the policy evaluation recursion, as in the earlier missions, rather than through a measure on trajectories.

Gains are Filter.limsup and Filter.liminf of $N^{-1}v^\pi_{N+1}(s)$ on $\mathbb R$; these are the source's because the sequence is bounded by $\max|r|$, and the suprema $g^*_\pm$ over the nonempty family of policies are genuine real suprema for the same reason. The residual $B(g,h)$ is a Finset.sup' over the admissible actions. Recurrence is "every state reachable from $i$ reaches $i$" and unichain is "any two recurrent states communicate", the definitions of Appendix A for finite chains, applied to $P_d$ for every admissible deterministic decision rule.

Restrictions relative to the printed text, all noted in the items: Theorem 8.4.1 is stated for finite $S$ where the source says countable, since the chapter's standing assumption and the model are finite; the gain $g^{d^\infty}$ of a stationary policy in (8.4.5) is written as its lim inf gain, which equals it; and the chain $ge=g^*=g^*_+=g^*_-$ of (8.4.6) is stated through $g^*_+$ and $g^*_-$, since $g^*$ presupposes existing limits. Nothing is trivialized: the existential in Theorem 8.4.5(a) has to produce a decision rule, and $B(g,h)=0$ with a junk maximum is impossible since every $A_s$ is nonempty. Welcome contributions beyond the milestones: Theorem 8.1.2 (reduction to Markov policies), Corollary 8.2.7 (the gain of a stationary policy from the evaluation equations), and the equivalence of the three optimality criteria in finite models.

Selected references

• Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, Chapter 8. doi:10.1002/9780470316887
• Ronald A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• David Blackwell, Discrete dynamic programming, Annals of Mathematical Statistics 33 (1962). doi:10.1214/aoms/1177704593
• Cyrus Derman, Finite State Markovian Decision Processes, Academic Press, 1970.
• Paul J. Schweitzer and Awi Federgruen, The functional equations of undiscounted Markov renewal programming, Mathematics of Operations Research 3 (1978). doi:10.1287/moor.3.4.308

Motivation

Introductory physics is normally taught as a sequence of unrelated chapters — kinematics, dynamics, energy, optics, gravitation — each with its own rules. A recurring proposal in physics education is to teach instead from a single organising statement: among all conceivable histories of a system, the one realised in nature is the one that makes a certain integral, the action, stationary. Edwin Taylor's editorial A Call to Action (American Journal of Physics, 2003) argued for building the first-year curriculum on it; Lachlan McGinness and Craig Savage reported classroom results for such a course at the Australian National University (Action physics, American Journal of Physics, 2016); Massimiliano Malgieri tested a sum-over-paths treatment in an Italian secondary school (2017).

The source monograph for this mission, Julliana Rodrigues Martins, A Ação Estacionária como Eixo Unificador do Ensino de Física no Ensino Médio (Trabalho de Conclusão de Curso, Universidade Federal do Ceará, 2025), develops this programme for secondary education. Its Chapters 2 and 3 are quantitative: they follow the historical line from antiquity to the nineteenth century and carry out every calculation in full. This mission formalises that quantitative core, and nothing of the pedagogical Chapter 4.

The historical line the monograph reconstructs, and which the milestone list follows:

• Heron of Alexandria (c. 60 AD), Catoptrics: the law of reflection derived from the shortest reflected path (§2.2).
• Galileo (1638), Two New Sciences: uniformly accelerated descent on an inclined plane, and the law of chords — descent from rest along any chord of a vertical circle takes the same time (§2.3).
• Fermat (1657–1662): the method of maxima and minima, and the law of refraction obtained by minimising travel time, with the velocities entering inversely to Descartes' version (§2.4, §2.4.1).
• Maupertuis (1744, 1746): the quantity of action $mvl$, the refraction law, and the equilibrium of a lever obtained by minimising action (§2.6).
• Euler (1744), Methodus inveniendi, including Additamentum II: the discretise–vary–pass-to-the-limit method, the resulting differential equation, and Keplerian orbits from Maupertuis' principle under conservation of total energy (§2.7).
• Lagrange (1760, 1788) and Hamilton (1834–1835): the general variational derivation and the principle of stationary action $\delta\int (T-U)\,dt = 0$ (Chapter 3, §3.1).

Setting

Fix real endpoints $x_1 < x_2$ and an integrand $f(y, y', x)$, a real-valued function of three real arguments. A path is a function $y : \mathbb{R} \to \mathbb{R}$, and its action over $[x_1,x_2]$ is

$$S[y] \;=\; \int_{x_1}^{x_2} f\bigl(y(x),\, y'(x),\, x\bigr)\, dx .$$

Neighbouring paths are produced by an admissible variation: a twice continuously differentiable $\eta$ with $\eta(x_1) = \eta(x_2) = 0$, giving the family $y(x,\alpha) = y(x) + \alpha\,\eta(x)$. The path $y$ is stationary when

$$\left.\frac{d}{d\alpha}\, S[\,y + \alpha\eta\,]\right|_{\alpha = 0} = 0 \qquad \text{for every admissible } \eta .$$

Writing $\partial f/\partial y$ and $\partial f/\partial y'$ for the partial derivatives of $f$ in its first and second slots, the Euler–Lagrange expression along $y$ is

$$E_f[y](x) \;=\; \frac{\partial f}{\partial y}\bigl(y(x), y'(x), x\bigr) \;-\; \frac{d}{dx}\left[\frac{\partial f}{\partial y'}\bigl(y(x), y'(x), x\bigr)\right].$$

In mechanics one takes $x = t$, $y = q$ and $f = L = T - U$, so that stationarity of $\int (T-U)\,dt$ is Hamilton's principle and $E_L[q] = 0$ is the Lagrange equation of motion.

Formalization targets

Goal — the Euler–Lagrange equation from stationary action

For $x_1 < x_2$, $f$ twice continuously differentiable in all three arguments and $y$ twice continuously differentiable, if $y$ is stationary for $S$ then

$$\frac{\partial f}{\partial y} - \frac{d}{dx}\,\frac{\partial f}{\partial y'} \;=\; 0 \qquad \text{at every } x \in [x_1, x_2].$$

This is equation (3.9) of the monograph, and — through the substitution $x \mapsto t$, $y \mapsto q_i$, $f \mapsto L$ — equation (3.17). It is stated as the weakest stable form: stationarity, not minimality, and an arbitrary admissible integrand rather than a particular Lagrangian.

Milestones

The supporting statements are the analytic ingredients of that derivation (the fundamental lemma, the first variation formula, the first integral for a cyclic coordinate), its two mechanical applications worked out in the monograph (harmonic oscillator, plane pendulum), its geometric application (shortest path), and the historical minimisation problems of Chapter 2 (Heron, Galileo, Fermat, Maupertuis).

Significance

The Euler–Lagrange equation is the bridge the whole unification argument rests on: once it is available, Newton's second law, the pendulum equation, Snell's law, geodesics and conservation laws all become consequences of one statement about an integral, which is exactly the claim the monograph makes to justify teaching physics this way. The Chapter 2 statements are the historically prior special cases, each obtained by a one-variable minimisation rather than by the general machinery, and together they exhibit how far elementary optimisation alone reaches before the calculus of variations is needed.

What this mission adds beyond the source is a machine-checked version of an argument that, in every textbook presentation including this one, is carried out at the level of rigour of formal manipulation: the interchange of differentiation and integration is performed without justification, the passage from a vanishing integral to a vanishing integrand is asserted, and the regularity needed for $\frac{d}{dx}\,\partial f/\partial y'$ to exist is left implicit. All of it is true under the stated hypotheses; none of it is proved in the source. Mathlib has the analytic infrastructure (interval integrals, differentiation under the integral sign, smooth bump functions) but, at the environment pinned for this mission, no Euler–Lagrange equation and no calculus-of-variations layer built on it. The definitions published here — action, admissible variation, stationary path, Euler–Lagrange expression — are reusable by any later variational mission.

Difficulty

The obvious argument is three lines: differentiate under the integral sign, integrate by parts, and conclude that the integrand vanishes because $\eta$ is arbitrary. Each line is where the work is.

Differentiating under the integral sign needs a dominating bound valid uniformly for $\alpha$ near $0$; it is available here because the data are $C^2$ and the interval is compact, but it has to be produced. The integration by parts needs $x \mapsto \partial f/\partial y'(y(x), y'(x), x)$ to be differentiable, which is where the second derivative of $y$ and the second derivatives of $f$ are consumed — a $C^1$ path is not enough for this formulation. The final step needs test functions: a $C^2$ bump supported in a small interval around a point where the continuous coefficient is nonzero, which is why the fundamental lemma is a separate milestone rather than a step.

A standing trap in the Lean formulation is that deriv returns $0$ at points where a function is not differentiable, so a statement about $\frac{d}{dx}\,\partial f/\partial y'$ can be accidentally true for the wrong reason unless the regularity hypotheses are genuinely strong enough. Every statement here carries the hypotheses that make each derivative a real derivative.

Formalization scope

The development is one-dimensional and real: paths are $\mathbb{R} \to \mathbb{R}$, the integrand is a curried $f : \mathbb{R} \to \mathbb{R} \to \mathbb{R} \to \mathbb{R}$ with argument order $(y, y', x)$ matching the source's $f(y(x), y'(x), x)$, and all integrals are interval integrals over $[x_1, x_2]$. Partial derivatives are one-dimensional derivatives in the frozen remaining arguments; smoothness of $f$ is stated for its uncurried form on $\mathbb{R} \times \mathbb{R} \times \mathbb{R}$. Regularity is $C^2$ throughout — for the integrand, for the path, and for the variations — matching the monograph's requirement that $\eta$ have continuous first and second derivatives.

Stationarity is a hypothesis quantified over all admissible variations, so the goal cannot be satisfied by exhibiting one convenient $\eta$; and the conclusion is an equation at every point of the closed interval, not almost everywhere, so it cannot be weakened to a null-set statement. The mechanical milestones are stated as equivalences between the Euler–Lagrange equation for the explicit Lagrangian and the classical equation of motion, which rules out a one-directional reading that would be vacuous for a path that never satisfies either.

Physical constants ($m$, $k$, $g$, $\ell$, the speeds $v_1, v_2$) are free real parameters, with positivity or non-vanishing assumed only where the source's conclusion requires it — the pendulum equivalence divides by $m\ell^2$, so $m \neq 0$ and $\ell \neq 0$ appear, while the oscillator equivalence needs no such assumption. Angles never appear as primitive objects in the optics milestones: the sines of the incidence and refraction angles are written as the ratios $x/\sqrt{a^2+x^2}$ that the figures define them by, so no convention about angle ranges is smuggled in.

Contributions welcome: proofs of any milestone, and reusable infrastructure for differentiation under the interval integral sign and for $C^k$ bump functions with prescribed support, both of which are of use well beyond this mission.

Selected references

• Julliana Rodrigues Martins, A Ação Estacionária como Eixo Unificador do Ensino de Física no Ensino Médio, Trabalho de Conclusão de Curso (Licenciatura em Física), Universidade Federal do Ceará, Fortaleza, 2025, 60 pp. (the source of every statement in this mission; Chapters 2–3).
• Alberto Rojo and Anthony Bloch, The Principle of Least Action: History and Physics, Cambridge University Press, 2018 (the historical reconstruction the monograph follows for Chapter 2).
• Edwin F. Taylor, A call to action, American Journal of Physics 71 (2003), guest editorial.
• Lachlan P. McGinness and Craig M. Savage, Action physics, American Journal of Physics 84 (2016).
• Massimiliano Malgieri, Test on the effectiveness of the sum over paths approach in favoring the construction of an integrated knowledge of quantum physics in high school, 2017.
• Leonhard Euler, Methodus inveniendi lineas curvas maximi minimive proprietate gaudentes, Lausanne, 1744, in particular Additamentum II.

Motivation

A fusion reactor only makes sense if the plasma gives back more energy than it loses. In 1955 J. D. Lawson turned that sentence into an inequality: for a hot, thermalized fuel, the product of the particle density $n$ and the energy confinement time $\tau_E$ must exceed a temperature-dependent threshold before the fusion products alone can keep the plasma hot. The criterion was published in 1957 (Lawson, Some Criteria for a Power Producing Thermonuclear Reactor, Proc. Phys. Soc. B 70 (1957) 6–10) and has been the standard figure of merit for magnetic and inertial confinement ever since: machines are compared by their $n\tau_E$ and by the triple product $nT\tau_E$.

Timeline, as far as this mission's material traces it:

• 1955 — Lawson derives the criterion in a classified AERE report, balancing the volumetric fusion rate against bremsstrahlung radiation losses and ignoring conduction losses.
• 1957 — the report is declassified and published.
• 2004 — the textbook derivation in the form used here, together with the reactivity fit $\langle\sigma v\rangle \approx 1.1\cdot 10^{-24}\,T^2\ \mathrm{m^3/s}$ valid near $T = 14$ keV (J. Wesson, Tokamaks, 3rd ed., Oxford, 2004).
• 2022 — an inertial-confinement experiment at the National Ignition Facility is reported to exceed the Lawson criterion for ignition (Abu-Shawareb et al., Phys. Rev. Lett. 129, 075001).

Setting

Consider a steady-state, fully ionized plasma of deuterium and tritium. All quantities are real numbers and strictly positive, and the temperature $T$ is measured in energy units (electronvolts), so Boltzmann's constant does not appear: the article's $k_\mathrm{B}T$ is our $T$.

• $n$ — the particle (electron) density. Under the standing assumptions of the derivation — all species at the same temperature, no ions other than fuel ions (no impurities, no helium ash), and deuterium and tritium in the optimal 50-50 mixture — the ion density equals the electron density and $n_\mathrm{d} = n_\mathrm{t} = n/2$.
• $W = 3nT$ — the energy density of electrons and ions together, by the ideal gas law.
• $\langle\sigma v\rangle$ — the fusion cross section times relative velocity, averaged over the Maxwellian velocity distribution at temperature $T$.
• $f = n_\mathrm{d} n_\mathrm{t}\langle\sigma v\rangle$ — the volume rate of fusion reactions (reactions per volume per time), which for the 50-50 mixture equals $\tfrac14 n^2\langle\sigma v\rangle$.
• $E_\mathrm{ch}$ — the energy carried by the charged fusion products, the only part that can heat the plasma; $E_\mathrm{ch} = 3.5$ MeV for D-T, the neutron's 14.1 MeV being lost.
• $P_\mathrm{loss}$ — the power loss density, and $\tau_E = W/P_\mathrm{loss}$ — the energy confinement time.

The plasma is self-heating when fusion heating exceeds the losses:

$$f\,E_\mathrm{ch} \;\ge\; P_\mathrm{loss}.$$

Target

The goal theorem is the Lawson criterion itself — equation (1) of the source — obtained by substituting the model quantities into the self-heating condition:

$$n\,\tau_E \;\ge\; L \;\equiv\; \frac{12\,T}{E_\mathrm{ch}\,\langle\sigma v\rangle}.$$

The milestones are the surrounding statements of the same derivation, in the order a reader meets them:

$$f = \tfrac14 n^2\langle\sigma v\rangle,\qquad P_\mathrm{loss} = \frac{3nT}{\tau_E},\qquad \tfrac14 n^2\langle\sigma v\rangle E_\mathrm{ch} \ge \frac{3nT}{\tau_E},$$

the triple-product form and its numerical D-T value,

$$nT\tau_E \;\ge\; \frac{12}{E_\mathrm{ch}}\frac{T^2}{\langle\sigma v\rangle},\qquad nT\tau_E \;\ge\; 3\cdot 10^{21}\ \mathrm{keV\,s\,m^{-3}}\quad (E_\mathrm{ch} = 3500\ \mathrm{keV},\ \langle\sigma v\rangle = 1.1\cdot10^{-24}T^2),$$

the inertial-confinement form obtained from $\tau_E \approx R\sqrt{m_i/T}$,

$$n R \;\ge\; \frac{12\,T^{3/2}}{E_\mathrm{ch}\langle\sigma v\rangle\sqrt{m_i}},$$

and the empirical tokamak scaling: if $\tau_E = c\,n^{1/3}/P^{2/3}$ and $P = a\,n^2T^2$, then $nT\tau_E = c\,a^{-2/3}T^{-1/3}$, independent of the density.

Significance

The result itself. The criterion is what makes different confinement concepts comparable at all: it converts "does this machine work?" into a single number that can be measured and plotted, and its triple-product form is the quantity reported by tokamaks and by inertial-confinement shots alike. The last milestone explains why the triple product, rather than $n\tau_E$, is the quantity of record for tokamaks: under the empirical energy-confinement scaling it does not depend on the density and depends on temperature only as $T^{-1/3}$.

Formalizing it. Nothing here is an open problem: every statement is a known consequence of the stated model, and the mathematical content is algebra and monotonicity over the positive reals. What the mission produces is a machine-checked, reusable encoding of the energy-balance model of a D-T plasma, with every degenerate case (zero density, zero confinement time, vanishing reactivity) explicitly excluded, and with the chain from the model assumptions to each published form of the criterion verified end to end. The value is in the faithfulness of the model layer, not in the difficulty of the deductions.

Difficulty

The deductive content is elementary; the difficulty is representational. Three places where a careless encoding silently changes the theorem:

• Division. $\tau_E = W/P_\mathrm{loss}$ and $12T/(E_\mathrm{ch}\langle\sigma v\rangle)$ are total functions in Lean and return $0$ on zero denominators. Without strict positivity of $n$, $T$, $\langle\sigma v\rangle$, $E_\mathrm{ch}$, $\tau_E$ and $P_\mathrm{loss}$, several of these statements become false or empty rather than merely degenerate.
• Direction of the inequality. The self-heating hypothesis and the conclusion point the same way only because one multiplies by the positive quantity $\tau_E/(n\,E_\mathrm{ch}\langle\sigma v\rangle)$; the factor $12 = 4\cdot 3$ comes from the $\tfrac14$ of the 50-50 mixture and the $3$ of $W = 3nT$, and either one dropped leaves a statement that still compiles.
• Fractional powers. The inertial-confinement and tokamak milestones involve $T^{3/2}$, $n^{1/3}$, $P^{2/3}$; these are Real.rpow, whose rules require positive bases, which is why the positivity hypotheses appear again there.

Formalization scope

The model is a Lean structure LawsonCriterion.DTPlasma bundling $n$, $T$, $\langle\sigma v\rangle$, $E_\mathrm{ch}$, $\tau_E$, $P_\mathrm{loss}$, all of type ℝ, with a strict-positivity field for each and one defining equation, tauE = energyDensity n T / Ploss where energyDensity n T = 3 * n * T. The 50-50 reaction rate is DTPlasma.rate, the heating rate is DTPlasma.fusionHeating = rate * Ech, and DTPlasma.SelfHeating is the proposition fusionHeating ≥ Ploss. Conventions this commits to:

• temperature in energy units, so T is $k_\mathrm{B}T$; the numerical milestone additionally fixes keV for T and Ech, m³/s for sigmav, and so keV·s·m⁻³ for the triple product;
• only the 50-50 D-T mixture and the charged-product energy enter; bremsstrahlung, conduction and impurities are not modelled separately — they are whatever Ploss is;
• Real.rpow for the fractional exponents, Real.sqrt for the thermal speed.

The statements are not vacuous: the definition file also publishes a witness, LawsonCriterion.unitDTPlasma, so the structure is inhabited and every hypothesis set here is satisfiable. Conversely, no statement is trivially true — each is an inequality between quantities that genuinely vary with the plasma parameters.

Contributions welcome beyond the listed milestones: a version that separates radiation from conduction losses, the D-D and D-³He variants, and the statement that $T \mapsto T/\langle\sigma v\rangle$ attains a minimum for a realistic reactivity model — the step where the source passes from the inequality to its "absolute lower limit", which this mission does not formalize.

Selected references

• J. D. Lawson, Some Criteria for a Power Producing Thermonuclear Reactor, Proceedings of the Physical Society, Section B 70 (1957) 6–10. doi:10.1088/0370-1301/70/1/303
• J. Wesson, Tokamaks, Oxford Engineering Science Series 48, 3rd ed., Clarendon Press, 2004.
• H. Abu-Shawareb et al., Lawson Criterion for Ignition Exceeded in an Inertial Fusion Experiment, Physical Review Letters 129, 075001 (2022). doi:10.1103/PhysRevLett.129.075001
• Lawson criterion, Wikipedia, revision 1367242125 — the source text this mission formalizes. link

Motivation

Hubble's law — officially the Hubble–Lemaître law — is the observation that galaxies recede from us at a speed proportional to their distance, $v = H_0 D$. It is the first observational basis for the expansion of the universe and one of the standard pieces of evidence cited for the Big Bang model. Georges Lemaître derived the proportionality from relativistic cosmology in 1927; Edwin Hubble published the observational relation in 1929, building on Vesto Slipher's redshifts and Henrietta Swan Leavitt's Cepheid distance scale. Alexander Friedmann had already shown in 1922 that the Einstein field equations admit expanding solutions, with an expansion rate governed by what is now called the scale factor.

Behind the astronomy sits a piece of elementary mathematics that is rarely written out in full: in a spatially homogeneous expansion, the linear velocity–distance relation is forced, it holds with the same constant for every observer, and the Hubble "constant" is in fact a function of time whose evolution is fixed by a single dimensionless parameter. This mission formalizes that kinematic core: the statements are about the scale factor and its derivatives, and involve no Einstein equations.

Setting

A scale factor is a function $a : \mathbb{R} \to \mathbb{R}$ of cosmic time $t$. A comoving point is labelled by a fixed coordinate $\mathbf{x} \in \mathbb{R}^3$ (with the Euclidean norm), and its proper position at time $t$ is

$$\mathbf{X}_{\mathbf{x}}(t) \;=\; a(t)\,\mathbf{x}.$$

The proper distance between the comoving points $\mathbf{x}$ and $\mathbf{y}$ is

$$D_{\mathbf{x},\mathbf{y}}(t) \;=\; \lVert a(t)\mathbf{x} - a(t)\mathbf{y}\rVert .$$

The Hubble parameter and the dimensionless deceleration parameter are

$$H(t) \;=\; \frac{\dot a(t)}{a(t)},\qquad q(t) \;=\; -\,\frac{\ddot a(t)\,a(t)}{\dot a(t)^{2}} .$$

$H_0$ denotes the present-day value of $H$; the name "Hubble constant" refers to the fact that $H$ is constant in space at a fixed time, not in time.

Target

The goal theorem is the idealized Hubble law, stated in the source as a theorem of Euclidean geometry: any two points moving away from the origin, each along a straight line and with speed proportional to its distance from the origin, move away from each other with a speed proportional to their distance apart. Formally, for $H \ge 0$, a time $t$ and curves $p, q : \mathbb{R} \to \mathbb{R}^3$ with

$$p'(t) = H\,p(t), \qquad q'(t) = H\,q(t),$$

the separation satisfies

$$\frac{d}{ds}\Big|_{s=t}\big(p(s) - q(s)\big) \;=\; H\,\big(p(t) - q(t)\big), \qquad \big\lVert H\,(p(t)-q(t))\big\rVert \;=\; H\,\lVert p(t)-q(t)\rVert .$$

The relative velocity is parallel to the separation vector and its magnitude is $H$ times the separation, with the same $H$ for every pair — so no comoving observer occupies a distinguished centre of the expansion.

The milestones supply the cosmological content that surrounds this geometric fact:

1. proper distances scale as $D(t) = \big(a(t)/a(t_0)\big) D(t_0)$;
2. a comoving point has velocity $H(t)$ times its proper position vector;
3. Hubble's law itself, $\dot D(t) = H(t)\,D(t)$;
4. the evolution law $\dot H = -(1+q)H^{2}$;
5. the zero-deceleration case: if $q \equiv 0$ then $H(t) = 1/t$, with $t$ the time since the Big Bang, so the Hubble time $1/H$ is exactly the age;
6. a constant Hubble parameter forces exponential growth $a(t) = a(t_0)e^{H_0(t-t_0)}$;
7. the small-redshift limit: with $1 + z = a(t_0)/a(t_\mathrm{e})$, the ratio $z/(t_0 - t_\mathrm{e})$ tends to $H(t_0)$ as $t_\mathrm{e} \to t_0$, which is the $z \approx H_0 D/c$ form of the law used observationally.

Significance

The result itself is elementary but load-bearing: it is what licenses reading a linear redshift–distance diagram as evidence for uniform expansion rather than for a privileged position in space, and items 4–6 are the statements through which cosmological observations (the sign of $q$, the approach of $q$ to $-1$ in $\Lambda$CDM) are turned into claims about the past and future behaviour of $H$ and $a$.

Formalizing it produces a small, reusable Lean layer for expansion kinematics: the scale factor, the Hubble and deceleration parameters, proper position and proper distance, with the differentiation lemmas that connect them. The platform already carries Friedmann-equation missions that fix the dynamics of $a$; this mission is the kinematic complement, and its Hubble parameter is the same function $\dot a/a$ that those developments use. Nothing here is an open research problem: every statement is a known textbook fact, and the work is the formalization.

Difficulty

The mathematical content is a few lines of calculus, so the difficulty is entirely in the encoding. Three places are easy to get wrong. First, proper distance is defined through a norm, so the identity $\lVert a(t)v\rVert = a(t)\lVert v\rVert$ needs positivity of $a$, and differentiating it needs positivity on a neighbourhood, not just at the point. Second, $q$ is defined by a quotient with $\dot a^{2}$ in the denominator: in Lean division by zero returns zero, so a statement about $q$ that forgets $\dot a(t) \ne 0$ silently changes meaning. Third, milestone 5 propagates a hypothesis stated on $(0,\infty)$ down to the endpoint $t=0$, where the Big Bang condition $a(0)=0$ lives; the continuity argument at the endpoint is the only step with any technical content.

Formalization scope

Time is $\mathbb{R}$ and space is EuclideanSpace ℝ (Fin 3); derivatives are Mathlib's deriv / HasDerivAt, so "velocity" is always a derivative at a point rather than a difference quotient. Smoothness is assumed exactly where it is used: differentiability at a single time for the first-order statements, ContDiff ℝ 2 for the statements involving $\ddot a$. Positivity of the scale factor is stated explicitly wherever it is needed, as is $\dot a(t) \ne 0$ in the statements mentioning $q$.

Degenerate readings are excluded: the goal's hypotheses are satisfiable (any pair of comoving points in an expanding universe satisfies them, as milestone 2 shows), and the milestones are non-vacuous for concrete scale factors such as $a(t) = t$ and $a(t) = e^{H_0 t}$. The goal theorem's second clause is a norm identity that is true for every $H \ge 0$; it carries the "speed proportional to distance" half of the source's statement, while the first clause carries the "moving away from each other along the separation" half.

The definition layer is a single self-contained file (scale factor derived quantities, proper position, proper distance); it is reusable by any mission about expansion kinematics. Contributions of the milestone proofs, and of variants such as the redshift relation $1+z = a(t_0)/a(t_\mathrm{e})$ derived from null geodesics rather than assumed, are welcome.

Selected references

• Wikipedia, "Hubble's law" (Hubble–Lemaître law), https://en.wikipedia.org/wiki/Hubble%27s_law — the source text for this mission, in particular the sections "Recessional velocity", "Time-dependence of Hubble parameter", "Idealized Hubble's law" and "Ultimate fate and age of the universe".
• E. Hubble, "A relation between distance and radial velocity among extra-galactic nebulae", PNAS 15 (1929) 168–173, https://doi.org/10.1073/pnas.15.3.168.
• G. Lemaître, "Un univers homogène de masse constante et de rayon croissant rendant compte de la vitesse radiale des nébuleuses extra-galactiques", Annales de la Société Scientifique de Bruxelles A47 (1927) 49–59.
• A. Friedmann, "Über die Krümmung des Raumes", Zeitschrift für Physik 10 (1922) 377–386, https://doi.org/10.1007/BF01332580.

Motivation

Battery-powered and energy-harvesting wireless devices cannot treat transmission power as free: a control algorithm that maximizes throughput without regard to energy will drain a device long before the network's other resources are exhausted. Chapter 6 of Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) extends the drift-plus-penalty framework of Chapter 5 to problems with an explicit average-resource-budget constraint, and works out the Energy Constrained Control Algorithm (ECCA) of Neely [116] as its flagship example: a joint flow-control and power-allocation policy that keeps every data queue and a virtual "excess energy" queue bounded by an explicit, finite constant on every single time slot — not merely in expectation or in the long run.

Setting

A multi-user wireless downlink serves $L$ users over $L$ channels with a time-varying collective topology state $S(t)$ and link rate function $C_i(P,S(t))$ under power allocation $P=(P_1,\dots,P_L)$, subject to a per-slot power budget $\sum_i P_i(t)\le P_{max}$ and a target average power constraint $P_{av}<P_{max}$. Exogenous arrivals $A_i(t)\le\hat R$ are entirely admitted or entirely dropped each slot (no transport-layer storage). The ECCA algorithm runs, every slot: flow control — admit $A_i(t)$ into queue $i$ if $U_i(t)\le V$ (a fixed parameter), otherwise drop it entirely; power allocation — choose $P(t)$ to maximize $\sum_i[U_i(t)C_i(P,S(t))-D(t)P_i(t)]$ subject to the power budget, where $D(t)$ is a virtual power queue tracking accumulated excess energy expenditure, updated by $D(t{+}1)=\max[D(t)-P_{av},0]+\sum_i P_i(t)$.

Formalization targets

Goal — Theorem 6.3 (ECCA Performance)

$$U_i(t)\le U_{max}:=V+\hat R\ \ \forall i,t,\qquad D(t)\le D_{max}:=\beta V+\beta\hat R+P_{max}\ \ \forall t,$$

$\text{and consequently, for every $T$-slot interval, } \sum_{\tau} \textstyle\sum_i P_i(\tau) \le P_{av}\cdot T+D_{max},$ where $\beta>0$ is the constant in the rate function's marginal-benefit inequality $C_i(P,S)\le C_i(P^{[i]},S)+\beta P_i$ ($P^{[i]}$ being $P$ with its $i$-th entry zeroed). These bounds hold for every topology state process $S(t)$ and every admissible arrival process $A(t)$, on every sample path — the weakest, most general level, with no distributional assumption whatsoever on either process.

Significance

Theorem 6.3 gives a hard, deterministic worst-case guarantee — every queue in the system, actual or virtual, is bounded by an explicit closed-form constant on every single slot, not merely on average or asymptotically — which is exactly the kind of guarantee a resource-constrained embedded or battery-powered device needs: a device can be provisioned with buffer and battery-reserve capacity of the theorem's own $U_{max}$, $D_{max}$ and know, with certainty rather than in expectation, that it will never overflow. The corollary that no $T$-slot interval spends more than $P_{av}\cdot T+D_{max}$ in energy translates directly into a battery-lifetime guarantee. This is also, methodologically, the one point in the whole book's drift-plus-penalty method where an elementary induction — not a probabilistic Lyapunov drift argument — suffices, because ECCA's flow control rule directly caps $U_i(t)$ regardless of what the channel or arrivals do.

Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for virtual queue, energy-constrained control, power allocation — no faithful hits; one unrelated coincidental keyword match in a neural-coding combinatorics item was checked and is not relevant). This mission is the first formalization of the ECCA performance guarantee.

Difficulty

The obvious first idea is to bound $U_i(t)$ and $D(t)$ by unrolling their recursions and applying a probabilistic drift argument, as in every other capstone in this series. This is unnecessary and would in fact obscure the actual mechanism: $U_i(t)\le U_{max}$ follows from a two-case induction that needs no probability at all — if $U_i(t)\le V$, the flow control rule admits at most $\hat R$ more, giving $U_i(t{+}1)\le V+\hat R$; if $U_i(t)>V$, flow control drops everything, so $U_i(t{+}1)\le U_i(t)\le U_{max}$ by the induction hypothesis. The harder part is $D(t)\le D_{max}$: it requires connecting the virtual queue's own accumulation to the fact that the power-allocation optimization (6.14) will stop spending power on link $i$ once $D(t)$ grows past $U_i(t)\cdot\beta$ — a consequence of $P(t)$'s optimality for (6.14) together with the $\beta$-inequality on $C_i$, not a property one can read off the $D$-recursion alone.

Formalization scope

The power-allocation rule is stated as an explicit optimality hypothesis (hPopt): for every competing power vector $P'$ respecting the budget, the objective (6.14) at the chosen $P(t)$ is at least as large — the faithful rendering of "$P(t)$ is chosen to maximize (6.14)" without needing Lean's argmax/IsMaxOn machinery. The rate function's $\beta$-inequality is stated exactly as the book gives it, using Function.update P i 0 for $P^{[i]}$. Out of scope for this mission: the throughput conclusion under i.i.d. $A(t), S(t)$ (an expectation/liminf statement, unlike the rest of this theorem, needing the same conditional-expectation machinery as the other chapters' capstones) and Theorem 6.2 (the general GCLC framework this specializes, which needs Assumptions 1-4's four simultaneous existential clauses over an "S-only" policy) — both left for a future mission. A trivializing formalization to rule out: weakening the two sample-path conclusions to a limsup/expectation-style bound (the convention used elsewhere in this series) would misstate this theorem, whose entire distinguishing content is that the bounds hold for every time slot and every sample path, not merely in the long run.

Selected references

• Georgiadis, Neely & Tassiulas, Resource Allocation and Cross-Layer Control in Wireless Networks, Foundations and Trends in Networking, Vol. 1, No. 1 (2006), pp. 1-144. https://doi.org/10.1561/1300000001
• Neely, "Energy optimal control for time-varying wireless networks", IEEE Transactions on Information Theory, 52(7), 2006. https://doi.org/10.1109/TIT.2006.876219