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.
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?
In stochastic linear optimization under bandit feedback a learner repeatedly chooses a decision from a fixed set and observes only the noisy cost of that one decision, whose expectation is a fixed but unknown linear function . The model covers online routing, ad and product selection with feature vectors, and any sequential decision problem whose decision set is too large to enumerate but whose expected cost is linear in a known representation. The multi-armed bandit is the special case where is the set of standard basis vectors.
Dani, Hayes and Kakade (COLT 2008) analysed the algorithm ConfidenceBall₂, a generalization of Auer's LinRel (JMLR 2002), and proved that its regret is with high probability for an arbitrary compact decision set, and that this is optimal up to logarithmic factors. Their confidence-ellipsoid construction became the template for later linear bandit algorithms (OFUL, LinUCB), and the ellipsoid-plus-potential analysis is the standard argument of the field (Lattimore and Szepesvári, Bandit Algorithms, Chapters 19–20).
Timeline: Auer (2002) introduced LinRel for finite decision sets; Dani, Hayes and Kakade (2008) extended it to arbitrary compact sets with the bound and a matching lower bound; Rusmevichientong and Tsitsiklis (Math. Oper. Res. 2010) studied linearly parameterized bandits with dimension-dependent regret bounds; Abbasi-Yadkori, Pál and Szepesvári (NeurIPS 2011) sharpened the confidence ellipsoids with self-normalized martingale bounds.
Fix and a compact decision set whose standard basis is a barycentric spanner: each and every lies in the cube . The paper's Section 5 adopts these coordinates without loss of generality. An unknown vector satisfies for , and minimises .
On round the learner plays , measurable with respect to the information before round , and observes a loss with . The regret after rounds is
ConfidenceBall₂ maintains the design matrix , the least-squares estimate , the radius
and the confidence ellipsoid . It plays the optimistic decision . The analysis uses the width , the error , and the noise .
For with and noise ,
A single event covers every horizon, so the bound is anytime.
The result gives a regret bound for linear bandits over an arbitrary compact decision set that depends on the dimension rather than on , holds uniformly over horizons, and requires no gap between the best and second-best decision. With the paper's lower bound it shows that the price of bandit feedback, compared with full information, is a factor . The two components, a confidence theorem for a least-squares ellipsoid under martingale noise and a deterministic potential argument on , are reused in the analysis of most optimistic linear and generalized-linear bandit algorithms.
The theorem has a published proof but, to our knowledge, no machine-checked one. The platform already has the elliptical potential lemma (BanditAlgorithm.elliptical_potential_lemma, Lattimore–Szepesvári Lemma 19.4), the matrix determinant lemma and the Woodbury identity, which cover the linear-algebra layer; the LinUCB regret theorem there (BanditAlgorithm.linear_bandit_linucb_regret_bound) is pathwise given confidence, for a different algorithm, so the probabilistic half is new. Formalization also settles the printed constants, three of which need correction (below).
The deterministic half is linear algebra. The difficulty is the confidence theorem. Hoeffding–Azuma applied to would need a deterministic step bound, and the natural one gives only a regret. The step sizes of are bounded in terms of the random widths , so the argument must control the conditional variances pathwise and apply Freedman's inequality, whose event is random. The escape indicator , which switches the martingale off after the first failure of confidence, is what makes the variance bound hold on every path, and the induction that turns Lemma 14 into Theorem 5 must be carried out on a single event for all simultaneously. Freedman's inequality itself is not in Mathlib.
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, rounds are indexed in ℕ. The spanner is the standard basis, as in Section 5 of the paper (the algorithm is equivariant under the linear change of coordinates). The probability model is a probability space with a general filtration ; is -measurable and is -measurable. The argmin is encoded as a joint minimiser over , which admits every tie-break and is required on every outcome; measurability of is a hypothesis, not derived from the selection. The optimum is a hypothesis (, minimising), not an sInf.
Corrections of the printed statements, each labelled in the item's Formalization Note:
A regret bound for an arbitrary decision sequence under the assumption for all is Theorem 6, not the goal; the goal carries the ConfidenceBall₂ selection rule, the conditional-mean and measurability hypotheses, and as the algorithm's own parameter. The hypotheses are jointly satisfiable, for example by a finite with a fixed tie-break and i.i.d. costs in .
Needed infrastructure: Freedman's inequality for a filtration (reusable across all of bandit theory), the potential lemma (available), and measurability of the algorithm's statistics. Contributions of alternative proofs of Theorem 5, for example via self-normalized bounds, are welcome.
In many operational problems (shortest paths, assignment, planning) the decision solves a linear program whose cost vector is unknown at decision time and is predicted from contextual features. The predict-then-optimize pipeline fits a model that maps a feature vector to a predicted cost vector , and then acts on the decision that is optimal for . Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed to measure the quality of such a model not by the prediction error but by the SPO loss (Smart Predict-then-Optimize loss): the excess true cost of the decision induced by the prediction over the best decision in hindsight.
The question is whether a small SPO loss on the training sample implies a small SPO loss on new data, uniformly over the models a training procedure may return. The SPO loss is neither convex nor continuous in the prediction, so the standard Lipschitz-based bounds for regression do not apply. El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3, Mathematics of Operations Research 2023; a preliminary version appeared at NeurIPS 2019) give the first such generalization bounds. This mission formalizes their first one, for polyhedral feasible regions, which treats every vertex of the feasible region as a class label of a multiclass classification problem. The bound has since been used by later work, e.g. Hu, Kallus and Mao (Fast rates for contextual linear optimization, Management Science 2022), who sharpen it by a factor (as noted on p. 4 of the paper).
A feasible region is nonempty, compact and convex. For a cost vector the nominal problem is . An optimization oracle is a fixed map with for every ; nothing is assumed about how it breaks ties. The SPO loss of a prediction when the realized cost is is
The linear optimization gap is , and for a set of cost vectors ; the SPO loss of a cost in lies in .
Data are pairs drawn from a distribution on . A hypothesis class is a family of predictors . The SPO risk is , and on an i.i.d. sample the empirical SPO risk is . The empirical Rademacher complexity with respect to the SPO loss is
with independent uniform signs , and is its expectation over the sample.
The decisions induced by form the class . A class N-shatters a finite set if there are two labelings that differ at every point of such that every mixture of them (follow on a subset , on the rest) is realized by some member of . The Natarajan dimension is the largest size of an N-shattered set. When is a polyhedron, denotes its finite set of extreme points.
For a polyhedral and every , with probability at least over an i.i.d. sample of size , every satisfies
UnderstandingML.natarajan_lemma): a class from an -point set to labels with Natarajan dimension has at most members.The bound controls the out-of-sample decision cost of every predictor in the class, not only of an empirical risk minimizer, so it applies to any training procedure (SPO+ surrogate minimization, decision trees, heuristics) that returns a member of . Its dependence on the feasible region is only through and : the number of vertices of a combinatorial polytope is typically exponential in , and enters only logarithmically. For linear predictors the paper's Corollary 2 bounds by , giving a rate of order .
The results are proved in the paper; this mission formalizes them. No statement about predict-then-optimize or the SPO loss is known to have a machine-checked proof. The platform already has the Natarajan lemma (proved) and several Massart-type lemmas for generic classes; this mission connects that multiclass machinery to decision losses, and its Theorem 1 is a reusable Rademacher generalization bound for a loss with range .
The obvious route through Lipschitz contraction fails: the SPO loss jumps when the prediction crosses a point where the optimum is not unique, so the Rademacher complexity of the composed class cannot be bounded by that of times a Lipschitz constant. Any argument through the finitely many vertices of needs the decisions to take finitely many values on a sample, i.e. the oracle to return vertices; for an oracle that returns a non-vertex optimal point under ties, may take infinitely many values on a sample. On the probabilistic side, the passage from the empirical to the expected complexity and the McDiarmid concentration step (Theorem 1) require the suprema over an uncountable class to be measurable, which the paper does not discuss.
Lean works in = EuclideanSpace ℝ (Fin d); cost vectors and decisions live in the same space and is the inner product. The standing assumptions of §2 are hypotheses of every theorem: nonempty, compact and convex; an arbitrary oracle (a hypothesis IsOracle S w, never a specific selection); nonempty and bounded, with the cost component of in almost surely (or, for fixed-sample statements, every ); . "Polyhedron" means the solution set of finitely many linear inequalities; with compactness it is a polytope, and is the cardinality of Set.extremePoints ℝ S. The expectation over signs is the exact average over the sign vectors; and are Bochner integrals. "With probability at least " is stated as: the product measure of the set of samples on which some violates the bound is at most .
The formalization commits to the following disclosed additions:
A formalization that let be an sSup in , or chose a specific tie-breaking oracle inside the definitions, would prove a different and in part trivial statement; both are excluded.
Infrastructure needed: McDiarmid's bounded-differences inequality and symmetrization for the product measure; Massart's finite-class lemma (a proved version is on the platform as RademacherMassart.rad_le_massart, with its own normalization); the Natarajan lemma (proved, UnderstandingML.natarajan_lemma, stated with its own but identical notion of N-shattering over finite types); finiteness and nonemptiness of the extreme points of a nonempty polytope. Theorem 1 and the Massart step do not use polyhedrality and are reusable for any bounded decision loss. Contributions of these infrastructure lemmas are welcome.
The uncapacitated facility location (UFL) problem is one of the basic models of location theory and operations research: a firm chooses which warehouses, plants or servers to open, paying a fixed cost for each open site and a service cost for every client according to its distance to the nearest open site. It is also a standard test case for approximation algorithms.
Local search is the simplest of these and the one most used in practice: start from any set of open facilities and repeatedly add, drop or exchange one facility while this lowers the cost. The question is how bad a solution can be when no such move helps. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) answered it for UFL with an exact constant.
Timeline. Korupolu, Plaxton and Rajaraman (SODA 1998, J. Algorithms 2000) analysed local search with add, drop and swap moves and proved a locality gap of at most 5; their analysis contains the service cost bound restated here as Lemma 4.1. Charikar and Guha (FOCS 1999) proved a locality gap of 3 for a different local search, in which one facility is added and any number are dropped. Arya et al. (STOC 2001; journal version 2004) proved that the add/drop/swap neighbourhood itself has locality gap at most 3, and gave an instance showing that 3 cannot be improved (§4.3).
A metric instance consists of a finite set of clients, a finite set of facilities, and a distance on that is nonnegative, symmetric and satisfies the triangle inequality. The cost of serving client by facility is ; the distance between two facilities is also available. Each facility has an opening cost .
A solution is a nonempty set of open facilities. Every client is served by its nearest open facility, so
The neighbourhood of is the set of solutions reachable by adding one facility, dropping one facility, or swapping one open facility for another:
is locally optimum if for every . The locality gap is the supremum, over all instances, of the ratio between the cost of a worst local optimum and the cost of a global optimum.
The proofs use the following notation, which appears in the milestones but not in the goal. Fix a second solution and nearest-facility assignments , ; write , , , and . A facility captures if ; is good if it captures no facility of and bad otherwise. The proof of the facility cost bound uses a permutation of the clients that maps each onto itself, moves every client of a non-capturing block out of that block (Property 3.1), and fixes every client of a capturing block that it would map into the same block.
This is the locality gap bound of Theorem 4.3 (p. 557) in its strongest printed form: is any solution, not only an optimal one.
A companion item, not a milestone, states the bound in the proof of Theorem 4.4 with : a local optimum of the instance with facility costs costs at most in the original instance.
The result. Theorem 4.3 shows that the simplest local search for metric UFL is within a factor 3 of optimal at every local optimum, with no LP and no rounding, and the tight example of §4.3 shows the analysis cannot be improved for this neighbourhood. Because Lemmas 4.1 and 4.2 hold against every solution , scaling the facility costs before running local search trades the two bounds against each other and gives the guarantee of Theorem 4.4. The same capture-and-reassign technique is used for k-median (§3) and capacitated facility location (§5).
Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of any locality gap bound for facility location is known to this mission. A formal development would check the reassignment arguments, which are stated case by case in the paper, and would produce reusable Lean infrastructure for metric facility location instances, nearest-facility costs and neighbourhood-based local optimality.
The service cost bound is routine; the facility cost bound is where the work lies. The natural first idea, closing a facility and sending each of its clients to the facility of nearest to that client's optimal facility, fails when serves most of the clients of some : the nearest facility of to may be itself, so the client has nowhere to go. The proof separates good facilities, which can be dropped, from bad ones, which must be swapped with a captured facility, and pays for the clients that cannot be moved through the distance between and its nearest captured facility. The combinatorial core is the construction of a permutation within each that avoids every non-capturing block and has fixed points only where they are unavoidable.
Clients and facilities are finite types Cl and Fa. The distance is a real-valued function on Cl ⊕ Fa that is nonnegative, symmetric and satisfies the triangle inequality; is not assumed, since the paper neither states nor uses it. Opening costs are a function f : Fa → ℝ with 0 ≤ f i, and demands are unit, as in the paper.
Solutions are nonempty Finsets. The service cost is (Finset.inf') and is defined only for nonempty sets, so no junk value for enters. Accordingly the drop move is considered only when a facility remains open; with at least one client, cannot serve anyone and is not a solution. Local optimality is required for all moves of : every added facility, every dropped facility and every swap, not only the moves used in the proof. The goal is stated as the multiplied-out inequality for every nonempty , never as a ratio, since may be .
In the milestones, the nearest-facility assignments , are arbitrary among the nearest ones (ties broken arbitrarily), and the family of bijections is a single permutation of the clients with . Inequality (5) assumes at least one client, which the paper assumes implicitly: with no clients and it would read . The goal and Lemma 4.2 need no such assumption.
A statement that assumes local optimality only for the moves the proof uses, that fixes to be a global optimum defined by hypotheses, or that allows the empty set a zero service cost would be a different theorem; none of these is used.
Needed infrastructure: sums over nearest-facility assignments and their fibers , the permutation , and bookkeeping of the three kinds of moves. The instance, cost and local optimality definitions are reusable for other local search analyses of metric location problems. Proofs of any milestone are welcome, as are alternative proofs of the goal.
Rotations of three-dimensional space are the most frequently used nontrivial Lie group in physics. Quantum mechanics requires more than the rotation group itself: particles of half-integer spin, such as the electron, transform under a group in which a rotation by acts as . That group is , the double covering group of . W. Siegel's graduate text Fields (arXiv:hep-th/9912205) introduces spin through this covering in Chapter II, Section A ("Two components", pp. 110–116). It encodes a 3-vector as a traceless hermitian matrix, reads the dot and cross products off the matrix product, and realizes rotations as conjugation by unitary matrices.
This mission is the first in a series formalizing results from Fields. It covers the algebra of §IIA1–IIA3, which ends with the statement that the map is two-to-one.
Let be the complex matrices, the conjugate transpose, the transpose and the entrywise complex conjugate.
In the Lean development these are SiegelFields.IsThreeVector, vecToMatrix, basisMatrix, matC and rotationOf. Components are indexed by .
Concretely: for all ; ; every element of is some ; and exactly when or .
The covering is the basic reason spinors exist. It gives the spin- representation, explains why a rotation acts as on fermions, and is the first instance of the low-dimensional Lie algebra identifications that Siegel lists in §IC5 (such as and ). Later chapters of Fields build spinor index notation, the Lorentz group and supersymmetry on this material.
The mathematics is classical and fully proved. What this mission adds is a machine-checked version stated in the book's own conventions: its basis, its normalization of the norm () and its matrix . The result is a dictionary between Siegel's matrix notation and Mathlib's matrix groups that later missions in the series can import.
Most milestones are identities about matrices and can be checked entrywise. The substantive parts of the goal are surjectivity onto and the kernel computation. Showing that every rotation is some requires constructing from , for example from an axis and an angle or by generating from simpler rotations. It cannot be done by an entrywise identity. Pinning the kernel to requires showing that a unitary matrix commuting with all of is scalar, and then combining this with . Showing rather than needs either a connectedness argument or an explicit formula.
Matrix.specialUnitaryGroup (Fin 2) ℂ and is Matrix.specialOrthogonalGroup (Fin 3) ℝ. Unitary matrices are Matrix.unitaryGroup (Fin 2) ℂ.rotationOf U is defined for every matrix and takes the real part of a trace. The statements restrict to the unitary or special unitary group, where that trace is real.crossProduct on Fin 3 → ℝ. The book's basis corresponds to the cyclically relabelled Pauli matrices , which preserves orientation.Contributions welcome: proofs of the matrix identities, a proof of surjectivity, and connections to Mathlib's quaternion and unit-sphere API.
The MDL and Occam principles of Chapter 7 rank hypotheses by description length and pay for a hypothesis according to its rank. Chapter 31 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), generalizes this to the PAC-Bayesian approach of McAllester: prior knowledge is a prior distribution over the class, the learner outputs a posterior , read as the randomized predictor that draws , and the price of is its Kullback–Leibler divergence from . The PAC-Bayes theorem (Theorem 31.1) says that with probability , simultaneously for every posterior, the generalization loss exceeds the training loss by at most . Its proof is a compact and elegant argument: Markov's inequality for an exponential moment, a change of measure from to by Jensen's inequality, an exchange of expectations that is possible because the prior does not depend on the sample, and a moment bound for the deviation of a single hypothesis. The bound suggests the learning rule of Remark 31.1, minimize plus the divergence penalty, which is regularized risk minimization in disguise, and for a finite class with a uniform prior it recovers an Occam-type bound (Exercise 2).
is a measurable space of hypotheses, a jointly measurable loss, a distribution over , and a prior probability measure on . For a posterior , , and , and is the Kullback–Leibler divergence, a real number when and the log-density is -integrable.
For and , with probability at least over , every probability measure with finite divergence satisfies
The identity (§31.1); the moment bound of the proof (p. 417); Exercise 2, the bound for a finite class with the uniform prior.
PAC-Bayes bounds are among the tightest generalization bounds known in practice, and the reason is visible in Theorem 31.1: the complexity term is not a property of the class but of the posterior actually chosen, measured against a prior, so a learner that stays close to its prior generalizes even in a huge class. The theorem is the ancestor of a large literature (Seeger, Langford, Catoni, Maurer) and of modern nonvacuous bounds for neural networks. Formally it is a pleasant target: the change-of-measure inequality is the Donsker–Varadhan inequality, of independent value, and the moment bound is a sharp sub-Gaussian fact. On the platform, the mission introduces Gibbs risks and the Kullback–Leibler divergence between measures on a class, ending the book's series with its last learning principle.
The Gibbs risk identity is Fubini for a bounded jointly measurable function. The moment bound is the delicate step: the book derives it from Hoeffding's tail bound through Exercise 1, whose one-sided hypothesis is not enough (a constant negative variable satisfies it with an unbounded moment), and even the two-sided tail integrates only to ; the claim is nevertheless true, for instance by writing for a standard Gaussian and applying Hoeffding's lemma to the sample mean, which gives . Theorem 31.1 then follows the book: Markov's inequality on with , the change of measure (31.2) by Jensen's inequality for applied to the density (the Donsker–Varadhan inequality, which needs and an integrable log-density), the exchange of expectations (31.4) by Fubini, the moment bound, and finally Jensen for in (31.6); formally the supremum over all posteriors is handled by proving the bound for each on the event , whose complement has probability at most by Markov, which sidesteps any measurability question about . Exercise 2 is the theorem with , for which .
The class is an arbitrary measurable space, priors and posteriors are probability measures on it, and is Mathlib's Radon–Nikodym derivative; the divergence is a Bochner integral, so the theorem quantifies over posteriors whose log-density is -integrable, exactly the posteriors with a finite divergence, for which the bound has content, and no junk value can make a case false. Posteriors may depend on the sample: the statement bounds the outer measure of the set of samples for which some admissible violates the bound. The loss is jointly measurable so that and are measurable and the Gibbs risks are genuine integrals; is forced by the denominator . The moment bound is stated as the claim the proof needs rather than as Exercise 1, whose printed hypothesis is insufficient; the item text records this. Exercise 2 is stated as a simultaneous bound over the finite class, the form in which the theorem delivers it.
Not stated: Remark 31.1 (a learning rule, not a theorem), Exercise 1 as printed, and the second part of Exercise 2.
A feedforward neural network is a directed acyclic graph of neurons, each computing a fixed scalar activation of a weighted sum of its inputs; fixing the graph and the activation and letting the weights vary gives a hypothesis class. Chapter 20 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), studies these classes through the book's three lenses. Approximation: every Boolean function is implemented by a network of depth 2 (Claim 20.1), but only at exponential size (Theorem 20.2), while a sign neuron implements conjunctions and disjunctions (Lemma 20.4), the bridge to Boolean circuits and hence to everything computable in bounded time. Estimation: the VC dimension of the class of sign networks over a graph with edges is (Theorem 20.6), so the sample complexity is governed by the number of weights. Optimization: training is NP-hard even for tiny networks, and the practical answer is SGD with the gradient computed by backpropagation, whose correctness the chapter derives from the chain rule.
A layered graph has layers , every edge joining to ; holds the inputs and a constant neuron outputting . With weights and an activation , the outputs are computed layer by layer, and . The class (20.1); for binary classification the output layer is a single neuron and is the sign function, so is a set of -valued predictors on . The size of the network is , its depth . The growth function extends to classes with any finite codomain (p. 275), and the proof of Theorem 20.6 uses two of its properties, stated as Exercises 3 and 4: the growth function of a product class is at most the product of the growth functions, and likewise for a composition class. For backpropagation the activation is any differentiable and the loss is ; the backward pass sets and .
The VC dimension of is . Explicitly, for a layered graph of depth at least with a single output neuron,
stated as: every satisfies this bound (so the VC dimension is finite).
Claim 20.1 (the depth-2 graph with whose sign class contains every function ); Theorem 20.2 (every sign network implementing all functions has ); Lemma 20.4 (conjunction and disjunction as sign neurons); Exercise 4 (growth function of a composition); the correctness of backpropagation (§20.6: the partial derivative for the edge is ). Further items: Exercise 3 (growth function of a product) and the intermediate bound of the proof of Theorem 20.6.
Theorem 20.6 is the reason networks are learnable at all in the book's sense: by the fundamental theorem, a class with finite VC dimension is agnostic PAC learnable with sample complexity linear in that dimension, and here the dimension is essentially the number of tunable parameters. The proof technique, due to Kakade and Tewari's lecture notes, is a composition-and-product argument on growth functions that applies to any layered class of threshold units and is reusable well beyond this chapter. Theorem 20.2 is the matching negative fact on expressive power, and it is a corollary of the same bound: a class that shatters points needs edges. Backpropagation's correctness is the one theorem about training the chapter can offer, given the hardness results, and it is the algorithm every practitioner runs.
Claim 20.1 and Lemma 20.4 are explicit constructions: the neuron detects because otherwise, and the output neuron takes the disjunction; formally one must build the weight function and evaluate the forward pass on the inputs. Exercises 3 and 4 are counting: a restricted product is determined by its two restricted factors, and a restricted composition on is determined by and , with . Theorem 20.6 then needs: the class of one neuron is the class of homogenous halfspaces on its incoming coordinates, of VC dimension at most (Mission VI), Sauer's lemma in the form for every (Mission IV; for use ), the layer class as a product and the network as a composition of layer classes, and finally the arithmetic , which replaces the book's appeal to Lemma A.2 (for one has ). Theorem 20.2 follows from the goal with . Backpropagation is a chain-rule computation in a single real variable: the loss as a function of one weight is a composition of finitely many differentiable maps, and the derivative unwinds to the backward recursion; the formal effort is in the induction along layers with the natural-number indexing of the model.
Layers and neurons are indexed by natural numbers: a LayeredGraph records the depth, the layer widths and, for each , the finite set of edges as pairs within the layer widths. Weights are functions on all index triples, and only those on edges are used, so the class is the image of all weight functions, as in (20.1). The forward computation netOutput is a recursion on the layer index; netInput is . The sign activation returns with , the book's convention elsewhere, and a neuron with no incoming edges outputs (p. 270). The binary class signNetClass n G is Bool-valued, true iff the output neuron's input is positive, and is stated for graphs of depth at least (for depth the edges out of the input layer would be used but not counted in ). Growth functions with finite codomain are growthY, an sSup over restriction sizes, well defined because the codomains are finite; the Bool case is Mission IV's growth, and VC dimension and shattering are Mission IV's. Theorem 20.6 and Theorem 20.2 are given with explicit constants derived from the proof, since statements have no formal content; the drafter verified numerically for up to and at , and . Backpropagation is stated for an arbitrary layered graph (phantom edges have weight , p. 279), any differentiable activation, and one edge at a time as a HasDerivAt of the loss in that weight; is defined by recursion on . The book's layer indices in (20.3) are shifted by one in the statement.
Not stated: Theorem 20.3 (Turing machines), Theorem 20.5 and Exercise 1 (sigmoid approximation, which needs a convention for outputs in that the chapter leaves open), Theorem 20.7 and Exercise 6 (NP-hardness), Exercise 5 (the sigmoid lower bound, which assumes an exact threshold), the sigmoid half of Theorem 20.2, and the SGD pseudocode of §20.6, which is a heuristic without a stated guarantee.
Whether the gravitational field must be quantized is a long-standing foundational question. A well-known family of arguments tries to settle it by consistency alone: if a classical field were coupled to a quantum system, some basic principle — momentum conservation, the uncertainty relations, or the impossibility of superluminal signalling — would allegedly be violated. The two best-known versions are the gedanken experiment of Eppley and Hannah (1977) and the measurement-theoretic argument of DeWitt (1962).
Albers, Kiefer and Reginatto (Phys. Rev. D 78, 064051 (2008)) re-examine both arguments. Their paper is largely conceptual, but several of its steps are precise, checkable mathematical claims. This mission collects those claims and makes them machine-checkable.
Timeline.
Photon pair and detector (Sec. II). Each photon carries a polarization qubit with orthonormal basis (horizontal) and (vertical). A detector with state space (an arbitrary complex inner-product space) is coupled to photon 1. Before the measurement the joint state of photon 1, photon 2 and the detector is
and after the detector has measured photon 1 it is
The reduced density operator of photon 2 is obtained from by tracing out photon 1 and the detector; the paper asserts that for both states it equals
Mass cube and gravitational wave (Sec. III B). The disturbance of the averaged energy density of the scattered wave depends on the cube's edge length and speed , with sensitivities and . With and the uncertainty has a strictly positive lower bound.
DeWitt's argument (Sec. V). A system observable reconstructed from apparatus data has uncertainty , where is the coupling constant.
For all unit vectors ,
The goal is the precise content of the paper's rebuttal of the superluminal-signalling branch of the Eppley–Hannah argument: the state of photon 2 accessible to a probe (such as a classical gravitational wave) is the same whether or not photon 1 has been measured, so a probe of photon 2 alone cannot tell whether photon 1 was measured. Milestones 3–6 are the quantitative estimates the paper uses in Sec. III B (a coupling to a test body obeying the uncertainty principle transfers a minimum uncertainty to the classical wave) and Sec. V (DeWitt's limitation on a single observable, Eq. (64)).
The results are elementary once stated; the value of the mission is to pin the paper's claims down exactly, including the hypotheses under which they hold. None of the statements has, to our knowledge, a machine-checked proof on the platform.
The goal and Milestones 1–2 need a workable representation of the partial trace over a factor that is an arbitrary (possibly infinite-dimensional) inner-product space; the cross terms between the two branches vanish because the two branches are orthogonal on photon 1, not because of any property of the detector states. Milestones 3–6 are single-variable optimization statements; the main care is in the side conditions (positivity, excluding and ).
The book The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) develops a perturbative, physics-style theory of wide deep neural networks. Every later computation in the book, from the statistics of preactivations at initialization to the neural tangent kernel, reduces to Gaussian expectations of polynomials. The single tool that evaluates these expectations is Wick's theorem (eq. 1.45), which the authors ask the reader to "put a box around". This mission formalizes Chapter 1, §1.1 (Gaussian Integrals), culminating in that theorem. It is the first mission of a series formalizing the book, all in the Lean namespace DeepLearningTheory.
Fix and a symmetric positive-definite real matrix , the covariance. Write for its inverse. The zero-mean multivariable Gaussian distribution with covariance (eq. 1.31) has density on
and the expectation of an observable is (eqs. 1.36, 1.46), an integral against Lebesgue measure. A pairing of the labels is a partition into unordered pairs; equivalently, a fixed-point-free involution of pairing with . There are pairings.
For all indices (repetitions allowed),
Wick's theorem (also known as Isserlis' theorem, 1918) is used throughout the book: the Gaussianity of the first layer (Chapter 4), the four-point correlators of deep linear networks (Chapter 3), and all perturbative expansions around the infinite-width limit are evaluated by Wick contractions. A machine-checked version stated in the book's own density-based conventions gives later missions of this series a dependable foundation. The result is classical; the work remaining is its formalization in exactly this form. A related statement for general (possibly degenerate) Gaussian measures already exists on the platform as FeynmanWick.wick_theorem_gaussian; the present mission keeps the book's formulation via the explicit density and a positive-definite covariance.
The book's derivation differentiates the generating function (1.41) times at , which requires justifying differentiation under the integral sign and organizing the combinatorics of the product rule into pairings. Both the analytic step (dominated convergence for Gaussian tails, in dimensions) and the combinatorial step (a bijection between surviving terms and pairings, with the normalization) are routine on paper but need care in Lean. Computing the normalization (1.30) itself requires diagonalizing and a linear change of variables.
Fin N → ℝ with Lebesgue measure; is a Matrix (Fin N) (Fin N) ℝ with K.PosDef (which includes symmetry). The inverse is Mathlib's K⁻¹.gaussianDensity K z and gaussExpect K F are exactly the book's and ; gaussQuadForm K z is .pairings (2m) is the finite set of fixed-point-free involutions of Fin (2m); the product is over labels with , so each pair contributes once.Dirac showed in 1931 that quantum mechanics permits isolated magnetic charges provided electric charge is quantized, but in Maxwell's theory such a magnetic monopole is a point singularity attached to an unobservable "Dirac string". In 1974 G. 't Hooft and, independently, A. M. Polyakov observed that in gauge theories where the electromagnetic group sits inside a larger group with compact covering group, monopoles arise instead as smooth, finite-energy solutions of the classical field equations, with no singularity and no string. 't Hooft's paper (Nucl. Phys. B79 (1974) 276) does this for the SO(3) model of Georgi and Glashow and computes the mass numerically. The resulting "'t Hooft–Polyakov monopole" became the model example of a topological soliton in gauge theory.
Timeline. 1931: Dirac's quantization argument (Proc. R. Soc. A 133, 60). 1972: Georgi–Glashow SO(3) electroweak model (PRL 28, 1494). 1974: 't Hooft and Polyakov (JETP Lett. 20, 194) describe the regular monopole, 't Hooft by a spherically symmetric ansatz, a reduced one-dimensional energy functional and a numerical minimisation. 1975: Prasad and Sommerfield find a closed-form solution in the limit (PRL 35, 760). For no closed form is known.
Space and isospin space are both . A static configuration in the gauge consists of a Higgs triplet and a gauge field , . With coupling , Higgs self-coupling and vacuum value (eqs. (2.1)–(2.3), with ),
and the static energy is
The vector masses are and the Higgs mass is . A static solution is a smooth configuration of finite energy at which is stationary under all compactly supported smooth variations. 't Hooft's gauge-invariant electromagnetic tensor (2.17) is
The spherically symmetric ansatz (2.8) is , with . The monopole boundary condition is as (eqs. (2.6), (2.11)).
For all , , there are radial profiles such that the configuration (2.8) is a smooth finite-energy static solution with
i.e. a regular magnetic monopole whose far field is (2.20).
The existence of a regular monopole is what makes the monopole a particle of the theory: its mass (eq. (3.3)) is finite and calculable, and its magnetic charge is fixed by topology rather than put in by hand. The ingredients (hedgehog ansatz, the zero of the Higgs field forced by the boundary condition, the reduction to an ODE system, the gauge-invariant electromagnetic tensor) are reused throughout the theory of solitons in gauge theories.
The result is established in the physics literature; 't Hooft's own argument is partly numerical (trial functions). The mission asks for a machine-checked development: the algebraic and calculus identities of Sects. 1–3, the topological zero, and a complete existence proof for the spherically symmetric solution for every . No machine-checked proof of any of these is known to the proposer.
The identities (milestones 1, 4, 6–9) are finite computations, but milestones 4, 5 and 9 must go through Fréchet derivatives of vector fields on and spherical coordinates, where most of the work lies. Milestone 3 is a degree-theoretic statement not available off the shelf. The goal needs an actual existence theorem for a nonlinear coupled ODE system on with singular coefficients at and boundary conditions at both ends, followed by regularity of the resulting fields at the origin and the passage from the reduced (radial) equations to the full field equations. 't Hooft's numerical minimisation over trial functions gives no proof that a minimiser exists or is smooth.
is EuclideanSpace ℝ (Fin 3) with Lebesgue measure; indices run over Fin 3 = {0,1,2}, the Levi-Civita symbol is an explicit formula, partial derivatives are Fréchet derivatives in coordinate directions. Fields are static and in the gauge , where the Gauss-law equation holds automatically, so "static solution" means: fields, integrable energy density, and zero derivative of the energy along every smooth compactly supported variation of and . Lean's total operations are used: division by zero is and the Bochner integral of a non-integrable function is ; every statement using them either excludes the degenerate input or is insensitive to it (the goal demands integrability explicitly). The constant is included so the vacuum has zero energy, as in (2.9).
Two deviations from the printed text, both flagged in the milestones: (i) with standard Pauli matrices, is , whereas (2.6) prints ; the milestone states the computed identity. (ii) With , (2.20) gives while (2.21) prints ; the flux milestone therefore states the magnitude , and the sign is fixed by (2.20). The asymptotic analysis (2.14)–(2.15) is formalized as an exact statement about pure power laws. The numerical values of in (3.3) are not formalized.
A trivializing reading of the goal is ruled out: the solution must satisfy the non-trivial boundary condition, which by milestone 3 excludes the vacuum, and the stationarity must hold for all variations, not only spherically symmetric ones.
Useful reusable infrastructure: spherical-coordinate integration of radial functions on , calculus of hedgehog fields, and a Brouwer-degree / no-retraction argument for maps of the sphere. Contributions of any milestone, and of alternative existence proofs (variational, shooting), are welcome.
A magnetohydrodynamic (MHD) equilibrium is a magnetic field and a scalar pressure on a region of satisfying
Under the substitution these are exactly the equations of a steady incompressible Euler flow, with replaced by the Bernoulli function, so every statement in this mission is simultaneously a statement about stationary solutions of the 3D Euler equations. Magnetic confinement of a fusion plasma requires equilibria whose pressure surfaces are nested tori, because forces to be constant on the surfaces swept out by field lines.
Whether such equilibria exist without a continuous symmetry has been open since Grad, who conjectured in 1967 that smooth toroidal equilibria with non-constant pressure do not exist unless the configuration is symmetric (for instance axisymmetric), and restated the claim in 1985 as the assertion that, apart from the symmetric exceptions, there are no families of solutions depending smoothly on a parameter. Modern formulations of the conjecture appear in the work of Constantin–Drivas–Ginsberg (2021), Enciso–Luque–Peralta-Salas (2025) and Cardona–Duignan–Perrella (2025, Conjecture 2.5). Partial results have always relaxed something: Lortz (1970) obtained non-symmetric toroidal equilibria only with mirror symmetry and vanishing rotational transform; Bruno–Laurence (1996) and Enciso–Luque–Peralta-Salas (2025) allow discontinuous pressure and current sheets; Weitzner–Sengupta (2020) work in a topological torus rather than true toroidal geometry; near-axis and high-aspect-ratio expansions (Mercier 1964, Garren–Boozer 1991) give only approximate solutions.
Landreman (2026) exhibits explicit, fully non-axisymmetric, smooth analytic solutions on a genuine solid torus, with exact nested flux surfaces, finite aspect ratio and non-zero rotational transform. This mission formalizes the first of the two families presented there — the family with uniform rotational transform — in Lean 4.
Fix a parameter and set , . For a Cartesian point (written in the paper) define
and the vector field
The natural domain is the open set , on which and all the expressions above are smooth. With
the flux label and the pressure are
where is an arbitrary constant. The level sets of are the pressure surfaces. For the region is a solid torus bounded by a -surface, and this is the plasma domain.
Field lines are described by a second coordinate system. For labels with , putting and , the position map is
The curve is an integral curve of , the pair labels the field line, and acts as a toroidal angle of period . The magnetic axis is the field line , , on which ; it is the non-planar closed curve .
The goal theorem asserts that for every , every and every constant , the pair above is a smooth equilibrium on that is genuinely three-dimensional:
together with smoothness of and on and the failure of axisymmetry: there is a rotation about the axis and a point of whose image lies in and carries a different pressure.
The milestones are the individual equations of Section 2 of the paper: divergence-freedom, the tension identity , force balance, invariance of along , the field-line position map and its Jacobian , the expressions and in field-line labels, the magnetic axis, the enclosed volume , the uniform rotational transform , and the averages and .
The solutions contradict the strict formulation of Grad's conjecture used in the recent literature (for example Conjecture 2.5 of Cardona–Duignan–Perrella), since they are smooth, have non-constant pressure, exact nested toroidal flux surfaces, no continuous Euclidean symmetry, finite aspect ratio and non-zero rotational transform, and they form continuous families parameterized by and . Because MHD equilibrium is isomorphic to steady Euler flow, the same objects are explicit non-symmetric stationary Euler flows with invariant tori. They also serve as exact benchmarks for numerical equilibrium codes, where analytic three-dimensional solutions with known flux surfaces are otherwise unavailable.
The paper's derivations are elementary but long: they are algebraic identities among square roots and rational functions, verified in the paper by hand and by supporting numerical scripts. A machine-checked development removes the remaining doubt about sign conventions and domains, which is precisely what a counterexample to a conjecture requires. Nothing in this development is currently formalized in Mathlib: there is no curl, no divergence, and no notion of MHD equilibrium, so the mission also produces a small reusable vector-calculus layer on .
Force balance is an identity between derivatives of expressions containing and division by ; differentiating it directly produces large expressions whose simplification needs the domain hypotheses ( and positive radicand) at every step, so field_simp-style automation must be driven with those side conditions in hand. The statements about field-line coordinates require knowing that the position map is a diffeomorphism onto its image, which the paper establishes by a covering argument rather than by computation. The transform is the hardest milestone: it is a winding-number statement about the poloidal displacement of a field line relative to the magnetic axis, and the paper's proof is a continuity-in- argument, which in Lean needs an honest treatment of continuous angle lifts. The volume and average identities need the change of variables theorem with the constant Jacobian over a solid torus.
Points of space are Fin 3 → ℝ; partial derivatives are fderiv applied to the standard basis vector, and gradient, divergence, curl, cross product, the directional derivative and the tension are defined from it in the first definition file. Squared length is , so the Pi-type norm is never used. All the paper's objects — , , , , , , , , , , , , , , rotation about the axis, and the complex poloidal displacement used for the transform — are given in the second definition file, in the same notation as this description. Smoothness is ContDiffOn ℝ ⊤; volumes are the Lebesgue measure on Fin 3 → ℝ; integrals are Bochner integrals.
Everything is stated with the explicit field of Section 2 rather than an abstract existence claim, so no statement can be satisfied by a degenerate or symmetric configuration. The equilibrium conditions are asserted pointwise on , which is open and non-empty for , so no milestone is vacuous. Contributions of the auxiliary calculus lemmas (differentiability of , and on , and the product and quotient rules in this partialD formulation) are welcome and reusable by the companion family of Section 3, which is not part of this mission.
Chapter 3 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks how many random examples suffice to learn a concept from an infinite class. The cardinality bound of Occam's Razor is useless there, yet the rectangle game of Chapter 1 shows that some infinite classes are learnable from a finite sample. The answer is the Vapnik–Chervonenkis dimension: the size of the largest set on which the class realizes every labeling. Sauer's lemma says that a class of VC dimension realizes only labelings on any points, polynomially many rather than , and the ε-net theorem of Blumer, Ehrenfeucht, Haussler and Warmuth turns this into a sample bound: a consistent hypothesis from a class of VC dimension is probably approximately correct once is of order . A matching lower bound shows that examples are necessary. The chapter thus gives a single combinatorial parameter that characterizes, up to a logarithmic factor, the sample complexity of learning any class in the distribution-free model.
For a class of concepts and a finite , is the set of dichotomies of realized by ; is shattered if all are realized; is the supremum of the sizes of shattered sets, possibly ; is the largest over ; and is defined by , . For a target the error regions are for in the hypothesis class, and a set of points is an ε-net if it meets every error region of weight at least under the target distribution . Samples, their product law, consistency and the error of a hypothesis are those of Mission I.
Let be a class of VC dimension at most , well-behaved for the target (the double-sample event of the proof is null-measurable), and . The points of a random sample of examples of a target fail to be an ε-net for the error regions with probability at most
so any algorithm that outputs a hypothesis in consistent with its sample has error greater than with at most that probability; with and the probability is at most ; and, if is nonempty, every class contained in for whose targets is well-behaved is PAC learnable using .
Lemma 3.1 (Sauer's lemma, ); Lemma 3.2 (); the polynomial bound of p. 57; Theorem 3.5 (the lower bound, in the two explicit forms of its proof).
Theorem 3.3 is the fundamental theorem of PAC learning: it replaces in Occam's Razor by the VC dimension and thereby covers rectangles, halfspaces, polygons, neural networks with a fixed architecture, and every class whose dichotomies grow polynomially. Its proof, the double sample and random partition argument, is the origin of symmetrization in empirical process theory. Sauer's lemma is a cornerstone of extremal combinatorics with independent proofs by Sauer, Shelah and Vapnik–Chervonenkis, and the lower bound of Theorem 3.5 shows that the upper bound is tight to within , so the VC dimension genuinely characterizes sample complexity. None of these is machine-checked. Formalizing them puts on the platform the VC dimension, the growth function and the ε-net theorem with explicit constants, stated on the same sample law as the rest of this series, and the first information-theoretic lower bound for learning.
Sauer's lemma is a double induction on and through the auxiliary class of dichotomies whose two extensions to a distinguished point are both realized, which needs care with the identification of dichotomies of and of . The ε-net theorem needs: the reduction from a failed ε-net on the first half to a region hit at least times by the second half, which is a Chebyshev bound on a binomial variable and is where enters; the exchangeability of the draws with a random partition into two halves; the counting bound ; and Sauer's lemma applied to the error regions, whose growth function equals that of . The explicit constants require the numerical inequality under the two stated conditions. The lower bound is a probabilistic argument with a random target: conditional on the sample, the labels of unseen points are fair coins, so the number of errors on them is binomial and exceeds half its range with probability at least ; the refined bound scales this construction to a region of weight and uses Markov's inequality to bound the number of draws landing in it. Measurability of the failure sets is avoided by stating outer-measure bounds, except for the double-sample event, which the proof integrates: it is assumed null-measurable (the well-behavedness of Blumer et al., without which the theorem is false for a class of VC dimension on ). For the lower bound it is avoided by working over a finitely supported distribution on a space with measurable singletons.
The VC dimension is a supremum in , the growth function a supremum in (bounded by ), and the book's recurrence, with its closed form and polynomial bound stated as separate theorems. The goal is stated for a hypothesis class (Theorem 3.4), Theorem 3.3 being the case ; it carries the exact bound of the proof, the explicit constants of Blumer et al. in place of the book's , the requirement of the proof's Chebyshev step, measurability of the hypotheses and the target, well-behavedness of for the target, and . PAC learnability of the subclasses of needs nonempty, since no algorithm outputs hypotheses in the empty class. The lower bound is stated for every deterministic learning function, on an instance space with measurable singletons, for a class shattering some set of points, with the explicit constants derived in the proof sketch (: error with probability ; and : error with probability ). Running time is not modelled. The composition bound for layered networks (Theorems 3.6 and 3.7) is not stated.
Trivializing readings are excluded: the ε-net event ranges over every hypothesis of , the failure bounds are uniform over all consistent learners, and the lower bound holds for every learning function. Welcome contributions: Sauer's lemma, the closed form and the bound, the random-partition counting lemma, and the binomial median inequality used in the lower bound.
The index theorem says that among several Markov reward processes, of which one may be advanced at each decision time, the right one to advance is the one of greatest Gittins index. Chapter 4 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks how far this extends when the constituents are not reward processes but decision processes, each with its own controls: a research project that can be run in several ways, a job that can be processed at different speeds, a sampling process that may be stopped and exploited. A family of such superprocesses requires two choices at every decision time, which superprocess to continue and with which control, and an index policy in the sense of Chapter 2 need not be optimal (Example 4.1). Whittle (1980) identified the condition under which it is: Condition D, that when a superprocess is played against a standard bandit process paying a constant rent, the control one should apply to it does not depend on the rent. Under that condition the index theorem survives (Theorem 4.3), the index is characterized (Note 4.2), stoppable bandit processes with improving stopping options satisfy the condition (Lemma 4.4), and the chapter adds two results about indices themselves: any index that works for all bandit processes is a strictly increasing function of the Gittins index (Theorem 4.8), and a policy that is within of the index policy loses at most (Theorem 4.18).
A decision process on a countable state space has in each state a nonempty finite set of controls; applying yields the reward and moves the state by . Adding the freeze control, which leaves the state unchanged and yields nothing, makes a superprocess . Operating under a feasible deterministic stationary Markov policy (that is, ) gives an ordinary bandit process , and the superprocess index is
with the Gittins index of the Bandit Algorithms model. A simple family of alternative superprocesses (SFAS) is superprocesses on a common ; at each decision time exactly one is continued, with a control from its control set, the others being frozen, and rewards are discounted by . A policy is a Markov kernel per decision time from the history to the pair (superprocess, control); it is optimal if it is feasible and attains the supremum of the discounted payoff over feasible policies from every initial state-vector, and it is an index policy if it always continues a superprocess and control of maximal .
Condition D. Let be a standard bandit process with parameter (one state, reward ). satisfies Condition D if there is a function such that, for every and for which it is optimal in the family to select in state , it is optimal to apply the control . A stoppable bandit process is a bandit process with a stop control that makes it behave as a standard bandit process with parameter ; its stopping option is improving if is almost surely nondecreasing in process time.
For a decision process with bounded rewards and a Condition-D control , every index policy with respect to that applies to the superprocess it continues is optimal for the family of superprocesses:
Note 4.2 (under Condition D, is selected in iff , and at a control is optimal iff ; the printed equivalence fails for ); Lemma 4.4 (Condition D for stoppable bandit processes with improving stopping options); Theorem 4.8 (an index for the bandit processes with discount factor is strictly increasing in ); Theorem 4.18 (the -index bound, for the discrete-time index).
Theorem 4.3 is the widest form in which the index theorem holds without further structure, and Condition D is exactly the right hypothesis: it says the superprocess has a canonical control, and once it does the family reduces to a family of bandit processes and the prevailing-charge argument goes through. Lemma 4.4 gives the model where the condition is known to hold, a research project that may be exploited at any time; the buyer's problem of Bergman and Bather is the case where it fails. Theorem 4.8 explains why every index theorem in the book is about the Gittins index: any function that orders bandit processes optimally must order them as does. Theorem 4.18 is the quantitative version of the index theorem that heuristics and computations rely on.
Nothing here is machine-checked. The mission builds the first controlled multi-armed model on the platform, a run law for families of decision processes with an explicit feasibility constraint, and states Whittle's condition as a property of the two-member family, which is how the literature uses it. Theorems 4.8 and 4.18 are statements about the existing Bandit Algorithms model and are usable by any later work on that model.
The obvious attack on Theorem 4.3, "replace each superprocess by the bandit process for its Condition-D policy and apply the index theorem", is the second half of the book's proof; the first half is to show that an optimal policy never gains by applying a control other than to a superprocess it continues, and that uses the prevailing-stake accounting of §4.3 with the other superprocesses treated as one bandit process, plus the observation that the class of policies deviating at most times is -exhaustive. Both halves require the whole run law of the family to be related to the run laws of its constituents, which is where a formalization spends its effort. Note 4.2 is short on the page but needs the optimal-stopping characterization of Chapter 2 for the bandit process under charge . Theorem 4.8 is elementary given the value of under a freezing rule, , but that identity is itself a computation on the run law. Theorem 4.18 has no proof in the book (Glazebrook 1982c); the natural route is the prevailing-charge upper bound with the charges perturbed by .
Decision processes carry their control sets as finsets with a nonemptiness proof and their kernels as Markov kernels; the state space is countable with measurable singletons (so stationary kernels and control-dependent maps are measurable without side conditions) and the control type is finite with measurable singletons. The family's run law is built decision time by decision time as the Bandit Algorithms model builds markovBanditMeasure, with the policy's kernel producing the pair (superprocess, control). Feasibility is an almost-sure condition on the policy kernel, and optimality is the book's: feasible, and the supremum from every initial state-vector. The superprocess index is a real supremum over feasible stationary policies with , bounded by the reward bound and nonempty for ; for an unavailable it is a default value that no index policy consults. Condition D is stated on the family on , where the standard state has every control available, all equivalent. A stoppable bandit process is the decision process with control type Bool. Theorem 4.8 quantifies over index functions defined on every measurable state space and takes as hypothesis only what its proof uses, optimality of -index policies for the families . Theorem 4.18 is on the -armed Bandit Algorithms model with and the bound : the book's is in continuous-time index units, times the discrete-time index used here, and read with the discrete index it is false for . Theorem 4.3's index policy applies the Condition-D control to the superprocess it continues, as the book's proof does; an index policy that breaks ties among controls otherwise need not be optimal.
Trivializing readings are excluded: index policies must be feasible, optimality is required from every initial state, and Condition D is a statement about optimal policies of a genuine two-member family, not about a chosen policy. Welcome contributions: the relation between the family's run law and the constituents' chain laws, the freezing-rule value identity behind Theorem 4.8, and the prevailing-stake accounting of §4.3.
A decision-maker has projects, each a Markov reward process, and at every decision time may advance exactly one of them; the others stay frozen. Which project to advance so as to maximize the expected total discounted reward? Posed as a dynamic program the problem has a state space that is the product of the state spaces, and the size of that product defeats every general method. The index theorem of Gittins and Jones (1974) says the dynamic program is solved exactly by an index policy: there is a real number , computable for each bandit process from its own data and its own current state , such that always advancing a process of greatest index is optimal. Chapter 2 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), introduces the index, proves the theorem three times, and works out the properties of the index that the rest of the book, from jobs and superprocesses to restless bandits, is built on: which stopping time attains it, how it is computed, how it moves with the discount factor, and when it collapses to the myopic rule.
The index theorem itself is already on the platform, proved, as BanditAlgorithm.gittins_index_theorem in the Bandit Algorithms series (Lattimore and Szepesvári, Theorem 35.9). This mission cites it and formalizes what Chapter 2 establishes around it.
A bandit process (§2.3–2.4) is a Markov reward process on a countable state space : transition probabilities , a bounded reward received each time the continuation control is applied in state , and a discount factor ; the freeze control leaves the state unchanged and yields nothing. The law of the process started at is and is its state at process time . A stopping time is a past-measurable rule for switching from continuation to freezing, taking values in . For such , is the expected discounted reward and the expected discounted time; their ratio (2.7) is the equivalent constant reward rate of that portion of . The Gittins index is
and, equivalently, the fair charge (2.5): the greatest rent per period for which continuing for one or more periods, paying each period, can be done without expected loss. A simple family of alternative bandit processes (SFABP) is such processes with a common discount factor, one of which is continued at each decision time; an index policy continues a process of greatest index. In the Lean development the single-arm model is the platform's (GittinsIndex): the chain law is built by the Ionescu–Tulcea construction, stopping times are adapted -valued maps on trajectories, and gittinsIndex P r a x is (2.6).
The supremum in (2.6) is attained. For the initial state , the attaining stopping rule may be taken to be "stop at the first time at which the state lies in " for any set with
and every such rule has .
Theorem 2.1 as a reference to the proved platform theorem; Eq. (2.5), the fair-charge characterization of the index; the restart-in-state formulation of §2.6.4 as the convergence of the Katehakis–Veinott value iteration; Theorem 2.3, monotonicity in the discount factor; Lemma 2.4, the interchange of two bandit portions; Propositions 2.5–2.8, the monotone-index cases in which the index is the immediate reward, or is attained only after the first step, or only at .
Lemma 2.2 is the working form of the index: it turns the supremum over all stopping times into a specific rule, the first time the index falls below its starting value, and it is what the interchange proof of §2.7, the modified-forwards-induction policies of §2.6.6, the monotone-index propositions of §2.11 and the treatment of jobs in Chapter 3 all use. The fair-charge form (2.5) is the prevailing-charge proof of the theorem (Weber 1992) and the interpretation that carries over to superprocesses and restless bandits. The restart formulation is how indices are computed in practice (Katehakis and Veinott 1987), and Theorem 2.3 is the first of the comparative statics used throughout Chapters 7 and 8. Lemma 2.4 is the elementary inequality behind the original proof of Gittins and Jones.
Of these, only the index theorem has a machine-checked proof today. Formalizing the rest gives the platform the index as a usable object: a characterization of the optimal stopping rule, a convergent algorithm for it, and the monotonicity facts, all stated against the existing model so that every later mission of this series and every future use of the L&S model can build on them.
The obvious first move for Lemma 2.2, "take the stopping time that achieves the supremum", is what has to be proved: the supremum is over an uncountable family, and attainment comes from the optimal stopping problem with charge , whose value function satisfies , together with the fact that its optimal stopping set is characterized by the strict and non-strict inequalities and . That last step is the content: it identifies the local decision "stop or continue" with a comparison of indices, which is why any set between the two level sets works. On the platform's model this requires the dynamic-programming theory of discounted optimal stopping on a countable space (Theorem 2.10 of the book), the identification of fairChargeProfit with that value function, and the strong Markov property of markovChainMeasure at a trajectory stopping time. Theorem 2.3 needs randomized stopping times (a geometric kill) and the fact that they do not enlarge the supremum. The restart iteration is monotone and bounded but its operator is not a contraction in the restart value, so its limit has to be identified with the restart problem's value directly; that value is , not , because restarting forever is free.
The state space is a countable type with measurable singletons, so every subset is measurable; rewards are bounded; . The chain law, stopping times, the discounted stopped sums and the index are the platform's, unchanged. Expectations are Bochner integrals; with bounded rewards they are finite and no total-function default value enters. IsPositiveStoppingTime fixes everywhere, so and the ratio (2.7) is a genuine quotient. The stopping rule of Lemma 2.2 is the hitting time from time of a set, with when the set is never hit. The fair-charge profit is a real supremum over the nonempty bounded family of positive stopping times, and (2.5) is stated with the outer supremum over , a nonempty set bounded above. The restart iteration is stated as a limit, with the value : for a nonnegative index this is the book's , and the maximum is forced by a one-state example with negative reward. The propositions' hypotheses are almost-sure events under , written as events of measure one.
Two trivializing readings are excluded: the index is never taken over all -valued maps but over adapted stopping times, and the stopping set of the goal is not restricted to the two extreme level sets. Contributions welcome: the optimal-stopping dynamic program on markovChainMeasure (value iteration, the strong Markov property at a stopping time), the equivalence of randomized and non-randomized stopping times for the supremum, and the monotone convergence of the restart iteration.
The derivation of Kepler's three laws from Newton's inverse-square law of gravitation is the calculation with which mathematical physics begins. Kepler published the laws in 1609 and 1619 as empirical regularities distilled from Tycho Brahe's naked-eye astrometry: planets travel on ellipses with the Sun at a focus, the Sun–planet segment sweeps equal areas in equal times, and the square of the orbital period scales as the cube of the orbit's size. That an attractive force falling off as forces exactly these three regularities was established by Newton in the Principia (1687); as David Tong remarks in the source notes, the third law was within reach of several of Newton's contemporaries, but the derivation of the first — that the orbit is a conic section with the centre of attraction at a focus — was Newton's alone.
This mission formalizes that derivation as it is presented in §4 (Central Forces) of David Tong's Dynamics and Relativity, the Cambridge Part IA Mathematical Tripos lecture notes (Lent 2013). It is the first mission in a series covering those notes, and it targets the chapter's capstone, Kepler's first law.
A point particle of mass moves in Euclidean -space along a trajectory , assumed twice continuously differentiable and never passing through the origin, where the field below is singular. Write and .
The particle moves in a central force field when it obeys Tong's equation of motion (4.1),
where gives the radial component of the force at distance ; for a force derived from a central potential one has . The Kepler problem (Tong §4.3.1) is the inverse-square special case, potential (4.12)
with for gravitational attraction by a mass fixed at the origin. (The same equations govern the Coulomb problem, with , which is repulsive when ; this mission fixes .)
Two conserved quantities organize the problem. The angular momentum is the vector
and we write for the angular momentum per unit mass, which in the plane polar coordinates of Tong (4.5) is . The total energy of the Kepler problem is
Tong's solution (4.14) of the orbit equation states that the trajectory lies on a conic section with a focus at the origin. Coordinate-free, this says that there is a fixed eccentricity vector , pointing towards the point of closest approach, with
which is Tong's with the eccentricity and measured from the direction of , and the semi-latus rectum.
Finally, a set is an ellipse with a focus at the origin when there are a nonzero normal vector , a second focus with , and a real number with , such that is exactly the set of points of the plane satisfying the two-foci (string) property
The inequality forces and rules out the degenerate loci; gives a circle.
The goal theorem is Kepler's first law, K1 of Tong §4.3.2: each planet moves in an ellipse, with the Sun at one focus. Formally, for a trajectory of the attractive inverse-square problem with nonvanishing angular momentum and negative total energy,
The hypothesis excludes purely radial free-fall, whose trajectory is a segment rather than an ellipse, and is the bounded regime, which by Tong (4.16) is exactly .
The milestones follow the source in order: conservation of angular momentum and the resulting planarity of the motion (§4, p. 48); Kepler's second law (K2), which holds for any central force; conservation of energy; the conic orbit (4.14); the identification of a conic of eccentricity as an ellipse with a focus at the origin (4.15); the energy–eccentricity relation (4.16); and Kepler's third law (K3, p. 62),
The result. K1 is the statement that fixes the inverse-square law among all central force laws: K2 holds for every central force, and dimensional analysis alone gives the shape of K3, but closed orbits that are exact ellipses with the attracting centre at a focus are special to the force (and to the harmonic force, with the centre at the centre of the ellipse). Everything quantitative in classical celestial mechanics — orbit determination, the mass–period relation used to weigh binary stars, and the perturbative treatment of precession that eventually exposed the anomaly in Mercury's orbit — is built on the Kepler solution.
Formalizing it. The mathematics has been settled for three centuries; what this mission produces is a machine-checked treatment of the Newtonian derivation, starting from the differential equation rather than from a prescribed orbit. Mathlib has no central-force or two-body library, so the definitions here — central force motion, angular momentum, conserved energy, swept area, and the two-foci characterization of an ellipse — are new and reusable across the rest of the series and by any later mission in classical mechanics. The existing platform mission Celestial Mechanics I: Binary Star Systems runs the complementary direction, verifying that a prescribed conic orbit satisfies the equations of motion and reducing the two-body problem to a one-body problem; the present mission asks for the converse, which is the harder half and the one Newton is credited with.
The derivation in the source changes the independent variable from time to the polar angle , substitutes , and solves the resulting linear oscillator equation (4.11). Each of those steps needs infrastructure that does not exist in Mathlib. There is no polar-angle function attached to a curve in the plane: one has to produce a continuously differentiable angle lifting the trajectory, show never vanishes so that is a legitimate change of variable, and then transport a second-order ODE through that reparametrization. Solving (4.11) then requires a uniqueness theorem for the inhomogeneous harmonic oscillator, and reading the conic back into Cartesian form requires the algebra of (4.15).
Kepler's third law carries an extra burden beyond the formula: the statement quantifies over the least period of the motion, so a solution must establish that a negative-energy orbit is periodic at all, and must identify and as the periapsis and apoapsis distances .
Trajectories are maps ℝ → EuclideanSpace ℝ (Fin 3), with ContDiff ℝ 2 smoothness and the standing hypothesis for all built into the definition of central force motion, together with . Time is all of : the trajectories considered are globally defined, so collision orbits are excluded by hypothesis rather than by a maximal-interval argument. Derivatives are Mathlib's deriv, so velocity and acceleration are the first and second derivatives of the trajectory.
Three conventions are worth flagging. First, the force is given by its radial profile rather than by a potential, avoiding any appeal to the junk value of a derivative at ; the Kepler case is the instance . Second, the swept area of K2 is the integral , which is the standard area element of the source written invariantly; the content of K2 is that this integrand is constant in time, so that the area depends on alone. Third, K1 asserts that the trajectory is contained in an ellipse; it does not assert that the particle traverses the whole ellipse, which is a separate (true) statement about periodic orbits.
The degenerate readings are ruled out explicitly. The eccentricity vector formulation of the conic is an equation holding at every time, not an existence claim at one time; the ellipse predicate carries , so a point or a segment does not qualify; and the hypothesis in K1 and in the conic milestone is necessary, since a radial trajectory satisfies every other hypothesis but lies on no ellipse.
Contributions of independent interest are welcome: a plane polar coordinate API for curves, uniqueness for the forced harmonic oscillator, and the classification of the loci into ellipse, parabola and hyperbola according to , , (this mission needs only the first case) would all be reusable well beyond this series.
Diffusion models in a bounded region need a rule for what happens when a path reaches the boundary. Two standard mechanisms are absorption, where the boundary kills the generator contribution, and oblique reflection, where a prescribed vector field pushes the process back into the region. Ethier and Kurtz treat these mechanisms as neighboring variants of the same uniformly elliptic model in Chapter 8, Section 1 of Markov Processes: Characterization and Convergence. The distinction is structural: the interior differential operator is shared, but its admissible generator graph changes with the boundary condition. This mission formalizes Theorems 1.4 and 1.5, retaining oblique reflection as the capstone and absorbed diffusion as the required related result.
Let be bounded, open, and connected, with . Its boundary is locally represented in orthogonal coordinates as the graph of a scalar function. The formal predicate C²,μ boundary regularity requires one positive chart radius valid at every boundary point, a connected local boundary patch, and a graphing function whose second partial derivatives satisfy the source's componentwise Hölder oscillation condition. The exponent obeys .
The diffusion coefficients are a symmetric positive-semidefinite matrix field and a drift field . Their entries satisfy the same local componentwise Hölder convention. Uniform ellipticity means that one satisfies
for every and every unit vector . For smooth , the interior operator is
Functions live on the compact closure as bounded continuous functions. Their ambient extensions are differentiated only at interior points. The second coordinate of each graph is itself continuous on the closure, so it records the boundary trace of rather than assigning an arbitrary value after differentiation.
Theorem 1.5 adds a reflection field whose components have C¹,μ boundary regularity. An outward unit normal is oriented by a local defining function that is negative precisely inside . Uniform obliqueness is the global lower bound
for one positive . The reflected graph requires a continuous derivative trace that agrees with in the interior and satisfies
The target asserts that the uniform closure of this graph is single-valued and is exactly the full generator of a positive strongly continuous contraction semigroup preserving the constant function one. The generator condition is a biconditional derivative limit, so it identifies the complete domain rather than only a convenient operator restriction.
Theorem 1.4 keeps the same smooth-region and ellipticity assumptions but uses the absorbed graph. Its continuous operator trace satisfies on the boundary. It has the same full generation conclusion: graph single-valuedness, a positive strongly continuous contraction semigroup, preservation of one, and exact identification of the generator. The absorbed zero trace is not imported into the reflected theorem, and the oblique derivative condition is not imposed on the absorbed graph.
These results connect a local elliptic expression and a geometric boundary condition to a global Markov evolution on continuous functions over the closed region. The conclusions contain more than existence of a semigroup: they determine the whole infinitesimal generator, ensure positivity and contraction, and retain the conservative convention used by Ethier and Kurtz. The paired statements make the effect of the boundary mechanism explicit while holding the interior model fixed.
The formal contribution is a machine-checkable statement layer, not a proof of the source theorems. It records the componentwise Hölder convention, uniform boundary charts, ellipticity, normal orientation, continuous derivative trace, the two distinct generator graphs, and every semigroup clause. These definitions can support later work on reflected processes, elliptic boundary problems, and martingale formulations without rebuilding the geometric conventions.
The main difficulty is simultaneous control of interior regularity, boundary geometry, and the closed generator domain. Pointwise obliqueness is insufficient: the source requires a uniform positive lower bound over the whole compact boundary. Likewise, merely writing for an arbitrary ambient extension would not supply a well-defined boundary derivative. The graph therefore carries a continuous derivative trace agreeing with the interior derivative. Replacing the biconditional generator equality by a one-way inclusion, or silently imposing the absorbed zero trace on the reflected graph, would weaken or change the source result.
The state space is EuclideanSpace ℝ (Fin (n + 1)) with 2 ≤ n + 1. Connectedness supplies nonemptiness. Matrix positive semidefiniteness supplies symmetry and nonnegative quadratic forms; a separate hypothesis gives strict uniform ellipticity. Local oscillation bounds apply within connected components of small intersections and do not compare different components.
The absorbed and reflected graphs use bounded continuous functions on closure Ω. The arbitrary zero extension outside the closure is never differentiated at a boundary point. The reflected boundary equation uses a continuous field of linear derivative maps, while the absorbed equation uses the continuous second graph coordinate. No vacuous region, pointwise-only ellipticity or obliqueness, weakened generator inclusion, proof-only theorem dependency, or synthetic theorem combining the two boundary mechanisms is admitted.
In 1985 R. S. Ward conjectured that "many (and perhaps all?) of the ordinary and partial differential equations that are regarded as being integrable or solvable may be obtained from the self-dual gauge field equations (or its generalizations) by reduction". The self-dual Yang–Mills (SDYM) equations are therefore often called the master integrable system: choosing a gauge algebra and a symmetry group to reduce by produces, on the one hand, the classical soliton equations and the Painlevé transcendents, and on the other — once infinite-dimensional gauge algebras are allowed — a family of third-order equations whose solutions have movable natural barriers and are therefore not of Painlevé type.
This mission formalizes the endpoint of one such reduction chain, as surveyed by Ablowitz, Chakravarty and Halburd, Integrable systems and reductions of the self-dual Yang–Mills equations, J. Math. Phys. 44 (2003) 3147–3173, Section V. Reducing SDYM to functions of a single variable gives the Nahm equations; taking the gauge algebra to be the divergence-free vector fields on turns them into a matrix flow which, after diagonalizing the symmetric part, becomes the generalized Darboux–Halphen system. Its trace is governed by the Chazy equation, written down by Chazy in 1909, and — this is the paper's historical observation — the Chazy equation is equivalent to the differential system Ramanujan derived in 1916 for the Eisenstein series , , . Chazy and Ramanujan worked on the same equation at nearly the same time and apparently did not know it.
Throughout, and are complex variables and all functions are complex-valued; a "solution on " means the stated derivative identities hold at every point of a set .
The classical Chazy equation is the third-order equation
The classical Darboux–Halphen system is the first-order system for
together with its two cyclic images. It arose in Darboux's study of triply orthogonal surfaces and was solved by Halphen. Its generalized form adds a term to each right-hand side, where and cyclically.
Ramanujan's system is
satisfied by , , , where .
Finally, the matrix flow obtained from the Nahm equations with the gauge algebra is
and the generalized Chazy equation with parameter is
If satisfy Ramanujan's system on a region of the punctured -plane, then
satisfies the classical Chazy equation on the preimage region. In particular is a solution of the Chazy equation, and knowing the general solution of Chazy gives the general solution of Ramanujan's system.
The milestone list covers the reduction chain in both directions: the matrix flow and its reduction to the Darboux–Halphen system (eqs. (51)–(54)), the first integrals (55), the passage from Darboux–Halphen to Chazy and back through the roots of a cubic, the symmetry (73) of the Chazy equation, Rankin's fourth-order equation for the discriminant cusp form, the change of variable between the two forms of Ramanujan's system, and the generalized Chazy equation (81).
The Chazy equation is the bridge between integrable systems and the theory of modular forms. Its particular solution makes the quasi-modularity of the second Eisenstein series an ODE statement; via it turns into Rankin's homogeneous fourth-order equation for the discriminant cusp form , whose Fourier coefficients are the Ramanujan -function. The action on solutions is exactly the weight-2 quasi-modular transformation law. In the other direction, the general solution of Chazy is a ratio of hypergeometric functions with a movable natural barrier, which is why these reductions are used as the standard counterexample to the identification of integrability with the Painlevé property.
None of this material is currently in Mathlib: there is no Chazy equation, no Darboux–Halphen system, no Ramanujan differential system, and no Eisenstein-series ODE. The mission builds that layer from scratch. Each statement is a closed-form differential identity, so the development is self-contained: it needs no analytic continuation theory, no modular-forms library, and no existence theory for ODEs. What a solver must supply is careful derivative bookkeeping and polynomial algebra.
Status honesty: every statement in this mission is a classical, published result — Darboux, Halphen, Chazy (1909–1911), Ramanujan (1916), Rankin (1956), and Ablowitz–Chakravarty–Halburd (1990s–2003). Nothing here is open mathematics. What is open is the machine-checked proof; to the captain's knowledge no formalization of these identities exists.
The obvious approach — "differentiate three times and call ring" — fails for two reasons. First, the statements are about functions, not about polynomials: each differentiation step requires producing the derivative of a product, a quotient, or a composition from the hypotheses, and only then is the resulting algebraic identity a ring problem. Second, two of the targets go against the flow of the hypotheses. Recovering the Darboux–Halphen system from a Chazy solution means recovering from the derivatives of the three elementary symmetric functions of the : this is a linear system whose matrix is a Vandermonde matrix in , invertible precisely because the roots are assumed distinct — which is why the distinctness hypothesis is not decoration. Similarly, the matrix milestone needs the conjugation-equivariance of , which holds for the transpose only because the conjugating matrix is complex orthogonal.
Everything is over , matching the paper. Solutions are represented pointwise on an arbitrary set rather than on all of , because the solutions of interest have movable singularities and natural barriers; no openness, holomorphy or connectivity is assumed unless a statement needs it.
Higher derivatives are carried as explicit extra function arguments joined by HasDerivAt hypotheses rather than through iterated deriv. This avoids junk values entirely: a statement never asserts anything about the value of a derivative that does not exist. The same convention is used for the matrix flow, where the derivative is imposed entrywise, so that no norm or normed-space structure on the space of matrices needs to be chosen.
Divisions are arranged so that no denominator can vanish under the stated hypotheses: Ramanujan's system is written in the form , with no division by ; the generalized Chazy equation carries the hypothesis ; and the first-integral and discriminant statements carry explicit nonvanishing hypotheses.
There is no trivializing formalization available here. Every statement is an implication between two systems of differential equations whose hypotheses are satisfied by the classical explicit solutions (, , for the Ramanujan system; Halphen's solutions for Darboux–Halphen), so none of them is vacuous, and none is an identity that holds for arbitrary functions.
A complete development needs only Mathlib's derivative calculus (HasDerivAt and its product, quotient and composition rules), Complex.exp, and Matrix.adjugate with the basic adjugate identities. Contributions of reusable pieces are welcome: in particular a clean statement of the derivative of the elementary symmetric functions of a triple of functions, and the Vandermonde inversion step, would both be of use beyond this mission.
Sums of independent random variables are well understood: Bernstein's inequality and its relatives give sharp, non-asymptotic tail bounds for whenever the are independent and light-tailed. Many quantities that arise in high-dimensional statistics and random matrix theory, however, are not linear but quadratic in an independent sample — the squared norm of a random vector after a linear transformation, a quadratic-form test statistic, the diagonal of a sample covariance matrix, or the number of edges cut by a random partition in a random graph. A quadratic form is a sum with dependent terms: and share the factor , so classical sum-of-independent-variables tools do not apply directly.
The Hanson-Wright inequality, first obtained by Hanson and Wright (1971) for sub-gaussian variables and later sharpened and popularized in this form by Rudelson and Vershynin (2013, "Hanson-Wright inequality and sub-gaussian concentration," Electronic Communications in Probability), closes this gap: it gives a concentration inequality for around its mean with the same two-regime (sub-gaussian near the center, sub-exponential in the tail) shape as Bernstein's inequality for linear sums. It is now a standard tool wherever quadratic statistics of independent data are analyzed: covariance estimation, compressed sensing, randomized numerical linear algebra, and the analysis of random matrices more broadly draw on it routinely.
Fix a probability space and let be a random vector whose coordinates are independent, mean zero, and sub-gaussian: each has a finite sub-gaussian (Orlicz ) norm , the smallest with . Write .
Let be an real matrix, with no constraint on its diagonal, and form the quadratic form
Two matrix norms measure the size of : the Frobenius norm (the Euclidean norm of 's entries) and the operator (spectral) norm (the largest singular value of ). Always , so the two norms can differ by a factor as large as — the gap between them is exactly what produces the inequality's two regimes below.
where is an absolute constant, not depending on , , , or . Stating the constant only as "some absolute " (rather than pinning it to a numeral) is deliberate: the book's own proof does not track a sharp value, and a goal that only asserts the shape of the bound survives any later improvement to .
The result itself. Hanson-Wright turns a two-dimensional (in ) dependency structure into a one-dimensional concentration statement controlled by two scalar quantities, and . This is what makes it usable: a practitioner bounding a quadratic statistic need only compute these two norms, not analyze the joint dependency structure of directly. It specializes to Bernstein's inequality (Chapter 2 of this book) when is diagonal, and it underlies non-asymptotic guarantees for covariance estimation, the Johnson-Lindenstrauss lemma via a different route, and the concentration of Lipschitz functions of sub-gaussian vectors.
Formalizing it. The published proof of Hanson-Wright is not a single argument but a chain of four steps: a decoupling reduction (Section 6.1), a direct computation for Gaussian chaos (Lemma 6.2.2), a comparison lemma extending the Gaussian bound to general sub-gaussian vectors via a replacement trick (Lemma 6.2.3), and a final assembly that separates the diagonal part (handled by Bernstein's inequality) from the off-diagonal part (handled by decoupling and comparison). This mission formalizes the goal theorem's statement and the first, most reusable link in that chain — the decoupling machinery of Section 6.1, which reduces the analysis of the dependent chaos to the independent-once-conditioned bilinear form — together with the chapter's separate contraction principle (Section 6.7), a general comparison tool for Rademacher-weighted sums used repeatedly in the book's later chaining chapters. The Gaussian MGF computation and the replacement-trick comparison lemma (Lemmas 6.2.2–6.2.3) are left as future milestones on top of this mission: they require Gaussian rotation invariance and the singular value decomposition of , substantially more machinery than the milestones included here.
The obvious first idea — treat as if it were a sum of independent terms and apply Bernstein's inequality termwise — fails immediately: the terms for fixed are not independent across , since they all share the factor . Decoupling (Theorem 6.1.1) is the non-obvious fix: it replaces the off-diagonal chaos by a bilinear form in an independent copy , which genuinely does become a sum of independent terms once one of the two vectors is conditioned on. The price is a universal constant factor of and the restriction to diagonal-free matrices, which is exactly why the full Hanson-Wright proof must separate the diagonal contribution to (handled directly by Bernstein's inequality, Chapter 2) before decoupling can be applied to what remains.
Random variables and vectors are real-valued on an explicit probability space . The sub-gaussian norm is HighDimProb.Concentration.subgaussianNorm, the
Orlicz--norm definition already published for this series (01-concentration), reused
here as a reference item rather than redefined. is written as a
finite supremum over the coordinate index, ⨆ i, subgaussianNorm P (X i); because the index
type is always a Fintype (Fin n), this supremum is well-defined and, at the degenerate index
, reduces to a true (if content-free) instance of the inequality rather than a vacuous or
false one. The Frobenius and operator norms of are this mission's own frobeniusNorm and
opNorm, stated directly from their defining formulas rather than through Mathlib's scoped
matrix-norm typeclass instances, which are deliberately not global defaults (to avoid a diamond
between the two norms) and so are unsuitable for a statement that needs both simultaneously.
Every place the goal or a milestone integrates a quantity, that quantity is required
Integrable, guarding against Mathlib's convention of returning 0 for the Bochner integral of
a non-integrable function — without these hypotheses, a mean-zero or expectation hypothesis
could hold vacuously, or a conclusion could hold trivially, for reasons having nothing to do
with the book's mathematics.
The formalization deliberately does not restrict 's diagonal in the goal theorem: doing so would collapse Hanson-Wright to a restatement of Bernstein's inequality for the special case of a diagonal matrix, discarding the chapter's actual content, which is handling the off-diagonal, genuinely quadratic dependence between coordinates. The diagonal-free restriction does appear, correctly, in the Decoupling theorem (6.1.1), whose proof needs it.
Reusable beyond this mission: frobeniusNorm and opNorm are needed by any future chapter
using matrix norms (Chapter 4's random matrix norms, Chapter 9's matrix deviation inequality);
the decoupling theorem and convex decoupling lemma are the standard entry point for any later
formalization of chaos concentration; the contraction principle is reused throughout the book's
chaining chapters (7 and 8). Welcome contributions include the Gaussian MGF and comparison
lemmas (6.2.2–6.2.3) needed to complete a full proof of the goal theorem, and the two-sided
version of Bernstein's inequality needed for the diagonal part of that proof.
A recurring question in high-dimensional statistics is how tightly a scalar quantity built from many random inputs concentrates around its mean, even as the number of inputs grows without bound. Two classical answers organize the whole toolkit: martingale methods, which control a sum of dependent increments one conditional step at a time, and Gaussian-specific isoperimetry, which shows that essentially any regular (Lipschitz) function of a high-dimensional Gaussian vector concentrates as tightly as a single Gaussian coordinate, regardless of dimension. This mission formalizes one representative theorem from each line: the general martingale Bernstein bound (Wainwright, High-Dimensional Statistics, 2019, Theorem 2.19) and the Gaussian concentration of Lipschitz functions (Theorem 2.26), following Chapter 2 of the same book.
A random variable with mean is sub-Gaussian with parameter (Definition 2.2) if for all ; it is sub-exponential with parameters (Definition 2.7, a strictly milder condition) if the same bound holds only for , with the convention so that recovers the sub-Gaussian case exactly.
A sequence , adapted to a filtration , is a martingale difference sequence if each is -measurable and . Such sequences arise throughout statistics via the Doob martingale construction: given a function of independent variables , setting telescopes to , converting a deviation question about into a martingale concentration question.
A function is -Lipschitz with respect to the Euclidean norm if for all (Eq. (2.38)).
Let be i.i.d. standard Gaussian and be -Lipschitz with respect to the Euclidean norm. Then is sub-Gaussian with parameter at most , and hence
The bound is dimension-free: it depends on only through 's Lipschitz constant, not the ambient dimension itself.
For any differentiable and convex , for independent — the interpolation identity Theorem 2.26's proof is built on.
Given a martingale difference sequence with a per-index sub-exponential conditional moment-generating-function bound for , the sum is itself sub-exponential with parameters , and satisfies the two-regime concentration inequality of Eq. (2.28): sub-Gaussian for small deviations, sub-exponential for large ones. This is the chapter's central general-purpose martingale concentration tool.
Theorem 2.19 is the source of two of the most-cited concentration inequalities in the field —
the Azuma–Hoeffding inequality (Corollary 2.20) and the bounded-differences/McDiarmid
inequality (Corollary 2.21), both already faithfully covered elsewhere on the platform
(azuma_hoeffding_two_sided, bounded_diff_martingale_two_sided) and included here as
kind: reference milestones rather than redrafted. Theorem 2.26's Gaussian Lipschitz
concentration is separately significant: it is the tool behind dimension-free operator-norm
bounds for random matrices, concentration of the empirical spectral distribution, and much of
the machinery of Chapters 5 and 6 of the same book.
Formalizing it. No faithful prior art exists on the platform for either the martingale
Bernstein bound or Lipschitz-Gaussian concentration itself (a fresh search for "martingale
Bernstein," "sub-exponential martingale," "Gaussian interpolation," and "Lipschitz
concentration" returned no hits; the existing Vershynin-book item
HighDimProb.Isoperimetry.lipschitz_concentration_sphere concentrates a Lipschitz function on
the sphere, a different underlying space and a different proof from Theorem 2.26's Gaussian
vector). Both goal-adjacent theorems and the Gaussian interpolation lemma are drafted here as
open goals (:= by sorry); the two Azuma–Hoeffding/bounded-differences corollaries are reused
from the platform's existing, already-proved formalizations.
The naive approach to Theorem 2.26 — try to bound directly via a Lipschitz-type argument in — has no obvious route to a dimension-free bound, since a union bound over coordinates (or over an -net of the domain) picks up a factor that grows with . The resolution, Lemma 2.27's interpolation identity, instead exploits a special structural fact about the Gaussian distribution — its rotation invariance — to replace the nonlinear quantity with the linear, and hence exactly computable, Gaussian quantity , at the mild cost of a non-optimal constant. Theorem 2.19's difficulty is bookkeeping rather than a conceptual obstruction: the recursive conditioning step (Eq. (2.29)) must be iterated exactly times while keeping track of the interplay between the two parameters per difference, and Proposition 2.9's two-regime tail bound (small-deviation sub-Gaussian behavior, large-deviation sub-exponential behavior) must be carried through unchanged into the final statement — dropping either regime understates what the theorem proves.
Expectations are Bochner integrals against an explicit probability measure, with integrability
required as an explicit hypothesis in IsSubGaussian and IsSubExponential (Mathlib's Bochner
integral silently returns for a non-integrable function, which this mission's definitions
rule out as a trivializing formalization). The sub-exponential condition's domain restriction
|λ| < 1/α is realized as the disjunction α = 0 ∨ |λ| < 1/α, since Lean's real division
convention 1/0 = 0 is exactly backwards from the book's own stated 1/0 = +\infty convention
for the degenerate sub-Gaussian case.
" independent" (Lemma 2.27, Theorem 2.26) is formalized via Mathlib's
HasGaussianLaw predicate together with explicit coordinatewise mean-zero and
identity-covariance hypotheses, which together pin down the standard multivariate normal law,
plus IndepFun. The inner product is realized as
fderiv ℝ f (X ω) (Y ω), the Fréchet derivative applied to — equal to
by the Riesz representation of the gradient on a
Hilbert space, avoiding the need to separately construct a gradient vector field.
Theorem 2.19's printed parameter pair for part (a), "," is formalized
as : Definition 2.7 parametrizes the sub-exponential MGF bound
by (with appearing in the exponent), so a literal transcription of the printed
pair's first entry would silently square the effective parameter and make part (a), read
literally, inconsistent with part (b)'s own tail-bound formula (which the book derives from
part (a) via the general sub-exponential tail bound, Proposition 2.9). The corrected pairing is
the one the book's own proof actually establishes; see MODERATION_NOTES.md for the full
derivation.
Out of scope for this mission: Proposition 2.5 (plain Hoeffding for a sum of independent sub-Gaussians), used in the book only as background for Theorem 2.26's proof and not redrafted, since the goal theorem's own statement does not depend on it once Lemma 2.27 is in hand.
Every algorithm in the first three chapters of Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making — ε-Greedy and UCB for the multi-armed bandit, Inverse Gap Weighting and SquareCB for contextual bandits — is a special case of the same two-step recipe: estimate a model of the world with an online regression oracle, then convert the estimate into a decision that trades exploration against exploitation. Chapter 4 asks whether this recipe can be made generic: given any structured decision-making problem, specified only by a function class and a decision space , is there a single quantity that governs the best achievable regret, the way governs the multi-armed bandit and governs the linear bandit? The chapter's answer is the Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian, and Rakhlin [40] as a complexity measure that both upper- and lower-bounds achievable regret for a general decision-making protocol, unifying results that were previously proved from scratch, case by case, for each structured setting. This mission formalizes the chapter's central upper bound (Proposition 13) together with the machinery that makes it computable in two concrete cases — the multi-armed bandit (Proposition 14) and the linear bandit (Propositions 16–17).
Fix a finite decision space and a class of candidate mean-reward functions, with a ground-truth (realizability). Over rounds, at each round the learner observes an estimate produced by an online regression oracle, plays a decision distribution (possibly depending on and the history), and the regret is
where . The oracle's cumulative estimation error is assumed bounded: with probability at least (Definition 7). Writing , the DEC game value at a reference model and scale is the min-max quantity
and the DEC of itself is . The Estimation-to-Decisions (E2D) algorithm plays, at each round, a certifying (i.e. attaining or beating) the value of this min-max game at .
with probability at least , for any exploration parameter . This is the weakest stable statement the chapter proves about E2D: it holds for an arbitrary function class and an arbitrary regression oracle, with no structural assumption on beyond realizability, and the chapter's later sections instantiate it rather than strengthen it.
The Decision-Estimation Coefficient is, in the book's own words, "the main result" of this line of work: Foster, Kakade, Qian, and Rakhlin [40] show it is not merely an upper bound but (in a suitable localized form, developed further in Chapter 6) a tight characterization of the minimax regret for structured bandits and, more generally, for the interactive decision-making protocol the rest of the book studies. Proposition 13 is the mechanism that makes this useful in practice: it reduces regret analysis for a new structured problem to a single, purely convex-analytic computation of , in place of a bespoke exploration argument. Propositions 14–17 are the demonstration that this reduction is not vacuous — they recompute, via the DEC alone, the two rates (multi-armed and linear bandit) that earlier chapters of the book derived by direct, setting-specific arguments, and the match is exact. Formalizing this chapter therefore captures the book's unifying abstraction itself, not just one more instance of it. No formalization of the Decision-Estimation Coefficient, in any form, currently exists on the platform (see Formalization scope).
The obvious formalization mistake is to state Proposition 13's conclusion with left as an unconstrained free real-number parameter satisfying only the inequality the theorem asserts — a formalization under which the "theorem" would be a triviality about an arbitrary real number, since nothing about the actual min-max game would ever be checked. The chapter's content is precisely the opposite: that this specific minimax quantity can be computed (Proposition 14) or bounded via a concrete strategy (Proposition 17), and — as Chapter 6 shows for a lower bound outside this chunk's scope — that no smaller quantity would do. A second difficulty is proof-theoretic rather than notational: the book's own proof of Proposition 13 bounds regret by an unconstrained supremum over all reference functions , and only identifies this with the official, -restricted of Eq. (4.16) via Proposition 24 — a fact stated on p. 80, outside this chapter's numbered range, whose own proof the book defers to an exercise. A formalization that quietly imports Proposition 24 to close this gap would rest the goal theorem on an unverified fact; this mission instead states the hypothesis the book's own text uses to motivate restricting to in the first place (online estimation algorithms produce ), so the goal is faithful to what is actually established within the chapter's own pages.
Every item fixes a finite decision space (Fin A, Fin n, or a generic Fintype S)
and states the DEC as the literal sInf-of-sSup transcription of the min-max game
(Eqs. (4.15)–(4.16)), never as an opaque bound — this is the trivializing
formalization the chunk's own reading of the chapter rules out (see Difficulty).
piStar : (S → ℝ) → S is a hypothesized global maximizer selector throughout,
constrained to be a genuine argmax only on the function class in scope (F or
Set.univ), matching how the book treats as a fixed but arbitrary
tie-breaking choice. The goal theorem (Proposition 13) adds the explicit hypothesis
hfhat : ∀ t, fhat t ∈ convexHull ℝ F, replacing an appeal to the out-of-range
Proposition 24 (see Difficulty); this is the one place this mission's statement is not
a line-by-line transcription of the book's own displayed proof steps, and it is
recorded here and in MODERATION_NOTES.md. Proposition 14's and Proposition 17's
are replaced by the explicit constants the book's own proofs establish
( exactly, and respectively — the latter obtained
by summing the three terms the proof of Proposition 17 isolates). Proposition 14's
Lean statement splits the book's single equality into an upper bound on the literal decGf, a lower bound restricted
to full-support distributions, and IGW's own exact game value, because the book's
min over the whole simplex is not provable as a literal Lean equality: a
distribution with a zero-weight arm makes the inner supremum genuinely unbounded, and
Lean's total Real.sSup returns a junk value smaller than there
(caught in moderation, MODERATION_NOTES.md); the three-conjunct statement recovers
exactly the book's real content without asserting that false literal equality. Lemma 9
is restated
inside FoundationsRL.Structured rather than imported from the Chapter 2 mission,
since draft items across chunks cannot import one another; its source citation still
points to its original location (p. 32). Proposition 16 is not drafted: the
platform's existing BanditAlgorithm.kiefer_wolfowitz_equivalence (Lattimore &
Szepesvári, Theorem 21.1) states the identical existence claim — compact set with
full-dimensional span, a design with G-value at most — as one clause of a larger
equivalence, and is reused as a reference item rather than redrafted. Proposition 22
(primal/dual DEC equivalence, §4.4) is deliberately excluded: the book states it "under
mild regularity conditions" it does not pin down in the statement itself, which is
exactly the kind of unquantified hypothesis this series' faithfulness standard
excludes from a goal or milestone. Contributions extending this mission with Chapter
6's lower bound (matching from below, establishing tightness)
or with a formalization of Proposition 24 itself (removing this mission's hfhat
hypothesis) are welcome.
The magic-square programme already on this platform works at fixed small orders: MacMahon's enumeration of the squares, both the magic count and the semi-magic count ; the classification of the normal squares; and the counts of the panmagic and symmetric order-three classes. Each of those is a statement about a single order. This mission changes the axis: it asks what the counting function does when the order itself is allowed to vary.
Timeline.
That split is the point of the mission, so it is worth naming before anything is proved. A quasi-polynomial of degree and period agrees with a degree- polynomial on each residue class modulo , the polynomials differing between classes; a polynomial is the case . For the magic squares the values do depend on modulo a period — at order three vanishes unless — and the same is true of every other class. For it never happens.
An semi-magic square of line sum is an array of nonnegative integers in which every row and every column sums to . Entries may repeat, and no condition is placed on the diagonals. Write for the number of such arrays.
In Lean the array is a Square n ℕ, that is, a Matrix (Fin n) (Fin n) ℕ; the condition is IsSemiMagic M t, which asks every rowSum and every colSum to equal t; and the counting function is semiMagicCount n t, the cardinality of the finset of all arrays over Fin (t + 1) satisfying IsSemiMagic. Restricting the entries to Fin (t + 1) loses nothing, since an entry of a square of line sum is at most .
Dividing by turns such an array into a doubly stochastic matrix, a nonnegative real matrix whose every row and column sums to . So is equally the number of lattice points in the -fold dilation of the Birkhoff polytope . Two geometric facts about are what the mission is about. Its dimension is : the entries satisfy line equations, exactly one of which is dependent. Its vertices are the permutation matrices, by the Birkhoff–von Neumann theorem, hence integral. The mission states that both facts are visible in the arithmetic of .
This is Theorem 1 of [BCCG 2003], stated there for . It is the shape of the truth, not a closed form, so no later improvement of the explicit formulas can invalidate it. The three parts are not independent: the degree is the dimension of , and the two identities are the reciprocity law for lattice-point counting, applied to .
The goal is far from the easy cases, and the mission is laid out so that each rung is an independently provable statement.
MagicSquares.semi_magic_count_two () and MagicSquares.semi_magic_count_three (MacMahon's ). Included as references, not as targets.Its leading coefficient is and its normalised volume is .
The result itself. The theorem makes the semi-magic squares countable in closed form at every order, and it is why the semi-magic count can be tabulated as a polynomial while the magic, symmetric and pandiagonal counts cannot: a polynomial is determined by finitely many values, a quasi-polynomial is not without knowing its period. The reciprocity identities are the same statement seen from the interior of , which is why they are what pins an explicit polynomial down once its degree is known. The order-four polynomial above was verified against direct enumeration on seventeen values of ; that verification is evidence, not proof, and is recorded because the general statement is what has to be proved.
Formalizing it. The theorem has been known since 1973 and has had an elementary proof since 1980; what does not exist anywhere is a machine-checked proof. Mathlib contains no Ehrhart theory, no quasi-polynomial machinery and no rational-generating-function toolbox — the string "Ehrhart" does not occur in it — so a formalization must construct its own lattice-point-counting argument for this family of polytopes, or find an elementary route that avoids polytopes altogether. Either outcome is reusable: the same absence blocks the quasi-polynomial counts , and of BCCG's Theorem 2, which the earlier missions approach only at order three.
The first idea anyone has is to interpolate: compute for enough values of and fit a polynomial. That works, and it is how the order-four rung was produced, but it cannot prove the general statement: the degree is what is being asserted, so the number of values needed is not known in advance, and with itself a variable no finite computation settles it. Interpolation is legitimate as a target at order four; it must not be mistaken for a route to the goal.
The second idea is to import the geometry as a black box: a rational polytope dilated by has a counting function that is a quasi-polynomial of degree equal to its dimension, with period dividing the least common multiple of the vertex denominators. That is Ehrhart's theorem, and it is the textbook route. It is not available here, and reconstructing it in general is a larger project than this mission; the statements the mission asks for are the ones that survive without it.
The part of the goal with no counting interpretation at all is the second line. is defined on ; the assertion that a polynomial agreeing with it there vanishes at and satisfies is a statement about the interior of the polytope, and it cannot be read off from the combinatorial definition. A solver who proves only the polynomiality and the degree has not finished the goal.
The formalization commits to the following conventions.
semiMagicCount n t, the Finset.card of the arrays over Square n (Fin (t+1)) satisfying IsSemiMagic. Entries are natural numbers, not integers or reals.ℚ and is quantified existentially. Negative arguments are handled by casting the integer into ℚ and evaluating there; Polynomial.eval₂ is unusable for the reciprocity, since it would need a ring homomorphism , which does not exist.p.natDegree = (n - 1) ^ 2, with natural-number subtraction, which makes the case harmless rather than degenerate.1 ≤ n is carried explicitly although the statement is meaningful at ; it matches the source.∀ t by a finite range of values, or replacing semiMagicCount by a smooth surrogate, would make the statement easy and empty. The universal quantifier over and the exact value of natDegree are what give the goal its content.Reusable beyond this mission: any development of lattice-point counting in the Birkhoff polytope, of dilations of rational polytopes, or of quasi-polynomials. The vocabulary of the programme (MagicSquares, MagicSquaresPandiagonal, MagicSquaresMostPerfect, MagicSquaresTransforms, MagicSquaresNormal3) is shared with the earlier missions and is included as reference items rather than redefined.
The real Clifford algebra is the smallest Euclidean Clifford algebra whose full structure carries a nontrivial multiplicity-eight representation-theoretic decomposition, and it has become a recurring object in programs that build internal gauge and family structure from Clifford generators rather than imposing it by hand. Within such programs, the single most basic representation-theoretic question one can ask about the algebra is: how does a distinguished subalgebra, acting by the adjoint action, decompose the odd part of the algebra as a representation?
This mission answers that question exactly, for the specific triple of bivectors built on the index set . The computation was carried out structurally (by splitting active indices from spectator indices) in the LeanProofs research program in 2026 and recorded with exact multiplicities; no machine-checked proof exists yet. The purpose here is to close that gap: the result is finite-dimensional linear algebra, completely within reach of a Lean 4 + Mathlib development, and every constant in it is explicit.
Fix with its standard inner product and the associated quadratic form , and let be the real Clifford algebra generated by symbols with
The algebra is -graded in the usual sense: it is the direct sum of its grade- subspaces, spanned by products of distinct generators, of dimension . The odd sector is the linear span of the odd grades,
On it, register three bivectors and their halved adjoint actions:
where . The triple satisfies the relations and cyclic permutations, so the generate a copy of with cyclically. The associated quadratic Casimir is the endomorphism
Because each is even, every preserves the odd sector, and so does .
the two eigenspaces spanning the whole odd sector. Equivalently, as a representation of the generated ,
eight copies of the spin-1 module and eight copies of the trivial module. The goal deliberately asserts only the eigenspace dimensions and their spanning property — the decomposition shape — not any particular basis or pairing.
the three weight spaces spanning the sector. This refines the goal: each copy contributes weights and each copy contributes weight .
The result itself. The spectrum pins down exactly how an acting from inside the algebra sees the odd sector: not irreducibly, but as a clean multiplicity split between spin-1 and spin-0. In the LeanProofs program this decomposition is load-bearing for everything downstream that distinguishes "active" indices from "spectator" indices — the multiplicity is the number of spectator degrees of freedom, and its appearance in the spectrum is what makes the split structural rather than coincidental. The weight decomposition further identifies the Cartan grading and is the natural first test case for any technology that must eventually handle larger Clifford algebras or other subalgebras.
Formalizing it. The computation is proved (structurally, by hand, in the research record) but not machine-checked. Everything needed lives in Mathlib: CliffordAlgebra, its grading CliffordAlgebra.evenOdd, Submodule, LinearMap, Module.finrank. What the mission produces is a fully verified finite spectral computation inside Clifford algebra — a reusable certificate that the platform's Clifford and grading infrastructure supports exact representation-theoretic bookkeeping, not just algebraic identities.
The obstruction is bookkeeping, not ideas. The natural attack — split indices into active and spectator , decompose as a tensor product of graded pieces, and read off the multiplicity from the spectator sector — requires transferring the action across such a tensor decomposition, which Mathlib does not provide ready-made for Clifford algebras. A purely computational route (fix the 64-element blade basis, build the matrices of the explicitly, compute kernels) is straightforwardly correct but laborious; making it readable is the real work. The statement is stated through arbitrary endomorphisms bound pointwise to the halved adjoint actions precisely so that solvers may choose either route.
The mission commits to: the quadratic form Q60 as QuadraticMap.weightedSumSquares ℝ (fun _ : Fin 6 => 1); generators e6 i = CliffordAlgebra.ι Q60 (Pi.single i 1); the odd sector as the Mathlib-native CliffordAlgebra.evenOdd Q60 1; and the registered triple as products of two generators. All theorems quantify over endomorphism witnesses bound pointwise to , so no particular matrix realization is privileged. Spectra are stated as eigenspace decompositions with exact Module.finrank multiplicities — never as pointwise eigenvalue claims, which would be false for mixed vectors. No trivializing formalization exists: the multiplicities are hard constants, and the dimension gate (32) rules out statements about degenerate sector choices. The definition file is reusable for any future mission on ; the su(2) relations and dimension gate are self-contained milestones. Contributions of either a structural (active/spectator split) or computational (explicit blade basis) proof are equally welcome.
Mathlib.LinearAlgebra.CliffordAlgebra.Grading (the evenOdd grading used as the odd sector).A robust counterpart draws a hard line. Inside the uncertainty set the constraint must hold; outside it, nothing is promised — and in a real problem the perturbation does sometimes land outside. Chapter 3 answered this for linear problems with the globalized robust counterpart: keep the constraint exactly on the normal range , and let it degrade at a controlled rate outside, proportionally to the distance from . That mission published Proposition 3.2.1, which says the GRC of an uncertain linear inequality is equivalent to two ordinary robust counterparts.
Chapter 11 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (Princeton, 2009) does the same for conic constraints, and the move is not routine. The left hand side of a conic constraint is a vector, not a scalar, so "the constraint is violated by at most " has no direct meaning. What replaces it is the observation that a scalar inequality is the inclusion , and that the violation is the distance from the left hand side to . In that form the notion lifts verbatim, and the whole chapter follows.
Definition 11.1.2. Consider an uncertain convex constraint
with nonempty, closed and convex. Let the perturbation space split as , each factor carrying a normal range , a closed convex cone and a norm , and let be a norm on . A candidate is robust feasible with global sensitivities if
where and .
The object that makes the analysis work is the recessive cone of (Definition 11.3.1): for any ,
which does not depend on and is a nonempty closed convex cone.
A candidate is feasible for the GRC (11.1.6) if and only if it satisfies the system
Line (a) is the ordinary robust counterpart over the normal range. Each line (b) is a bounded semi-infinite constraint — the perturbation ranges over the unit ball of a cone, not over an unbounded set — measuring the distance to the recessive cone rather than to itself.
The goal is the chapter's structural result and it does exactly what Proposition 3.2.1 did one level down: it converts a single semi-infinite constraint over an unbounded perturbation set into a robust counterpart over the bounded normal range plus finitely many constraints over unit balls. That matters because every tractability result of Chapters 6 to 9 is about bounded uncertainty sets; without the decomposition none of them applies to a GRC.
The two halves of the decomposition are genuinely different objects. Line (a) is familiar. Lines (b) are not: they measure the distance from a linear image of a ball to the recessive cone, and that is the function
of §11.4, which is almost a norm on linear maps — nonnegative, positively homogeneous, subadditive, but neither symmetric nor strictly positive. Proposition 11.4.1 says this function is self-dual in the precise sense that of a map with respect to a setup equals of the adjoint map with respect to the dual setup: dual norms, dual cones, source and destination exchanged. That single identity is what lets every bound on be computed on whichever side of the duality is tractable, and it is the engine of §11.4's tractability results.
The recessive cone results are the vocabulary. The one that earns its place is : the conic sets of this book are all of that form, so it says the recessive cone of every constraint in sight is computed by deleting the constant term.
The goal is an equivalence and the two directions are asymmetric.
Forward — GRC implies the system — is where the recessive cone is discovered rather than used. Fix and in the unit ball of , and run out along the cone. The GRC bounds the distance to by , so there are with ; the rescaled points stay bounded, and a limit point of them lies in by the limit characterization of the recessive cone. This is a genuine compactness argument, and it is why the recessive cone — not — is what appears in lines (b).
Backward is a decomposition-and-assemble: split each with , realizing the distance, get a point of from line (a) and a recession direction from each line (b), and add them — using that .
Proposition 11.4.1 is a chain of polarity identities: the polar of is for compact convex containing the origin, the polar of a norm ball of radius is the dual-norm ball of radius , and bipolarity. Each step is standard and the composition is not.
Built on the module published by the third mission of this series, which carries the linear-case globalized robust counterpart and the dual cone. New here: norms as functions with their defining properties, dual norms, the two distances, the recessive cone, the conic GRC, and the function .
Conventions committed to:
IsNormOn bundles definiteness, absolute homogeneity and the triangle inequality, and
nonnegativity follows from them.Erlang's formula, the subject of mission I of this series, sizes a single telephone link. Real networks are not single links: a call occupies a circuit on every link of its route simultaneously, and it is lost unless every one of those links has a free circuit. That is the loss network, the model of Chapter 3 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), and it describes not only circuit-switched telephony but any system in which a request must acquire several resources at once or be refused: wavelength assignment in optical networks, radio channel allocation under interference constraints, slot booking, and admission control generally. The term used in those application areas is circuit-switched: before a request is accepted it is checked that enough resource is available for each stage of it.
The exact equilibrium distribution of a loss network is known and has product form. It is also useless for computation — its normalizing constant is a sum over the feasible states, and for a general resource matrix computing it is NP-hard. What practitioners use instead is the Erlang fixed point: pretend the links block independently, so that the traffic offered to link is the traffic on the routes through it thinned by the blocking probability of every other link on each route, and then apply Erlang's formula link by link. The result is a system of coupled copies of Erlang's formula. The chapter's aim, in its own words, is to give insight into why that approximation works as well as it does; the first step is to show that it is well posed at all.
The links are , link carrying circuits. A route belongs to a set of routes, and the link-route incidence matrix records how much of each link a route needs: a call on route requires circuits from link and is lost if any link has fewer than free. (The classical case is a – matrix and exactly when ; from section 3.3 the book allows any non-negative integers.)
Calls requesting route arrive as a Poisson process of rate , independently across routes, and hold their circuits for an exponentially distributed time of unit mean. Writing for the number of calls in progress on route , the process is Markov on
and is called a loss network with fixed routing.
Write for Erlang's formula, , published in mission I of this series. The Erlang fixed point equations are
The factor removes link 's own thinning from the product, so in the – case the argument is , the reduced load offered to link .
The goal fixes no formula for and no rate of convergence: it asserts only that the approximation the field has used since the 1960s names a single, well-defined object. Existence alone is a short argument from Brouwer's theorem, since (3.7) defines a continuous self-map of the compact convex cube ; uniqueness is the substance.
The exact theory that the fixed point approximates: Lemma 3.4 on truncating a reversible process; the uncapacitated network as an instance of the open migration product form of mission II; equation (3.3), the exact equilibrium distribution on ; and the acceptance probability . Then the optimization side: that and the utilization are strictly increasing in , which is what makes the revised dual objective strictly convex; and Theorem 3.10, that a minimizer of the Dual problem (3.5) over the positive orthant satisfies the conditions on , equation (3.6).
The result itself. Without Theorem 3.20 the phrase "the Erlang fixed point" is not well formed, and neither is any engineering procedure that computes one — repeated substitution converges to a solution, and damped iteration is guaranteed to converge to one, but "the blocking probabilities predicted by the reduced-load approximation" names a unique vector only because of this theorem. The proof is also the interesting part: the fixed point equations are re-read as the stationary conditions of a strictly convex minimization, the revised dual (3.8), which is the Dual problem (3.5) of the maximum-probability analysis with its linear term replaced by . That connection is what later lets the book prove the approximation asymptotically exact in a limiting regime: Corollary 3.22 says the Erlang fixed point converges to the vector coming from the maximum-probability problem.
Formalizing it. Nothing here is open. What the mission produces is the loss network model in
Lean — state space, truncated rates, normalizing constant, incidence matrix — and a machine-checked
statement of the object the reduced-load approximation computes. It is also where this series'
earlier missions pay off: the uncapacitated network is literally the open migration process of
mission II with , , , and the exact distribution
(3.3) is its truncation by Lemma 3.4 to the feasible set, using the DetailedBalance layer of
mission I. Mathlib has no loss network theory and no Erlang formula beyond what mission I
published.
Existence of a fixed point is easy and is not where the difficulty lies. Uniqueness resists every direct attack: the map defined by (3.7) is not a contraction in any obvious metric, its monotonicity structure is not the kind that forces a unique fixed point, and iterating it undamped can cycle. The book's route is indirect — exhibit a strictly convex function whose stationary conditions are exactly (3.7) — and finding that function is the whole content. Its strict convexity comes from a monotonicity fact about Erlang's formula, that the utilization is strictly increasing in , which is itself a milestone here.
A second, formal difficulty: the equations involve , so a solution with would be meaningless. It is worth checking before starting that no such solution exists for , rather than assuming it.
Routes and links are indexed by finite types, the incidence matrix has natural-number entries (the general case of section 3.3, not only –), capacities are natural numbers, and arrival rates are positive reals. The feasible set is a subset of the state space, and a truncated process is the rate matrix restricted to that subset — which is exactly the book's truncation, since a transition leaving the set simply has no target.
Conventions: holding times have unit mean throughout, matching the book, so the departure rate from route is and no separate service-rate parameter appears. Normalizing constants are introduced through summability hypotheses that assert convergence and the value together, rather than as possibly-infinite quantities; is the reciprocal of the sum in the book's notation. Capacities are assumed at least in the goal: a link with no circuits blocks everything, identically, and the factor would then be undefined rather than merely large.
The goal cannot be satisfied trivially: it is a uniqueness statement, so a vacuous or degenerate reading would have to produce no solution, and existence is half of what is asserted.
Contributions welcome beyond the listed items: the Brouwer argument for existence of a solution to the – equations (3.1) of section 3.2; the utilization function and the revised dual (3.8); the central limit theorem 3.14 and Corollary 3.17; Lemma 3.21 and Corollary 3.22 on the limiting regime; and the diverse-routing models of section 3.7.
Consider a decision maker who must choose, at each of rounds, between two actions on the advice of "experts," none of which is known in advance to be reliable. This is the prediction-from-expert-advice problem, introduced by Littlestone and Warmuth [Littlestone & Warmuth, The Weighted Majority Algorithm, FOCS 1989/Inf. Comput. 1994] and generalized to real-valued losses by Freund and Schapire's Hedge algorithm [Freund & Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, JCSS 1997]. It is one of the two founding problems of online learning (the other being universal portfolio selection, also introduced in this book's first chapter) and the historical origin of the multiplicative-weights update method, later recognized as a single algorithmic idea underlying results across game theory, optimization, and computational complexity [Arora, Hazan & Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 2012]. This mission formalizes the chapter's three central guarantees: a matching deterministic lower bound, the Weighted Majority mistake bound, and Hedge's loss bound — the earliest instance, in the book's own development, of the "online convex optimization" phenomenon that its later chapters generalize to arbitrary convex losses.
At each round , a decision maker chooses one of two actions, or . After the choice, the true outcome for that round is revealed, and any action that disagrees with it is charged a mistake. experts also each commit to a prediction every round, and the decision maker may consult their record.
The Weighted Majority (WM) algorithm maintains a weight for each expert , initialized to . It predicts whichever action currently carries at least half the total weight, and after seeing the outcome, multiplies the weight of every expert who erred by for a fixed parameter , leaving correct experts' weights unchanged. denotes the algorithm's own mistake count through round , and expert 's.
The Randomized Weighted Majority (RWM) algorithm uses the same weights, but instead of following the majority it samples an expert with probability proportional to its weight, , and follows that expert's prediction; is its expected mistake count.
Hedge generalizes further, from binary mistakes to arbitrary non-negative real-valued losses suffered by expert at round . It samples expert with probability from weights updated multiplicatively in the loss, . Writing losses and the mixed strategy as vectors, the algorithm's expected loss at round is .
where . This is the chapter's most general result and the one the book reuses later on; it leaves free (no asymptotic tuning), so it survives whatever later chapters do with .
Theorem 1.1 shows the mistake-bound question has no trivial answer: even against only two
maximally simple experts, any deterministic strategy is beaten by a factor of by an
adversary who knows its code. Lemmas 1.3 and 1.4 show this factor is essentially removable —
first by relaxing "guarantee" to "guarantee in expectation" (RWM halves the deterministic
penalty from to ), then Theorem 1.5 removes the
binary-mistake restriction altogether, replacing it with an explicit second-moment correction
term that vanishes as losses shrink. Together they trace
the chapter's own narrative arc from "no algorithm beats " to "an explicit, parameter-free
family of algorithms gets within of the best expert for any ."
All four results are proved by the book via the same device — a potential function
— one of the first instances of the potential-function method that
recurs throughout the rest of the book (e.g. Online Gradient Descent's regret proof) and
throughout online learning generally. None of these four statements, in this exact form, has a
formalized proof on Prove2Me or (to the extent searchable) elsewhere: the platform's closest
existing result, BanditAlgorithm.ftrl_simplex_exp_weights_regret (see Formalization scope
below), proves an asymptotically similar bound by an entirely different route and under a
different loss model.
The natural first attempt at any of these bounds is to track (or , or ) directly and induct on ; this fails because the quantity itself has no useful recursive structure — knowing the algorithm's mistake count through round says nothing about round 's outcome, which the adversary chooses to inflict maximum damage. The proofs instead introduce an auxiliary potential that is not the quantity being bounded, track it in two directions — an upper bound in terms of the algorithm's own performance (using , or, for Hedge, for ) and a lower bound via the single best expert's weight, — and only convert back to the mistake/loss bound at the very end via one logarithm. Getting the direction of every inequality right (each of the four proofs chains four or five inequalities, each valid only in the stated parameter range) is the entire difficulty; there is no shortcut that avoids introducing .
Each algorithm is represented as a Prop-valued run predicate parametrizing over the weight
sequence, the input (expert predictions/losses and true outcomes), and the algorithm's own
output (predictions or mixed strategy), rather than as an executable program: IsHedgeRun
fixes W 0 i = 1, the update W (t+1) i = W t i * exp(-ε * ℓ t i), and
x t i = W t i / ∑ j, W t j; IsWeightedMajorityRun additionally fixes the majority-vote
prediction rule explicitly (per the triage rubric, the algorithm is part of the audited
statement here, not a black box the proof is free to instantiate). Randomization in RWM and
Hedge is captured exactly as the book itself does — as a deterministic expectation, i.e. the
inner product of the probability vector with the {0,1}-mistake or loss vector — rather than as
a measure-theoretic random variable; the book's own Section 1.3.3 makes this identification
explicit ("denote in vector notation the expected loss of the algorithm by
"), so no probability space is introduced. Theorem
1.1's "deterministic algorithm" is a causal map from an outcome history to a prediction
(prediction at round depends only on outcomes before ), instantiated at the book's own
two-expert construction (one expert always predicts , the other always ) rather than a
fully general -expert adversary argument — a strictly weaker instance of the general claim,
but the exact one the book's proof establishes, so no scope is lost relative to what is proved.
is kept as an explicit free parameter throughout, per the book's own presentation
(no substitution of the corollary's optimized
into the milestone statements).
A trivializing formalization to rule out: fixing (a single expert) would make Lemmas 1.3–1.5 hold vacuously with regardless of the potential-function argument; every formal statement here quantifies over an unconstrained with , not a hard-coded small case.
The mission needs no Mathlib infrastructure beyond finite sums, Real.log, and Real.exp; the
book's own OCO protocol and regret definition (§1.1) are not needed, since this chapter's
proofs work directly with mistake/loss counts (per the chunk brief). BanditAlgorithm.ftrl_simplex_exp_weights_regret (Bandit Algorithms XII, Prop. 28.7, arXiv:2003.05963 §28) proves
for exponential weights on the simplex against -valued losses,
via an FTRL/mirror-descent instantiation — the same asymptotic phenomenon as Theorem 1.5, but a
different proof technique, a different (bounded, not merely non-negative) loss assumption, and
stated for simplex-comparator regret rather than the per-expert loss comparator here; it is
listed as a reference/comparison point, not reused.
Two-stage stochastic linear programming with recourse models a decision made before uncertainty resolves (the first-stage variables ) followed by a corrective decision made after (the second-stage, or recourse, variables ). Solving such a program means minimizing , where is the expected cost of the best recourse action given -- an object defined only implicitly, as the value of an embedded linear program that must be solved (or bounded) for every realization of the uncertain data. Before any algorithm for this problem can be justified -- the L-shaped method, stochastic decomposition, scenario decomposition, all developed in later chapters of Birge & Louveaux, Introduction to Stochastic Programming (Springer, 2011) -- one needs to know that is well-behaved enough to optimize over at all: that the feasible region is closed and convex, that itself is a finite, Lipschitz, convex function on it, that an optimal solution is actually attained rather than only approached in the limit, and finally what an optimality condition for the resulting nonsmooth convex program even looks like. This mission formalizes exactly that foundational layer, Chapter 3, Section 3.1 of the book.
Fix natural numbers and a finite scenario count . A two-stage recourse instance consists of first-stage data , , , a fixed recourse matrix , and, for each scenario , a cost vector , a right-hand side , a technology matrix , and a probability with (Eq. (1.1)). The first-stage feasible region is .
For a fixed and scenario , the second-stage value is
(Eq. (1.6)), taken as an extended real: if no feasible exists, if the inner program is unbounded below. The expected recourse value is (Eq. (1.3)), combined so that -- the book's own convention (p. 109): infeasibility in one scenario is treated as fatal even if another scenario is unboundedly favorable. The second-stage feasibility set is , and the deterministic-equivalent objective is (Eq. (1.2)). For with finite, the subdifferential is the set of satisfying for every (p. 115).
A simple-recourse instance is the special case : the recourse cost splits as , and decomposes componentwise via the closed form of Eq. (1.9)-(1.10) using the (left- and right-limit) distribution functions of each .
given that (1.2) has a finite optimal value. This is the KKT-style necessary and sufficient optimality condition for the two-stage recourse LP, and the weakest of the mission's targets in the sense that everything else supports it: convexity and finiteness of (Theorem 6) are what make the left-to-right implication meaningful, closedness/convexity of (Theorem 5) makes the feasible region well-posed, and attainment (Theorem 8) is what makes " is optimal" a statement about a point that exists rather than an infimum that may not be reached.
Theorem 9 is the hinge on which the rest of the book's algorithmic chapters turn. The L-shaped method (Chapter 5) is a cutting-plane scheme whose cuts are literally elements of ; stochastic decomposition and sampling-based methods use the same subdifferential structure with estimated cuts; the differentiable specialization (Eq. (1.14), ) underlies nonlinear-programming approaches to the smooth case. None of this is meaningful without first knowing is convex, finite where it needs to be, and that a minimizer exists to characterize. Formalizing this mission's four milestones from the actual definition of as an embedded linear program's value -- rather than assuming these properties -- is exactly the content the book itself proves (or, for Theorem 6, explicitly cites to Wets [1972] and Kall [1976] rather than proving); this mission asks for genuine Lean proofs of Theorems 5, 8, 9 and Corollary 10 from the LP structure of , and records Theorem 6 as a stated (not re-derived) input, matching the book's own presentation.
The obvious shortcut is to treat as an opaque convex function and apply a textbook convex-KKT
theorem off the shelf. This fails to capture what Theorem 9 actually is: a statement about the
specific function , built from finitely many parametric linear programs, each of which can be infeasible
() or unbounded () depending on . Convexity of
must come from convexity of the value function of a parametric LP in its right-hand side
(the book's Theorem 2 argument: a convex combination of optimal solutions at two right-hand
sides is feasible, hence suboptimal, at the combined right-hand side) -- not from an assumed
hypothesis. Handling correctly is a second, easy-to-miss source of error: the book
fixes an explicit, non-default convention ( dominates ) for combining
per-scenario values, the opposite of the convention Mathlib's own extended-real arithmetic uses,
so any formalization that reaches for EReal's built-in addition to aggregate silently
states a different theorem. Theorem 8's attainment condition is a genuine existence result, not
an automatic consequence of convexity: continuity alone does not give attainment on an unbounded
feasible region, and the book's own counterexample (Eq. (1.11), a negative-exponential tail with
infimum attained by no finite ) shows the boundedness/recession hypotheses are load-bearing.
The scenario set is modeled as Fin K, a finite discrete random variable, matching Section
3.1b's development; under this model " has finite second moments" (the standing hypothesis
of Theorems 4-11 in the general, possibly-continuous case) holds automatically and so does not
appear as a separate hypothesis anywhere in this mission. Q(x,\xi_k) is defined as an EReal
via sInf of the second-stage LP's feasible objective values -- sInf of the empty set is
⊤, and of a set unbounded below is ⊥ -- and is genuinely derived from that inner
minimization rather than assumed convex; this rules out the chapter's trivializing
formalization, which the paper-level triage explicitly warns against: taking Q(x) as an
opaque convex-function hypothesis instead of deriving its properties from the inner LP's
structure. Aggregating the per-scenario values into uses a bespoke bookAdd operation
implementing the book's stated convention , since Mathlib's EReal
addition is defined with the opposite convention (). is
the ordinary subgradient-inequality set for this extended-real-valued function.
Theorem 8's condition (b) is stated with the book's own quantifier structure: the threshold
and the recession value depend on the point and direction exactly as
written, with no strengthening. Theorem 6(a)'s Lipschitz bound is stated, not derived -- the book
itself cites it to Wets [1972] and Kall [1976] without proof -- so a faithful Lean proof of that
milestone is expected to remain out of scope for this mission. Corollary 10 similarly takes the
closed form of from Eq. (1.10) as a hypothesis on an abstract , matching how
the book itself uses (1.10) as an already-established fact rather than re-deriving it from the
second-stage LP in the corollary's own proof. Theorem 11's subdifferential-decomposition result
() is deliberately left out of
this mission's scope: it is not needed by Theorem 9's own proof, and its normal-cone term would
require relatively-complete-recourse machinery this mission does not otherwise need. No prior-art
match was found on the platform: VectorSpaceOpt.fenchel_duality and the Luenberger-derived
VectorSpaceOpt.generalized_kuhn_tucker / kkt_complementary_slackness family use a
differentiable (Gateaux-derivative) or conjugate-function KKT model over general normed spaces,
not this chapter's finite-dimensional, possibly-nondifferentiable subgradient formulation over
the specific polyhedral set , so none is a faithful match and all items here are original
drafts.