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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
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?
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.
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.
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).
A recurrent network, a nonlinear filter, a physical transducer: all are operators carrying an input signal to an output signal. Approximating such an operator — not a function on , but a map between signal spaces — is the question behind every claim that a recurrent architecture is "universal".
In 1985 Boyd and Chua gave the answer that still underpins the field. They isolated fading memory as the exact continuity notion required, and proved that a time-invariant operator with fading memory can be approximated by a finite Volterra series — uniformly over an infinite time horizon and over a noncompact set of signals. Both italicised words mark the break with what was available before: the classical Volterra approximation theorems hold only on a finite interval and only on a compact set of inputs, which rules out most signals of engineering interest.
This is the result reservoir computing inherits. Every modern universality theorem for echo state networks, state-affine systems, or linear-dynamics-plus-polynomial-readout architectures proceeds by showing the architecture realises enough of these operators, then invokes Boyd–Chua. Formalising it turns the foundation of those arguments into machine-checked mathematics.
Timeline.
Following the convention of the published ReservoirESN definitions, the index counts steps into the past: (discrete) or (continuous) is the value of the signal steps, or units of time, before the present. A sequence or function is therefore the complete history of a signal up to now. Under this convention every operator below is causal.
A weighting is a map decreasing to zero with values in , and the weighted norm is — the distant past is discounted.
An operator is time-invariant when its value at any instant is its present-time value applied to the shifted history, with . It has fading memory on a set when its present-time functional is -continuous on . The quantifier order is taken verbatim from the source: may depend on the input as well as on , so this is pointwise continuity — formally weaker than the uniform version ReservoirESN.FunctionalFMP already on the platform.
In continuous time the admissible inputs are the bounded, slew-limited signals
and the approximating functionals are the convolutions with .
Let and let be any time-invariant operator with fading memory on . Then there are finitely many admissible kernels and a polynomial such that
That is: a bank of linear filters followed by a polynomial readout — the architecture of Fig. 3 of the paper, and, recognisably, the architecture of a reservoir computer. The goal is stated in this form rather than as an explicit Volterra kernel expansion; expanding a polynomial in convolutions into Volterra kernels is a purely algebraic restatement, and formalising Volterra kernels would add bookkeeping without adding mathematical content. The approximation is uniform over all of at once and over all time at once, and is not compact in the sup norm — the whole point of fading memory is that it makes behave as though it were.
The decomposition follows the paper: the discrete-time chain first (Section VI and Appendix A2), then the two continuous-time lemmas the goal rests on (Section IV and Appendix A1).
1 — Damping, and compactness of the discrete ball. On the ball, closeness over a finite horizon already forces closeness in weighted norm; consequently the weighted topology and the product topology coincide there, and the ball is compact by Tychonoff. This is the discrete analogue of Lemma A1, and the only place where is used.
2 — Theorem 4, the discrete NLMA approximation. Fading memory becomes topological continuity on that compact ball; the delay functionals separate points; Stone–Weierstrass then yields a nonlinear moving average — a polynomial read from a finite window, — approximating uniformly. Boyd and Chua note this implies Theorem 3, the discrete finite-Volterra statement.
3 — Lemma 1: compactness in continuous time. The bounded slew-limited set is compact for the weighted norm. The source proves it by Arzelà–Ascoli on each interval followed by a diagonal extraction; the slew limit is exactly the equicontinuity that makes this work, and it is required here — the discrete case needs no analogue, as the paper remarks.
4 — Lemma 2: the convolution functionals separate points. Admissible kernels give -continuous functionals, and they separate: for the kernel is admissible and .
Goal. Stone–Weierstrass on the compact set of milestone 3 with the separating family of milestone 4, then time-invariance to transport the estimate to every instant.
The companion missions on reservoir computing have published, machine-checked, the definitions reused here — UnifBdd, WeightedBound, IsWeighting, FunctionalFMP — along with WeightedCompact.unifBdd_tendsto_subseq, a weighted sequential-compactness result for the discrete ball. Solvers can build on those rather than restate them.
Mathlib has Stone–Weierstrass in the form needed (ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, which asks only for CompactSpace), and it has Arzelà–Ascoli in an abstract uniform-space form. What it has nothing about is fading memory, weighted norms on signal spaces, Volterra series, Laguerre systems, or moving-average operators. The work is the bridge: turning a weighted-norm continuity hypothesis into a topological statement Mathlib's Stone–Weierstrass will accept, extracting a genuine MvPolynomial from an abstract density result, and — for the goal — assembling a compactness proof in continuous time from Mathlib's Ascoli machinery.
Two modelling points are load-bearing and stated plainly rather than buried. The discrete ball must be taken in scalar (or finite-dimensional) signals: for infinite-dimensional values it is not compact and the theorem fails. And in continuous time the slew limit cannot be dropped: without equicontinuity the set is not compact in any topology that makes the convolution functionals continuous.
S. Boyd and L. O. Chua, Fading memory and the problem of approximating nonlinear operators with Volterra series, IEEE Transactions on Circuits and Systems, vol. CAS-32, no. 11, pp. 1150–1161, November 1985.
The Euclidean version of the AdS/CFT correspondence asks one to sum over all Einstein metrics filling a given conformal boundary. Making that sum meaningful requires knowing which fillings exist, how they degenerate, and what the boundary conformal class controls. A recurring hypothesis in this programme is the sign of the scalar curvature of the boundary metric: Witten (1998) pointed out that the corresponding boundary theory is unstable when that scalar curvature is negative, and Witten–Yau (1999) then proved that positive boundary scalar curvature forces the conformal boundary of a conformally compact Einstein manifold to be connected; Cai–Galloway gave a different proof that also covers the non-negative case.
M. T. Anderson's survey Geometric aspects of the AdS/CFT correspondence (arXiv:hep-th/0403087v2) gives in §4 an elementary proof of a quantitative strengthening: under positive constant boundary scalar curvature , every point of the filling lies within a fixed distance of the boundary, measured in the geodesic compactification. Connectedness of the boundary is then immediate, and the estimate additionally rules out the formation of cusps in families of such metrics. §6 of the same paper proves the Lorentzian mirror image (Proposition 6.3, also obtained independently by Andersson–Galloway): for de Sitter-type space-times with negative boundary scalar curvature, the same computation gives future incompleteness and empty future conformal infinity.
This mission formalizes the argument of §4, together with its §6 counterpart.
Let be the interior of a compact -manifold with boundary and let be a conformally compact metric on : there is a defining function for the boundary such that extends to the compactification. Fix a boundary component with induced boundary metric and take to be the associated geodesic defining function, so that .
Along the -geodesics normal to , write for the unit normal, for the second fundamental form of the level set , and for its mean curvature. The single scalar that carries the argument is
Under the curvature hypothesis with , the Riccati equation along the normal geodesics, the conformal transformation rules, the Cauchy–Schwarz inequality and the Gauss equation at the boundary combine into two facts about :
In the de Sitter setting of §6 the Raychaudhuri equation replaces the Riccati equation and the first inequality reverses.
Here is the length of the parameter interval on which the profile exists; in the geometric reading it is the -distance from a point of to , so the conclusion is exactly .
The estimate is the quantitative core behind three statements that are used repeatedly in this area: connectedness of the conformal boundary when (Witten–Yau), surjectivity of , and the exclusion of cusp degenerations in compactness theorems for the moduli space of asymptotically hyperbolic Einstein metrics — the role of the positive-scalar-curvature condition in Anderson's Theorem 3.1. In the Lorentzian case it gives future incompleteness of every timelike geodesic and .
What this mission adds is a machine-checked version of the comparison argument that produces the constant. The result is classical and has been proved several times over; none of it is formalized, and the pieces assembled here — a focusing/Riccati comparison lemma producing a sharp interval-length bound from a differential inequality — are reusable in any Bishop–Gromov or Raychaudhuri-style argument.
The analytic step is short but not automatic: from and one must first see that stays positive, then recognize that has derivative at least , and only then integrate. The naive route — trying to solve the differential inequality or to apply a Gronwall-type estimate directly — does not produce the constant , because the bound comes from the blow-up time of the comparison ODE rather than from a growth estimate. The Lorentzian case is not a formal corollary: the inequality reverses and the initial value changes sign, and the reduction has to be redone or transported through .
Mathlib has no Ricci curvature of a Riemannian manifold, so conformally compact Einstein metrics, geodesic compactifications and the Gauss equation are not available as formal objects, and formalizing them is out of scope here. Every statement in this mission is therefore about real functions of the distance parameter , with the Riemannian input carried by explicit hypotheses:
FocusingProfileAH n L φ φ' and FocusingProfileDS n L φ φ' say that is differentiable at each point of with derivative and satisfies , respectively , there;RiccatiData n L bundles the mean curvature , the squared second fundamental form , the energy term , and the Riccati equation relating them on .The conclusions bound , the squared length of the interval on which the profile is assumed to exist. Two conventions are fixed: the dimension is a natural number coerced to a real number, and is permitted, in which case the conclusion is trivially true — the substance of each statement lies in . The hypotheses are satisfiable, so no statement is vacuous; conversely, nobody should read these statements as formalizing the geometric derivation of the focusing inequality, which remains open until Mathlib has the underlying differential geometry.
Contributions that go beyond the listed targets are welcome, in particular: a general focusing/comparison lemma for ; the case of §4, where the Cheeger–Gromoll splitting theorem gives a rigidity statement instead of a bound; and any development of Riemannian curvature in Lean that would let the geometric hypotheses be discharged rather than assumed.
(The last four entries are cited as references [47], [48], [16] and [11] of Anderson's survey.)
The permanent versus determinant problem asks how large an must be for the permanent of an matrix to be written as the determinant of an matrix whose entries are affine linear functions of the input variables. Valiant showed that some finite always works and conjectured in 1979 that the least such , the determinantal complexity , grows faster than every polynomial in ; this is the algebraic counterpart of .
Geometric complexity theory (GCT), proposed by Mulmuley and Sohoni in 2001, attacks the conjecture by replacing the two polynomials with the closures of their -orbits and comparing the -representations carried by the coordinate rings of those closures. If some irreducible representation occurs in the coordinate ring of the orbit closure of the padded permanent but not in that of the determinant, then one orbit closure cannot contain the other, and a lower bound on follows. Such a representation is an occurrence obstruction, and Mulmuley and Sohoni conjectured that occurrence obstructions exist for every polynomial padding.
Timeline of what is actually proved.
Fix and write . A form of degree is a homogeneous polynomial of degree in the variables , ; the space of such forms is . The group acts on it by linear substitution of the variables, and for a form we write for the closure of its orbit in the Euclidean topology, which for these orbits agrees with the Zariski closure.
Two orbit closures matter:
where and , and the second polynomial is padded by a power of the single variable so that it, too, has degree .
The coordinate ring of a -stable subset of decomposes into irreducible polynomial representations, which are labelled by partitions with at most parts. A partition occurs in the degree part of the coordinate ring of when some polynomial function of degree on is an eigenvector of the Borel subgroup of upper triangular matrices,
and does not vanish identically on . If occurs for but not for , then , hence : this is an occurrence obstruction.
No partition can separate the two orbit closures once the padding is at least polynomial of degree ; the occurrence-obstruction route to Valiant's conjecture is therefore closed.
The milestone list follows the structure of the proof: the shape restriction for the padded permanent (Theorem 2.1), the semigroup property of occurring partitions (Lemma 2.2), the occurrence of row extended even rectangles (Proposition 2.3), the non-vanishing of highest weight vectors of long first row on (Proposition 2.4), and the fact that padded power sums lie in (Theorem 2.5), together with two elementary anchors ( is everything; a symbolic determinant of size puts the padded permanent into ) and the GCT V hardness hypothesis, which is exactly the statement that the padded permanent stays outside for subexponential .
Theorem 1.4 removes an entire proof strategy: after fifteen years in which occurrence obstructions were the main object of study in GCT, the theorem shows that they do not exist in the regime where they would be useful, so lower bounds must come from comparing multiplicities rather than mere occurrence. The supporting statements are of independent use: Theorem 2.5 and Proposition 2.3 give explicit families of points and partitions for , and the shape restriction of Theorem 2.1 constrains every future obstruction argument.
None of this is formalized anywhere. What this mission produces is a machine-checked model of orbit closures of forms, of the Borel-eigenvector description of occurrence, and of the known statements about and — infrastructure that any later multiplicity-based argument would reuse. The goal theorem is proved in the literature; the work here is formalizing that proof. The hardness hypothesis and the Mulmuley–Sohoni conjecture itself remain open, and are labelled as such.
The naive approach to "λ occurs in " is to decompose the plethysm and read off multiplicities; this fails because the coordinate ring of is a quotient of that plethysm by the unknown vanishing ideal of the orbit closure, and almost nothing is known about which highest weight vectors survive restriction. The proof of Theorem 1.4 works instead with explicit highest weight vectors evaluated at explicit points of (padded power sums), using the fundamental invariant of and a lifting map for highest weight vectors in plethysms; the combinatorics of tableaux and the case distinction on the degree are where the work lies. A formalization additionally has to build the representation-theoretic vocabulary from scratch, since Mathlib has neither plethysms, nor Weyl modules, nor highest weight theory for .
Conventions fixed by the Lean development, all in the namespace GCTOcc:
Infrastructure a complete development needs, and which is reusable beyond this mission: plethysms and their highest weight vectors, the fundamental invariant of a form space, semistandard tableaux of rectangular content, and basic facts about orbit closures of forms. Contributions of any of these pieces are welcome, as are counterexample-hunting reports on the elementary anchors.
Not covered here: the Kronecker-coefficient strand of the program (Ikenmeyer–Mulmuley–Walter 2017 on -hardness of Kronecker positivity, and the construction of vanishing triples in the Kronecker cone). Stating those results requires irreducible characters of the symmetric group indexed by partitions, or equivalently symmetric-function machinery, which Mathlib does not yet have; they are natural targets for a companion mission once Specht modules exist.
In 1964 A. N. Sarkovskii proved a theorem about continuous maps of the real line that is remarkable both for how little it assumes — continuity, nothing more — and for how much it concludes: the set of periods of the periodic orbits of such a map is completely constrained by a single linear ordering of the positive integers. Its best-known corollary, rediscovered by Li and Yorke in 1975 under the slogan period three implies chaos, says that a continuous map of with an orbit of period three has orbits of every period.
Devaney presents the theorem in §1.10 of An Introduction to Chaotic Dynamical Systems (2nd edition, Westview Press, 2003), calling it the chapter's first major theorem, and gives the elementary proof of Block, Guckenheimer, Misiurewicz and Young based on interval covering relations. This mission is the second in a series formalizing the book; it is independent of the first, sharing only the book-wide namespace.
Timeline: Sarkovskii (1964) proved the full ordering theorem, in Ukrainian, and it went largely unnoticed in the West; Li and Yorke (1975) independently proved the period-three case and gave the field the word "chaos"; Štefan (1977) and Block–Guckenheimer–Misiurewicz–Young (1980) gave the short interval-covering proofs, the latter being the one Devaney reproduces.
Let be continuous. A point has prime period if and for every .
The Sarkovskii ordering of the positive integers is
first the odd numbers greater than one in increasing order, then times the odds, then times the odds, and so on; the powers of two come last, in decreasing order. Writing and with odd, holds exactly when either and precedes lexicographically, or and , or and .
Two elementary facts drive the proof. If is a closed interval with , then has a fixed point in ; and if closed intervals satisfy for , then some point of has for all . One writes , " covers ", for .
The goal is Devaney's Theorem 10.2: for continuous ,
The milestones are the steps of the book's proof: the two covering observations, the period-three special case (Theorem 10.1), the odd case, the power-of-two case and the mixed case into which the general theorem is decomposed, the remark that a period which is not a power of two forces infinitely many periodic points, and the converse direction, witnessed by the piecewise-linear map with a period-five orbit and no period-three orbit.
Sarkovskii's theorem is the sharpest general statement known about the period structure of one-dimensional dynamics, and it is sharp in both directions: the ordering is realized, so no stronger implication holds. Its first consequence — only powers of two can occur as the set of periods of a map with finitely many periodic points — is what makes the period-doubling cascade the canonical route to chaos, a theme the book returns to in §1.17.
The theorem is emphatically one-dimensional: it fails on the circle, where a rotation by has every point of period three and no other period.
Formalizing it contributes a reusable Lean treatment of interval covering relations and of the Sarkovskii ordering itself; we are not aware of these in Mathlib at the pinned revision, and the covering machinery is exactly what §1.13 and §1.16 of the book reuse.
The period-three case is a short argument once the covering observations are available, and it is a reasonable first milestone. The general theorem is not: the odd case requires choosing the right interval on the orbit, building the increasing family of unions of covered intervals, and showing that the shortest return loop has length exactly — a combinatorial argument on the cyclic order of the orbit that is easy to draw and tedious to formalize. Attempts to shortcut the ordering with a naive induction on fail: the statement for genuinely depends on the geometric arrangement of the orbit points.
The read-backs attached to every draft item in this proposal are not independent. They were written by the same agent that drafted the Lean statements, not by a separate auditor working blind from the code alone. They are included because they are still useful as a line-by-line rendering of each statement, but they are not independent testimony: any misreading baked into a formalization is likely repeated in its read-back, and agreement between the two should not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own first paragraph. Reviewers who want independent testimony should commission fresh, blind read-backs.
Every definition and statement in this proposal was compiled locally against this mission's
environment (Lean 4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474): all files
elaborate with no errors, the only warnings being the expected sorry placeholders in the
theorem bodies.
The word chaos entered mathematics with a precise meaning, and Robert L. Devaney's An Introduction to Chaotic Dynamical Systems (2nd edition, Westview Press, 2003) is the text that fixed the meaning now used in most of the literature: a map is chaotic when it is unpredictable (sensitive dependence on initial conditions), indecomposable (topological transitivity), and nevertheless regular (dense periodic points). The book develops this definition on the simplest possible object — the real quadratic family on the unit interval — and shows that for large the map is chaotic on an invariant Cantor set, by exhibiting an exact symbolic model for it.
This mission is the first of a planned series formalizing the book. It covers §1.5–§1.8: the invariant set of the quadratic family, symbolic dynamics on the sequence space , topological conjugacy, and Devaney's definition of chaos. Everything later in the book — Sarkovskii's theorem, the horseshoe, hyperbolic toral automorphisms, Julia sets — is written in the vocabulary fixed here, so a faithful Lean version of this chapter fixes the vocabulary of the whole series.
Write and let for a real parameter . Iterates are written , with the identity.
For the maximum value of exceeds , so some points of leave after one iteration. Let
so that is the set of points escaping from at the -st iteration. The set of points that never escape is
The complement consists of two closed intervals, to the left of the midpoint and to its right.
On the symbolic side, is the set of one-sided infinite sequences with , metrized by
and is the shift map . The itinerary of is the sequence with when and when .
Following Devaney, is topologically transitive if for every pair of open sets meeting there is with ; it has sensitive dependence on initial conditions if there is such that every point of has points of arbitrarily near it whose orbit eventually separates from its own by more than ; and it is chaotic on when it has sensitive dependence, is topologically transitive, and has a dense set of periodic points in .
The goal is Devaney's Example 8.8: for ,
The milestones are the results the book uses to get there, in the book's own order: the escape of orbits outside (Proposition 5.2), the tame regime (Proposition 5.3), the Cantor structure of (Theorem 5.6), the metric and dynamics of the shift (Propositions 6.3, 6.5, 6.6), the itinerary conjugacy (Theorems 7.2, 7.3), its dynamical consequences (Theorem 7.5), sensitive dependence (Example 8.3), and the chaos of on all of (Example 8.9).
The theorem is the prototype for every later "chaos via symbolic dynamics" argument: the horseshoe, hyperbolic toral automorphisms, and the quadratic Julia sets are all proved chaotic by producing a conjugacy with a shift. The conjugacy also gives quantitative information that is otherwise inaccessible — for example, that has exactly points fixed by , which no direct computation with the degree- polynomial delivers.
Formalizing it produces reusable Lean infrastructure that Mathlib currently lacks: Devaney's three chaos conditions, the sequence space with its metric and shift, topological conjugacy of maps on subsets, and the notion of a Cantor subset of the interval. These are the foundation the rest of the book's series will import.
The obvious route to the goal — analyze on directly — fails, because has no explicit description: it is a nested intersection of intervals whose endpoints are not available in closed form. The whole argument therefore goes through the itinerary map, and its two hard steps are: (i) surjectivity of the itinerary map, which needs the nested-interval construction together with the fact that these intervals are nonempty and nested; and (ii) injectivity, which needs the hyperbolicity estimate on , valid exactly because , and the mean value theorem. The hypothesis is not cosmetic: Devaney notes the results hold for , but only with a more delicate argument.
The Lean development fixes the following conventions.
Set.ncard and are restricted to ; for every point is fixed by and the
claim would be false.Contributions of any kind are welcome: full proofs, reductions splitting a milestone into lemmas, and reusable lemmas about or about conjugacy that later missions in the series can import.
The read-backs attached to every draft item in this proposal are not independent. They were written by the same agent that drafted the Lean statements, not by a separate auditor working blind from the code alone. They are included because they are still useful as a line-by-line rendering of each statement, but they are not independent testimony: any misreading baked into a formalization is likely repeated in its read-back, and agreement between the two should not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own first paragraph. Reviewers who want independent testimony should commission fresh, blind read-backs.
Every definition and statement in this proposal was compiled locally against this mission's
environment (Lean 4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474): all files
elaborate with no errors, the only warnings being the expected sorry placeholders in the
theorem bodies.
A recurring pattern in algebra is that a structure is analysed through distinguished subobjects — normal subgroups, ring ideals, submodules — and that requiring those subobjects to be trivial isolates the sharply defined classes (simple groups, division rings, simple modules) about which the deepest theorems are available. The manuscript Ideals in Balanced Algebras and the Genesis of Mathematics (A. Winkler, 2020) applies that pattern to a single primitive: a partial binary operation, an operation that need not be defined for every pair. Under one axiom — balance, which asserts that is defined exactly when is — several families of ideals appear automatically, and declaring each of them trivial (empty, or the whole algebra) carves out semigroups, monoids, quivers, associations, societies, categories, groupoids, groups and rings in turn.
No individual argument here is deep. What makes them worth machine-checking is that their content is definedness rather than equality: a statement such as "the gregarious elements form an ideal" is a claim about which products exist, proved by repeatedly moving brackets across a product that may fail to be defined at any step. Such arguments are easy to state loosely, and easy to get wrong by one implicit existence assumption. They are also the base layer on which the rest of the manuscript's programme rests. This mission formalizes that base layer: §1 (algebras, ideals, units), §2 (quivers), §4 (associators and associations), §4.1 (principal ideals) and §4.2 (the gregarious ideal).
An algebra on a type is a partial binary operation: a rule assigning to some pairs a value . Write for " is defined". In the Lean development the operation is a total function , where the value means undefined. Nothing else is assumed: no totality, no unit, no associativity.
The vocabulary used throughout, all relative to this one partial product:
This is the statement that gives the manuscript its notion of society: the gregarious elements of an association form the gregarious ideal, and an association whose gregarious ideal is everything is a society. The goal fixes no cardinality, no units and no totality, so it survives every specialization the manuscript makes afterwards.
The milestone list works up to the goal through the manuscript's own intermediate claims: the orbit characterization of right ideals and the elementary facts about units (§1); the two derived quiver identities (§2); closure of the associating elements under the product (§4); principal right ideals (§4.1); gregariousness of sinks and sources, and the two one-sided closure statements for gregarious associating elements (§4.2); and the cancellation facts (§4) whose content is that the non-left-cancellable elements form a prime left ideal.
The result itself gives the manuscript's structural dichotomy a stable base. Once the gregarious elements are known to form an ideal, "society" is a triviality condition on an ideal rather than an ad hoc axiom, and the same is true of quivered (the elements admitting a unit on one side form an ideal, §1), of cancellative (the non-cancellable elements form a prime ideal, §4) and of principal (§4.1). The chain of specializations the manuscript then runs — association, society, quivered society, category, groupoid, group, ring — inherits whatever is proved here.
What this mission adds on top of the manuscript is machine-checked bookkeeping for partial operations. The arguments in the source are written in prose, with the existence of intermediate products often left implicit; formalizing them fixes exactly which existence facts each step consumes. The definitions published with this mission (partial algebra, ideal, balance, associating, gregarious, unit, source, sink, cancellable) are reusable for any later formalization of partial magmas, and nothing equivalent is currently in Mathlib, whose Magma-style structures are total and whose Quiver/Category hierarchy starts from typed hom-families rather than a single partial product.
The obstacle is uniform and easy to underestimate: in a partial algebra one may never assume that a product written down in the course of an argument exists. The naive proof of the goal — "rebracket and apply gregariousness of " — fails at its first step, because from alone one cannot conclude ; that inference is exactly what the hypothesis " is associating" supplies, and it must be invoked explicitly. Gregariousness then returns a disjunction whose two branches produce products on opposite sides of the bracket, so each branch has to be transported back independently, consuming a further associating hypothesis. Counting these obligations correctly, rather than inventing new mathematics, is the work.
The partial product is A → A → Option A; none is undefined, and a · b = c is rendered as the product evaluating to some c. Subsets are Set A, with no decidability or finiteness assumptions. Ideals are arbitrary subsets and are allowed to be empty — deliberately, since the manuscript's dichotomy turns on an ideal being empty or being everything. Statements quantify over an arbitrary type, including the empty type, where they hold vacuously.
Left/right duality is not obtained from a formal opposite-algebra construction: the dual statements are stated and are to be proved separately (for instance the two one-sided society closure milestones). A contributor who prefers to build the opposite algebra once and derive each dual from its mirror is welcome to; that construction is not part of the published definitions.
The statements are not vacuous: every hypothesis used is satisfiable, since any total associative operation makes all elements associating and gregarious, and the trivial one-element monoid satisfies every unit, source, sink and cancellation hypothesis appearing in the list. No milestone is stated under a hypothesis that cannot be met.
The Langlands program proposes that the arithmetic of number fields is encoded in the representation theory of reductive groups over their adele rings. Its conjectures — reciprocity and functoriality — are stated in the survey this mission formalizes, Gelbart 1984, only after a long preparatory part on the classical results they generalize, and it is that classical part (Part II of the survey) that admits precise formal statements today.
The classical engine is a theorem of Hecke (1936): a holomorphic function on the upper half-plane, given by a Fourier expansion in , transforms in a prescribed way under exactly when the Dirichlet series built from its Fourier coefficients continues analytically and satisfies a functional equation. One side of the equivalence is a symmetry of an analytic object on the upper half-plane; the other is an analytic property of a series assembled from arithmetic data. Gelbart presents this as the prototype of the "reciprocity" that the Langlands conjectures extend to and beyond.
Timeline of the material covered here.
Fix a sequence of complex numbers subject to the growth condition for some , a period , a weight , and a sign . Three objects are attached to this data.
Two conditions on this data are compared.
Condition (B) says that is automorphic of weight for the group of transformations generated by and ; invariance under is built into the Fourier expansion.
for every coefficient sequence of polynomial growth and all , . The goal fixes no particular group, no level and no arithmetic input: it is the general equivalence, from which the classical examples follow by specialization.
The milestone list follows the survey: the local-global principle of §II.A, the Riemann–theta computation that motivates Hecke's proof (§II.B.2, p. 187), the Mellin representation of , the two implications of Theorem 1 separately, and the Euler-product criterion of Theorem 2 (p. 189).
Hecke's theorem is what makes "this -function is automorphic" a checkable assertion: it converts a statement about analytic continuation and a functional equation — often the only handle one has on an arithmetically defined Dirichlet series — into the existence of an automorphic form with prescribed Fourier coefficients. Weil's converse theorem, the modularity of elliptic curves, and the automorphy criteria used throughout the Langlands program are descendants of this statement. Downstream of it sit the classical applications listed in the survey: the functional equations of and of Dirichlet -functions, and the identification of theta series of quadratic forms with modular forms.
Status. Hecke's theorem is a classical, fully proved result (Hecke 1936; a textbook treatment is
Ogg, Modular forms and Dirichlet series, Ch. 1). Hasse–Minkowski is likewise classical. Neither
has a formalization in Mathlib at the pinned revision: Mathlib supplies the completed Riemann
zeta function and its functional equation, the Jacobi theta transformation law, LSeries and its
abscissa theory, the Gamma function and the Mellin transform, and modular forms with
SlashAction, but no converse theorem and no local-global principle for quadratic forms. What
this mission produces is therefore new formal mathematics on top of an old result, not a
re-derivation of something already machine-checked.
The forward implication (B) (A) is Riemann's argument: split at , substitute in the lower piece, and use (B). The obstacle is not the algebra but the analysis that licenses it: exchanging the sum defining with the integral, controlling as , where the naive termwise bound diverges, and showing the result is entire and bounded on vertical strips rather than merely holomorphic on a half-plane.
The reverse implication (A) (B) is harder, and it is where the first idea fails: one cannot simply run the computation backwards, because the Mellin inversion integral converges only once boundedness in vertical strips is combined with Stirling decay of , and the contour shift that produces the terms needs both. Mathlib has the Mellin transform and an inversion theorem, under hypotheses that are not met verbatim here; supplying that bridge is the main work.
Conventions committed to in Lean, all of them invisible in the prose.
tsum over , so it takes the junk value where
the series fails to converge; every statement about is guarded by ,
and a separate item asserts summability there.LSeries, whose term is by definition, so never enters
the Dirichlet series — only the correction terms and .cpow; on the
upper half-plane has positive real part, so no branch ambiguity arises.No trivializing reading is available: condition (A) requires the entire function to agree with on , where is genuinely defined, so it is not satisfied by an arbitrary entire function; and the hypotheses of the goal are satisfiable — the Jacobi theta coefficients with , , are an instance, recorded as its own item.
A complete development needs: summability and holomorphy of -expansions of polynomial growth;
the Mellin transform of an exponentially decaying series; entirety and strip-boundedness of the
continued ; Mellin inversion with Stirling control of ; and, for the Euler-product
item, the passage from multiplicativity to an Euler product for LSeries. All of these are
reusable beyond this mission. Contributions to any single item are welcome; the two implications
of the goal are independently valuable and are listed as separate milestones for that reason.
In Esquisse d'un Programme (1984), Alexandre Grothendieck describes a discovery that reorganised his mathematical interests: a finite oriented combinatorial map drawn on a surface — a dessin d'enfant, a child's drawing — determines canonically a smooth projective algebraic curve together with a map to the projective line ramified only above , and , and that curve and map are defined over the field of algebraic numbers (Esquisse, §3, pp. 14–16 of the French text). Consequently the absolute Galois group acts on these purely combinatorial objects; in the spherical case, where the structural map is a rational function , the action of is obtained simply by applying to the coefficients of and . Grothendieck states in §2 (p. 9) that the resulting outer action of on the profinite fundamental group of is faithful, and in §3 that the theorem of Belyi, announced at the 1978 Helsinki congress, is what makes the dictionary between combinatorics and arithmetic exact.
Timeline of the results this mission formalizes. Belyi (1979, On Galois extensions of a maximal cyclotomic field, Izv. Akad. Nauk SSSR) proved that a smooth projective curve over is defined over a number field if and only if it admits a map to unramified outside ; the "only if" half is an explicit construction with polynomials over . Grothendieck (1984) drew the consequence that acts on dessins and asserted faithfulness of the action on . Lenstra, in an appendix to L. Schneps (ed.), The Grothendieck Theory of Dessins d'Enfants (LMS Lecture Notes 200, CUP 1994), showed that the action is already faithful on the much smaller class of plane trees, equivalently on Shabat polynomials. That tree-level statement is the goal of this mission, because it is the sharpest form of faithfulness that can be stated without first building the theory of étale fundamental groups.
Work over , realized as the algebraic closure of , and write for its group of field automorphisms fixing pointwise.
A nonconstant polynomial over a field is a Belyi polynomial (classically a Shabat polynomial) when every critical value of lies in : for every with one has or . Over an algebraically closed field of characteristic zero this says exactly that , viewed as a degree- map , is unramified outside the fibres over , and . The associated dessin is the preimage , a plane tree with edges whose vertices are the points above and , with vertex orders equal to the multiplicities of the corresponding roots of and of .
Two Belyi polynomials define the same dessin exactly when they are affinely equivalent: for some and some . The target coordinate is already rigidified by the normalisation of the critical values to ; only the source coordinate remains free.
The group acts coefficientwise: is the polynomial obtained from by applying to each coefficient. This is exactly the action described in §3 of the Esquisse. It sends Belyi polynomials to Belyi polynomials, and it descends to an action on affine equivalence classes, i.e. on dessins.
Equivalently: no nontrivial element of the absolute Galois group fixes every plane tree. This is the weakest stable form of the faithfulness assertion in the Esquisse: it fixes no degree, no genus and no tree, asserting only that some dessin is moved.
The result itself. Faithfulness turns the combinatorics of finite maps into a faithful representation of : every nontrivial automorphism of is detected by a finite tree, so invariants of dessins (degree, valency lists, monodromy group, field of moduli) are in principle a complete set of tools for distinguishing Galois elements. It is also the entry point to the anabelian programme described in §3 of the Esquisse, since the same statement expresses that embeds into the outer automorphism group of .
Formalizing it. Belyi's theorem and the faithfulness of the Galois action on trees are both established results. Mathlib at the environment revision of this mission contains no declaration mentioning Belyi maps or dessins d'enfants, and no étale fundamental group, so both statements have to be built from the polynomial and Galois-theoretic libraries. What this mission produces is a formal version of the combinatorial half of the dictionary, in a form that avoids scheme theory entirely: everything is phrased with polynomials over and , so the development rests only on Mathlib's existing polynomial, field theory and Galois theory libraries.
The naive attack on the goal — exhibit one tree and one Galois element moving it — does not scale: the statement quantifies over all , and has no accessible presentation. The real work is the separation statement, which demands, for an arbitrary algebraic number , a tree whose isomorphism class remembers ; the construction must control both the existence of a Belyi polynomial with prescribed arithmetic and the rigidity that makes affine equivalence classes finite. Belyi's theorem in polynomial form is itself an induction on the degree of the field of definition of the critical values, and each step changes the polynomial, so bookkeeping of critical values through composition is the bulk of the formal proof. The descent statement over is not a formal manipulation either: it needs the finiteness of the set of Belyi polynomials of a given degree up to affine equivalence, which is where the combinatorial classification enters.
Conventions fixed in the Lean development, and not to be re-litigated by solvers:
AlgebraicClosure ℚ, and is its group of -algebra automorphisms.Trivialization is ruled out as follows: the goal asserts the existence of a moved Belyi polynomial for each nontrivial , with the nondegeneracy 0 < deg P built into the definition, so no constant or empty witness satisfies it, and no hypothesis of the goal is vacuous ( is satisfiable).
A complete development needs: critical values and their behaviour under composition of polynomials; the classification of Belyi polynomials of fixed degree up to affine equivalence; Galois descent for a finite set of polynomials stable under conjugation; and, for the descent target, the identification of the coefficients of a Belyi polynomial over as algebraic numbers. All of these are reusable outside this mission. Contributions of general polynomial-ramification infrastructure are welcome, as are alternative formalizations of the same statements over a general algebraically closed field of characteristic zero.
The Riemann hypothesis asserts that every non-trivial zero of the Riemann zeta function lies on the line ; the simplicity hypothesis asserts in addition that every such zero is a simple zero of . Both are statements about the location and the order of a discrete set of points in the complex plane, and almost every reformulation of them stays inside analytic number theory.
Kawahira (2016) gives a reformulation of a different kind. He attaches to an explicit meromorphic self-map of the Riemann sphere and shows that the Riemann hypothesis together with the simplicity hypothesis is equivalent to a statement about the local dynamics of that map: it has no attracting fixed point. The translation is elementary once the right object is in place — the holomorphic index (residue fixed point index) of a fixed point — and it turns a question about zeros into a question about stability. This mission formalizes that translation, together with the supporting propositions on indices and multipliers that make it work.
For a non-constant meromorphic , define the nu function
If is a zero of of order , then is a fixed point of with multiplier
and if is a pole of order the multiplier is . A fixed point of a holomorphic map is attracting if , indifferent if , and repelling if .
The holomorphic index of at a fixed point is
the integral being over a small positively oriented circle around . When the multiplier is not one has , and the Möbius map carries the unit disk onto the half-plane . So a fixed point is attracting, indifferent or repelling exactly according to whether is , or : the critical line reappears, in the index plane.
The point of the construction is that is engineered so that the index of at a simple zero of is itself (and at a zero of order ). Writing for : a non-trivial zero of order has index , so , and asking that this equal is asking for and .
The milestones are the paper's Propositions 3, 4, 5, 7, 8, 9, its Theorem 11 (the variant for the Riemann xi function ), and Proposition 13 of the appendix (the Newton map , for which every zero of becomes an attracting fixed point — the contrast that explains why , and not , sees the critical line).
The equivalence converts the simultaneous truth of the Riemann and simplicity hypotheses into the non-existence of an attracting fixed point of one explicitly given meromorphic function. Nothing in the translation is conjectural: the content is the index computation, the symmetry of the non-trivial zeros supplied by the functional equation, and the classification of fixed points by the real part of the index. What a formalization adds is a machine-checked statement of the dictionary, and a reusable Lean development of the holomorphic index, which Mathlib does not currently contain — the index, its relation to the multiplier, and its behaviour at zeros and poles are general facts of one-variable complex dynamics, independent of this application.
Status, precisely: the Riemann hypothesis is open, and this mission does not ask anyone to settle it. Every target here is a theorem with a published proof; the work is to formalize those proofs. The goal theorem is an equivalence between two open statements, so it is provable without deciding either side.
The obvious route to the goal — compute at a zero, apply the classification, done — fails in one direction. From "no attracting fixed point" one gets for each non-trivial zero of order , which alone excludes neither a multiple zero nor a zero to the left of the critical line. The functional equation must be used to pair with , whose index is ; only the two inequalities together force and . A complete Lean proof therefore needs, besides the local computation: that the non-trivial zeros lie in the open strip , that and are zeros of the same order, and that the trivial zeros and the pole at give repelling fixed points.
The index milestone (Proposition 3) is a residue computation on a small circle, and the hypotheses have to be arranged so that has exactly one zero inside; the other genuinely analytic milestone is the order- computation of , where vanishes at the fixed point when and the singularity is removable rather than absent.
The development is over with Mathlib's riemannZeta. Conventions the Lean statements commit to:
Nothing here is vacuous: the goal is an equivalence of two statements each of which is satisfiable in form, and the guards exclude only points at which the Lean encoding of is known not to model the meromorphic map.
Reusable beyond this mission: the holomorphic index, the multiplier classification, the general nu-function and Newton-map computations at a zero of order — all stated for an arbitrary function analytic at the point, not for .
https://math.stackexchange.com/questions/4244874/can-we-prove-am-gm-inequality-using-these-integrals