Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Graphene is a single sheet of carbon atoms arranged on a honeycomb lattice. Its electrons are described, to a first approximation that is quantitatively good near the Fermi level, by a nearest-neighbour tight-binding model: a hopping amplitude between adjacent carbon sites and nothing else. What makes the model worth studying is that this two-parameter lattice problem produces a band structure with two bands that touch at isolated points of the Brillouin zone and disperse linearly around them, so that low-energy electrons obey a two-dimensional massless Dirac equation rather than a Schrödinger equation with an effective mass. That observation organises the standard review literature on graphene (Castro Neto, Guinea, Peres, Novoselov, Geim, The electronic properties of graphene, Rev. Mod. Phys. 81 (2009) 109), and goes back to Wallace's 1947 band theory of graphite.
This mission formalises a self-contained set of lecture notes that carries the computation out in full: F. Utermohlen, Tight-Binding Model for Graphene (2018). It is the two-dimensional, two-sublattice counterpart of the tight-binding chain: the chain gives a single band with no band touching, while the honeycomb lattice, whose unit cell contains two inequivalent sites, produces a Bloch matrix and the conical band touchings targeted here.
Fix a carbon–carbon distance and a hopping amplitude . The honeycomb lattice is two interpenetrating triangular lattices, the and sublattices, with lattice unit vectors , and nearest-neighbour vectors
each joining an site to one of its three neighbours. The corners of the first Brillouin zone — the Dirac points — are
Fourier transforming the second-quantised hopping Hamiltonian gives with and the Bloch Hamiltonian
where is called the structure factor. The mission takes this matrix as its starting point: the second-quantised derivation (Eqs. 2–8 of the notes) is not formalised, and together with is defined by the displayed formulas. The band energies are the eigenvalues of , and is the quantity the statements are written in terms of. The Fermi velocity is (units with ).
with , and . The three clauses say, in order, that really are the eigenvalues of the Bloch Hamiltonian, that the two bands touch at the Brillouin-zone corner , and that they disperse linearly and isotropically around it. The goal deliberately asserts the shape of the low-energy dispersion — a first-order expansion, with no quantitative remainder — so it is not invalidated by sharper error estimates.
The milestone list follows the notes equation by equation: the closed form of (Eq. 11), the characteristic polynomial of (Eq. 9), the two explicit forms of the dispersion (Eqs. 12 and 13–14), the Pauli-matrix form of (Eq. 18), the vanishing of at and , the first-order expansions at both Dirac points (Eqs. 22–23 and 30), the spectrum of the linearised Hamiltonians (Eq. 32), and the gap opened by a mass term (Eqs. 33–34).
The three clauses of the goal are what turn a lattice hopping problem into the massless-Dirac-fermion picture used throughout graphene physics: they are the precise sense in which "graphene has Dirac cones at and with Fermi velocity ". Downstream, the same objects carry the valley structure — the two expansions are complex conjugates of one another — and the mass milestone shows how a sublattice-asymmetric on-site potential (boron nitride rather than graphene) opens a gap , the standard model of a gapped Dirac material.
The mathematics is classical and the physics literature regards it as settled; what this mission adds is a machine-checked development in which the honeycomb geometry, the Bloch matrix, its spectrum and the Dirac-point expansions are reusable definitions and lemmas rather than a computation redone by hand. No part of the development is claimed to be new mathematics.
The obstacles are in the analysis, not the algebra. The first two clauses of the goal are a trigonometric identity and a determinant. The third is a genuine differentiability statement, and the naive route — expand , cancel the zeroth-order terms, read off the linear term — has to be carried out uniformly in the direction of ; moreover the quantity being expanded is , a modulus, which is not differentiable at a zero of . The linear behaviour of survives only because the modulus of a function with a nonzero complex-linear differential at a zero is asymptotically the modulus of that differential, and the elementary estimate is what lets the error be transported through the modulus. Note also that itself is not differentiable at — the cone has a vertex there — so no Taylor theorem applies to directly.
Wave vectors and lattice vectors are pairs of reals, . Because that product type carries the sup norm, the Euclidean length is introduced as a separate definition and is the one used in every statement; the little-o statements are taken with respect to the neighbourhood filter of the origin, for which the two norms agree up to constants. is a finite sum over a three-element index set, is a concrete complex matrix, and "eigenvalues" are always expressed through the characteristic polynomial rather than through an eigenvector predicate. Lattice constant and hopping amplitude are real parameters; the standing hypotheses of the goal are exactly and , and several milestones need less. Units are , so .
Two things the formalization deliberately does not do: it does not derive the Bloch Hamiltonian from the second-quantised hopping Hamiltonian (Eqs. 2–8), which would require a Fock-space development, and it does not claim that and are the only zeros of . No statement is vacuous: every hypothesis is satisfiable (take ), and the goal's third clause is a nontrivial asymptotic rather than an identity.
Contributions welcome beyond the milestone list: the second-quantised derivation, the identification of the full zero set of modulo the reciprocal lattice, eigenvector-level (pseudospin) statements, the density of states, and the extension to next-nearest-neighbour hopping.
Which workers end up at which firms, and does higher quality always land at the more productive employer? This is the question of assortative matching: whether an efficient assignment pairs the best workers with the best firms, the second-best with the second-best, and so on down the line. The question has a long history in labor economics. Becker [1973] showed, for the simplest case of two-sided homogeneous firms and a single worker characteristic, that profit maximization under complementarity forces exactly this kind of sorting. Kremer [1993] extended the analysis to firms with many workers of a single type, under a specific Cobb–Douglas production function. What was missing was a general theory: one that covers firms hiring several types of workers simultaneously, firms that differ in efficiency, and labor markets of any degree of tightness, while still deriving sorting from a single primitive economic condition rather than from functional-form assumptions.
Topkis's Chapter 3, §3.2 supplies exactly that theory, as an application of the book's central tool — supermodularity — to the assignment problem. The condition that drives every result in this mission is a single complementarity hypothesis on the firms' profit functions: no concavity, no differentiability, no specific functional form. That a purely order-theoretic hypothesis pins down the qualitative shape of an optimal assignment is the mission's central content, and the platform currently has no lattice-theoretic treatment of matching at all — its one matching result formalizes Gale–Shapley two-sided stable matching by preference, an entirely different mechanism (see Formalization scope below).
Fix worker types, indexed , each with a lattice of available worker qualities, and firms, indexed . A matching assigns to each firm a vector of qualities — one worker of each type hired by that firm (a firm that hires no worker of some type, or several, is accommodated by adjoining an artificial "no worker" element to , or by splitting a type into several, as Topkis notes on p. 97; the model itself needs neither device). If firm hires the quality vector , it earns profit ; the dependence on reflects differences among firms such as technology or management efficiency. A matching is optimal if it maximizes the total profit over every matching.
A matching is increasing if — a single chain, firm by firm, under the pointwise order on — and ordered if every two of its firm-assignments are comparable (a weaker, only pairwise, condition). The labor market is loose if each firm's hiring problem can be solved by unconstrained maximization over the whole quality space , without regard to the other firms' decisions, and tight if the supply of each worker type is exactly , so a feasible matching must assign every available worker to exactly one firm.
The hypothesis common to every result is that is supermodular in the joint variable on : for every and , . By Theorem 2.6.1 of Chapter 2, this is equivalent to having increasing differences both between any two worker types' qualities (complementarity among the worker types) and between each worker type's quality and the firm index (complementarity between quality and firm efficiency).
Existence of an increasing optimal matching, with no loose-market hypothesis — the general case, and the harder of this mission's results to formalize, since its proof is a non-constructive lexicographic-minimization argument rather than a direct reduction to per-firm optimization.
The result gives a clean, hypothesis-light account of assortative matching: sorting by quality is a structural consequence of complementarity in the profit function, not an artifact of a particular production technology. It generalizes Becker's and Kremer's special cases to arbitrarily many worker types, heterogeneous firms, and any degree of labor-market tightness, identifying supermodularity in as the single condition doing all the work. Formalizing it contributes a genuinely new object to the platform: a firm-quality matching model driven by lattice-theoretic complementarity rather than by preference orderings, together with the four distinct comparative-statics conclusions (loose-market optimality, general existence, orderedness, increasingness) that the strength of the supermodularity hypothesis buys. No prior formalized proof of any of these four theorems exists on the platform or, to the author's knowledge, in any other proof assistant library.
The obvious approach — prove the goal (Theorem 3.2.3) by reducing to the loose case, firm by firm, as in Theorem 3.2.1 — does not work, because the loose-market argument crucially uses that each firm's decision does not constrain any other's; without that, a locally optimal per-firm choice need not combine into a globally optimal matching. Topkis's actual proof is non-constructive: among all optimal matchings, pick one that lexicographically minimizes the "latest" failure of the increasing property (a well-ordering argument over the finite but unbounded set of optimal matchings, not an inequality chase), then show that if it still fails to be increasing, exchanging the two offending firms' assignments via strictly increases total profit — contradicting optimality by supermodularity. Formalizing this requires setting up the lexicographic minimization (over pairs ordered by then ) as a well-founded induction, not merely restating the inequality (3.2.3) at the end of the proof.
Worker-type quality spaces are modeled as finite, nonempty lattices (Lattice,
Fintype, Nonempty); firms are indexed by Fin m. A matching is Fin m → ∀ i, X i with no
constraint beyond membership — the general matching problem (3.2.1) imposes no injectivity or
supply constraint on its own, a modeling choice Topkis's own text supports (p. 96: the
"" representation of a matching "may not distinguish between
all distinct assignments of workers to firms if the qualities of different workers of any given
type are not all distinct, but that ambiguity is inconsequential"). Tightness is instead
formalized as an explicit feasibility predicate (a bijection between firms and the available
workers of each type) supplied as a hypothesis exactly where a tight-market theorem needs it,
never folded into the general optimality predicate.
A trivializing formalization to avoid: collapsing Theorem 3.2.4's "ordered" conclusion and
Theorem 3.2.5's "increasing" conclusion into the same statement, or conflating their two
distinct supermodularity hypotheses (joint-non-strict-plus-per-firm-strict versus jointly
strict) — the mission's four milestones are kept as four genuinely different claims with their
own hypotheses, not variations proved once and restated. AGT.stable_matching_exists
(Gale–Shapley) is not reused here, despite the shared word "matching": it produces a
two-sided, preference-based stable matching with no notion of aggregate profit, a mechanism
unrelated to this mission's profit-maximizing, supermodularity-driven assignment.
Reused from earlier missions in this series: the induced set ordering InducedSetOrder
(mission I) and joint supermodularity SupermodularOn (mission II), both published platform
definitions. Contributions most welcome on the goal theorem's lexicographic-minimization
argument, the mission's hardest step.
Two-stage stochastic programs with recourse are already hard to optimize when the recourse problem is a linear program: Chapters 4–6 of this series show how the L-shaped method exploits the recourse function's convexity and polyhedrality to converge finitely by cutting planes. Adding integrality restrictions destroys both properties. Birge and Louveaux open Chapter 7 by naming the consequence directly: "properties of stochastic integer programs are scarce," duality is lost, and the recourse value for even a single first-stage point may itself require solving an integer program from scratch, with no warm start available across scenarios (Birge & Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer 2011, p. 290).
Section 7.2 isolates the one structural feature that still buys finite convergence: first-stage variables restricted to . Laporte and Louveaux's Integer L-shaped method (1993) exploits this by combining a branch-and-bound search over the finitely many binary first-stage points with a new family of optimality cuts, valid wherever a finite lower bound on the recourse value is available. This mission formalizes that method's specification and its finite-convergence guarantee, together with the two propositions its proof rests on.
A stochastic integer program (SIP) extends a two-stage stochastic linear program with fixed
recourse (Chapter 3's Recourse.Instance: first-stage data , fixed recourse matrix ,
and scenarios of with probabilities ) by two further restrictions:
where restricts the first stage and restricts the recourse variable — typically requiring
integrality of . Section 7.2's standing hypothesis narrows further: every coordinate of
is binary. Write for the resulting recourse value (a possibly-infinite expectation, by
the same convention as the continuous case) and for the value of the continuous
relaxation, obtained by dropping the restriction and keeping only — exactly the
recourse value Chapter 3's Recourse.Instance already computes.
The method needs one further hypothesis, Assumption 2: a finite lower bound with , not required to be tight. For a subset of the first-stage index set, write , and let be the binary point with for , otherwise — measures how far a binary point is from matching exactly, reaching its maximum only at .
Any L-shaped optimality cut valid for the continuous relaxation's value remains valid for the true, integrality-restricted recourse value, since pointwise.
is a valid lower bound on for every binary first-stage-feasible , given a binary feasible point with true recourse value and a lower bound satisfying Assumption 2.
Under Assumption 2, the Integer L-shaped method — the branch-and-bound search over binary first-stage points, tightened at each iteration by a fresh cut of the Proposition 3 form — finitely converges to an optimal solution of an SIP with relatively complete recourse and binary first-stage variables, when one exists. "Finitely" is quantified explicitly: a bound of on the number of iterations, the number of distinct binary first-stage points.
Proposition 4 is the chapter's payoff: it turns "solve an SIP with binary first-stage variables" from an open-ended search into a procedure with a certified stopping point, at the cost of one additional hypothesis (a computable lower bound ) that is often easy to obtain by relaxing the second-stage integrality restriction, as the book's Example 1 illustrates directly. Propositions 1 and 3 are the two soundness facts the method's cuts rest on: Proposition 1 lets an implementation reuse the continuous L-shaped method's own optimality cuts as valid (if weaker) constraints, and Proposition 3 supplies the chapter's genuinely new cut, tailored to the binary structure and strong enough by itself to guarantee termination.
Formalizing this mission fixes, machine-checkably, the exact hypotheses under which the method is correct — in particular, that "binary" is load-bearing (the finiteness bound is literally ) and that "relatively complete recourse" cannot be dropped, since it is what keeps the recourse value from becoming at a feasible point. No result here has, to the mission's knowledge, been formalized elsewhere; the propositions and the method's specification are drafted fresh.
The recourse function is neither convex nor polyhedral once is integer-restricted, so the argument cannot follow the continuous L-shaped method's proof line for line — that proof leans on 's convexity to certify a cut from finitely many bases. Proposition 3's cut instead argues purely combinatorially: for every binary , with equality forcing , so the cut's right-hand side collapses to the true value exactly there and falls to at most everywhere else — a fact about the finitely many binary points of , not about 's analytic structure. The natural first idea, adapting a continuous L-shaped cut by simply restricting its domain to binary , fails: nothing forces such a cut to be tight at the current iterate, so it need not exclude a revisited point, and finite convergence (the content Proposition 4 actually asserts, not just "an optimum exists") would be lost.
The mission represents first-stage points as Fin n1 → ℝ with a Binary predicate
(∀ i, x i = 0 ∨ x i = 1) rather than a Fin n1 → Bool type, so that the master problem's
feasible region and its binary-restricted subset share one ambient space, matching how the book
moves between and its binary points. The second-stage restriction is left an arbitrary
Set (Fin n2 → ℝ); taking it to be all of recovers exactly Chapter 3's continuous
recourse value, without a second definition. Flagged (moderator review, 2026-09-19):
Proposition 1's own is the book's -based continuous/LP-relaxation of
(Eq. (1.3)-(1.4)), which can retain bounds imposes beyond integrality — the book's own
worked example on the same page gives binary , so , not
alone. This mission's prop1_cuts_valid_for_sip uses the dropped- relaxation
(only ) rather than , which coincides with the book's only when
is itself an unbounded integrality restriction; the theorem is a narrower result than the
book's Proposition 1 whenever carries additional structure, though it remains true as
stated because the dropped- value is unconditionally the book's -based
, which is itself — see the item's own Formalization Note for the full
argument. The existential lower bound of Assumption 2 is kept a bare existentially-quantified real, never
sharpened to a formula, matching the book's own "no requirement is made that the bound should
be tight."
The Integer L-shaped method's branch-and-bound bookkeeping (Steps 0, 1, 3, 4: pendant-node list management, bound-based fathoming, and branching on a violated integrality restriction) is abstracted into a direct optimization over the binary first-stage feasible set at each iteration, since Proposition 3's cut is proved valid there without appeal to any specific branching order — the same level of abstraction the Chapter 5 mission uses for the continuous L-shaped method's own master-problem bookkeeping. What is retained explicitly is the part the finiteness bound actually depends on: Step 5's recourse-value computation and Step 6's binary choice between fathoming and adding a fresh cut, modeled as a state machine whose state is the finite set of binary points already excluded by a cut. A formalization that dropped this state machine — asserting only "if Assumption 2 and relatively complete recourse hold, an optimal solution exists" — would trivialize the proposition's actual content, the finite bound on the number of steps; this mission keeps that bound as an explicit, checkable part of the goal statement.
Definitions reused from earlier missions in this series: StochasticProg.Recourse.Instance
(Chapter 3) for the underlying two-stage recourse data and its continuous-relaxation value.
Contributions welcome on strengthening Proposition 4's proof to also derive Proposition 3 as a
lemma, and on formalizing the improved cuts of Propositions 5–7 (out of scope here, left for a
possible follow-up mission).
A "rule of thumb" classifier — a single pixel's brightness distinguishing handwritten "0" from "1" — is trivial to produce and barely better than a coin flip. A rule that gets every example right is, in general, far harder. Boosting asks whether many weak, easy-to-produce rules can be combined into one strong, hard-to-produce rule, and Chapter 11 answers it via a black-box reduction: any online convex optimization algorithm with sublinear regret, paired with access to a weak learner, yields a boosting algorithm — the same OCO-to-learning-theory template Chapter IX used for generalization, now applied to training-set fitting.
A concept class is -weakly-learnable (Definition 11.1) if some algorithm, given enough labeled samples, returns a hypothesis with error at most with high probability — better than random guessing by a fixed margin , far short of the arbitrarily-small error strong (PAC) learning demands. Section 11.2.1 fixes a simplified setting: binary zero-one loss, a realizable concept class (some has zero error), and a weak-learning oracle returning, on distribution over a fixed sample of size , a hypothesis with .
Algorithm 34 runs an OCO algorithm over the -dimensional simplex (distributions over the sample): at each round it calls the weak learner on the current distribution , builds the -valued cost vector recording which examples got right, updates for the linear cost , and finally outputs the majority vote .
For chosen so , Algorithm 34 returns with : with high probability, classifies the entire training sample perfectly.
This is one of the cleanest reduction theorems in the book: it needs no property of the weak
learner beyond its -margin guarantee, and no property of the OCO algorithm beyond a
regret bound — any of Chapters III–X's algorithms (multiplicative weights, OGD, RFTL, ONS...)
plugs in directly, and §11.2.3 specializes the reduction with multiplicative weights to recover a
close relative of AdaBoost, one of machine learning's most influential algorithms. The proof
technique — a contradiction argument on the existence of a "hard" residual distribution
uniform over the misclassified examples — is itself instructive and structurally different from
Chapter IX's martingale/concentration argument, despite both chapters being "OCO implies a
learning-theoretic guarantee" reductions. No prior art was found on the platform for boosting or
AdaBoost (planning search: q=boosting, q=AdaBoost — 0 hits); this mission drafts the theorem
fresh.
The proof's key step packages the algorithm's regret guarantee (a worst-case statement, true for every cost sequence including an adversarially-constructed one) into a proof by contradiction: assuming some nonempty set of misclassified examples survives, the uniform distribution over is shown to make every perform at best exactly at the threshold on average (since 's sign disagrees with the true label on every point of , at most half of the rounds' hypotheses can have agreed there), while the weak-learner guarantee (via a union bound over all rounds) forces the actual played distributions to see average performance — and the algorithm's low regret against specifically then closes the gap into an outright contradiction (, impossible for ). This chain — union bound over rounds, regret bound against one specific (adversarially-identified) comparator, and an averaging argument over the residual set — is more intricate than its short proof suggests.
EmpiricalErrorWeighted/EmpiricalError give the (weighted and uniform) training-error
quantities exactly as the book states them, with real-valued (±1) labels and predictions — the
convention this chapter's sign-based majority vote needs, distinct from Chapter IX's
Bool-valued zero-one loss (a deliberate, chunk-local choice, not a conflict, since the two
chapters use different label conventions for different reasons — see MODERATION_NOTES.md).
IsBoostingRun formalizes Algorithm 34's five lines, with the weak learner's round-t call
modeled as a random hypothesis h_t : Ω → X → ℝ (since a weak-learning call is itself
probabilistic) rather than a deterministic function, matching the book's own probabilistic
per-call guarantee. The goal theorem states the weak-learner guarantee (hweak), the OCO
regret guarantee (hA), and the choice of T (hTreg) as explicit hypotheses, per BRIEF.md's
own instruction that these are the theorem's real content, not incidental setup. h̄ is typed as
an arbitrary X → ℝ, never coerced into H — the book's own explicit remark that the boosted
hypothesis need not belong to the original weak-hypothesis class.
This chunk has no milestones: Chapter 11 is short and largely monolithic around Theorem 11.2,
with Section 11.2.1 ("Simplification of the setting") and 11.2.2 ("Algorithm and analysis")
building directly to it with no other numbered lemma on the relevant pages (PDF 207–211).
Definition 11.1 (weak learnability) is drafted as a definition, not manufactured into a
milestone, per CAPTAIN_BRIEF.md's own rule that definitions are never milestones and
BRIEF.md's explicit allowance for a mission with fewer than 3. §11.2.3's AdaBoost
specialization (a corollary discussion, not a separately numbered theorem on these pages) is not
formalized.
Reflection positivity turns a factorized weight across a reflection plane into a positive-semidefinite kernel of observables. The first mission in this series certified that finite split-weight mechanism and its two-observable chessboard inequality. A physical finite-volume Gibbs model needs one more layer before it can consume those results: its unnormalized weight must have a strictly positive partition function, normalization must preserve the split representation, and the hypotheses used for probability normalization must not be confused with those used for reflection positivity.
This mission isolates that finite algebraic layer. It does not present the results as new mathematics; its purpose is to make the interfaces and their failure modes explicit enough for later clock and XY consumers.
Let be a finite half-configuration space and let a full configuration be . A split weight is
where is finite, , and . Its partition function and normalized weight are
For observables , define the reflected kernel
Positive semidefiniteness means symmetry together with nonnegativity of every real quadratic form.
The mission keeps two logically independent requirements visible. Nonnegative split coefficients give reflection positivity through a weighted Gram factorization. Pointwise nonnegativity , together with one strictly positive value, gives and probability normalization. Neither requirement is silently substituted for the other.
The positive targets prove:
Two controls freeze the boundary. The symmetric two-point matrix with diagonal and off-diagonal is pointwise positive and normalizes to a probability weight, but its raw and normalized delta-observable kernels are not PSD. Conversely, zero split data have nonnegative coefficients and PSD raw kernels, but and their formally normalized weight is not a probability weight.
The result is a reusable adapter between an unnormalized finite Gibbs factorization and the previously certified reflection-positive kernel API. It prevents a later model proof from treating pointwise positivity as if it were a Gram representation, or treating reflection positivity as if it guaranteed a nonzero normalizer. The next physical consumer can therefore focus on proving an explicit nonnegative factorization of its cross-plane Boltzmann weight.
All types and sums used for normalization and kernels are finite, and all weights, coefficients, features, observables, and matrices are real. The mission proves no clock- or XY-specific Gibbs factorization, no spectral or Gaussian-domination theorem, no thermodynamic limit, and no Kosterlitz--Thouless conclusion. Those require separate missions. Physical and are not conclusions here.
Finite Reflection Positivity Methods I: Split Weights and Infrared Modes, mission db962332-7a71-4d34-a01c-e85cdee243ce.ReflectionPositivityInfraredBound.lean, repository snapshot
dbf503b2909cc17787d40a21eb75a0c9354cc6ef:
https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.leanA Markov process is reversible when, in equilibrium, transitions from to occur at the same average rate as transitions from to . Algebraically this is the detailed balance condition , and it is the single most useful structural property a network process can have: it replaces a global linear system by one equation per pair of states, and it hands you the equilibrium measure as a product of rate ratios rather than as the solution of anything.
The catch is that detailed balance mentions , which is exactly what one is trying to find. Chapter 2 of Richard Serfozo's Introduction to Stochastic Networks (Springer, 1999) removes the circularity. Kolmogorov's criterion characterizes reversibility by a condition on the rates alone: around every closed path, the product of the forward rates equals the product of the backward rates. And the proof is constructive — once the criterion holds, the invariant measure is
along any path from a fixed origin to , the criterion being precisely what makes the answer independent of the path chosen.
is a non-negative rate function on a state space , with the two-way communication property that and are positive together — a process failing this is visibly not reversible, since some transition would be possible but its reverse would not. A path is a sequence with throughout, and is assumed irreducible: every state is reachable from every other along a path. Write for the rate ratio.
is reversible when some positive satisfies the detailed balance equations. Such a is automatically an invariant measure, the total balance equations being the sum of the detailed ones.
Three statements are equivalent:
And when they hold, fixing any origin there is a positive with satisfying detailed balance and given at every state by the product of ratios along any path from .
The canonical form (2.2), that is reversible with respect to exactly when for a symmetric non-negative ; Example 2.1, the birth–death process with ; Theorem 2.2, that a process whose communication graph is a tree is reversible; and Theorem 2.5, the time-reversal criterion, which identifies a stationary distribution from a candidate reversed rate function without mentioning reversibility at all.
The results themselves. Kolmogorov's criterion is the working test. It is how one checks that a birth–death process, a random walk on a tree, a reversible Jackson network or a Whittle network with reversible routing is reversible, and it is a finite check on cycles rather than a search for an unknown measure. The ratio form (iii) is what gets used in practice: it says the product of ratios along a path is a well-defined function of the endpoints, which is exactly what licenses defining by that product.
Theorem 2.2 is the structural special case with no computation at all — a tree has no cycles, so the criterion is vacuous and reversibility is automatic. Theorem 2.5 points in a different direction: it identifies a stationary distribution from a guess at the time-reversed rates, and it is the tool Serfozo uses later to prove the Whittle equilibrium theorem a second way and to establish that departure processes from networks are Poisson.
Formalizing them. Mathlib has no reversibility theory for Markov processes: no detailed balance,
no Kolmogorov criterion, no time reversal of a rate function. It has SimpleGraph.IsTree, which the
tree item uses, and nothing else that bears on this chapter. The whole apparatus is contributed
here.
The goal is a genuine equivalence with a constructive core, and the three implications are of quite different character.
(i) (ii) is the easy one: multiply the detailed balance equations around the closed path and cancel the 's, which is legitimate because the values are positive. Note the criterion is asserted for arbitrary closed sequences, not only for paths; the two-way property is what makes both sides vanish together when some rate is zero.
(ii) (iii) is a cycle-splicing argument: two paths with the same endpoints concatenate, one reversed, into a closed path, and the criterion says its forward and backward products agree, which is the equality of ratio products.
(ii) (i) is where the construction lives. Fix an origin ; irreducibility gives a path to every state; define by the ratio product; (iii) makes it well defined; and then detailed balance at an edge follows by extending a path by that edge. Serfozo's Remark 2.9 gives the same construction as a recursion over the sets of states reachable in steps, which may be the easier route to organize.
The birth–death item is a telescoping recursion, , and the observation that the two families of detailed balance equations — for and for — are the same family. Theorem 2.2 is a cut argument: removing an edge of a tree splits the state space into two pieces joined by that edge alone, so the flow balance across the cut is the detailed balance equation for that edge. Theorem 2.5 is two lines of rearrangement once the sums are known to converge.
The state space is an arbitrary type and is an arbitrary non-negative real rate function; nothing here needs a process, a measure space or even countability, because reversibility as Serfozo defines it "applies to any nonnegative rates or probabilities as an algebraic property, not necessarily associated with a stochastic process". The same statements therefore cover discrete-time chains with read as transition probabilities, which is what the book points out.
Paths are functions with positive consecutive rates. A path of length zero is a single state and its ratio product is the empty product , which is consistent with .
Kolmogorov's criterion is stated for arbitrary closed sequences, exactly as the book states it, not only for closed paths. Under two-way communication the two readings agree — if one rate in the sequence vanishes then so does its reverse and both products are zero — but the book's form is the one that is directly checkable.
The canonical measure is not defined by a choice function. Instead the conclusion asserts the existence of a positive with satisfying detailed balance and agreeing with the ratio product along every path from the origin. That is the content of (2.9) without needing to pick a path for each state.
Theorem 2.2 is stated for a finite state space. Serfozo assumes the process is ergodic, and the cut-flow argument then sums the balance equations over one side of the cut; on an infinite state space that summation needs an integrability condition that the book leaves implicit in "ergodic". Finiteness makes the rearrangement unconditional and the statement clearly true; the general case is listed under contributions.
Theorem 2.5 is stated as the conclusion that satisfies the balance equations, with explicit summability hypotheses for the three families of sums involved. That is the stationary distribution additionally requires it to be normalized and the process to be ergodic, neither of which is part of the algebraic content.
Contributions welcome beyond the listed items: Theorem 2.4, the characterization of reversibility by invariance of the finite-dimensional distributions under time reversal; Remark 2.9's recursive construction of the canonical measure; Theorem 2.22 on reversible network processes with batch movements; Theorem 2.31 and the partition-reversible processes of Sections 2.8 and 2.9; and the reversibility criteria for Jackson and Whittle networks in Examples 2.24 and 2.25.
Convex optimization — minimizing a convex function over a convex set — is the offline problem that online convex optimization (OCO) generalizes: an OCO algorithm run against a single, fixed cost function repeated every round is exactly an algorithm for this classical problem. Its convergence theory, developed over decades and surveyed comprehensively in Nesterov [Introductory Lectures on Convex Optimization, 2004] and Boyd and Vandenberghe [Convex Optimization, 2004], supplies the analytical toolkit — potential functions, strong convexity, smoothness — that every regret bound in the rest of this book reuses. This chapter is the book's own self-contained account of that toolkit: it proves nothing about regret or adversaries, but the algorithms and inequalities it establishes for gradient descent recur, essentially unchanged, in the online setting three chapters later.
The chapter's own capstone, a linear convergence rate under a joint strong-convexity and smoothness assumption, traces to Nesterov's classical analysis of gradient descent under a condition-number bound; the Polyak step size predates it, going back to Polyak's 1969 subgradient method for problems with a known optimal value.
Fix a real, complete inner product space (a Hilbert space) and a convex, closed set , the decision set. A function is -strongly convex (with gradient map ) if for every ,
and -smooth if for every ,
Strong convexity lower-bounds by a quadratic of curvature at least at every point; smoothness upper-bounds it by a quadratic of curvature at most . When is twice differentiable these say for every . A function that is both is called -well-conditioned, where is its condition number.
Write for a minimizer of (over , or over in the constrained case), and for any point define three measures of distance to optimality: the value gap , the Euclidean distance , and the gradient norm . Gradient descent starts at and iterates for a step-size schedule ; in the constrained case each step is followed by a projection back onto .
for constrained gradient descent (Algorithm 4) on a -well-conditioned over , with the constant step size . This is the chapter's strongest rate: for the best-conditioned class of functions it considers, the optimality gap shrinks by a constant factor every round, rather than polynomially in .
when minimizes over a convex . The multi-dimensional first-order optimality condition for constrained minimization, generalizing in the unconstrained case ().
for unconstrained gradient descent with step size , where achieves the smallest value among . A single algorithm, needing no prior knowledge of , , or beyond the (assumed available) optimal value , automatically attains whichever of the four rates applies to .
For -strongly-convex and -smooth , at every point :
The chapter's basic toolkit: four inequalities letting a proof substitute one measure of progress (value gap, distance, gradient norm) for another as needed.
Theorem 2.6 is the model result behind every subsequent linear-rate claim in convex optimization: it isolates the exact mechanism (strong convexity plus smoothness, combined multiplicatively through the condition number) that turns a or rate into an one. Theorem 2.3 demonstrates the opposite phenomenon — a single step-size rule that adapts to whatever structure happens to have, without needing to know which structure that is — a design principle the book's later chapters (adaptive regret, adaptive gradient methods) return to repeatedly. Lemma 2.4 is used directly inside the book's own proof of Theorem 2.6 and is stated separately because later chapters cite its four bounds individually.
None of these four statements has a machine-checked proof on the platform prior to this mission (see Formalization scope). Formalizing them establishes strong convexity and smoothness, in the book's own quadratic-bound form, as reusable definitions, together with the constrained- and unconstrained-gradient-descent update rules that Chapter III's online algorithm specializes.
The linear rate of Theorem 2.6 does not follow from Lemma 2.4 alone: chaining the smoothness upper bound and the strong-convexity lower bound gives only a bound relating to , not to itself, and a naive one-step decrease argument stalls at a rate of per round rather than — the factor of four comes from combining the projection's contraction property (the constrained analogue of Theorem 2.3's telescoping argument) with the smoothness bound simultaneously, not from either alone. The Polyak step size of Theorem 2.3 is remarkable, and its analysis correspondingly delicate, because the step size depends on the unknown optimal value through ; the proof must derive all four regimes (general convex, smooth, strongly convex, well-conditioned) of from the same one-line per-round inequality, rather than running four separate arguments.
is formalized as an arbitrary real, complete inner product space, not fixed to
, matching this book's chapter-wide convention (Chapter III's mission of this
series does the same). Strong convexity and smoothness are formalized in the book's own
quadratic-bound form with an explicit gradient map as a separate parameter (not tied to
by automatic differentiation), rather than via the second-derivative characterization; a
theorem needing to be the actual gradient of adds that as a separate hypothesis. This
avoids a trivializing formalization under which the predicate could be satisfied by an
unrelated : every theorem here that uses StronglyConvexOn/SmoothOn also assumes g is
a global gradient map for f. Theorem 2.3's realized-gradient bound is
formalized only over the run's own iterates (not as a global Lipschitz bound
on ), matching the book's own statement ("assuming "): a global
gradient bound would be jointly unsatisfiable with global strong convexity on any
infinite-dimensional or unbounded , since a strongly convex function's gradient grows
without bound away from its minimizer. Sequences are 0-indexed, so a book statement at round
(1-indexed) is stated here at index ; each theorem's docstring records the exact
shift. The projection in Algorithm 4 reuses OnlineConvexOpt.FirstOrder.IsMetricProjection,
already published for this series' Chapter III, rather than redeclaring it.
Theorem 2.10 (the chapter's further, book-stated-without-proof rate) is out of scope: the book explicitly defers its proof to outside references, so it cannot be a faithful milestone under this platform's provenance requirement. Section 2.4's reductions of non-smooth or non-strongly-convex problems to this chapter's setting (via randomized smoothing) are left for a future extension, since they introduce a new construction not needed by the goal or its milestones.
A Brownian path is continuous, and that is essentially all it is. It has no derivative anywhere, it crosses zero infinitely often in every interval , and it becomes positive and negative immediately after time zero. None of this is visible from the finite-dimensional distributions; it is a statement about the germ of the path at a point, and the tool that unlocks it is a zero-one law.
Chapter 7 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) develops that tool. The natural filtration is enlarged to , which allows "an infinitesimal peek at the future" — a quantity like is -measurable but not -measurable. Blumenthal's 0-1 law (Theorem 7.2.3) says that at this enlargement buys nothing probabilistically: the germ -field is trivial.
Everything local follows. If the path had any chance of staying non-positive on some interval , that would be a germ event of probability at least by symmetry, so it has probability one — and the path enters immediately. Continuity then forces it to return to zero immediately as well. Combined with the time inversion , which turns the germ at into the tail at , the same law gives and the recurrence of one-dimensional Brownian motion.
Let be a probability space and a Brownian motion: its finite-dimensional laws are centred Gaussian with covariance , and almost every path is continuous. In particular almost surely, so this is Durrett's .
Three -fields organize the chapter:
The first is the past, the second the germ at time zero, the third the tail at infinity.
A path is Lipschitz at the point with constant when for all within some positive distance of . A path differentiable at is Lipschitz at , so failing this at every point and for every constant is a strong form of nowhere differentiability.
In words: the germ -field is trivial. Nothing about the path in an arbitrarily short initial interval is genuinely random.
Theorem 7.1.5, that Brownian paths are Hölder continuous of every exponent on every bounded interval; Theorem 7.1.6, that with probability one they are not Lipschitz at any point, hence nowhere differentiable — the Paley–Wiener–Zygmund theorem in the proof of Dvoretsky, Erdős and Kakutani; Theorem 7.2.4, that the path enters immediately; Theorem 7.2.5, that its zero set accumulates at ; and Theorem 7.2.8, that and .
The results themselves. Blumenthal's law is the gateway to every local path property of Brownian motion, and Durrett uses it immediately for exactly that. Theorems 7.2.4 and 7.2.5 together say the path oscillates across zero infinitely often in every initial interval — the reason the zero set is an uncountable closed set of Lebesgue measure zero, and the reason the "first return to zero" is not a useful notion at time . Theorem 7.2.8 is the same law pushed to by time inversion, and it is what makes one-dimensional Brownian motion recurrent (Theorem 7.2.9).
The Hölder pair is the sharp description of path regularity. Exponent always works, never does, and the borderline is subtle: for each fixed , but Davis (1983) showed . Nowhere differentiability is the historical headline — Paley, Wiener and Zygmund (1933) — and the proof given here is a short covering argument rather than a series construction.
Formalizing them. Mathlib has the object but almost none of the theory. It defines
IsPreBrownianReal and IsBrownianReal, proves that a centred Gaussian process with covariance
is pre-Brownian, and supplies the invariances — negation, scaling
, the shift , and the time inversion
— together with the weak Markov property IsPreBrownianReal.indepFun_shift. It
does not have the germ or tail -fields, Blumenthal's law, the strong Markov property,
any path-regularity result, or the Kolmogorov–Chentsov continuity theorem: Probability/Process/Kolmogorov.lean
defines IsKolmogorovProcess, the hypothesis, and stops there. So this mission supplies the
-fields and then everything Durrett proves with them.
The goal reduces to Durrett's Theorem 7.2.2, that
for bounded path-measurable ; at , is trivial because
almost surely, so
almost surely, and an indicator almost surely equal to a constant forces that constant to be
or . Theorem 7.2.2 itself is a monotone class argument on top of the Markov property, and the
Markov property in this setting is Mathlib's indepFun_shift plus the observation that the
conditional expectation of a product over lands in
. Assembling that is the work.
Theorem 7.2.4 is then three lines — by symmetry of the Gaussian, let , apply the goal — provided the event has been shown to lie in the germ field, which is where continuity of paths enters. Theorem 7.2.5 follows from 7.2.4 applied to and together with the intermediate value theorem.
Theorem 7.1.5 needs the Kolmogorov–Chentsov continuity theorem, which has to be built: from
one gets Hölder- control for
, and gives every . The dyadic chaining and Borel–Cantelli
step is the substance, and it is worth building as a general theorem about
IsKolmogorovProcess rather than only for Brownian motion.
Theorem 7.1.6 is self-contained and short: fix , let be the event that some has whenever , and bound ; since increases, every .
Theorem 7.2.8 needs the tail 0-1 law, Theorem 7.2.7, which is the goal transported through the time
inversion — Mathlib's IsPreBrownianReal.inv — because the tail field of is the
germ field of . With that,
by scaling, so the probability is one, and is arbitrary.
The process is Mathlib's IsBrownianReal, indexed by ℝ≥0, on an abstract probability space —
not the canonical path space that Durrett uses. This is why the shift operators
and the family do not appear: there is one measure, the process starts
at almost surely, and each statement is about that process. Theorem 7.2.7 as Durrett states it
quantifies over all starting points and has no direct analogue here; the tail 0-1 law for the
process started at does, and is listed under contributions as the route to Theorem 7.2.8.
The three -fields are built as suprema and infima in the lattice of -algebras on
: pastSigma B t is the supremum of the pullbacks of the Borel field along for
, and germSigma B, tailSigma B are the corresponding infima. The goal carries the
hypothesis that each is measurable, not merely almost-everywhere measurable, which is what
IsPreBrownianReal gives and what puts these -fields below the ambient one; the canonical
construction satisfies it, and without it "" for a germ event would be an outer
measure.
Hölder continuity is stated locally — for almost every path, every admits a constant — since global Hölder continuity on is false. The order of quantifiers puts the null set first, so a single path works for every at once.
The hitting statements avoid an infimum over a possibly empty set. " almost surely" is
written as: almost surely, for every there is with ; and
" almost surely" as the same with . These are equivalent to Durrett's statements and
say what the infimum is there to say. Similarly Theorem 7.2.8 is written with ∃ᶠ … in atTop rather
than as an extended-real , which is what "" means and avoids a coercion.
LipschitzAtPoint f s C is "there is a scale on which ". Its
negation for every and every is Theorem 7.1.6, and it has content in both directions: the
identity path is Lipschitz at every point with , while is not Lipschitz at
with — both checked in Lean before publishing.
Existence is not part of this mission. Mathlib proves nothing of the form "a Brownian motion exists", and nothing here needs it: every item takes a Brownian motion as a hypothesis. That the hypothesis is satisfiable is a theorem — Durrett's 7.1.1, via Kolmogorov extension and the continuity theorem — and it is listed under contributions, where it belongs, since building it is a project of its own.
Contributions welcome beyond the listed items: Kolmogorov–Chentsov as a general statement about
IsKolmogorovProcess; Theorem 7.1.1, the existence of Brownian motion; Theorem 7.2.2 in full, for
every ; the tail 0-1 law and Theorem 7.2.9, recurrence; the strong Markov property and the
reflection principle of section 7.3; and Exercise 7.1.5, that no path is Hölder of any exponent
.
A Markov chain forgets. Run it long enough and the distribution of its position stops depending on where it started — that is the intuition behind shuffling a deck, behind Markov chain Monte Carlo, behind PageRank, and behind the stationary analyses of every queueing model. Chapter 5 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) makes it a theorem, and identifies exactly what can go wrong.
Two things can. The chain may fail to reach parts of the state space, and the answer is irreducibility. Or it may reach them only on a lattice of times — a chain alternating between two halves of its state space never forgets whether the clock is even or odd — and the answer is aperiodicity. Theorem 5.6.6 says that is the complete list: an irreducible, aperiodic chain with a stationary distribution has , for every pair of states, whatever the starting point.
Let be a countable state space and a transition probability: non-negative, with each row summing to one. The -step transition probabilities are the matrix powers, and .
Hitting is described by the first-passage probabilities , given by and — the chain moves once and then reaches for the first time, having avoided it meanwhile. Summing them gives
A state is recurrent when , the chain is irreducible when for all , and a state is aperiodic when the greatest common divisor of is . A stationary distribution is a probability vector with .
The goal asserts pointwise convergence of the transition probabilities, not convergence in total variation and not a rate; those are strengthenings, and stating the weakest useful form is what keeps the theorem stable.
Theorem 5.3.1, that a state is recurrent exactly when diverges — the bridge between the hitting picture and the matrix picture; Theorem 5.3.2, that recurrence is contagious; Theorem 5.5.10, that every state in the support of a stationary distribution is recurrent; and Theorem 5.5.11, that for an irreducible chain with a stationary distribution .
The result itself. Theorem 5.6.6 is what licenses reading a stationary distribution as a long-run frequency. Without it, is merely a fixed point of a linear map; with it, is the limiting probability of being at , from any start. Theorem 5.5.11 then gives the quantity a second, purely local meaning — is the reciprocal of the mean return time to — which is the identity behind every renewal-reward computation in applied probability and behind the "expected time between visits" estimates that Monte Carlo methods rely on. The two necessary hypotheses are sharp: a periodic chain has oscillating rather than converging, and Durrett's Theorem 5.7.2 gives the corrected statement in that case.
Formalizing it. Mathlib has no countable-state Markov chain theory. It has ProbabilityTheory.Kernel
and an Irreducible notion for kernels, but nothing about recurrence, transience, first-passage
decompositions, stationary measures or the convergence theorem, and nothing that specializes to a
transition matrix on a countable set. The mission therefore contributes the whole apparatus of
sections 5.3, 5.5 and 5.6 — the -step and first-passage probabilities, , the mean
return time, recurrence, irreducibility, aperiodicity and stationarity — together with the results
that make it usable.
The usual proof of the goal is a coupling argument, and it is short but not obvious: run two independent copies of the chain, one from and one from , on the product space with transition probability ; aperiodicity plus irreducibility make the product chain irreducible, is stationary for it, so it is recurrent and the two copies meet almost surely; after they meet they can be exchanged. Each step of that is a separate obligation, and the one that consumes aperiodicity is the irreducibility of the product chain — for a periodic chain it fails, which is exactly why the theorem does.
The number-theoretic ingredient is worth flagging: irreducibility of the product needs that , being closed under addition with , contains every sufficiently large integer. That is the numerical semigroup fact, and it is where aperiodicity is actually used.
The state space is any countable type with decidable equality, and the transition probability is a
plain function constrained by IsTransition: non-negative entries,
summable rows, rows summing to one. Sums over the state space are unconditional sums, so no
finiteness is assumed anywhere.
The chain's law is not constructed. Every quantity here — , , , — is defined by an explicit recursion on the transition matrix, not as an expectation against a measure on path space. This is a deliberate choice: building the path measure is a substantial project of its own, and none of the statements in these sections need it. The recursions are the standard ones and they are the definitions the book's own computations use. The cost is that probabilistic statements about paths, such as Theorem 5.6.1 on the almost-sure limit of the visit counts , cannot be phrased in this language and are not part of the mission.
Conventions: is the identity matrix; vanishes at ; and are unconditional sums over , so an infinite mean return time appears as a non-summable series rather than as an extended real. Theorem 5.5.11 is therefore stated as summability together with , which asserts finiteness of the mean return time rather than silently relying on a division convention.
Aperiodicity is "the only natural number dividing every element of is ", which is written without needing a gcd of a set; it is false when is empty, which is correct, since the period of such a state is undefined.
The goal is not vacuous: the hypotheses are satisfiable by any strictly positive transition matrix on a finite set.
Contributions welcome beyond the listed items: Theorem 5.3.3 on finite closed sets; the decomposition theorem 5.3.5; existence of a stationary measure from a recurrent state (5.5.7) and its uniqueness (5.5.9); the equivalence of positive recurrence and the existence of a stationary distribution (5.5.12); Theorem 5.7.2 for the periodic case; and the path-level results of section 5.6, which need the chain's law on path space.
Chapter 7 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) studies a network with a fixed set of users, and shows that a decentralized rate control converges to a fair allocation. Chapter 8 asks the question one time scale up. Files finish and their flows leave; new files arrive and new flows appear. The number of flows on each route is therefore itself a random process, and the rate allocation — assumed to settle instantly, since rate control runs much faster than files arrive and depart — depends on it.
The question is whether this system is stable: does the number of flows in progress stay bounded, or does it grow without limit? The answer is the best one could hope for. A weighted -fair allocation, the family that contains proportional fairness, TCP fairness, max-min fairness and throughput maximization as special cases, is stable exactly when the offered load at each resource is below that resource's capacity. No more is required — no condition coupling different resources, no dependence on , no dependence on the topology beyond the loads themselves.
A network has resources and routes with incidence matrix . Let be the number of flows active on route and the rate given to each of them, so route consumes at each resource it uses. Flows arrive on route as a Poisson process of rate and carry files that are exponentially distributed with parameter , so
and is the load on route .
Given weights and , the weighted -fair allocation is the solution of
with in place of the objective when . Written in the aggregate rates this becomes
The family interpolates between the fairness notions of Chapter 7: with maximizes throughput, is weighted proportional fairness, with is TCP fairness, and with approaches max-min fairness.
Suppose the load respects every capacity, for all . Then there is an , depending only on the loads and capacities, such that for every flow count and the -fair aggregate rates ,
The left-hand side is the drift of the Lyapunov function , by the identity (8.3); the right-hand side is the book's displayed bound. The single is uniform in , which is what a Foster–Lyapunov argument needs, and it is the whole deterministic content of Theorem 8.2's sufficiency half.
The derivative of the objective, in the same form for every including (Exercise 8.3); strict concavity of the objective; the characterization of the optimum by with primal and dual feasibility and complementary slackness (Exercise 8.4); the tangent-plane inequality (8.5) that concavity gives at the optimum; the drift identity (8.3); and that recovers weighted proportional fairness, connecting this chapter to Proposition 7.4 of mission VII.
The result itself. Theorem 8.2 says the stability region of an -fair network is the largest it could possibly be — the same region a single isolated resource would have — and that it does not shrink as varies. That is a strong statement about a large design space, and it is not automatic: section 8.4 of the book exhibits rate allocation schemes for which it fails, so the natural condition (8.2) is a property of -fairness and not of rate allocation in general. Since the family covers the fairness notions actually implemented in transport protocols, the theorem is what licenses treating "is the load below capacity?" as the only capacity-planning question at flow level.
Formalizing it. Nothing here is open; the theorem is due to Bonald and Massoulié (2001), with
the fluid-limit machinery from Gromoll and Williams and from Massoulié. What the mission produces
is a machine-checked -fair allocation — objective, derivative, concavity, KKT conditions —
and the exact drift inequality, on top of the congestion-control layer published in mission VII of
this series, whose networkFeasible and linkFlow it reuses. Mathlib has no network utility
maximization and no fairness criteria.
The proof is short but the step that makes it work is easy to miss. The drift is , and there is no reason for this to be negative term by term — some routes are over-served and some under-served. What makes the sum negative is that is itself a feasible point of the same optimization problem (8.4) that solves, and is concave, so the tangent plane at lies above :
Since , taking gives the drift immediately. Strict negativity comes from taking instead, which is still feasible because (8.2) is a strict inequality, and then dividing through by . The whole argument is one application of concavity at a cleverly chosen point, and the choice of that point is the content.
The scaling that makes it uniform in is the other thing to notice: depends only on how much slack (8.2) leaves, not on , because enters only through the common factor that appears on both sides.
Resources and routes are indexed by finite types, the incidence matrix is real-valued with entries
or , and the feasible set is mission VII's networkFeasible, so Chapters 7 and 8 agree on
what a feasible flow vector is. The objective is stated in the aggregate variables of
problem (8.4) rather than the per-flow rates of (8.1): they are equivalent, but (8.4) is the form
the drift argument uses and the form in which the feasible set does not depend on .
The objective is defined with an explicit case split at , exactly as the book defines it, and the derivative milestone asserts that the resulting derivative has the same form in both cases — which is the point of Exercise 8.3. Powers are real exponents, so positivity of the flow counts, weights, loads and rates is hypothesised wherever a power appears.
What is formalized and what is quoted. Theorem 8.2 is a statement about positive recurrence of a Markov process, proved by a Foster–Lyapunov criterion whose remaining hypotheses the book leaves to Exercises 8.6 and D.2. There is no theory of continuous-time Markov chains on a countable state space in Mathlib to state positive recurrence against, so this mission formalizes the deterministic drift inequality that carries the argument and quotes the probabilistic wrapper. The inequality is exactly the one the book displays, including the , and the necessity half — that the process is unstable when (8.2) fails — is a coupling argument and is quoted too.
The goal is not vacuous: the hypotheses are satisfiable, and for a single resource of capacity the -fair optimum is , for which the inequality holds with and strictly positive slack.
Contributions welcome beyond the listed items: the single-resource equilibrium distribution of Exercise 8.1 and the geometric law of the total number of flows; the bounded-drift estimate of Exercise 8.6; the necessity half of Theorem 8.2; the limiting cases and ; and the instability examples of section 8.4.
When a file is transferred over the Internet, no part of the network decides how fast it should go. The machines inside the network forward packets; when a resource is heavily loaded it drops or marks one; the destination reports that to the source; and the source slows down, then gradually speeds up again until the next signal. This end-to-end cycle of increase and decrease is TCP, and it is the mechanism by which the Internet discovers available capacity and divides it among competing flows.
Chapter 7 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) asks what such a scheme converges to. The answer is the chapter's organizing idea: the decentralized dynamics solve a global optimization problem that no participant can see. Each source knows only its own rate and the congestion signals it receives; no machine anywhere holds the link-route incidence matrix; and yet the flow rates converge to the unique maximizer of a concave network utility, and that maximizer is the proportionally fair allocation. This is the same phenomenon as the electrical network of Chapter 4, now with the local rule chosen so that the global objective is the one we want.
A network has resources and routes, with link-route incidence matrix : when route uses resource . Route carries a time-varying flow rate , and the load on resource is .
Each resource generates congestion signals at rate
where is non-negative, continuous, increasing and not identically zero — one may read as the probability that a packet is dropped or marked at resource under load . The primal algorithm is the response of the sources:
with : a steady increase proportional to the weight , and a decrease proportional to the stream of congestion signals received. Both sums are local — over the resources on route , and over the routes through resource — so nothing in the network needs to know .
The network problem of section 7.1 is to maximize over with , and a feasible is weighted proportionally fair when every feasible satisfies .
is a Lyapunov function for (7.5): the unique maximizer of over the positive orthant is an equilibrium point, and every trajectory of the primal algorithm converges to it.
The goal asserts both halves of the book's last sentence: that maximizes , and that the trajectory converges to it. It fixes no rate of convergence and no basin restriction beyond starting in the interior, which is what "global" means here.
Proposition 7.4, that solving and being weighted proportionally fair are the same condition; strict concavity of on the positive orthant; the partial derivative that identifies the maximizer; the equivalence between a stationary point of and an equilibrium of (7.5); and the Lyapunov identity (7.7),
The result itself. Theorem 7.6 is the statement that a decentralized rule solves a centralized problem. Its practical content is that the choice of and determines what is optimized, so a protocol designer who wants a particular notion of fairness can get it by choosing the local rule accordingly — the -fair family of Chapter 8 is exactly this dial. Its theoretical content is the identification of the limit: because 's first term is , the limit is the weighted proportionally fair allocation, which by Proposition 7.4 is the solution of the network problem and, by Remark 7.5, also the Nash bargaining solution and a market-clearing equilibrium. Three quite different notions of "the right allocation" coincide, and a simple end-to-end feedback rule finds it.
Formalizing it. Nothing here is open; the model and the theorem are from Kelly, Maulloo and Tan (1998). What the mission produces is a machine-checked congestion-control model — the network problem, proportional fairness, the primal dynamics and the Lyapunov function — and a statement of the convergence result in a form later work can cite. Mathlib has no network utility maximization and no congestion control.
The Lyapunov identity is a chain-rule computation and is not the hard part, and neither is . The gap the book flags explicitly is between " increases along trajectories" and "": a strictly increasing Lyapunov function does not by itself force convergence, because the derivative could decay fast enough for the system to stall short of the maximum. The book closes it with a compactness argument — the trajectory is trapped in , which is compact, and on the complement of an -ball around within that set the derivative (7.7) is continuous and therefore bounded away from zero, so only finite time can be spent there. Reproducing that argument is the substance of the goal, and it needs the compactness of the sublevel set, which comes from strict concavity and the growth of .
A second difficulty is one of representation rather than mathematics. The primal algorithm is an ODE, and a formal statement must say what a trajectory is. Here a trajectory is given as a differentiable function satisfying (7.5) pointwise, with positivity assumed rather than derived; deriving positivity from the dynamics is a separate (true, and welcome) result.
Resources and routes are indexed by finite types and the incidence matrix is real-valued with
entries constrained to or , matching the book and the convention of mission IV of this
series, whose linkFlow is reused here. Flow vectors live in the positive orthant, stated as
∀ r, 0 < x r: the utility contains , which has no meaning at , and the book's
own maximum is interior to the positive orthant.
The network problem's objective is maximized over the intersection of the feasible set with the positive orthant rather than over , since is not a real number; the fairness condition, by contrast, is quantified over all feasible including boundary points, exactly as the book states it, and the inequality is meaningful there.
A trajectory is a function of real time satisfying the derivative condition at each , and staying in the positive orthant is a hypothesis. The equilibrium is given by its stationarity condition rather than by an existence claim, so the goal is about the trajectory rather than about solving the fixed-point equation; that the stationary point is the maximizer is the first conjunct of the conclusion, so nothing is assumed about it that is not also proved.
The goal cannot be satisfied vacuously: the hypotheses are jointly satisfiable — for instance one resource, one route, , , — and the conclusion is a genuine limit.
Contributions welcome beyond the listed items: that the positive orthant is invariant under (7.5); uniqueness and existence of the max-min fair allocation; Theorem 7.2 on problem decomposition into user and network problems; Theorem 7.8, the corresponding global stability result for the TCP-like system of section 7.4; and the dual algorithm of section 7.6.
When many stations share one broadcast channel, something has to decide who transmits. A token passed around the stations works when there are few of them and none is silent for long, but it scales badly and breaks if the token is lost. The alternative is to let stations transmit whenever they like and use randomness to recover from the resulting collisions. That is the design of ALOHA, built in the 1970s to connect terminals across the Hawaiian islands, and of Ethernet, and of essentially every contention-based access protocol since.
Chapter 5 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) asks what such protocols can achieve, and the answers are largely negative. ALOHA with a fixed retransmission probability jams: with probability one there is a finite random time after which every slot contains a collision and no packet ever succeeds again, for every positive arrival rate. Ethernet's binary exponential backoff does better, but only just: it has a positive critical arrival rate, above which only finitely many packets are ever transmitted, and it is still not positive recurrent at rates where it does transmit infinitely many. The chapter's general statement is the one this mission targets: any backoff slower than exponential jams at every positive arrival rate.
Time is slotted, and a transmission attempt occupies exactly one slot. New packets arrive in a Poisson stream of rate , so the number arriving in a slot is Poisson with mean . A slot in which exactly one station transmits carries its packet successfully; a slot in which two or more transmit is a collision and carries nothing.
In an acknowledgement-based scheme a station learns nothing about the channel except whether its own transmissions succeeded. A packet arriving in slot attempts transmission in slots with , the sequence chosen independently for each packet, and
is the retransmission function. For ALOHA, for every ; for Ethernet's binary exponential backoff, .
Now imagine the channel externally jammed from time , so that every retransmission actually occurs. The attempts in slot are then Poisson with mean , and the probability that fewer than two attempts are made in slot is
The expected number of such slots is , which is decreasing in , and the critical rate is
Theorem 5.11 of the book says deserves its name: below it infinitely many packets are transmitted with probability one, above it only finitely many.
Since for every positive , the critical rate is , and by Theorem 5.11 the expected number of successful transmissions is finite at every positive arrival rate. The goal fixes no constant and no rate: it says only that the dividing line between "jams always" and "has a positive capacity" sits at logarithmic growth of , which is exponential growth of the backoff.
The ALOHA drift calculation of section 5.1 and its consequence that the drift is positive once the backlog is large enough; the summability that combines with Borel–Cantelli to give Proposition 5.3; the monotonicity of in ; the opposite extreme, that a scheme with — one that gives up on a packet after finitely many attempts — has ; that ALOHA's own retransmission function satisfies condition (5.7); and the bound of Remark 5.14, that a positive recurrent acknowledgement-based scheme needs and hence , which is strictly below Ethernet's .
The result itself. Condition (5.7) is the chapter's structural statement about random access, and it is a sharp one. Any retransmission rule under which a packet keeps trying at a rate that does not decay fast enough — a fixed probability, a polynomially growing backoff, anything short of exponential — has critical rate zero: the channel jams at every positive load. Exponential backoff is not a tuning choice, it is the minimum that makes the protocol work at all, and the formula for a backoff by factor (Exercise 5.7) then says how much capacity each choice of buys. The gap recorded in Remark 5.14 is the other half of the picture: even above the threshold, "infinitely many packets get through" is much weaker than "the backlog is stable", and between and Ethernet does the first and provably not the second.
Formalizing it. None of this is open; the analysis is due to Kelly and MacPhee (1987) and Aldous (1987). What the mission contributes is a machine-checked account of the analytic core: the definitions of , and , the two extremes of the classification, and the ALOHA calculations. Mathlib has no protocol analysis and nothing about random access channels.
The obstacle is a modelling one and it is worth stating plainly rather than discovering halfway through. The chapter's headline results — Proposition 5.3 that ALOHA jams almost surely, Theorem 5.11 that is the critical rate, Theorem 5.15 that geometric Ethernet is transient — are statements about sample paths of a Markov chain built on a Poisson arrival stream, and their proofs are coupling arguments comparing a system started empty with one started with a backlog. Nothing in Mathlib supports that construction, and building it is a research-scale project rather than a chapter. This mission therefore formalizes the analytic half and quotes the probabilistic half, which is the same division the book itself makes when it computes for a scheme: Theorem 5.11 is proved once, and every subsequent statement about a protocol is a convergence question about .
Within that analytic half the difficulty is real but ordinary. The summand is a product of a factor growing with and one decaying exponentially in it, so the growth hypothesis has to be turned into a summable bound without assuming any regularity of beyond non-negativity — in particular need not be eventually monotone in any useful quantitative sense, only divergent faster than .
The retransmission function is any non-negative real sequence; the normalization is not imposed, since none of the statements need it and imposing it would exclude the comparison schemes. and the partial sums are real-valued, and "" is stated as summability of the sequence rather than as a bound on an extended-real sum, so convergence is asserted rather than assumed. The goal is stated for each fixed separately, which is what makes ; it is not stated as a claim about the infimum, because the infimum of the set adds nothing once the set is known to be all of .
The growth hypothesis is the book's condition (5.7) verbatim: . Note that at and the quotient involves and is not meaningful; divergence to infinity is an eventual statement, so this costs nothing, but it is why the hypothesis is a limit rather than a pointwise bound.
The mission is not vacuous in either direction: the ALOHA milestone exhibits a retransmission function satisfying the hypothesis, and the milestone exhibits one that fails it as strongly as possible, with for every .
Contributions welcome beyond the listed items: Ethernet's and the resulting ; the generalization of Exercise 5.7; the scheme with ; the continuous-time halving of Kelly and MacPhee; and, for anyone willing to build the probabilistic layer, Proposition 5.3 and Theorem 5.11 themselves.
A network of resistors solves an optimization problem. Nobody tells the electrons what to do; each one moves under a purely local rule, and the current distribution that emerges minimizes energy dissipation over all distributions satisfying Kirchhoff's node law. Add a wire and the network can only become easier to traverse. This is the encouraging case, and Chapter 4 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) opens with it.
Road traffic is the discouraging case. Drivers also follow a local rule — take the fastest route — and the pattern that emerges is again characterized by an optimization problem, but not the one anyone wants solved. Braess's paradox is the sharp form of the discrepancy: in a small road network carrying six cars per unit time, every route takes 83 time units at equilibrium; open an extra road, and at the new equilibrium every route takes 92. Building road capacity made everyone slower. The difference from the electrical case is that a driver's choice imposes a delay on everyone else sharing the road and the driver does not pay for it, and correcting that — pricing the externality — is how a decentralized rule can be made to produce good global behaviour. That idea recurs in Chapters 7 and 8 of the book as the basis of Internet congestion control.
The network is a set of directed links. A route is a subset of links, and is the set of routes under consideration — not necessarily all physically possible ones. The link-route incidence matrix has when and otherwise. Writing for the flow on route , the flow on link is
Each link has a delay function , continuous and increasing in the flow on that link, and the delay along a route is the sum of the delays of its links, . Drivers care only about getting from origin to destination: is the set of source–destination pairs, each route serves exactly one of them, written , and the flow requirement between pair is .
A routing pattern is stable when no driver has an incentive to switch. Definition 4.2 makes this precise: a Wardrop equilibrium is a feasible vector of route flows such that
Every route actually carrying traffic is a shortest route, in delay, for the traffic it carries.
The goal asserts existence only, for an arbitrary network, arbitrary route set and arbitrary continuous increasing delay functions. It fixes no uniqueness claim, because the equilibrium flows need not be unique even though the link loads are, and no efficiency claim, because Braess's paradox is precisely the statement that the equilibrium is not efficient.
Kirchhoff's node law as the equations satisfied by the expected reward in the random-walk game of section 4.1; the two Braess networks of Figures 4.4a and 4.4b, with their equilibrium delays and ; convexity of for increasing ; the optimization characterization that makes the goal reachable — a minimizer of over the feasible flows is a Wardrop equilibrium; and the exact externality decomposition of the queueing network of section 4.3.1.
The result itself. Theorem 4.3 is what makes the Wardrop equilibrium a usable object: a traffic model that could fail to have an equilibrium would be describing nothing. Its proof does more than establish existence — it identifies the equilibrium as the solution of a specific convex program, minimizing . That function is not the total delay , and the gap between the two is exactly Braess's paradox: selfish routing optimizes the wrong objective. Once the two objectives are written side by side, the fix is readable off them, and it is the fix used in practice — a toll on link equal to , the marginal delay a driver imposes on everyone else, makes the selfish objective coincide with the social one. Section 4.3 then carries the same accounting into queueing and loss networks, where the derivative of the mean cost splits into a term for the delay a customer suffers and a term for the knock-on cost it inflicts.
Formalizing it. Nothing here is open; Wardrop stated the principle in 1952 and Beckmann, McGuire and Winsten gave the optimization formulation in 1956. What the mission produces is a machine-checked model of selfish routing — incidence matrix, link flows, delay functions, the equilibrium condition — and a formal record of Braess's paradox as a concrete pair of networks rather than a story. Mathlib has no traffic or congestion-game theory.
Existence is not a fixed-point argument in the obvious variable: the best-response map of the routing game is not continuous, since a small change in flows can flip which route is shortest and move all the traffic. The book's route is to replace the equilibrium condition by the stationarity conditions of a convex program on a compact feasible set, where existence is routine and the content is the translation. The translation is where the care is needed, and it is stated here as a separate milestone: the first-order conditions say the Lagrange multiplier equals the route delay on routes carrying traffic and is a lower bound on the others, which is Definition 4.2 restated.
The subtlety worth naming in advance is that "increasing" is doing real work in two different places. It makes convex, which is what makes the program tractable; and it is what makes each interpretable as a price. Neither convexity of itself nor strict monotonicity is needed, and assuming them would be assuming more than the book does.
Links, routes and source–destination pairs are indexed by finite types. The incidence matrix is real-valued with entries constrained to be or , matching the book's definition in this chapter (unlike Chapter 3, which allows general non-negative integers). The map from routes to source–destination pairs is given as a function rather than as the matrix , which is exactly the book's statement that each column of sums to .
Delay functions are total functions , continuous and monotone. This excludes the vertical asymptote that Figure 4.5 permits — a link with a finite capacity at which delay blows up — and that restriction is recorded here rather than left implicit. The equilibrium condition is stated as the inequality " for every serving the same pair", which is Definition 4.2 with the minimum written out; the two are equivalent because itself serves , and the inequality form avoids having to produce a minimum over a possibly empty set.
The goal is not vacuous: the feasibility hypotheses (, and each source–destination pair served by at least one route) are exactly what makes the feasible set non-empty, and without them the existence claim would be false rather than trivial.
Contributions welcome beyond the listed items: uniqueness of the equilibrium link loads ; the marginal-cost toll that aligns the selfish and social optima; Rayleigh monotonicity (Exercise 4.3, that effective resistance does not decrease when a resistance is increased); the price of anarchy for affine delays; and Theorem 4.6 on the derivatives of the loss-network rate of return with respect to offered traffic and capacity.
A queueing network is a collection of service stations through which customers — jobs, packets, telephone calls, patients — move one at a time. The state of such a network is a vector of occupancy counts, one per station, and the number of states grows exponentially in the number of stations, so solving the equilibrium equations directly is hopeless for any network worth modelling. The product form is what rescues the subject: for a large and identifiable class of networks the equilibrium distribution factorizes into one term per station, as if the stations were independent, and a network of stations costs one-dimensional calculations instead of one exponentially large one.
Chapter 2 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) establishes this for migration processes, the Markov model in which individuals move between colonies one at a time at a rate that factorizes as : a part depending only on the two colonies and a part depending only on the occupancy of the source. The class covers single-server and -server queues, infinite-server queues, and networks of them, open or closed.
There are colonies, and a state is a vector of non-negative integers, being the number of individuals in colony . Three operators move one individual:
An open migration process is the Markov process on with transition rates
where : nothing leaves an empty colony. Immigration into colony is Poisson of rate . Taking and and restricting to states of a fixed total gives a closed migration process. Setting models an -server queue at colony ; models individuals moving independently.
The traffic equations define from the rates. In the open case they are
and in the closed case with and . Finally set
If then
is an equilibrium distribution: it satisfies the equilibrium equations for the open migration rates, and it sums to one over . Both halves are asserted, because the first alone is satisfied by every positive multiple of and the second is what makes the convergence hypothesis do work.
The closed-network product form of Theorem 2.4; the two families of partial balance equations (2.3) and (2.4) that the proof reduces to; Theorem 2.9, that the time reversal of a stationary open migration process is again an open migration process with rates , and ; the single M/M/1 queue that the chapter starts from; the cycle identity (2.6) behind Little's law; and the traffic equations of Kendall's family-size process, an open migration process with infinitely many colonies.
The result itself. Theorem 2.8 says that at a fixed time the occupancies of an open migration network are independent, each distributed as if its colony were fed by a Poisson stream of rate — even though the actual arrival stream into a colony is in general not Poisson, and the occupancies are emphatically not independent as processes. That gap between the one-time-marginal and the process is the reason the theorem is useful and the reason it is easy to misapply. Everything downstream in the book rests on it: the loss networks of Chapter 3 are the truncation of a product-form process to a capacity set, and the flow-level models of Chapter 8 ask when a product form survives a bandwidth-sharing policy. Theorem 2.9 supplies the reversibility argument from which Burke's theorem and the Poisson character of the exit streams follow.
Formalizing it. The mathematics is classical — Jackson (1957), Whittle (1968), Kelly (1979) —
and none of it is open. What the mission produces is a machine-checked model of a queueing
network: the migration operators, the rate matrix, the traffic equations and the product form, in
a form later missions in this series import rather than restate. Mathlib has no queueing theory
and no theory of continuous-time Markov chains on a countable state space, so this is the first
such development. It builds on the DetailedBalance / FullBalance layer published in mission I.
An open migration process is not reversible — the detailed balance equations fail, as Figure 2.5 of the book shows with an arrival stream of geometrically sized bursts — so the method of Chapter 1 does not apply and the equilibrium equations must be met head on. The content of the proof is that they split: a separate balance holds for each colony (rate of individuals leaving colony equals rate arriving into it) and one more across the boundary with the outside world, and each of those is equivalent to a traffic equation. Finding that split is the step, and it is why the partial balance equations are milestones in their own right.
The formal obstacle is different and worth naming. The equilibrium equation at a state sums over the states that can jump into , and the naive transcription silently assumes is a state, which fails when . Over such a term must be dropped, and a formalization that keeps it — with read as truncated subtraction — states something false.
The state space is Fin J → ℕ, a function from a finite index type of colonies to occupancy
counts, with J finite; no irreducibility is assumed, since none of the statements below need it.
Rates are real-valued and the whole rate matrix is a single function of two states, assembled as a
sum of indicator terms over the possible transitions, so the equilibrium equations can be stated
as the FullBalance predicate of mission I, with unconditional sums over the countable state
space. This is what avoids the trap above: a sum over actual states never includes a
would-be-negative one, and any spurious coincidence of operators at a boundary carries a
factor and contributes nothing.
Conventions the development commits to: , so a transfer is always between distinct
colonies; and for ; ; and is asserted
via HasSum, which states convergence and the value at once, rather than as an extended real that
might be infinite. Occupancy vectors use truncated natural subtraction, so the partial balance and
reversed-rate statements carry an explicit where the book's state space carries it
implicitly; the goal itself does not need such a guard.
A trivializing formalization is ruled out by the second conjunct of the goal: the equilibrium equations alone are a homogeneous linear condition satisfied by , whereas the requirement that sum to forces the constants to be exactly the ones stated.
Contributions welcome beyond the listed items: Burke's theorem (2.1) and the Poisson character of the exit streams, Corollary 2.10, the closed-form of the telephone banking example (Exercise 2.6), the Chinese restaurant process of Exercise 2.13, and Bartlett's theorem (2.17) on linear migration processes over a general space.
In the early twentieth century Agner Krarup Erlang worked for the Copenhagen Telephone Company and faced a sizing question that every shared-resource operator still faces: how many parallel circuits must a telephone link carry so that an arriving call is almost never turned away? The answer he published — the Erlang loss formula — is still the standard dimensioning tool for circuit-switched links, call centres, hospital beds, rental fleets, and any system in which a customer who finds every server occupied leaves rather than waits.
The formula is the first capstone of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), where it closes Chapter 1 and supplies the building block for the loss networks of Chapter 3. It is also the cleanest possible demonstration of the book's method: write down the transition rates of a Markov process, guess that the process is reversible, solve the detailed balance equations, and read the answer off the normalizing constant. This mission formalizes that chapter: the reversibility apparatus, the birth-and-death chain of the loss link, and Erlang's formula itself.
A link carries parallel circuits. Calls arrive as a Poisson process of rate and each call, while it lasts, occupies one circuit for an exponentially distributed holding time of parameter ; holding times are independent of one another and of the arrival times. A call that arrives to find all circuits busy is lost — it does not queue.
Let be the number of busy circuits. Then is a Markov process with transition rates
and otherwise. A collection of numbers is in detailed balance with rates when
and satisfies the equilibrium (full balance) equations when
Detailed balance is the statement that, in equilibrium, transitions from to occur as frequently as transitions from to . Writing for the traffic intensity, Erlang's formula is
The goal fixes no numerical constant: it says that whatever probability vector solves the detailed balance equations of the loss link assigns exactly to the blocking state. The hypothesis is detailed balance rather than full balance, which is what the book's derivation actually uses and is the stronger assumption to discharge.
together with the reversibility results that justify the method: detailed balance implies full balance, the reversed process of Proposition 1.1 has rates and retains as an equilibrium distribution, and holds exactly when and are in detailed balance.
The result itself. is the blocking probability of the link, so it converts a traffic measurement and a target grade of service into a circuit count. It is insensitive: the same formula holds for any holding-time distribution with mean , which is why it survives as an engineering tool far outside the exponential model that produces it here. Chapter 3 of the book builds loss networks on top of it, and the Erlang fixed point that approximates a whole network is a system of coupled copies of this one formula. The derivative identity is the ingredient that makes tractable in optimization: it shows is increasing in , and the recursion it encodes is how the formula is evaluated numerically without overflow.
Formalizing it. Nothing here is open mathematics; the value of the mission is a
machine-checked statement of the loss model and a reusable reversibility layer. Mathlib has no
theory of detailed balance or of reversible Markov processes over a countable state space, so
this mission contributes the first: the predicates DetailedBalance and FullBalance, the
reversed rate matrix, and the three structural facts relating them. Those are shared by every
later mission in this series — the migration processes of Chapter 2 and the loss networks of
Chapter 3 are all proved reversible or quasi-reversible by exactly these means.
The obvious route to is to solve the equilibrium equations directly, and for a
birth-and-death chain that is a three-term recursion whose general solution needs two boundary
conditions. Detailed balance replaces it with a two-term recursion and one boundary condition,
and the whole content of the reversibility section is that the substitution is legitimate.
The remaining work is bookkeeping that Lean makes less forgiving than the page does: the
detailed balance equations must be indexed so that the and boundaries are not
silently assumed away, the normalizing sum must be shown positive before it can be inverted,
and the induction that produces has to carry the Fin (C+1) index through
Nat.factorial. For the derivative identity, the naive differentiation of a quotient gives
in the numerator, and recognizing it as
times the denominator is the step that produces the stated form.
The state space is Fin (C + 1), so the link with circuits has states and finiteness
is built in; is a plain function Fin (C + 1) → ℝ constrained by hypotheses rather than a
PMF, so that the normalization appears explicitly wherever it is used.
FullBalance is written with unconditional sums (tsum) over an arbitrary state space, so the
same predicate serves the countable chains of later chapters; over a Fintype it is the finite
sum. Rates are real-valued and q j j = 0 by construction, matching the book's convention that
a Markov process must change state when it jumps.
The rates carry as hypotheses. This rules out the degenerate reading in which
makes every downward rate vanish: with the detailed balance equations force
for , so the only normalized solution is the point mass at , and
while Lean evaluates for ; the goal would be false.
Erlang's formula is stated for the last state Fin.last C, not for an unconstrained index, so
it cannot be satisfied by a degenerate reindexing.
Contributions welcome beyond the listed items: the insensitivity of to the holding time distribution, the recursion , the finite-source variant and the PASTA statement that an arriving call in that model sees , and the parking-space identity of Exercise 1.9.
The central limit theorem tells us that a normalized sum of independent random variables converges in distribution to a Gaussian. For applications — bounding the failure probability of a randomized algorithm, controlling the error of a Monte Carlo estimator, proving a generalization bound in learning theory — a limiting distribution is not enough: what is needed is a single, explicit, non-asymptotic inequality that holds for every fixed sample size , not merely as . Hoeffding's inequality (Wassily Hoeffding, 1963) and Bernstein's inequality (Sergei Bernstein, 1920s–1940s, in the form used here due to Vadim Bennett and later authors) are the two archetypal answers: both give an explicit Gaussian-type tail bound for a weighted sum of independent random variables, valid for every , with all constants made explicit. They are the workhorses behind concentration of measure, high-dimensional statistics, and the non-asymptotic analysis of randomized algorithms; a textbook trying to reach the Johnson–Lindenstrauss lemma, random matrix norms, or the restricted isometry property has to pass through this chapter first, because every one of those results is itself an application of a weighted-sum concentration inequality to a specific choice of random variables.
The central limit theorem's own error term is the obstruction that direct concentration inequalities are built to avoid: the Berry–Esseen theorem (Andrew C. Berry, 1941; Carl-Gustav Esseen, 1942) bounds the normal approximation's error at order , which is too slow to recover a genuinely exponential tail bound for finite . Hoeffding's and Bernstein's inequalities are proved instead by a direct argument — bounding the moment generating function of the sum and optimizing a Markov/Chernoff exponential tilt — that never invokes the central limit theorem or its error term at all.
Fix a probability space . For a real random variable on , define its sub-gaussian norm
and its sub-exponential norm
In both definitions, the requirement that the exponential moment be finite (i.e. that the moment-generating integrand be integrable), and not merely satisfy "" as a bare inequality, is essential: without it a moment that is genuinely infinite for a given would vacuously count as "" under the Bochner integral's convention that a non-integrable function integrates to , and every random variable — however heavy-tailed — would trivially have norm . is called sub-gaussian (respectively sub-exponential) when this infimum is over a nonempty set, i.e. when some finite makes the moment finite and at most . These are genuine norms (up to the identification of almost-surely-equal random variables) on the vector space of random variables for which they are finite, and they are the natural non-asymptotic yardsticks for tail heaviness: characterizes a Gaussian-type tail , while characterizes an exponential-type tail . Every bounded random variable — in particular every Bernoulli or Rademacher (symmetric Bernoulli) random variable — is sub-gaussian, and the square of a sub-gaussian random variable is sub-exponential; a genuinely sub-exponential (not sub-gaussian) example is the squared coordinate of a standard Gaussian vector, or the exponential distribution itself.
Goal — Theorem 2.8.2 (Bernstein's inequality, weighted sum). Let be independent, mean-zero, sub-exponential random variables on , and let . Then, for every ,
where and is an absolute constant that does not depend on , the , , or .
The goal is deliberately the weighted and sub-exponential form, the weakest of the chapter's results that is still stable under the improvements a solver might find: it neither fixes (the unweighted Theorem 2.8.1, a special case) nor restricts to the lighter sub-gaussian tail (Theorem 2.6.3, which follows from a strictly stronger hypothesis). Both weaker theorems, plus Hoeffding's and Chernoff's inequalities, are included as milestones because Bernstein's own proof is built directly from them.
The result itself. Bernstein's inequality is the two-tail-regime concentration bound: a sub-gaussian tail near the mean, transitioning to a heavier sub-exponential tail far from it, exactly the behavior one should expect from a mixture of light-tailed terms with one heavy-tailed outlier. It underlies the concentration of quadratic forms (Chapter 6's Hanson–Wright inequality controls -type terms, which are themselves products of sub-gaussians and hence sub-exponential by Lemma 2.7.7), and it is the standard tool for bounding empirical-process suprema whose summands are not bounded but merely light-tailed.
Formalizing it. No formalization of Bernstein's inequality — in either the weighted or
unweighted, or sub-gaussian or sub-exponential form — exists yet on Prove2Me (GET /theorems?q=Bernstein and q=sub-exponential return no relevant hits, checked
2026-09-17). What this mission produces is not just the statement but the machinery
underneath it: a working Orlicz-norm treatment of and that a later mission
(the Hanson–Wright inequality, or any future chapter that needs sub-exponential
concentration) can build on directly.
The obvious first idea — squaring both sides and applying Chebyshev, as one does to prove the weak law of large numbers — gives only a polynomial tail bound decaying like , far too weak to be useful (this is exactly the point made by the chapter's opening discussion of the coin-tossing example, comparing the linear decay from Chebyshev against the target exponential decay). The central limit theorem promises the right shape of tail asymptotically but, per Berry–Esseen, with an error of order that swamps any exponential gain for large deviations — the CLT approximation is simply not valid in the tail regime the inequality needs. The actual argument instead controls the moment generating function of the full sum directly and optimizes an exponential (Chernoff) tilt; this is why the sub-gaussian and sub-exponential norms — MGF-control objects, not moment or tail objects per se — are the right technical vehicle, even though Proposition 2.5.2 and 2.7.1 show all these characterizations are equivalent up to constants. The min of two terms in Bernstein's exponent is not an artifact of a loose proof: it reflects a genuinely two-regime tail (Gaussian near the mean, exponential in the far tail), and collapsing it to a single term in either direction would either be false (dropping the exponential term) or needlessly weak (dropping the Gaussian term, which is what a naive union bound over the worst single term would give).
Random variables are ℝ-valued functions on an explicit probability space (Ω, mΩ, P)
(Ω : Type, MeasurableSpace Ω, P : Measure Ω, [IsProbabilityMeasure P]), matching the
book's setup throughout. Independence is Mathlib's ProbabilityTheory.iIndepFun, and
tail probabilities are stated with P.real, Mathlib's ℝ-valued measure evaluation, which
corresponds directly to the book's .
Both Orlicz norms are defined locally, as genuine infima matching Definitions 2.5.6 and
2.7.5 verbatim (subgaussianNorm, subexponentialNorm, each
sInf {t > 0 : Integrable (fun ω => E[...]) P ∧ E[...] ≤ 2}), rather than reused from
Mathlib's HasSubgaussianMGF (Mathlib.Probability.Moments.SubGaussian). The Integrable
conjunct is not optional dressing: Mathlib's Bochner integral of a non-integrable function is
0 by convention, so a bare E[...] ≤ 2 (without asserting integrability) would be satisfied
by every t for which the moment is actually infinite, collapsing the sub-gaussian norm of
a standard Gaussian (and, symmetrically, the sub-exponential norm of any heavy-tailed
variable) to 0 — a trivializing formalization the mission was moderated to rule out. The
same Integrable conjunct appears in every moment hypothesis (general_hoeffding,
bernstein_unweighted, bernstein_weighted): ∃ s > 0, Integrable (...) P ∧ ∫ ... ≤ 2, so
that the hypothesis is not satisfied vacuously by non-integrable exponential moments either.
HasSubgaussianMGF bounds the moment generating function directly with a variance-proxy
parameter (E exp(tX) ≤ exp(c t²/2)), which is a different object definitionally
from the Orlicz norm — equivalent up to a constant factor by the book's own
Proposition 2.5.2, but not interchangeable without restating that equivalence — and
Mathlib has no sub-exponential analogue at all. Since the goal theorem and two of its
milestones need the sub-exponential norm, one consistent convention (the book's own Orlicz
norms) is used for both and throughout the mission, rather than mixing
Mathlib's MGF-based sub-gaussian convention with a locally defined sub-exponential one.
Every occurrence of the book's " is an absolute constant" is formalized as a genuine
existential quantifier fixed before the random variables, the vector a, and t are
introduced: ∃ c : ℝ, 0 < c ∧ ∀ ..., P.real {...} ≤ 2 * Real.exp (-(c * ...)). No numeral is
substituted for c anywhere; a solver's proof may use any positive constant it can establish,
exactly mirroring the book's own non-constructive existence claims. The trivializing
formalization this rules out is fixing c to a specific small numeral (which would be a
strictly stronger, easier, and unfaithful claim) or, in the other direction, weakening the
statement by allowing c to depend on N, the , a, or t (which would make the
theorem vacuous, since any such bound trivially holds for a small enough depending on the
instance).
Chernoff's inequality (Theorem 2.3.1) needs no Orlicz norm — Bernoulli parameters are
given directly via P.real {X i = 1} = p i ∧ P.real {X i = 0} = 1 - p i, and the conclusion
uses Real.rpow (^ on ℝ → ℝ → ℝ) for the real exponent in . Hoeffding's
inequality for symmetric Bernoulli variables (Theorem 2.2.2) is likewise self-contained,
needing only the two-point probability hypothesis defining the Rademacher distribution.
Many arguments in high-dimensional geometry, statistics and computer science need to approximate a point of a convex set by an average of a handful of extreme points, rather than represent it exactly. The classical Carathéodory theorem (1907) answers the exact question: every point of the convex hull of a set is a convex combination of at most points of . That bound is tight and grows with the dimension , which makes it useless whenever is large — exactly the regime of interest in high-dimensional probability.
B. Maurey's empirical method — an unpublished 1980–81 result reported by G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle 1980–1981 — and later applied by B. Carl to bound covering numbers of operators between Banach spaces (Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces, Ann. Inst. Fourier 35(3), 1985, 79–118), replaces the exact question with an approximate one and removes the dimension dependence entirely: to approximate to accuracy , the number of points needed depends only on , never on . Vershynin's High-Dimensional Probability opens with this result as its "Appetizer," using it to illustrate the book's central theme — that randomness is a tool for constructing deterministic combinatorial objects — before any probabilistic machinery has been introduced.
A convex combination of finitely many points is a sum with and . The convex hull of a set is the set of all convex combinations of all finite collections of points of . The diameter of is , the Euclidean norm throughout.
The classical Carathéodory theorem states that every is a convex combination of at most points of — with generally unavoidable, attained by a simplex. The question this mission answers is different: given that we are willing to approximate rather than represent it exactly, and willing to use only combinations with equal coefficients (an average of points, with repetition allowed), how large must be as a function of the desired accuracy?
The quantifiers are exactly this order: for every bounded , every point of its convex hull, and every target , such an averaging set exists. This is the weakest stable statement carrying the theorem's content — the number of points does not depend on the dimension , and the coefficients are forced to be uniform — and it is the form the corollary below invokes directly.
This is a direct application of the goal to computational geometry's covering problem: how many balls of radius are needed to cover a polytope, and where should they be centered.
The result itself. The approximate Carathéodory theorem is the prototype of a dimension-free approximation result: whenever a set is bounded, a fixed number of points (depending only on the target accuracy, not the ambient dimension) suffices to approximate any point of its convex hull. This is what makes possible dimension-independent covering-number bounds such as Corollary 0.0.4, which in turn are the starting point for the book's later treatment of entropy, packing and generic chaining (Chapters 4, 7–8). The technique generalizes far beyond : it underlies covering-number bounds for operators between Banach spaces (Carl's original application) and is a recurring device in learning theory for bounding the size of an -net of a hypothesis class.
Formalizing it. Both results are elementary and already fully proved in the literature; no open mathematical content remains. What this mission contributes is a machine-checked, faithful Lean statement of Maurey's construction and its corollary, phrased over Mathlib's existing convex-hull and metric-diameter machinery, so that later missions in this series (concentration inequalities, Johnson–Lindenstrauss, chaining) can build on a verified base case of "probability constructs a deterministic covering," and so that the empirical method itself becomes a reusable, linked component on the platform. The proof of the goal (via the probabilistic argument sketched by the book: interpret a convex combination as a probability distribution, average i.i.d. samples, and bound the variance) is left open for solvers.
The identity that makes the proof work — averaging independent copies of a random vector concentrates around its mean at rate in mean-square — is a two-line computation once the convex combination is reinterpreted probabilistically. The step that is easy to miss is this reinterpretation itself: nothing in the statement mentions probability, so the "obvious" attack of manipulating the convex-combination weights directly, or trying to construct by some explicit combinatorial recipe, does not see a path to a bound independent of . The probabilistic argument produces the points non-constructively, via an averaging/existence argument (the expected squared distance is small, so some realization achieves it) rather than an explicit formula — a solver has to introduce a probability space and a random vector that does not appear anywhere in the formal statement to be proved.
Both results are stated over EuclideanSpace ℝ (Fin n) for an explicit dimension n : ℕ, so
‖·‖ is the Euclidean norm and Mathlib's Metric.diam is used directly for
. The convex hull is Mathlib's convexHull ℝ T; by
Mathlib's convexHull_eq, this already coincides with the book's own definition of a convex
combination of finitely many points of , so no bespoke convex-combination definition is
introduced — this mission needs no supporting definitions of its own. In the corollary, "a
polytope with vertices" is formalized, following the book's own proof, as
for a finite vertex set with , rather than via a
separate Polytope structure (which Mathlib does not provide and the book's argument does not
need). The covering bound is an exponent, not a product with
— matching the book's own proof, which counts the ordered -tuples of vertices with
repetition, ; the typeset "" in
the corollary statement is the same juxtaposition-as-exponent notation the proof uses for
"" one line earlier.
A trivializing formalization is ruled out explicitly: the goal must hold for every integer and every , not merely some convenient choice — e.g. together with trivially satisfies the inequality but proves nothing about the theorem's actual content, that a fixed, dimension-independent works uniformly over all points of the hull. The formal statement quantifies , then , then , and only then asserts existence of the , exactly in that order.
Classical Carathéodory (Theorem 0.0.1, stated for context in the source but not used by
either formalized result's proof) is not drafted here: Mathlib already proves the corresponding
statement via affine independence
(Caratheodory.eq_pos_convex_span_of_mem_convexHull, Analysis/Convex/Caratheodory.lean),
from which the book's " points" bound follows via
AffineIndependent.card_le_finrank_succ. It is not added as a kind: reference milestone
because no corresponding theorem is yet published on the Prove2Me platform to point at (checked
2026-09-17: GET /theorems?q=Caratheodory returns only unrelated tropical-convexity results),
and re-drafting existing Mathlib content as a new platform theorem would duplicate rather than
reuse it.
Many results in economics and operations research reduce to a single question: does a
system of interacting, mutually reinforcing choices settle at an equilibrium? A firm
choosing input levels that are complements, a Cournot duopoly whose best responses move
together, a matching market where agents' preferences reinforce assortative pairings —
each is a fixed-point problem, but classical fixed-point theory (Brouwer, Kakutani) asks
for convexity and continuity that these problems rarely have. Tarski's fixed point
theorem [1955] showed that order, not topology, suffices: every increasing (monotone)
self-map of a nonempty complete lattice has a fixed point, and the fixed points themselves
form a nonempty complete lattice, with no continuity or convexity assumed at all. Zhou
[1994] extended this from single-valued functions to set-valued correspondences,
which is what is needed once "best response" becomes "the (possibly non-unique) set of
optimizers." This mission formalizes Zhou's theorem (Topkis's Theorem 2.5.1) together
with its parametric extension (Theorem 2.5.2), the two capstones of the lattice-theoretic
toolkit that the rest of Topkis's monograph — and, within this series, its mission on
supermodular games (Supermodularity and Complementarity V) — builds on directly.
A lattice is a partially ordered set in which every pair of elements has a join (least upper bound) and a meet (greatest lower bound). is a complete lattice if every subset (not just every pair) has a supremum and an infimum in ; a nonempty complete lattice always has a greatest element and a least element .
To compare sets of points — not just points — Topkis defines the induced set ordering : for , holds when every and satisfy and . Restricted to singletons, says exactly , so is the natural extension of from points to sets, and it is the order with respect to which set-valued maps (correspondences) are called increasing: implies .
A subset is a sublattice if it is closed under the binary join and meet of . is subcomplete if, more strongly, the supremum and infimum in of every nonempty subset of exist and lie in — so a subcomplete sublattice is itself a complete lattice under the order it inherits. A point is a fixed point of a correspondence if .
Let be a nonempty complete lattice and an increasing correspondence with subcomplete for every . Then:
and the set of fixed points of , under its inherited order, is itself a nonempty complete lattice.
Let be a partially ordered set and a jointly increasing, subcomplete-valued correspondence on . Then for each the greatest and least fixed points , of exist and are increasing functions of ; under the further hypothesis that whenever , both become strictly increasing in . This is the theorem that gives comparative statics their bite: it says an equilibrium moves monotonically — even strictly — as a parameter of the underlying system changes.
Two supporting results are formalized as milestones because Theorem 2.5.1's own proof invokes them directly: Lemma 2.4.2 (supremum and infimum are monotone under , whenever they exist) and Theorem 2.4.2 (an intersection of increasing correspondences, if it stays nonempty, is itself increasing).
The result itself. Tarski–Zhou is the order-theoretic alternative to Brouwer–Kakutani: where the latter needs a convex, compact strategy space and a continuous map, Tarski–Zhou needs only a lattice order and monotonicity, and it delivers something Brouwer–Kakutani does not — a greatest and a least fixed point, with an explicit order-theoretic formula for each, and the guarantee that the whole fixed-point set is a complete lattice in its own right. This is exactly the machinery behind existence proofs for supermodular games (Topkis's own Theorem 4.2.1, where the fixed points of the best-response correspondence are the pure-strategy Nash equilibria) and behind monotone comparative statics more broadly (Milgrom–Roberts [1994], of which Theorem 2.5.2 is a strict generalization to correspondences).
Formalizing it. Mathlib already has Tarski's theorem for single-valued monotone
functions (OrderHom.lfp/gfp, fixedPoints.completeLattice, Knaster–Tarski). Nothing
in Mathlib currently proves it for set-valued correspondences: this mission is a genuine
strengthening of existing formalized mathematics, not a restatement of it, and it
introduces the induced set ordering and subcompleteness — reused throughout the rest of
this book's mission series — for the first time.
The natural first idea — "apply Knaster–Tarski to some selection function built from " — fails because there is no canonical way to select a single point from each that remains monotone without already knowing the theorem: an arbitrary selection from an increasing correspondence need not itself be increasing (this is exactly the subtlety Topkis's Theorem 2.4.3 addresses only for correspondences with a greatest/least element). The real argument instead builds the candidate fixed point directly as a supremum over an auxiliary set and establishes it is a fixed point using the monotonicity lemma (Lemma 2.4.2) at each step — no selection is ever made. A second subtlety is that the fixed-point set is not, in general, a sublattice of : Topkis's Example 2.5.1 exhibits an increasing self-map of whose four fixed points are not closed under /. Part (b)'s claim that the fixed points form their own complete lattice must therefore be proved without ever assuming, or implying, that ambient joins and meets of fixed points are again fixed points.
is formalized as an abstract CompleteLattice, not ℝⁿ — the theorem is genuinely
about order, and specializing to would hide exactly the generality Zhou's result
adds over finite-dimensional fixed-point theorems. The induced set ordering
InducedSetOrder and the predicate Subcomplete are defined once in this mission and
reused by every later mission in the series that reasons about correspondences ordered
by . A formalization that replaced the correspondence by a single-valued
function would trivialize the mission into a restatement of Mathlib's existing
Knaster–Tarski theorem; the set-valued, subcomplete-ranged correspondence is not an
optional generality but the entire content being added. Part (b) of Theorem 2.5.1 is
formalized as a completeness statement about the induced order on the fixed-point set
itself — not as a claim that the fixed-point set is closed under 's ambient join and
meet, which Example 2.5.1 refutes. "Partially ordered set" throughout is Lean's
PartialOrder, matching the book's own usage in Chapter 2.
Decision-making problems rarely present the same fixed choice twice. A doctor prescribing a treatment sees each patient's medical history and symptoms before deciding; a website choosing which article to show sees the visitor's profile first. The multi-armed bandit model — where the learner repeatedly picks from a fixed set of arms with no side information — cannot express this: it is blind to the covariates that any real decision-maker actually observes. The contextual bandit model closes this gap by letting the learner see a context before acting, and asks for a decision rule that generalizes across contexts rather than memorizing a policy per context. Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making (arXiv:2312.16730v1, Section 3, pp. 38–53) develops this model and its algorithms as the bridge between supervised learning and sequential decision making, en route to general reinforcement learning. Contextual bandits with a learned reward-function class underlie production systems for content recommendation, online advertising, and adaptive clinical trial design (Li et al., A Contextual-Bandit Approach to Personalized News Article Recommendation, 2010, https://arxiv.org/abs/1003.0146; Agarwal et al., Making Contextual Decisions with Low Technical Debt, 2016, https://arxiv.org/abs/1606.03966).
The algorithmic history in this chapter runs through two distinct principles. The optimism principle (LinUCB, Section 3.2) generalizes the UCB algorithm to contexts under a linear reward model, but the chapter's own Example 3.1 (Section 3.3) shows optimism fails outside such structured classes, incurring regret linear in the size of the context space or the class. Foster and Rakhlin then present two "black-box" alternatives that use any function class through an abstract regression subroutine: the naive -Greedy method (Section 3.4), and the Inverse Gap Weighting (IGW) strategy underlying the SquareCB algorithm (Bietti, Agarwal & Langford, A Contextual Bandit Bake-off, 2018, https://arxiv.org/abs/1802.04064; Foster & Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, 2020, https://arxiv.org/abs/2002.04926). SquareCB attains a regret rate that both generalizes across contexts (no dependence on the size of the context space) and matches the optimal rate — improving on -Greedy's rate — while remaining agnostic to the internal structure of .
Over rounds, a decision-maker faces the contextual bandit protocol: at each round , it observes a context , selects a decision from a finite action set , and observes a reward . Rewards are generated independently as for a fixed, unknown conditional model ; write for the mean reward function and for the optimal, context-dependent policy. The context sequence is arbitrary — fixed in advance or adversarially chosen — while rewards remain stochastic. Performance is measured by regret against :
where is the learner's (possibly randomized) action distribution at round .
To generalize across contexts, the learner is given a class with , and aims for regret scaling with the statistical complexity rather than with . Both algorithms in this mission access only through an online regression oracle (Definition 3, p. 47): given the history , it returns an estimate satisfying, with probability at least , — for instance, exponential weights on a finite class achieves . SquareCB (p. 50–51) then samples its action from the Inverse Gap Weighting distribution (Definition 4, p. 50): given a vector of estimated values with greedy action , and an exploration parameter , is for the unique making a probability distribution.
This holds for any and any , with no reference to or to how was produced — it is the purely algebraic core the goal theorem invokes at every round.
with probability at least , for SquareCB run with , for any context sequence . This is the weakest stable target level in the chapter's oracle-based development: it is stated for an arbitrary class and oracle, so it survives any future improvement to the oracle's own bound, unlike a version hard-coded to a specific class or oracle.
Proposition 10 shows that Inverse Gap Weighting converts any estimation-error guarantee into a regret guarantee with the same statistical rate, with no algorithm-side dependence on the structure of or the size of : the same SquareCB template, driven by a plug-in regression oracle, is minimax optimal whenever the oracle itself is. When is finite, this yields , matching the optimal rate for stochastic multi-armed bandits (Section 2) while generalizing across contexts — a guarantee that optimism (Proposition 7) provably cannot deliver outside linear classes (Example 3.1), and that the simpler -Greedy baseline (Proposition 8) only delivers at a slower rate. Foster and Rakhlin describe Proposition 9 itself as being "at the core of the development for the rest of the course": the same IGW mechanism reappears, generalized, in the book's treatment of general decision-making and the Decision-Estimation Coefficient.
Both propositions are proved results, not open questions; this mission's contribution is a
machine-checked formalization of their exact statements and hypotheses — the precise
OracleGuarantee hypothesis Proposition 10 requires, the exact constant (, not a bare
) its proof yields at the stated optimal , and the universally-quantified form
of the IGW inequality (Proposition 9) that makes it reusable independently of any particular
oracle or class.
The obvious first idea for exploiting an estimator is a UCB-style optimism approach: build a confidence set around and act greedily on its upper envelope, as in LinUCB (Proposition 7). Example 3.1 shows this fails in general: a class can force the confidence set to remain wide on a fresh action at every new context, driving regret linear in — the confidence width in the regret bound does not shrink merely because the oracle's cumulative estimation error is small, since that error is not localized to the specific action the confidence-set approach tries next. Uniform exploration (-Greedy) sidesteps this but wastes exploration budget on actions already known to be far from optimal, which is what caps its rate at (Proposition 8). Inverse Gap Weighting instead ties the sampling probability itself to the estimated gap from the greedy action, so cheap-to-rule-out actions are down-weighted continuously rather than either fully explored (ε-Greedy) or trusted outright (optimism); the technical content of Proposition 9 is showing this specific reciprocal-gap form gives a bound with no hidden dependence on or , for every pair simultaneously — a guarantee optimism cannot match because its confidence sets are class-dependent by construction.
Contexts form an arbitrary type X; actions are Fin A for A : ℕ. A finite probability
distribution over Fin A is represented directly as p : Fin A → ℝ with ∀ π, 0 ≤ p π and
∑ π, p π = 1, and as the finite sum ∑ π, p π * g π, rather than
via Mathlib's PMF (which is ℝ≥0∞-valued) — an equivalent and lighter-weight representation of
a distribution on a finite type. The normalizing constant of Definition 4 and the
optimal actions , are each specified by their defining property (existence
of realizing the IGW formula; ) rather
than constructed explicitly via an intermediate-value or Finset.argmax argument, avoiding
committing to one choice function for a value the book itself leaves implicit. The class
enters neither proposition's statement directly: it appears in the source only through the
abstract bound , which is carried as an explicit real-valued
parameter and hypothesis (OracleGuarantee) rather than as a literal subset of a function space,
since no property of beyond producing this bound is ever used. The probability-
qualifier attached to the online regression oracle's guarantee is likewise the explicit
hypothesis OracleGuarantee ... EstSq on a fixed realized run, rather than a statement
quantified over an underlying probability space of histories — every subsequent step in both
propositions' proofs is deterministic given that this event holds, so this does not weaken either
conclusion. A trivializing formalization would fix (a single ever-optimal action, making
both Reg and the IGW inequality vacuous) or take EstSq as an unconstrained free variable with
no positivity hypothesis (making in Proposition 10 undefined); this mission's statements
require 0 < EstSq and leave , , , -via-EstSq fully general.
This mission omits Proposition 7 (LinUCB): its proof rests on an entirely disjoint apparatus
(finite linear parameter sets, least-squares confidence sets, the elliptic potential lemma) that
neither Proposition 9 nor 10 requires, and Example 3.1 (the failure of optimism) is a worked
example rather than a numbered, formalizable claim. It also omits Proposition 8
(-Greedy): the source leaves the optimal unspecified ("choosing
appropriately"), and deriving its own optimal value and matching constant
independently — rather than reusing the book's own explicit constant, as Rule 7 of this
formalization effort requires — was judged too likely to introduce an unfaithful, invented
constant within this mission's time budget; both are natural extensions for a follow-up mission
or contribution. Reusable infrastructure: the Fin A-indexed finite-distribution convention and
the OracleGuarantee/optimal-action-by-property pattern extend directly to any later chapter
built on the same online-regression-oracle abstraction.
The multi-armed bandit is the simplest model of sequential decision-making under partial feedback: a learner repeatedly picks one of finitely many options and observes a reward only for the option chosen, never for the alternatives. It formalizes problems ranging from clinical trial design (which treatment to offer a patient) to online advertising (which ad to show) and A/B testing more generally. The framework dates to Robbins' 1952 paper on sequential design, and the algorithm this mission's goal theorem concerns — the Upper Confidence Bound (UCB) algorithm of Lai and Robbins [1985] and Auer, Cesa-Bianchi and Fischer [2002] — is the canonical answer to how to explore efficiently: instead of exploring uniformly at random, act optimistically with respect to the current uncertainty about each option's value. This mission draws its formalization from Chapter 2 of Foster and Rakhlin's 2023 lecture notes, Foundations of Reinforcement Learning and Interactive Decision Making, which develops the bandit problem as the first rung of a ladder of increasingly general interactive decision-making settings (contextual bandits, structured bandits, reinforcement learning) that the book's later chapters build.
Fix a finite decision (action) space . In the multi-armed bandit protocol, for each round the learner selects a decision , possibly at random according to a distribution depending on the history observed so far, and then observes a reward drawn independently from a fixed conditional distribution (the stochastic rewards assumption). Writing for the mean reward function and for an optimal decision, the learner's performance is measured by the regret
Because the learner observes a reward only for the action played (bandit feedback), a purely greedy strategy that always plays the current empirical maximizer can commit to a suboptimal action forever, incurring linear regret; some form of deliberate exploration is necessary. The chapter's central construction is the confidence interval: a pair of functions such that, with probability at least , for every round and decision simultaneously. The UCB algorithm plays the optimistic action at every round, using the confidence interval built from Hoeffding's inequality around the empirical mean .
holding with probability at least , for the UCB algorithm using the confidence radius of Eq. (2.19). This is the weakest stable statement the chapter proves: it is optimal up to the log factor, and strengthening it (e.g. to the sharper instance-dependent bound of Remark 10) is explicitly left to later work by the book itself.
UCB is the prototype of the "optimism in the face of uncertainty" principle that recurs, in increasingly abstract form, throughout the rest of the book: the same two-step argument (Lemma 7 + Lemma 8) reappears for linear bandits, structured bandits via the Decision-Estimation Coefficient, and UCB-VI for tabular reinforcement learning. Formalizing Chapter 2 in full therefore front-loads the proof pattern every later chapter in this series specializes. The result itself is also of standalone interest: the minimax rate is the benchmark every subsequent bandit algorithm in the literature is compared against, and the -vs- contrast between ε-Greedy and UCB is the standard illustration, in any course on the subject, of why adaptive exploration matters.
No formalization of this exact statement — realizability with respect to a function class and a generic confidence interval, rather than a per-arm sub-Gaussian empirical mean — currently exists on the platform (see Formalization scope below); the mission both proves this specific regret bound and seeds the generic optimism/potential lemma pair (Lemma 7, Lemma 8) that the book's later, more structured settings specialize.
The natural first attempt — bound the regret of the empirical-mean-greedy algorithm directly — fails outright: on a two-armed instance where one arm is deterministic and the other only slightly better in expectation, the greedy algorithm can commit to the worse arm forever with constant probability, giving linear, not sublinear, regret (§2.1). The obvious fix, ε-Greedy, forces exploration uniformly across all actions regardless of how much is already known about each, so the exploration cost scales with even for actions whose value is already well determined — this is exactly what caps ε-Greedy at the rate. UCB's optimism principle resolves this by exploring an action only in proportion to how uncertain it still is; the technical core, isolated in Lemma 7 and Lemma 8, is disentangling "the algorithm made a mistake" from "the algorithm is still uncertain," which are conflated in the naive per-round regret decomposition used for ε-Greedy.
Both the goal and the milestones fix a finite decision space Fin A, a mean reward
function fStar : Fin A → ℝ with fStar π ∈ [0,1], and an optimal decision
piStar. Regret is defined generically (Eq. (2.3)) via per-round decision weights
p : ℕ → Fin A → ℝ, so it applies uniformly to a randomized algorithm (ε-Greedy) and
a deterministic one (UCB, via the point mass at the played action). The book's "with
probability at least " qualifier on both Proposition 4 and Proposition 5 is
formalized as the deterministic consequence of the underlying concentration event
(Eq. (2.9) and Eq. (2.18) respectively) holding — exactly the move the book's own
proofs make ("Let us condition on the event in (2.18) ... "). The concentration
events themselves rest on Hoeffding's inequality for adaptive stopping times
(Lemma 33) and Bernstein's inequality (Lemma 5), both stated in the book's technical
appendix outside this chapter, and are not drafted here; a solver may either take
them as a hypothesis (as this mission's statements do) or import/prove them
separately. A trivializing formalization is ruled out explicitly: taking δ outside
, or dropping the fStar π ∈ [0,1] hypothesis, would make the stated
constants vacuous or false, so both are retained as explicit hypotheses in every
theorem. In every ≲ statement (Prop. 4, Lemma 8, Prop. 5) the witnessed constant
C is quantified before the instance parameters (A, T, δ, and the realized
sequences): ∃ C, 0 < C ∧ ∀ A T δ ..., Reg ≤ C * (rate), not the other order. This
is deliberate, not stylistic: quantifying C after the instance lets it depend on
A, T, δ, making the bound satisfiable by an arbitrarily large C chosen per
instance and hence content-free, which is not what the book's ≲ means (a single
constant working uniformly over all instances). Proposition 5's UCB decision rule
is stated in the book's own two clauses, not collapsed into a single "maximize the
upper confidence bound" rule: the confidence radius of Eq. (2.19) is at
(an action never yet sampled), so the book's UCB always plays an
unsampled action before ever comparing indices, and only compares finite upper
confidence bounds once every action has been sampled at least once; the confidence
event of Eq. (2.18) is correspondingly assumed only at sampled actions, since the
book's own bound is vacuous otherwise. An earlier draft instead capped the radius
at when , which is a true statement about a different algorithm (a
sampled action can have index above the capped unsampled index), and was corrected
to the book's own rule after moderation. Reuse from the platform's existing bandit library (BanditAlgorithm,
Lattimore & Szepesvári) is deliberately avoided: that library's UCB
(bandit_ucb_regret_bound, bandit_ucb_minimax_regret_bound) is stated for
per-arm 1-sub-Gaussian rewards with fixed by the horizon, whereas
this chapter's UCB is stated for a free failure probability and a generic
confidence-interval abstraction (the multi-armed case being of the book's general realizability framework) — the two are
related but not the same statement. Contributions extending the mission with the
generic confidence-interval form of Lemma 7/8 applied to other chapters in this
series (contextual and structured bandits) are welcome.
Two-stage stochastic programs with recourse require evaluating , the expected value of a recourse function, at every candidate first-stage decision . When is high-dimensional or continuously distributed, this expectation is a multivariate integral of a piecewise-linear, generally nondifferentiable integrand, and classical quadrature rules — built for smooth integrands in low dimension — do not apply (Birge & Louveaux, §8.1). What does apply is convexity: is convex whenever the recourse problem is a linear program in , and convexity alone is enough to sandwich between two computable discrete approximations. This chapter develops that sandwich, and it is the standard device used throughout the stochastic-programming literature to bound and iteratively refine the recourse function: the lower bound goes back to Jensen [1906]; the upper bound is due to Edmundson [1956] and Madansky [1959], with the mean-consistent LP refinement due to Madansky [1960] and Gassmann & Ziemba [1986]. Refinements of both bounds appear in Huang, Ziemba & Ben-Tal [1977], Kall & Stoyan [1982] and Frauendorfer [1988].
Fix a probability space and an integrand , where is the (convex, closed) support of a random vector and is a real vector space (in the recourse application, and is the first-stage feasible region). Write .
A partition of into measurable blocks determines, for each block, its probability and its conditional mean . Equivalently — and this is the convention this mission's Lean development uses — the blocks may be taken directly on the sample space as the pulled-back sets , with and the Bochner integral average of over the block; the two descriptions coincide.
This is the sharpest statement the chapter proves for the lower bound: it holds for every finite measurable partition, with no assumption beyond convexity of and integrability.
For compact, let be the extreme points of , carrying the Borel field of all its subsets. If, for every , is a probability measure on with barycenter (i.e. ) and is measurable for every , then
Together the two targets give the chapter's headline sandwich: for convex , the finite-partition Jensen value and the Edmundson-Madansky value bracket the true expectation, and refining the partition (resp. the disintegration) tightens both sides toward it.
The Jensen bound is the workhorse of discrete-distribution approximation in stochastic
programming: it is what makes a valid, refinable
lower-approximation of the true recourse function, and it underlies the partition-refinement
schemes (§8.2, following Birge & Wets [1986] and Frauendorfer & Kall [1988]) used inside the
-shaped method and separable-programming solvers described later in the chapter (§8.3). The
Edmundson-Madansky bound is its indispensable upper counterpart: without it there is no
certificate of how far a lower approximation can be from the truth, and the mean-consistent LP
refinement (eq. 2.9, not part of this mission) reduces to a moment-problem computation over
. Both bounds are, to date, unformalized: the platform holds no theorem matching either a
finite-partition conditional-Jensen inequality or an extreme-point disintegration bound (searched
GET /theorems?q=... for "Jensen", "conditional expectation", "Edmundson Madansky", "partition
convex" — no relevant hits), so this mission is a first formalization of both, not a
reformulation of existing platform content. Mathlib supplies the raw convexity substrate this
mission is built from — finite Jensen (Analysis/Convex/Jensen.lean) and, critically, the
set-average integral Jensen inequality (ConvexOn.map_set_average_le in
Analysis/Convex/Integral.lean), exactly the per-block step the book's proof of Theorem 1
performs — but no existing lemma assembles these into the partitioned, conditional-mean statement
the book actually states.
The obvious shortcut is to prove "convex functions lie above their tangent line" and stop — this captures no partition structure at all and is not the theorem the book states (the theorem is about , a sum over blocks, not a single linearization). The real content is bookkeeping across the partition: writing as (an exact identity, no convexity needed), then applying ordinary Jensen inside each block to replace by from below — the inequality only enters at the second step, once per block. Proving this in Lean means correctly discharging, for every block, the side conditions Mathlib's integral-Jensen lemma needs (closedness of , continuity of on , integrability on the block) and then summing the per-block inequalities against weights that themselves depend on the partition — an easy step to get wrong by, e.g., letting be an arbitrary point of rather than exactly its conditional mean, which understates what Jensen actually forces. Theorem 2 additionally requires setting up the disintegration correctly: is a probability measure defined as an integral of the kernel-like family against , and both the barycenter condition on and the measurability of are load-bearing — dropping either makes ill-defined or the bound's proof inapplicable.
for a complete real normed vector space (NormedAddCommGroup E,
NormedSpace ℝ E, CompleteSpace E); no finite-dimensionality is assumed since neither theorem's
proof needs it. The parameter ranges over an arbitrary type with ,
and is left as a bare function α → E → ℝ, matching the book's level of abstraction (the
recourse LP's own data is never used in either proof).
The partition is formalized directly on the sample space (a Partition structure:
pairwise-disjoint measurable blocks covering , each of positive measure) rather than on
, per the equivalence noted under Setting; is defined as the Bochner-integral
average , so it is forced to be the conditional mean and cannot be
weakened to an arbitrary sample point of the block — the change the chunk brief flags as the main
faithfulness trap for this chapter.
Two explicit hypotheses are added beyond the book's own statement of Theorem 1, both needed by
Mathlib's integral-Jensen lemma rather than narrowings of the mathematical content:
ContinuousOn (g x) Ξ (finite-dimensional convex functions are automatically continuous on the
interior of their domain, which is what the book implicitly relies on; stated explicitly since
is not assumed finite-dimensional) and integrability of and of
(needed for and each to be well-defined). For Theorem 2, the
disintegrating family is E → Measure Ext for an abstract type Ext (standing for
) with the discrete MeasurableSpace (every subset measurable, matching the
book's "Borel field ... the collection of all subsets"), mapped into by an embedding toE
whose range is exactly (convexHull ℝ Ξ).extremePoints ℝ; the measure (named μExt in
the Lean code, since λ is a reserved keyword) is a hypothesis satisfying its defining equation
(2.6) rather than constructed, since constructing a measure from a set function is a separate,
book-external piece of measure theory the chapter's own proof does not perform either — it simply
asserts is the probability measure with that value on every set.
A trivializing formalization is ruled out explicitly: a version that lets range over an arbitrary point of , or that proves only the ordinary (unconditional) Jensen inequality without ever introducing the partition, states something strictly weaker than the book and is not what is formalized here.
Both draft theorems end in := by sorry; a full Lean proof of Theorem 1 combines Mathlib's
ConvexOn.map_set_average_le applied per block with the exact decomposition of into
over the partition's disjoint, covering blocks. Reusable beyond this mission:
the Partition structure and its weight/condMean accessors generalize to any chapter needing
a finite measurable partition with conditional means (this book's later approximation schemes,
§8.2-8.5 and Chapter 10, all build on the same device). Contributions solving either theorem, or
formalizing the partition-refinement monotonicity (eq. 2.3, not part of this mission's milestone list since it is not itself a
numbered theorem) as a follow-up, are welcome.
Every stochastic program is, in practice, compared against a shortcut. A decision maker facing genuine uncertainty is tempted either to replace the random data by its mean and solve one deterministic problem, or to imagine that perfect information about the future were available and solve a separate deterministic problem per scenario. Both temptations have precise answers: the expected value of perfect information (EVPI) measures how much a decision maker should be willing to pay for a perfect forecast, and the value of the stochastic solution (VSS) measures the cost of ignoring uncertainty altogether by solving the mean-value problem. Both concepts originate in decision analysis — EVPI traces to Raiffa and Schlaifer (1961) — and were brought into stochastic programming by Madansky (1960), who proved the first chain of inequalities relating the wait-and-see value, the recourse value and the expected-value-solution's cost. Birge and Louveaux, Introduction to Stochastic Programming, 2nd ed. (Springer, 2011), Chapter 4, gives the standard modern treatment, including a refined family of bounds — built from pairs subproblems against a chosen reference scenario — that sharpen VSS beyond the original mean-scenario comparison. This mission formalizes that chapter's capstone: the five-quantity, four-inequality chain that pins VSS between two computable optimal values.
Fix a two-stage stochastic program with fixed recourse: a finite family of K scenarios
in , each occurring with probability ,
; a first-stage feasible set ; and, for every
first-stage decision and every scenario , a
scenario cost — the optimal value of . By convention when has no feasible second-stage recourse under
, and when the second-stage program is unbounded below.
From , five basic quantities are defined (Birge & Louveaux §4.1–§4.2):
Section 4.6 refines VSS by replacing the mean scenario with an arbitrary reference scenario (not necessarily one of the possible scenarios, e.g. a worst case), with assumed probability :
Four links, each with independent content: nonnegativity of the leftmost gap, then two genuine inequalities (from the pairs-subproblem comparisons of Propositions 7 and 8), then the identity folded against 's reverse-direction cousin. This is the weakest statement that keeps all five quantities distinct — stating only the outer bound would erase exactly the refinement (via pairs subproblems) that makes the chapter's method useful.
The chain gives a decision maker two computable, non-obvious bounds on VSS — a quantity that is otherwise expensive to pin down exactly, since itself already requires solving the full recourse problem. and are both computable from (or ) two-scenario LPs, far cheaper than the full -scenario recourse problem, so Theorem 9 turns an expensive exact quantity into a pair of cheap certified bounds. Formalizing it fixes, once and for all, the exact hypotheses and quantifier structure of Madansky's original inequality (Proposition 1) together with the later pairs-subproblem refinement (Propositions 6–8, Birge 1982), often cited informally as "the VSS bounds" without distinguishing , , and . No part of this chain is on Mathlib or Formalpedia today (checked by concept query, not title); this is a first, from-scratch treatment of two-stage recourse value-of-information theory as formal objects.
The obvious first idea — collapse , , , , , , to one "the optimal value of the LP" and prove a single inequality — throws away the entire content of the chapter. Each quantity restricts the minimization to a different feasible object: minimizes jointly over ; swaps the order of and ; / evaluate one fixed under every scenario; and each minimize over a family of pairs subproblems rather than the full -scenario problem. The chain's proof (Propositions 7–8) depends on this precisely: Proposition 7's lower bound uses that each pairs-subproblem-optimal is feasible (not necessarily optimal) for the single-scenario problem at , and its upper bound uses that the recourse-optimal is feasible (not necessarily optimal) for the pairs subproblem — a feasible-but-not-optimal argument in each direction, not a direct comparison of objective values. Losing track of which solution is fixed and which is optimized destroys the argument entirely.
An Instance bundles the finite scenario set (Fin K, probabilities p : Fin K → ℝ with
p ≥ 0, ∑ p = 1, scenarios xi : Fin K → (Fin d → ℝ)), the first-stage feasible set
K1 : Set (Fin n1 → ℝ), and the scenario cost z : (Fin n1 → ℝ) → (Fin d → ℝ) → EReal, using
the extended reals to carry the book's own +∞/−∞ conventions for infeasibility and
unboundedness rather than silently restricting to a finite-valued special case (a genuine risk
of trivialization here, since Example 2 of the chapter exhibits ). All optimal
values (RP, WS, EV, EVPI, EEV, VSS, EVRS, generalized VSS, SPEV, EPEV) are
defined directly from z, matching the book's own level of abstraction in this chapter (which
never unfolds z into the underlying LP's data — those appear only in Chapter
3). Because EEV, the mean-scenario VSS, EVRS, the generalized VSS, and EPEV are each
defined relative to an optimal solution of some sub-problem — the book itself only ever says
"let denote some optimal solution" — every theorem using them states that
solution and its optimality as explicit hypotheses (x ∈ K1 and z x … = ⨅ …), never baking it
into a Classical.choiced value; this keeps the quantifier structure faithful to the book's own
"let ... be an optimal solution" phrasing. Proposition 5's part (b) — the upper bound
, "for stochastic programs with fixed recourse matrix and
fixed objective coefficients" — needs a different scope: that hypothesis is a structural
property of the underlying LP data (, , fixed across scenarios) invisible once is
abstracted away as above, and pinning it down would require modeling the LP's
data explicitly (as Chapter 3's mission does for its convexity theorem). That part is out of
scope here and is not needed for Theorem 9's own chain, which rests only on Proposition 5(a).
Collapsing any two of , , , , , , to a single "value of the LP" — the trivialization this book-wide series flags for Chapter 4 — is ruled out by construction: each is its own definition over its own feasible object, and Theorem 9's statement names all five quantities in the chain rather than only its outer bound. The two occurrences of "VSS" in the chapter (the original mean-scenario of §4.2, and the reference-scenario generalization of §4.6, used only in Theorem 9) are likewise kept as two distinct definitions rather than conflated under one name.
Every addition and subtraction between EReal values in this mission — inside expect, WS,
EVPI, VSS, EVRS's appearance in VSSRef, the pair sum inside pairsValue, the sum inside
SPEV, and all four differences in Theorem 9's own chain — uses three explicit operations,
badd/bsub/bsum, that implement the book's own convention (p. 164) that +∞ (infeasibility)
dominates, i.e. (+∞)+(−∞)=+∞, rather than Mathlib's native EReal addition, whose
⊤+⊥=⊥ would make VSS ≥ 0 (Proposition 5(a)) and the goal's own leftmost inequality false
whenever a witness solution is infeasible in a positive-probability scenario — exactly the
situation of the book's own Example 2 (pp. 174-175). The reference scenario's probability
(p. 172) is likewise not a free parameter but a definition, refProb,
computed from the instance itself as ; SPEV's sum is correspondingly
restricted to the scenarios other than the reference scenario (), matching the
book's own proof of Proposition 7, which uses . The single hypothesis
refProb I xir < 1 on Propositions 7, 8 and the goal says that some other scenario remains
possible, which the book's own factor presupposes.
Reusable beyond this mission: the Instance definition and the RP/WS/EV quantities are
the natural base for any later chapter of this series that needs the two-stage recourse value
(e.g. Chapter 3's convexity mission, Chapter 5's L-shaped method); contributions extending this
Instance to the full LP data of the underlying two-stage program, or adding Proposition 5(b)
and Proposition 2's Jensen-inequality argument on top of it, are welcome.
Thompson's group is the group of piecewise-linear order-preserving homeomorphisms of with finitely many breakpoints, all at dyadic rationals, and all slopes powers of . Two earlier missions formalize its definition and its first structural facts (§1 and §4: the commutator subgroup is simple, is not elementary amenable) and its tree-diagram normal form (§2). What neither says is how looks as an abstract group: by generators and relations.
That is §3 of Cannon, Floyd and Parry's Introductory notes on Richard Thompson's groups (L'Enseignement Math. 42 (1996), doi:10.5169/seals-87877), which gives two presentations of and proves that both present the group of homeomorphisms:
The finite presentation is the form in which enters most of the literature — the word problem, the growth and amenability questions, the homological results of Brown and Geoghegan all start from it — and the infinite presentation is the one that makes the normal form of §2 visible as an algebraic fact.
Throughout, , the source's convention, and groups are written multiplicatively with composition of maps as the product: .
The functions. and are the two specific homeomorphisms of from the §1
mission (mapA, mapB: halves , is a translation on ,
and doubles ; is the identity on and acts like , scaled,
on ). For , and ; these are the
functions X n of the §2 bundle. Corollary 2.6 of the source, proved in the §2 mission, says
and generate .
The formal symbols. and are presented groups: the free group on the listed
symbols modulo the normal closure of the listed relators. In Lean they are Mathlib's
PresentedGroup applied to explicit relator sets: relsF1, a two-element set of words in
the free group on the two-element type FormalAB, and relsF2, the set of words
for in the free group on . The symbols
are distinct objects from the functions; the whole content of the section is that the map
"symbol function" is an isomorphism.
Auxiliary objects. In the source sets and
for (Y), the intended images of the . In a list of nonnegative
exponents determines the positive word
(wordF2), the formal counterpart of the §2 bundle's word; the normal-form conditions of
Corollary-Definition 2.7 are the §2 predicate IsNormalFormData, reused verbatim.
The goal is the finite presentation, Theorem 3.4 for :
On the way, in the order the source proves them:
A one-line consequence closes the list: is finitely presented, in Mathlib's sense
Group.IsFinitelyPresented.
The result. A presentation is what makes an object of combinatorial group theory. The two relators are what one checks a homomorphism against, the infinite presentation is what the normal form is a normal form for, and "finitely presented" is the hypothesis under which is a test case for conjectures about finitely presented groups. Every later algebraic statement about — the word problem is solvable, the abelianization is , the automorphism group, the presentations of and — is stated relative to one of these two presentations.
Formalizing it. Both theorems are proved in the source and their proofs are short, so what this mission produces is the machine-checked bridge between the two existing developments: the analytic definition of and its tree-diagram normal form on one side, an abstract presented group on the other. The isomorphism is where §2's uniqueness theorem is used rather than merely proved: injectivity of is exactly the statement that distinct normal forms give distinct functions. Nothing here is machine-checked anywhere else; the platform has no presentation of .
Theorem 3.1 is a computation in and offers no surprises once lines (3.2) and (3.3) of the source are set up as their own statements: the induction that establishes from the two relators is the only place care is needed, and the source spells it out.
The central difficulty is the paragraph on p. 226 proving that is injective. The
source argues in prose that "every nontrivial element of can be expressed as a
positive element times a negative element", and then "put in normal form" by deleting an
from both parts and re-indexing when is absent. Formally this is a rewriting
argument inside the abstract group , with no geometry to lean on: one needs the three
derived relations , ,
(for ), an induction that sorts an arbitrary word into
positive-times-negative form, and a second induction that reduces such a form until the
normal-form conditions hold. The obvious shortcut — "every element of is the image of
some function, and functions have normal forms" — is circular, because it presupposes the
injectivity being proved. The milestone exists_isNormalFormData_F2 isolates this step.
word/wordFrom and the predicate
IsNormalFormData are the published definitions of the §1 and §2 missions
(CannonFloydParry, CannonFloydParry_Trees, CannonFloydParry_TreeDiagrams), imported
unchanged. Elements of are order isomorphisms of the subtype ,
and is the subgroup they generate; membership of , , in is a proved
theorem, not a definition.CannonFloydParry_Presentations adds only the formal side: the symbol type
FormalAB, the relator sets relsF1, relsF2, the presented groups F1, F2, the
symbol maps symF2 (into ) and symF (into the interval maps), the elements Y, and
the words wordF2. Relators are written out as ; no commutator notation
is used in published statements.MulEquiv sending the named generators to the
named images. Nothing is asserted about uniqueness of the isomorphism (it is unique, since
the generators generate).closure_mapA_mapB_eq_F), the §2 normal-form
theorems (exists_isNormalFormData, word_ne_one_of_isNormalFormData), and the §4
mission's mem_commutator_iff if a solver prefers to verify the relators of in
through supports rather than by direct computation. Solutions may import them.Group.IsFinitelyPresented instance built from
the isomorphism (the last milestone), and, further off, the presentations of and
from §5–§6, which extend by one and two generators.Thompson's group is a finitely presented group of piecewise-linear homeomorphisms of the unit interval that has served since the 1960s as a standard supply of counterexamples in combinatorial group theory: its commutator subgroup is simple, every proper quotient of it is abelian, it contains no free subgroup of rank two, it is not elementary amenable, and whether it is amenable is a question Cannon, Floyd and Parry report as having been raised by Geoghegan in 1979 and still open when they wrote (CFP96, §4 and p. 227).
Almost nothing about is computed directly from that analytic definition. What makes the group tractable is a combinatorial calculus: each element is encoded by a pair of finite binary trees, and multiplication becomes a cancellation between trees. Cannon, Floyd and Parry credit the device to Brown and devote §2 of their notes to it; everything later in those notes that requires a computation — the two presentations of §3, the normal subgroup lattice of §4, the treatment of Thompson's group in §5 — runs through it.
This mission formalizes that calculus and the normal form it yields.
A real number is dyadic when it has the form with an integer and a nonnegative integer. Thompson's group consists of the increasing homeomorphisms of that are piecewise linear with finitely many breakpoints, all breakpoints dyadic and every slope an integer power of , under composition. Two of its elements are
and from them come and for , so that .
A standard dyadic interval is one of the form with and nonnegative integers and . A partition of is a standard dyadic partition when every is a standard dyadic interval.
An ordered rooted binary tree is a finite tree in which each vertex has either no children or an ordered left child and right child. Its childless vertices are its leaves, which carry a canonical left-to-right order; its right side is the path from the root always taking the right child; a caret is a vertex with its two children. Assigning to the root and splitting each interval at its midpoint between the two children gives every vertex a standard dyadic interval, and the leaves then cut out a standard dyadic partition — the sense in which such a tree is a -tree. The exponents of a -tree are one nonnegative integer per leaf, in order: the th is the length of the longest arc of left edges beginning at the th leaf that does not reach the right side.
A tree diagram is an ordered pair of -trees with equally many leaves. An element of has that diagram when is affine on each interval cut out by the leaves of and carries those intervals, in order, onto the intervals cut out by the leaves of . Adjoining a caret to and to at the same leaf gives another diagram for the same ; a diagram admitting no such reduction — no position where both trees carry a caret — is reduced.
Every in is
for exactly one choice of nonnegative integers , , subject to two conditions: exactly one of and is nonzero, and if and for some then or .
It fixes no bound on and no normalization beyond those two conditions, so no later refinement of how the exponents are presented can invalidate it.
The milestone list follows §2 in order: the correspondence between standard dyadic partitions and -trees, the bijection between and the reduced tree diagrams, the word read off the exponents of , a criterion for a diagram to be reduced, generation by and , and closure under multiplication of the positive elements — those of the form with every exponent nonnegative.
A normal form is a decision procedure: two words in the generators name the same element exactly when their normal forms agree, so the word problem for is solved by computing them. The generation statement is what licenses treating as a two-generator group, and it is the input to both presentations in §3. The positive elements and their closure under multiplication are used, with the normal form, throughout §5 on Thompson's group .
The §2 results this mission targets — Lemma 2.2, the correspondence between and the reduced tree diagrams, Theorem 2.5, Corollary 2.6, Corollary-Definition 2.7 and Lemma 2.8 — are proved mathematics: Cannon, Floyd and Parry are expounding material that goes back to Thompson's unpublished notes. None of them has a machine-checked proof on this platform, and the library contains no tree-diagram machinery to build on, so the definitions published here fix the interface for anyone later formalizing Thompson's groups and , which occupy the same notes and are built from the same trees.
There is also a concrete dependency. The companion mission on §4 of the same paper has eleven of its fifteen milestones machine-checked, and all four that remain wait on this section: Cannon, Floyd and Parry prove their Theorem 4.1 through Corollary 2.6 and their Theorem 4.3 through the normal form. Corollary 2.6 appears in this milestone list as the same theorem object that is open there, so closing it here closes it there.
The obvious way to attach a diagram to an element is to use the partition given by its breakpoints. That fails twice over: the breakpoints of need not be the division points of any -tree, and even when they are, their images under need not be either, since the definition of constrains the breakpoints and slopes of and says nothing about where the image partition sits. Both failures must be repaired by refining the partition before any tree appears, which is why that refinement is a milestone rather than a preliminary.
Uniqueness of the reduced diagram is a difficulty of a different kind: two reduced diagrams for the same element admit no a priori map between their trees, so they cannot be compared directly.
A third is not visible in the source. For trees with leaves the exponent lists always end in , so the outermost factors of the word above vanish; but the normal form demands that exactly one of , be nonzero. The two indexings differ, and a re-indexing step sits between the theorem producing the word and the corollary stating the normal form. The paper prints them one under the other. That step is a milestone of its own, flagged as absent from the source, so a solver working from the paper alone is not ambushed by it.
Ordered rooted binary trees are an inductive type — a leaf, or a pair of subtrees — rather than graphs with a root and valence conditions. Those conditions say exactly that every non-leaf vertex has two distinguished children, so both descriptions pick out the same objects, but the inductive type is a reformulation of the paper's definition and the definition bundle says so. The infinite tree of all standard dyadic intervals is likewise never built: the subdivision of comes from a recursion halving at each node, which turns the paper's observation that the leaves of a -tree are the intervals of a standard dyadic partition from something given into something proved.
is imported rather than redefined, from the published definition bundle of the companion mission, where it is the subgroup generated by the piecewise-linear maps described above; membership in that subgroup is identified with the piecewise-linear description by a theorem already machine-checked there. Exponent data is carried by finite lists, and the uniqueness in the goal is uniqueness of that list data.
The goal is vacuous in neither direction: its hypothesis is met by and themselves, and a separate milestone asserts that every choice of exponent data meeting the two conditions names an element other than the identity.
The tree combinatorics — leaf counts, right sides, the subdivision map, the exponents, carets — is published here as a separate definition node that mentions nowhere and needs nothing but Mathlib, so it is reusable as it stands; the diagram vocabulary is built on it. Any milestone is open to contribution, as are routes other than the paper's.
Within that paper tree diagrams are credited to Brown and the word-length algorithm to Fordham, cited there as [Bro1] and [Fo].
Perturbative quantum field theory produces algebraic varieties. In the parametric (Feynman–Symanzik) formulation of a momentum-space Feynman integral of a graph , the integrand is built from the Kirchhoff (first Symanzik) polynomial , and the period that the integral computes is governed by the graph hypersurface . Because has integer coefficients, is defined over , and one can ask arithmetic questions about it: how many points does it have over a finite field , is that count a polynomial in , and what is its class in the Grothendieck ring of varieties?
A separate line of work asks when a variety defined over carries an additional structure over the "field with one element" . Tits observed in 1956 that is a polynomial in whose behaviour as is governed by the symmetric group, and several inequivalent theories of -geometry have been proposed since. In the formulation of López Peña and Lorscheid, an -structure is witnessed by a torification: a decomposition of the variety into split tori inducing a bijection on -points for every field .
Bejleri and Marcolli, Quantum field theory over (Journal of Geometry and Physics, 2013, doi:10.1016/j.geomphys.2013.03.002), brought these two lines together: they asked which varieties of perturbative QFT admit an -structure, proved a blow-up formula for torified varieties, and deduced that the wonderful compactifications of graph configuration spaces and the moduli spaces are -varieties. Along the way they recorded elementary but sharp necessary conditions for an -structure, and tested them on concrete families of graph hypersurfaces. This mission formalizes that necessary-condition layer for the simplest infinite family, the banana graphs. The programme continues to be cited in the physics literature (arXiv:2401.07822).
For , the banana graph has two vertices joined by parallel edges. Its graph hypersurface is cut out by the Kirchhoff polynomial of , and is its complement.
Write for the Lefschetz class in the Grothendieck ring of varieties and set
If a variety admits a torification by tori , then its class is , so it is a polynomial in with non-negative integer coefficients; this is Lemma 3.8 of the paper. Writing , the Euler characteristic is the constant term , because positive-dimensional tori have vanishing Euler characteristic — whence the coarser necessary condition of Proposition 3.1. Non-negativity of the coefficients is therefore a necessary condition for an -structure, and one that can be checked by pure computation once the class is known.
For the banana graphs the class is known in closed form (Aluffi–Marcolli, quoted as equation (3.8) of the paper):
The first summand is , and the two quotients are exact divisions: they are the polynomials and of equations (3.9) and (3.10).
The goal is the first half of Lemma 3.9: for all , every coefficient of , as a polynomial in , is non-negative,
so that passes the necessary condition of Lemma 3.8.
The milestones are the steps the paper uses, and the contrast it draws:
Item 5 is the point of the lemma: the necessary condition separates from , so it is not vacuous on this family.
The combination " passes, fails" is the paper's concrete evidence that the torification condition is a usable filter on the varieties of perturbative QFT: it rules out an -structure on the hypersurface complements — the objects whose periods are the Feynman integrals — while leaving the hypersurfaces themselves as candidates, and it motivates the paper's Question 3.10 (whether the graph hypersurfaces satisfying the condition actually admit torifications).
What this mission produces on top of the paper is a machine-checked version of that computation. The mathematics here is not open: Lemma 3.9 is proved in the source, and the six statements of this proposal are elementary consequences of the closed formula (3.8) once the two divisions are performed. The captain has checked that all six compile and are provable in Lean 4 with Mathlib. The deliverable is therefore a formalization, not a new theorem: a reusable Lean model of Grothendieck classes in the variable for this family, with the coefficient positivity and the failure of positivity for the complement both verified, and the printed expansion for in the paper reproduced by the formalized coefficient formula.
The obstruction is bookkeeping, not depth. Equation (3.8) is a rational expression; the two fractions are exact divisions only after one knows the quotients, so a formalization has to fix polynomial representatives and prove the two division identities rather than manipulate fractions. The alternating tail has an exponent that depends on both and the summation index through a truncated natural-number subtraction, which is the main source of friction: the parity rearrangement is valid only for and has to be justified in that form. Finally the positivity argument is a case split — the coefficient at is exactly , while every other coefficient is — and the degenerate small- cases must be excluded, which is why the goal carries .
Everything is stated in , i.e. Polynomial ℤ with X playing the role of ; no Grothendieck ring, no scheme theory, and no torification is formalized. The classes of equation (3.8) are defined to be the polynomial representatives above: the mission takes the closed formula of the source as given and proves the statements about it. This is the sense in which the goal is faithful to Lemma 3.9, and it should be read that way: it is a statement about the coefficients of an explicitly given polynomial, not a proof that is or is not an -variety.
Conventions fixed in Lean: the index ranges over ℕ and all subtractions in exponents (n - 1 - j, n - 2, n - 4) are truncated natural subtraction, which is harmless under the stated hypotheses (, resp. ) but is why those hypotheses appear; coefficients are read off with Polynomial.coeff, so the goal quantifies over all , including beyond the degree, where the coefficient is . The goal is not trivially true: for the sibling statement about exhibits a coefficient equal to in the same formalism, so the ambient set-up does admit negative coefficients.
Contributions welcome: direct proofs of the six statements; and, beyond this mission, formalizations of the other necessary-condition computations of the paper (the wheel and lemon-wedge families of section 3.6, the Chern-class condition of Lemma 6.3).