All missions

Motivation

A multicommodity flow problem asks to route many source–sink demands through one capacitated network at the same time. Its min-cut (sparsest cut) is the smallest ratio, over all cuts, of the capacity crossing the cut to the demand separated by it. Routing is always limited by every cut, so the max-flow never exceeds the min-cut. For a single commodity the two are equal (Ford–Fulkerson); for many commodities they are not, and the size of the gap governs a large family of approximation algorithms for graph partitioning, layout and routing problems.

Leighton and Rao (J. ACM 46 (1999), extended abstract FOCS 1988) proved that for uniform problems, where every pair of nodes demands one unit, the gap is at most $O(\log n)$ (their Theorem 2). This mission formalizes the other half: Section 2.1 of the paper, A bad example, which shows that the $\log n$ is necessary. On a 3-regular expander graph the max-flow is a $\Theta(\log n)$ factor smaller than the min-cut, so Theorem 2 cannot be improved beyond the constant.

Timeline. Ford and Fulkerson (1956) and Elias–Feinstein–Shannon (1956): single-commodity max-flow equals min-cut. Hu (1963): equality for two commodities. Leighton and Rao (1988, journal 1999): uniform and product problems have an $O(\log n)$ gap, and expanders show it is tight. Klein, Agrawal, Ravi and Rao (1990) and later Linial–London–Rabinovich (Combinatorica 1995) and Aumann–Rabani (1998): an $O(\log k)$ gap for general demands with $k$ commodities, tight by the same expander example.

Setting

Let $V$ be a finite set of $n$ nodes. A network assigns a capacity $C(u,v)\ge0$ to every pair, symmetric and zero on the diagonal. For $U\subseteq V$ with complement $\bar U$, the cut capacity $C(U,\bar U)$ is the total capacity of the pairs with one end in $U$ and the other in $\bar U$.

In the uniform multicommodity flow problem (UMFP) every pair of distinct nodes is a commodity with unit demand. Its max-flow $f$ is the largest fraction such that $f$ units of every commodity can be routed simultaneously without exceeding any capacity (concurrent flow). Its min-cut is

$$\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|}.$$

Section 2.1 takes a 3-regular $n$-node graph $G$ with unit edge capacities, so that $C(U,\bar U)=|\langle U,\bar U\rangle|$ is the number of edges between $U$ and $\bar U$, and assumes that $G$ is a $c$-edge-expander:

$$|\langle U,\bar U\rangle|\ \ge\ c\,\min\{|U|,|\bar U|\}\qquad\text{for all }U\subseteq V,$$

for a constant $c>0$. Families of such graphs exist for a sufficiently small $c$ (Margulis 1973; a random 3-regular graph has the property with high probability). Throughout, $\log$ is $\log_2$.

Formalization targets

Goal: the gap on an expander

For a 3-regular $c$-edge-expander with unit capacities and $n\ge 8$,

$$f\ \le\ \frac{6\,\mathcal S}{c\,\bigl(\lfloor\log n\rfloor-2\bigr)} .$$

This is the final display of §2.1 (pp. 794–795), with the floor that the argument actually supports (see Formalization scope). It leaves the expander family unspecified: it holds for every graph with the two properties.

Milestones, in the order the argument uses them

1. $\mathcal S\ge c/(n-1)$ for the expander (p. 794).
2. In a 3-regular graph, at most $n/2$ nodes lie within distance $\lfloor\log n\rfloor-3$ of any node.
3. Hence at least half of the source–sink pairs are at distance at least $\lfloor\log n\rfloor-2$.
4. A uniform flow of fraction $f$ uses capacity at least $\tfrac12\binom n2 f(\lfloor\log n\rfloor-2)$, and the total capacity is $3n/2$.
5. Hence $f\le 3n/\bigl(\binom n2(\lfloor\log n\rfloor-2)\bigr)=6/\bigl((n-1)(\lfloor\log n\rfloor-2)\bigr)$.

Companions: Theorem 1

Theorem 1 (p. 795) states that for any $n$ there is an $n$-node UMFP with $f\le O(\mathcal S/\log n)$. It is stated twice: conditionally on a family of 3-regular $c$-expanders (the form §2.1 proves), and unconditionally, with one constant $K$ for all $n\ge2$.

Significance

The result shows that the $O(\log n)$ max-flow min-cut gap of Leighton and Rao's Theorem 2 is tight up to the constant, and, through the same example, that the $O(\log k)$ bound for general demands is tight. Every approximation algorithm that rounds a multicommodity flow, or its dual, to a cut loses a $\Theta(\log n)$ factor in the worst case for this reason; improving on it, as Arora, Rao and Vazirani did (J. ACM 2009) with an $O(\sqrt{\log n})$ approximation for sparsest cut, requires a stronger relaxation than the flow LP.

The result is classical and proved. To our knowledge it has no machine-checked proof. Formalizing it requires the concurrent-flow LP, the uniform sparsest cut, graph distance balls in bounded-degree graphs and a counting argument that converts path lengths into capacity usage; each of these is reusable. The unconditional Theorem 1 additionally needs the existence of bounded-degree expanders on every number of nodes, which is a substantial formalization project in its own right.

Difficulty

The min-cut bound and the ball bound are elementary. The central step is milestone 4: turning "the shortest path of a commodity has at least $\ell$ edges" into "the commodity uses at least $f\ell$ units of capacity". In an arc-flow formulation a commodity is a conservation-respecting function on arcs, not a set of paths, so the step needs either a path decomposition of each commodity's flow or a weak-duality argument with unit edge lengths. The obvious attempt, summing the conservation equations directly, gives only the net flow across one cut and loses the factor $\ell$.

The unconditional Theorem 1 is hard for a different reason: the paper cites the existence of 3-regular expanders and does not prove it, and the theorem asks for every $n$, including odd $n$, where no 3-regular graph exists.

Formalization scope

Nodes are a Fintype $V$ with decidable equality and $n=|V|$. A network is a symmetric nonnegative real capacity function with zero diagonal; the unit-capacity network of a simple graph $G$ has $C(u,v)=1$ on edges and $0$ elsewhere. Commodities are ordered pairs $(s,t)$, $s\ne t$, each with demand $\tfrac12$ (the paper's footnote 2), so each unordered pair carries one unit; a flow is a nonnegative arc flow per commodity, and both directions of an edge share its capacity. The max-flow is the supremum of feasible fractions. The min-cut ranges over nonempty proper $U$ only: at $U=\emptyset$ or $V$ the ratio is $0/0$, which Lean reads as $0$ and which would make $\mathcal S=0$.

Conventions and added hypotheses:

• The floor. The page writes $\log n-2$. Its argument shows that far pairs have distance at least $\lfloor\log n\rfloor-2$, which differs from $\log n-2$ for non-integer $\log n$. The goal and milestones state $\lfloor\log n\rfloor-2$ (Nat.log 2 n), a different constant in the same $\Theta(\log n)$.
• $n\ge 8$ makes $\lfloor\log n\rfloor-2\ge1$, so the bound divides by a positive number.
• Graph distance is the extended distance, $\infty$ between components, never Lean's junk value $0$.
• Regularity is SimpleGraph.IsRegularOfDegree 3.
• Theorem 1 requires the network to be connected (the paper's standing assumption, p. 789); a disconnected network has $f=\mathcal S=0$ and would make the statement empty. Its constant is quantified before $n$.
• Polynomial-time claims are not formalized.

The hypotheses of the goal are satisfiable: the 3-cube $Q_3$ ($n=8$) is 3-regular and a $1$-edge-expander. Contributions welcome: the arc-flow path-length lemma, the ball bound for bounded-degree graphs, and an existence theorem for 3-regular expanders.

Selected references

• T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
• G. A. Margulis, Explicit constructions of concentrators, Problems of Information Transmission 9(4):325–332, 1973.
• N. Linial, E. London and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
• S. Arora, S. Rao and U. Vazirani, Expander flows, geometric embeddings and graph partitioning, J. ACM 56(2):5, 2009. https://doi.org/10.1145/1502793.1502794

Motivation

Solving a system of nonlinear equations $F(x)=0$, with $F:\mathbf R^n\to\mathbf R^n$ continuously differentiable, is a basic task in numerical analysis and optimization: it is the inner step of interior-point and sequential quadratic programming methods, of implicit time-stepping for differential equations, and of equilibrium computations in operations research. Newton's method converges fast near a solution at which the derivative $F'$ is invertible, but from a poor starting point it may fail. Trust region methods are a standard globalization: each step minimizes the norm of the local linear model $F(x_k)+F'(x_k)s$ over a ball $\|s\|\le\delta_k$, and the radius $\delta_k$ is shrunk or enlarged according to how well the model predicted the actual decrease of $\|F\|$ (Moré and Sorensen 1983; Dennis and Schnabel 1983, §6.4).

Eisenstat and Walker (1994) developed a general global convergence theory for inexact Newton methods, in which steps only reduce the linear model's norm by a factor $\eta_k<1$ and must also give sufficient decrease of $\|F\|$. Their §4, Application 1, shows that this theory also covers trust region methods. This mission formalizes that application.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ (the paper's $\mathbf R^n$; the norm need not be Euclidean), and $F:E\to E$ continuously differentiable with derivative $F'(x)$. For a point $x_k$ and a step $s$, the actual reduction and predicted reduction are

$$\operatorname{ared}_k(s)=\|F(x_k)\|-\|F(x_k+s)\|,\qquad \operatorname{pred}_k(s)=\|F(x_k)\|-\|F(x_k)+F'(x_k)s\|.$$

A point $x$ is a stationary point of $\|F\|$ if $\|F(x)\|\le\|F(x)+F'(x)s\|$ for every $s$: no step decreases the norm of the linear model. A point $x_*$ is a limit point of $(x_k)$ if every ball around $x_*$ contains $x_k$ for infinitely many $k$.

Algorithm TR is given $x_0$, $\bar\delta_0>0$, $0<t\le u<1$ and $0<\theta_{\min}<\theta_{\max}<1$. At iteration $k$ it sets $\delta_k=\bar\delta_k$ and picks a step

$$s_k\in\arg\min_{\|s\|\le\delta_k}\|F(x_k)+F'(x_k)s\|.\tag{4.5}$$

While $\operatorname{ared}_k(s_k)<t\cdot\operatorname{pred}_k(s_k)$, it replaces $\delta_k$ by $\theta\delta_k$ for some $\theta\in[\theta_{\min},\theta_{\max}]$ and picks a new $s_k$ by (4.5). Then $x_{k+1}=x_k+s_k$, and the next initial radius satisfies $\bar\delta_{k+1}\ge\delta_k$ if $\operatorname{ared}_k(s_k)\ge u\cdot\operatorname{pred}_k(s_k)$, and $\bar\delta_{k+1}\ge\theta_{\min}\delta_k$ otherwise. The algorithm does not break down if it generates an infinite sequence of iterates.

Formalization targets

Goal: Theorem 4.4

If Algorithm TR does not break down, then

$$\text{every limit point } x_* \text{ of } (x_k) \text{ is a stationary point of } \|F\|,$$

and if $x_*$ is a limit point with $F'(x_*)$ invertible, then

$$F(x_*)=0,\qquad x_k\to x_*,\qquad s_k=-F'(x_k)^{-1}F(x_k)\ \text{for all sufficiently large }k.$$

The statement has no constants, and it holds for every choice the algorithm leaves open: the minimizer in (4.5), the factors $\theta$, and the new radii.

Milestones

1. Corollary 3.7. Any sequence with $\operatorname{pred}_k(s_k)\ge0$ and $\operatorname{ared}_k(s_k)\ge t\cdot\operatorname{pred}_k(s_k)$, $s_k=x_{k+1}-x_k$, for which $\|s_k\|\le\Gamma\cdot\operatorname{pred}_k(s_k)$ near a limit point $x_*$, converges to $x_*$.
2. Lemma 4.2. If $F'(x_*)$ is invertible, then for some $\Gamma>0$, $\epsilon_*>0$, every minimizer $s$ of (4.5) with any radius $\delta>0$ and $\|x-x_*\|<\epsilon_*$ satisfies $\|s\|\le\Gamma\{\|F(x)\|-\|F(x)+F'(x)s\|\}$ (4.6).
3. Lemma 4.3. If $x_*$ is not a stationary point of $\|F\|$, then (4.6) holds for radii $0<\delta\le\delta_*$ and $x$ near $x_*$.
4. Lemma 4.1. For a run of Algorithm TR, if $\|s_k\|\le\Gamma\cdot\operatorname{pred}_k(s_k)$ (4.1) holds for every trial step of iterations with $x_k$ near a limit point $x_*$ and $k$ large, then $x_k\to x_*$ and $\liminf_k\delta_k>0$.

An extra item, Corollary 3.6, states that such a sequence with $\sum_k\operatorname{relpred}_k(s_k)$ divergent has $F(x_k)\to0$, where $\operatorname{relpred}_k(s_k)=\operatorname{pred}_k(s_k)/\|F(x_k)\|$ (or $1$ if $F(x_k)=0$).

Significance

Theorem 4.4 is a global convergence result that assumes neither bounded level sets, nor the existence of a solution, nor an inner-product norm. It separates two conclusions: without any regularity, the only possible accumulation points are stationary points of $\|F\|$; at an accumulation point where $F'$ is invertible, the method finds a solution, converges to it, and eventually takes the full Newton step. The paper assumes only continuous differentiability, which does not by itself give a quadratic convergence rate. Lemmas 4.2 and 4.3 are local facts about minimizers of the linear model's norm over a ball and apply to any method that uses such steps.

The result is proved in the paper. As far as we know, none of it is formalized: Mathlib has the Fréchet derivative, the inverse function theorem and invertible continuous linear maps, but no trust region or inexact Newton convergence theory. This mission produces machine-checked versions of the paper's statements for an arbitrary norm, together with a reusable vocabulary (actual/predicted reduction, stationary points of $\|F\|$, model minimizers, trust region runs) for later formalizations of trust region and Levenberg–Marquardt type methods.

Difficulty

The obvious argument shows that $\|F(x_k)\|$ decreases, so it converges, and then tries to conclude that the predicted reductions tend to zero. That step fails without control on the radii: if $\delta_k\to0$, small predicted reductions say nothing about stationarity, and the steps could shrink while the iterates still wander. The central difficulty is to show that near a non-stationary or regular limit point the radii stay bounded away from zero, while at the same time proving that the whole sequence converges to that limit point, not just a subsequence. Under an arbitrary norm the model minimizer is not unique and the model norm is not smooth, so arguments based on gradients of $\frac12\|F\|_2^2$ do not apply.

Formalization scope

• $\mathbf R^n$ with an arbitrary norm is a finite-dimensional real normed space E; $F'$ is fderiv ℝ F, and "continuously differentiable" is ContDiff ℝ 1 F.
• A run of Algorithm TR is the predicate IsTRRun. Iteration $k$ records the number $m_k$ of while-loop passes, the factors $\theta_{k,j}\in[\theta_{\min},\theta_{\max}]$, and trial steps $s_{k,0},\dots,s_{k,m_k}$, each a minimizer of (4.5) for its radius. Trials $j<m_k$ fail the test $\operatorname{ared}\ge t\cdot\operatorname{pred}$, and trial $m_k$ passes it. "Does not break down" is the existence of such a run. Any minimizer in (4.5) may be chosen.
• "Limit point" is MapClusterPt. "Sufficiently near $x_*$ and $k$ sufficiently large" is: there exist $\rho>0$ and $K$ such that the property holds for $k\ge K$ with $\|x_k-x_*\|<\rho$. "Whenever $k$ is sufficiently large" is ∀ᶠ k in atTop.
• "$F'(x_*)$ invertible" is (fderiv ℝ F xstar).IsInvertible. $F'(x_k)^{-1}$ is ContinuousLinearMap.inverse, which is the true inverse for all large $k$.
• "$\liminf\delta_k>0$" is "eventually $\delta_k\ge c$ for some $c>0$"; "$\sum\operatorname{relpred}$ divergent" is ¬ Summable.
• In Lemma 4.1, (4.1) is required for every trial step $s_{k,j}$ of iterations with $x_k$ near $x_*$ and $k$ large: in Algorithm TR the symbol $s_k$ takes the value of each trial step, and the proof on p. 403 applies (4.1) to trial steps. Requiring it for the accepted step alone would make the lemma false. Lemmas 4.2 and 4.3 are stated with $\Gamma>0$.
• No statement assumes $F(x_*)=0$, $x_k\to x_*$, bounded level sets, a Euclidean norm or a Lipschitz derivative: those are conclusions or absent from the paper. A run predicate that forced zero steps or zero radii would make the convergence claims trivial; IsTRRun forces neither, and it has a run with nonzero steps (for $F=\mathrm{id}$ on $\mathbf R$).

Needed infrastructure: the continuity of $x\mapsto F'(x)^{-1}$ near an invertible point (Lemma 1.1 of the paper), a uniform linearization bound $\|F(y)-F(x)-F'(x)(y-x)\|\le\varepsilon\|y-x\|$ near a point (Lemma 1.2), and the telescoping argument of Theorem 3.5. These are reusable well beyond this mission. Contributions are welcome on each milestone separately, and on general lemmas about minimizers of $\|a+Ls\|$ over a ball.

Selected references

• S. C. Eisenstat and H. F. Walker, Globally Convergent Inexact Newton Methods, SIAM Journal on Optimization 4(2) (1994) 393–422. https://doi.org/10.1137/0804022
• J. J. Moré and D. C. Sorensen, Computing a Trust Region Step, SIAM Journal on Scientific and Statistical Computing 4(3) (1983) 553–572. https://doi.org/10.1137/0904038
• J. E. Dennis Jr. and R. B. Schnabel, Numerical Methods for Unconstrained Optimization and Nonlinear Equations, Prentice-Hall 1983; SIAM reprint 1996. https://doi.org/10.1137/1.9781611971200
• R. S. Dembo, S. C. Eisenstat and T. Steihaug, Inexact Newton Methods, SIAM Journal on Numerical Analysis 19(2) (1982) 400–408. https://doi.org/10.1137/0719025

Motivation

A flexible manufacturing system routes several part types through a set of machines; a machine that switches from one kind of part to another must spend a set-up time first. Each machine has to decide, in real time and from local information only, which of its waiting buffers to work on and for how long. Long runs waste little time on set-ups but starve other buffers; short runs do the opposite.

Kumar and Seidman (IEEE TAC 35(3), 1990) showed in §III of the paper that natural distributed rules (clearing policies, which keep processing a buffer until it is empty) can be unstable when parts revisit machines, even though every machine has enough capacity. Their §IV gives a sufficient condition for a subclass of such rules to be stable, which is stricter than the capacity condition. §V, the subject of this mission, asks for something stronger: a simple, distributed mechanism that a supervisor can add to any scheduling policy and that makes the system stable whenever the capacity condition alone holds.

Timeline. Perkins and Kumar (1989) proved that the capacity condition is sufficient for the existence of some stabilizing policy, and that every clear-a-fraction policy is stable on acyclic systems. Kumar and Seidman (1990) gave the instability examples for nonacyclic systems and the universal supervisor formalized here.

Setting

There are $P$ part types and $M$ machines. Part type $p$ arrives at rate $d_p>0$ and follows a route of $n_p$ operations; operation $i$ is done by machine $\mu_{p,i}$ and takes $\tau_{p,i}>0$ per part. Parts awaiting operation $i$ wait in buffer $b_{p,i}$, with level $x_{p,i}(t)\ge 0$. Machine $m$ serves $B_m=\{b_{p,i}:\mu_{p,i}=m\}$, and switching from $b$ to $b'$ costs $\delta_{b,b'}\ge 0$. Flows are continuous: a machine processing a nonempty buffer $b_{p,i}$ drains it at rate $1/\tau_{p,i}$, the output feeds $b_{p,i+1}$ instantly, and a machine on an empty buffer passes its inflow through. Each machine works in runs: a set-up, then a processing phase on one buffer.

The load of machine $m$ and the capacity condition are

$$\rho_m:=\sum_{(p,i):\,\mu_{p,i}=m}d_p\tau_{p,i}<1\qquad(1\le m\le M). \tag{1}$$

The system is stable if $\sup_{0\le t<\infty}x_{p,i}(t)<\infty$ for every buffer.

The supervisor picks $\gamma_m$ with

$$\gamma_m(1-\rho_m)>\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b} \tag{24}$$

and thresholds $z_{p,i}\ge0$. It truncates every processing run of $b_{p,i}$ at $\gamma_m d_p\tau_{p,i}$; it keeps a first-come first-served queue $Q_m$ of the buffers that are not being processed and whose level exceeds $z_{p,i}$; when a run ends and $Q_m\ne\emptyset$, the head of $Q_m$ is processed next, for exactly $\gamma_m d_p\tau_{p,i}$ unless it clears earlier. When $Q_m$ is empty the underlying policy is free. Write $\zeta_m:=\gamma_m(1-\rho_m)-\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b}>0$ (26) and $\beta_{p,i}(t):=\sum_{j\le i}\tau_{p,i}x_{p,j}(t)$, the backlog of part type $p$ for machine $\mu_{p,i}$.

Formalization targets

Goal: Theorem 2

Under (1), (24) and $z\ge 0$, every supervised trajectory, from every initial state, satisfies

$$\sup_{0\le t<\infty}x_{p,i}(t)<+\infty\qquad\text{for all }p,i.$$

The bound is allowed to depend on the trajectory; no uniformity in the initial state is claimed.

Milestones: Lemma 1

1. A buffer that enters $Q_m$ at $t_{\rm in}$ completes its next run by $t_{\rm in}+\gamma_m-\zeta_m$ (25).
2. If it enters $Q_m$ with $x_{p,i}(t_{\rm in})\ge\gamma_m d_p$, that run lowers the backlog: $\beta_{p,i}(t_{\rm complete})\le\beta_{p,i}(t_{\rm in})-\zeta_m d_p\tau_{p,i}$.
3. A buffer that enters $Q_m$ at $t_{\rm in}$ and stays above $\max(\gamma_md_p,z_{p,i})$ (strictly above $z_{p,i}$ after $t_{\rm in}$) up to $t'$ has $t'-t_{\rm in}\le(1+\beta_{p,i}(t_{\rm in})/(\zeta_md_p\tau_{p,i}))(\gamma_m-\zeta_m)$.
4. Any interval on which $x_{p,i}\ge g_{p,i}:=\max(\gamma_md_p,z_{p,i})+\gamma_md_p$ has length at most $a_{p,i}+c_{p,i}\beta_{p,i}(t)$.

Significance

The theorem separates two concerns of real-time scheduling. The underlying policy can be tuned for performance (low set-up overhead, short buffers) without any stability analysis; the supervisor guarantees stability under exactly the condition that is necessary for it. The mechanism is distributed: each machine uses only its own buffer levels. With $z=0$ it enforces FCFS with truncated runs; with large $z$ and $\gamma$ it never intervenes on a policy that is already stable, so the degree of intervention is tunable. Combined with the §III instability examples, it shows that instability of clearing policies is a design defect that a local safeguard removes.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of continuous-flow manufacturing systems with set-up times and runs, a formal definition of the supervisor, and the four parts of Lemma 1 as reusable statements about it. Part 3) is stated with a corrected hypothesis (see Formalization scope).

Difficulty

The underlying policy is arbitrary, so no structure of the trajectory between interventions can be used: the policy may idle on empty buffers, switch at will, and re-select a buffer as soon as its run is truncated. The natural approach of bounding the total work at a machine fails, because work arrives at machine $m$ from upstream machines whose behaviour depends on $m$ itself through re-entrant routes, so a machine-by-machine argument is circular. A further difficulty is that the supervisor acts only on buffers above their thresholds, so a buffer can be ignored for as long as it sits at or below $z_{p,i}$; any bound has to account for the time spent below the threshold and for repeated re-entries into $Q_m$, with a set-up paid at each.

Formalization scope

• Model. Part types Fin P, machines Fin M, buffers Σ p, Fin (n p); paper index $i$ is Lean index $i-1$. Time is real with $t\ge0$. Set-up times satisfy $\delta_{b,b}=0$: a set-up is paid only on a switch. No transport delays or assembly, as in the paper.
• Runs. Each machine is always in a run (no idling outside runs); a run is never cut during its set-up; run starts do not accumulate; zero-length runs are allowed. Processing is at rate at most $1/\tau_b$ and only in a processing phase of $b$, and at exactly $1/\tau_b$ while $b$ is nonempty.
• Queue. Membership of $Q_m$ is determined by the trajectory: not on the current run and level strictly above $z_b$. The FCFS key is the start of the current sojourn; ties, including the initial queue at time $0$, are broken arbitrarily, so every initial queue order is covered. A buffer whose run just ended is in $Q_m$ at that instant if its level exceeds $z_b$.
• Lemma 1. Parts 1)–3) assume, as the page does, that the buffer enters $Q_m$ at $t_{\rm in}$. Part 3) adds $x_{p,i}>z_{p,i}$ on $(t_{\rm in},t']$: with the printed non-strict hypothesis the buffer can sit at exactly $z_{p,i}$, never be re-queued, and wait arbitrarily long. In 4), $c_{p,i}$ is $(\gamma_m-\zeta_m)/(\zeta_md_p\tau_{p,i})$.
• Ruled out. The base policy is not restricted to clearing, CAF or any fixed rule, the system is not restricted to few machines or acyclic routes, and the hypothesis of the goal is (24), not $\zeta_m>0$. A non-vacuity witness (one machine, one buffer) shows the class of supervised trajectories is nonempty.
• Reusable. The trajectory model (runs, set-ups, processing law) is the same as in the other missions of this series and applies to any distributed scheduling policy with set-ups.

Contributions welcome: proofs of the Lemma 1 parts, and lemmas on the model (Lipschitz continuity of levels, monotonicity of a buffer's level while it is not processed).

Selected references

• P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Trans. Automat. Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
• J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Trans. Automat. Control 34(2), 139–148, 1989. https://doi.org/10.1109/9.21085

Motivation

Exponential tail bounds for sums of bounded martingale differences (Bernstein, Bennett, Hoeffding, Freedman) are the workhorses of probability, statistics and learning theory. They bound how far a martingale can travel in a given amount of conditional variance. The converse question is just as basic: how much conditional variance does a martingale need before it reaches a given level? An answer controls the time a martingale spends below a barrier, and it is the ingredient that turns the upper half of a law of the iterated logarithm into the lower half.

David A. Freedman's paper On Tail Probabilities for Martingales (Ann. Probab. 3 (1975) 100–118) derives both kinds of result from a single observation: the exponential process $Q_\lambda(T_n, S_n)$ is a supermartingale and $R_\lambda(T_n, S_n)$ a submartingale. The first gives the inequality now called Freedman's inequality (Theorem (1.6)/(4.1)); the second gives Theorem (1.8), the subject of this mission, a lower bound on the Laplace transform of the conditional variance accumulated up to the first crossing of a level. From (1.8) the paper derives Corollary (1.9), the tail bound $P\{W_a \ge b\} < 5(a+1)/b^{1/2}$, Lévy's theorem that $\sup_n S_n = \infty$ almost surely on $\{\sum V_i = \infty\}$ (Corollary (4.5)), and, through a separate analytic argument, the lower-tail bound (1.10).

Setting

Let $(\Omega, \mathcal F, P)$ be a probability space and $\mathcal F_0 \subset \mathcal F_1 \subset \cdots$ an increasing sequence of sub-$\sigma$-fields of $\mathcal F$. Let $X_1, X_2, \dots$ be real random variables with $X_n$ measurable with respect to $\mathcal F_n$, satisfying the standing condition (1.1):

$$|X_n| \le 1 \quad\text{and}\quad E\{X_n \mid \mathcal F_{n-1}\} = 0 \qquad (n \ge 1).$$

The conditional variance of the $n$-th step is $V_n = \operatorname{Var}\{X_n \mid \mathcal F_{n-1}\}$. The partial sums are $S_n = X_1 + \cdots + X_n$ and the intrinsic time is $T_n = V_1 + \cdots + V_n$, with $S_0 = T_0 = 0$.

For a real $\lambda$, let $f(\lambda) = e^{-\lambda} - 1 + \lambda$ (positive for $\lambda > 0$), and $R_\lambda(v, y) = \exp\{\lambda y - f(\lambda) v\}$.

A stopping time is a random variable $\sigma$ with values in $\{0, 1, 2, \dots, \infty\}$ such that $\{\sigma = n\} \in \mathcal F_n$ for every $n$; it is uniformly bounded if $\sigma \le N$ everywhere for some integer $N$.

Fix a level $a > 0$. The crossing time $\tau_a$ is the least $n$ with $S_n \ge a$, and $\tau_a = \infty$ if there is none. The crossing variance is

$$W_a = T_{\tau_a} = \sum_{i=1}^{\tau_a} V_i \in [0, \infty],$$

the total conditional variance the process needs to cross the level $a$ if it crosses, and otherwise the total conditional variance $\sum_{i \ge 1} V_i$, which may be infinite.

Formalization targets

Goal: Theorem (1.8)

For every $\lambda > 0$ and $a > 0$,

$$E\{\exp[-f(\lambda) W_a]\} \ge \exp[-\lambda(a+1)],$$

with the convention $\exp[-f(\lambda)\cdot\infty] = 0$.

Milestones

1. The two-point cases of (3.7): for $X$ taking only the values $-1$ and $a > 0$ (Case 1), or only $-b$ and $a$ with $0 < b \le 1$ (Case 2), with $E(X) = 0$ and $\lambda \ge 0$,

$$E\{\exp(\lambda X)\} \ge \exp\{f(\lambda) \operatorname{Var} X\}.$$

2. Inequality (3.7): the same bound for every random variable $X \ge -1$ with $E(X) = 0$.
3. Proposition (3.6): under (1.1), $E\{R_\lambda(T_\sigma, S_\sigma)\} \ge 1$ for every $\lambda \ge 0$ and every uniformly bounded stopping time $\sigma$.
4. From (4.2): $S_n \le a + 1$ for $n \le \tau_a$, and for every $n$,

$$1 \le E\{\exp[\lambda S_{\tau_a\wedge n} - f(\lambda)T_{\tau_a\wedge n}]\} \le \exp[\lambda(a+1)]\cdot E\{\exp[-f(\lambda)T_{\tau_a\wedge n}]\}.$$

Significance

The result. Theorem (1.8) says that the Laplace transform of $W_a$ cannot be small, so $W_a$ cannot be large: a bounded martingale difference sequence crosses any level after a finite amount of conditional variance with high probability. The paper turns this into the explicit tail estimate (1.9), into Lévy's theorem that a bounded martingale with divergent conditional variance is almost surely unbounded above and below, and, combined with the upper bound (4.8) on the same Laplace transform, into the lower-tail estimate (1.10) that gives the lower half of the law of the iterated logarithm for martingales in intrinsic time. Example (4.3) of the paper shows the theorem fails when the increments are only bounded below, so the two-sided bound in (1.1) is needed.

Formalizing it. The result is classical and proved in the paper; to the best of current knowledge it has no machine-checked proof. Mathlib has conditional variance, stopping times and optional stopping for bounded stopping times, but no reverse moment-generating-function inequality such as (3.7), no submartingale property for exponential processes in intrinsic time, and no crossing-time variables valued in $[0,\infty]$. The mission produces these, with the conventions at infinity made explicit, as a base for the remaining results of the paper (Corollary (1.9), Corollary (4.5), the lower-tail bound (1.10)).

Difficulty

The obvious route is optional stopping at $\tau_a$ itself. It fails: $\tau_a$ is unbounded and may be infinite with positive probability, and Proposition (3.6) holds only for uniformly bounded stopping times. The argument must stop at $\tau_a \wedge n$, use the overshoot bound $S_{\tau_a \wedge n} \le a + 1$ (which relies on $X_n \le 1$), and pass to the limit $n \to \infty$ in a way that sends the integrand to $0$ on $\{W_a = \infty\}$; the limit exchange needs $T_n \to W_a$ in $[0, \infty]$ and $f(\lambda) > 0$. A second obstacle is the one-step inequality (3.7): it is a lower bound on a moment-generating function, valid for random variables bounded only from below, where $E\exp(\lambda X)$ may be infinite; the usual convexity bounds go in the opposite direction.

Formalization scope

The source is the published Annals of Probability article (a scanned copy); all page numbers are the journal's.

Conventions. Increments are a sequence X : ℕ → Ω → ℝ used from index $1$; $X_0$ is never read. Measurability is "$X_n$ is $\mathcal F_n$-strongly measurable for $n \ge 1$", and the two parts of (1.1) are assumed almost surely. $V_n$ is Mathlib's condVar of $X_n$ given $\mathcal F_{n-1}$; under (1.1) every $X_n$ is square-integrable, so this is a genuine conditional variance and no square-integrability hypothesis is added to the martingale statements. Stopping times are Ω → WithTop ℕ (⊤ is $\infty$). $\tau_a$ is WithTop ℕ-valued and $W_a$ is $[0,\infty]$-valued (ℝ≥0∞), built from the nonnegative parts of the $V_i$, which agree with $V_i$ almost surely. The integrand of the goal is the function that equals $e^{-f(\lambda) W_a}$ on $\{W_a < \infty\}$ and $0$ on $\{W_a = \infty\}$; replacing it by $\exp(-f(\lambda)\cdot\mathrm{toReal}(W_a))$, which is $1$ on $\{W_a = \infty\}$, would formalize a strictly weaker statement and is ruled out. In (3.7), where $\exp(\lambda X)$ need not be integrable, the expectation is a lower Lebesgue integral in $[0,\infty]$, and $X$ is assumed square-integrable so that $\operatorname{Var} X$ is finite.

Corrected misprints. Definition (1.2)(e) prints $R_\lambda(v,y) = \exp\{\lambda h - f(\lambda) v\}$; $h$ is read as $y$. The display in (4.2) prints the last factor without its expectation sign; the $E$ is restored.

Ranges. The goal uses $\lambda > 0$ and $a > 0$ as in (1.2) and (1.7); (3.6), (3.7) and its two cases are stated for $\lambda \ge 0$ as on p. 107.

Lemma (3.1) ($g(x) = (e^x - 1 - x)/x^2$ is increasing), used in Case 2, is posed in the companion mission on Freedman's inequality and not here. Contributions welcome: proofs of the milestones, a general lemma that $R_\lambda(T_n, S_n)$ is a submartingale, and Corollary (1.9) as a follow-up.

Selected references

• David A. Freedman, On Tail Probabilities for Martingales, The Annals of Probability 3(1), 1975, 100–118. https://doi.org/10.1214/aop/1176996452
• Paul Lévy, Théorie de l'addition des variables aléatoires, Gauthier-Villars, 1937 (Theorem 68, p. 247, cited in (4.5)).

Motivation

In a birth-and-death population model, an expected population curve does not determine the amount of random variation. Births and deaths can occur frequently while nearly canceling in the mean, or one of the two rates can vanish while giving the same mean. This distinction matters when a prescribed growth curve is used to model a population: two processes can agree on their expected size at every time and differ substantially in their uncertainty. In §6 of Kendall's 1948 paper, the question is posed directly: among time-varying birth and death rates giving a fixed mean curve, which choice minimizes the variance of the population size?

Kendall cites Arley's observation for constant rates with the same positive net growth. His §6 moves from that special case to an arbitrary prescribed mean curve and identifies a unique minimum-fluctuation rate pair. The paper also gives a logistic-growth example, connecting the stochastic rate choice to a familiar deterministic population law. The historical result is proved in the paper; this mission concerns its Lean formalization, including the exact time-dependent variance comparison and uniqueness claim.

Setting

The process starts with one ancestor. At time $t$, each member gives birth at rate $\lambda(t)$ and dies at rate $\mu(t)$; the rates are nonnegative. Let $n_t$ be the population size and $\bar n_t$ its expectation. Kendall works with the population probabilities and their generating function rather than constructing sample paths. This mission likewise uses his explicit formulas for the mean and variance, so that the comparison has a precise real-valued expression.

Define the integrated net death rate and the fluctuation by

$$\rho_{\lambda,\mu}(t)=\int_0^t\bigl(\mu(\tau)-\lambda(\tau)\bigr)\,d\tau, \qquad V_{\lambda,\mu}(t)=e^{-2\rho_{\lambda,\mu}(t)} \int_0^t e^{\rho_{\lambda,\mu}(\tau)} \bigl(\lambda(\tau)+\mu(\tau)\bigr)\,d\tau.$$

Kendall's equations (13) and (14c) identify $\bar n_t=e^{-\rho_{\lambda,\mu}(t)}$ and $V_{\lambda,\mu}(t)=\operatorname{Var}(n_t)$ for the one-ancestor process. A pair $(\lambda,\mu)$ is admissible here when both rates are continuous and nonnegative on $[0,\infty)$. It has mean $\bar n$ when $e^{-\rho_{\lambda,\mu}(t)}=\bar n_t$ for every $t\ge0$. In particular, the initial value is $\bar n_0=1$. These definitions let the mission quantify over every admissible rate pair with the prescribed mean.

For a positive continuously differentiable mean curve, write $g(t)=\bar n_t'/\bar n_t$. The minimum-fluctuation rates are $\lambda_*(t)=\max\{g(t),0\}$ and $\mu_*(t)=\max\{-g(t),0\}$. When the mean decreases, only deaths occur; when it increases, only births occur; when it is locally constant, both rates are zero. This is Kendall's equation (56), expressed without first naming intervals of monotonicity.

Formalization targets

The goal is the simultaneous variance bound

$$V_{\lambda_*,\mu_*}(t)\le V_{\lambda,\mu}(t) \quad\text{for every }t\ge0 \text{ and every admissible }(\lambda,\mu)\text{ with mean }\bar n.$$

The statement also establishes that $(\lambda_*,\mu_*)$ is admissible and has the required mean. Its uniqueness clause says that if one admissible pair has the same variance as the candidate at every nonnegative time, then its two rates equal the candidate rates at every nonnegative time. Equality at only one selected time does not express Kendall's claim. The formal milestones record the fixed rate difference (55), the integral decomposition displayed in §6, and the nonnegative excess in variance that precedes (56). A companion statement covers the logistic example (58)–(60): for $a>1$ and $b>0$, $\bar n_t=a/(1+(a-1)e^{-bt})$ has minimum-fluctuation death rate zero and birth rate $b(1-\bar n_t/a)$.

Significance

The result distinguishes mean growth from population risk. Fixing $\lambda-\mu$ fixes the mean curve, but it leaves room for births and deaths that offset one another. Kendall's theorem determines the lowest variance compatible with the given curve and specifies the rate pair attaining it. The uniqueness statement identifies a model, rather than only a numerical lower bound. His logistic example shows the choice concretely: positive logistic growth is realized by a purely reproductive process in the minimum-fluctuation model.

The paper already derives these formulas. A complete formalization would connect the exact variance expression to a universal optimization claim over continuous nonnegative rate functions, and it would verify that equality throughout time identifies the rates. The definitions of the integrated rate, mean condition and variance functional can also support the other results in Kendall's paper. This proposal uses a local copy of $\rho$ because the geometric-solution mission is being drafted in parallel and its definition has not been published for import.

Difficulty

The constraint imposed by a given mean fixes the difference $\lambda-\mu$ but not either rate separately. The variance is an integral over the full past, multiplied by a term involving that same integrated difference. Consequently, a pointwise observation about the current sum $\lambda(t)+\mu(t)$ does not by itself state the required comparison of variances over every time horizon. The equality case is also global: a single time's variance cannot generally identify the rates at all earlier times. The formal result must keep the shared mean condition, the variance integral and the quantifiers over both rate pairs and all nonnegative times aligned.

Formalization scope

The Lean development represents rates and the prescribed mean as functions $\mathbb R\to\mathbb R$. Every stochastic claim is restricted to $t\ge0$; the integrals are oriented interval integrals from zero. Both rates are continuous on all of $\mathbb R$ and nonnegative on nonnegative time. The mean is $C^1$, positive on all of $\mathbb R$, and equals one at zero. Extending the regularity and positivity assumptions to negative time makes the total functions defining $g$, $\lambda_*$ and $\mu_*$ continuous without changing any comparison on $[0,\infty)$. These are explicit convenience assumptions beyond Kendall's wording. No denominator is used without the positivity assumption.

Kendall presents (56) after assuming that positive time splits into decreasing, increasing and constant intervals of $\bar n$. The goal uses positive and negative parts of $g$ and therefore covers any positive $C^1$ curve, including one without such a partition. On each of Kendall's three types of interval the formula agrees with his stated rates. The variance functional is exactly the last expression in (14c); its identification with the variance of the geometric population law is treated in the companion geometric-solution mission. The local statements do not construct a Markov process. The minimum is taken over all admissible continuous nonnegative rate pairs with the prescribed mean, not merely over the two candidate functions or over pointwise values of $\lambda+\mu$.

The development needs real differentiation, continuity, exponentials and interval integrals from Mathlib. Contributions that relate the explicit functional to the population law, prove the comparison and its equality case, or extend the regularity regime while preserving Kendall's claim are within scope. The logistic example provides a concrete instance of the general result.

Selected references

• D. G. Kendall, On the generalized “birth-and-death” process, Annals of Mathematical Statistics 19(1), 1–15, 1948. DOI: 10.1214/aoms/1177730285.