Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Applying the circle method to an additive problem about primes requires counting primes in arithmetic progressions with an error term uniform in the modulus: the modulus is not fixed in advance, it grows with the size of the numbers being represented. The Siegel–Walfisz theorem is the classical statement of that uniformity, valid for every modulus up to a fixed power of , and it is the one analytic ingredient the standard proof of Vinogradov's three primes theorem cannot do without.
The history is a sequence of partial uniformities:
The von Mangoldt function equals if is a prime power and otherwise. The Chebyshev function counts primes with weights; the prime number theorem is the assertion .
A Dirichlet character modulo is a multiplicative function , supported on the units and taking root-of-unity values there. The principal character is the indicator of the units; a character is quadratic (real) if and , and primitive if it is not induced by a character of a proper divisor of . The Dirichlet -function , defined for , extends meromorphically to , entire except for a simple pole at when is principal.
The two counting functions of the mission are the twisted von Mangoldt sum and the progression sum
related by finite character orthogonality. Write for principal and otherwise. A zero of lying inside the classical zero-free region is an exceptional zero (a Siegel zero); the set of such zeros for a given is the exceptional set , which the results below constrain to have at most one element.
The attack path follows Davenport, Multiplicative Number Theory, 3rd ed., §§14, 18, 20, 21, 22.
(1) zero_free_region (§14, pp. 88–96). There is an absolute such that for
every and every ,
with at most one exception, which is real, lies in , is a simple zero, and can occur only for quadratic non-principal .
(2) pnt_dlvp (§18, pp. 111–114). For some and all ,
(3) psi_char_of_region (§20, pp. 121–125). For a region constant there are
such that, whenever is an exceptional set for with
respect to and ,
(4) siegel (§21, pp. 126–131). For every there is
such that for every real primitive non-principal ,
(5) siegel_zero (§21, second form). For every there is
such that for every real primitive non-principal ,
(6) siegelWalfisz (§22, pp. 132–134). For every there are such
that for all , all , and all with ,
This is literally the platform proposition ThreePrimes.SiegelWalfisz.
A corollary, not a milestone, records the progression form siegel_walfisz_ap: for
and ,
Goal (three_primes, §26). There is such that every odd is a sum
of three primes. It follows from milestone (6) by the existing platform theorem
deducing ThreePrimes.ThreePrimesExistence from ThreePrimes.SiegelWalfisz. The goal
leaves unspecified rather than hard-coding a numeric threshold, so it is not
invalidated by later improvements to that threshold.
Siegel–Walfisz is the standard uniform input downstream of which sit the circle method for ternary Goldbach, the Bombieri–Vinogradov theorem, and much of sieve theory. Without it, the three primes theorem's major-arc analysis has no main term.
Platform status is the reason this mission exists. A complete, machine-checked
formalization of the three primes theorem already exists in the namespace ThreePrimes
(by user tabbott), following Vaughan, The Hardy–Littlewood Method, Ch. 3, and
Davenport §26. It is conditional: it takes Siegel–Walfisz as an explicit hypothesis
ThreePrimes.SiegelWalfisz. Discharging that hypothesis makes the three primes theorem
unconditional, and is the whole content of this mission.
Mathlib contains the analytic continuation of
(DirichletCharacter.LFunction),
its functional equation, the non-vanishing of on ,
Dirichlet's theorem, and the Chebyshev function. It does not contain the zero-free
region for , the explicit formula for , Siegel's theorem, or
Siegel–Walfisz. The platform additionally hosts the
PNT+ project contour
machinery for — Borel–Carathéodory, the
inequality, a zero-free rectangle, and MediumPNT,
. That is a template for the
analogues, not a proof of them, and its error term is weaker than the de la Vallée
Poussin form milestone (2) asks for.
The first idea is to run the argument character by character. It works for complex and breaks for real ones. The positivity device that pushes zeros off compares , and the trivial character at nearby points; when is quadratic, is principal and contributes the pole of at at exactly the height where the putative zero sits, so the inequality degrades from "no zeros" to "at most one zero" and stops there. Every later step inherits that unexcluded zero: milestone (3) can only be stated with the term present, and milestone (6) is exactly the assertion that for this term is small — which Siegel's ineffective bound supplies and nothing effective is known to.
A second shortcut, deducing uniformity from Mathlib's non-vanishing of on together with Dirichlet's theorem, also fails: those results are qualitative, carry no rate, and are not uniform in .
Sums run over with , matching Vino.vmSumChar and
ThreePrimes.SiegelWalfisz; Davenport sums over . The two differ by the single
term , negligible against every error term above. Milestone (2)
alone uses a real argument, via Mathlib's Chebyshev.psi. is Mathlib's
DirichletCharacter.LFunction, so no continuation is reconstructed.
The zero-free region is Davenport.InRegion c q s, namely
; the exceptional zero
is packaged as IsExceptionalSet c χ E: is a subsingleton, every element is a real
zero of in and can exist only for quadratic non-principal ,
and at every of the region outside . Milestone (1) adds
simplicity as for .
Milestone (3) takes the region constant as a parameter rather than importing it
from milestone (1), so the milestones can be attempted in any order. For large the
hypothesis IsExceptionalSet c χ E may be unsatisfiable for some , making the
statement vacuous there — a harmless weakening, not a falsehood, and not a trivializing
reading: milestone (1) produces a definite small with a witness for every
, so instantiating milestone (3) at that discharges the hypothesis rather than
voiding it.
Siegel's theorem is stated for χ.IsQuadratic, χ ≠ 1, χ.IsPrimitive characters, with
the conclusion a lower bound on ; since is real
for real , this is the value itself, not a weakening. The constants in milestones
(4), (5) and (6) are ineffective; the statements are plain existentials, so
ineffectivity is invisible to Lean, but no numeric constant can be extracted from
anything downstream of them.
The principal character is included in the character-form statements, with main term
(if χ = 1 then (N : ℂ) else 0); milestones (3) and (6) therefore contain the prime
number theorem itself and cannot be proved by restricting to non-principal .
Milestone (6) requires strictly, which is what makes a
genuine saving over the trivial ; with allowed it would be
empty.
Beyond the six milestones, a complete development needs Hadamard factorization for as an entire function of order , the zero-counting estimate (§16, pp. 101–103), the truncated explicit formula for (§19, pp. 115–120), Perron-type contour truncation, and the imprimitive-to-primitive reduction . All of it is reusable well beyond this mission, being the standard prerequisite for Bombieri–Vinogradov, Linnik's theorem, and effective Chebotarev. Contributions of these supporting results, of alternative routes to milestone (3) following Montgomery–Vaughan Ch. 11, of the versions, and of sharper constants are welcome.
Mathlib.NumberTheory.LSeries.DirichletContinuation.
docsPolynomial representations provide a concrete way to study modules over Lie algebras: the underlying vector space is a polynomial ring, while the Lie generators act by explicit multiplication, shift, and differential operators. Chen and Tan classify a family of modules over the symplectic Lie algebra that are free of rank one over the universal enveloping algebra of an abelian nilradical. Their paper determines the family, its isomorphism classes, its weight and simplicity criteria, its finite-length behavior at exceptional parameters, and an application to Hamiltonian Lie algebras. This mission packages those headline results into one common Lean target, corresponding to Theorems 1.1--1.3 of Chen--Tan.
The common-family formulation matters. The source does not assert three unrelated existence theorems: one explicit two-parameter family carries all of the classification, simplicity, finite-length, and Hamiltonian consequences. The Lean goal therefore quantifies that family once and requires all headline properties of the same witness.
Fix and the complex symplectic Lie algebra . The relevant maximal parabolic subalgebra has an abelian nilradical . Its enveloping algebra is a polynomial algebra in the root generators, represented formally by a multivariate polynomial ring. A rank-one free -module can consequently be modeled on that polynomial ring.
The definition bundle presents the simple Chevalley generators and their action by explicit operators depending on a scalar and a polynomial parameter . Rather than assuming that these formulas already form a representation, the target asks for a generator presentation satisfying the symplectic Lie relations and for a representation family realizing the formulas. It also formalizes module equivalence, weight spaces, simplicity, Noetherian and Artinian conditions, finite composition factors, and the Shen--Larsson construction for a Hamiltonian Lie algebra.
Prove that for every there is one generator presentation and one family
of -representations on the polynomial ring, free of rank one over the abelian nilradical, satisfying the explicit generator formulas. Prove the source's classification and isomorphism criteria, including that is a weight module exactly when is constant, and the stated simplicity criterion outside the exceptional arithmetic set
For exceptional , prove the Noetherian/Artinian and finite-composition-series conclusions and the weight/nonweight classification of the composition factors. Finally, prove that the canonical Hamiltonian Shen--Larsson construction has the exact degree-weight spaces and the source's simplicity and weight-module consequences. All clauses must be witnessed by the same family .
The result gives a complete algebraic description of a large concrete class of non-highest-weight modules. It separates the generic simple regime from an exceptional finite-length regime and shows how nonweight symplectic modules generate weight modules over an infinite-dimensional Hamiltonian Lie algebra. The explicit formulas make the family suitable for calculation, while the classification prevents duplicate parameter choices from being mistaken for genuinely different modules.
Formalization adds checks that are easy to blur in prose. In particular, the generator formulas cannot be called a Lie representation until the defining relations have been verified, and the same witness must support every later theorem. A completed proof will contribute reusable Lean infrastructure for symplectic root data, polynomial representations, module-theoretic finiteness, exact weight-space descriptions, and Hamiltonian Lie-algebra functors. The paper's proofs are known; the open task is their machine-checked reconstruction.
The first obstacle is structural rather than computational. Checking formulas on individual generators is insufficient: all Chevalley and Serre relations must hold with the correct operator order and signs, after which the action must extend to the full Lie algebra. Classification then requires controlling arbitrary rank-one-free modules, not merely verifying that the displayed examples exist.
The exceptional parameters introduce a second layer. Generic simplicity and exceptional finite length are logically different claims, and the composition-factor statement must be tied to the same parameterized representation. The Hamiltonian application adds another algebra and a tensor construction; exact weight spaces and simplicity cannot be obtained by treating the functor as an opaque interface. The Lean goal deliberately keeps these obligations inside one theorem so that separate convenient witnesses cannot satisfy different portions.
The mission works over with natural rank . The definition bundle uses concrete multivariate polynomials, matrices and linear maps, a presented symplectic Lie algebra, Lie representations, submodules, and tensor products. The exceptional set is expressed with complex coercions, so no accidental natural-number division is involved. The nilradical action, freeness, parameter equivalence, weight-space equalities, simplicity, finite-length properties, and Hamiltonian brackets are transparent propositions in the bundle.
The final theorem is a single conjunction under one existentially quantified presentation and one existentially quantified family . Several convenient corollaries can be projected from it, but they are not independent targets and do not permit different witnesses. The bundle contains no custom axioms or opaque semantic assumptions, and the only admitted term is the main theorem's sorry. Contributions may split the proof into source-numbered lemmas about generator relations, classification, exceptional submodules, or the Shen--Larsson application, provided the shared-family quantifier structure is preserved.
For many natural chains, convergence to stationarity is not gradual: the distance stays near its maximum for a long time and then collapses to zero in a comparatively negligible window. A deck of cards under riffle shuffles is "not at all mixed" for six shuffles and "essentially mixed" after eight. This abrupt transition is the cutoff phenomenon, discovered by Aldous and Diaconis in the 1980s, and Chapter 18 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develops its theory: precise definitions of cutoff and cutoff windows, the product criterion necessary for cutoff, and complete proofs for two model families — the biased walk on a segment and the lazy hypercube walk, the latter with the sharp location and window , in both total variation and separation. Chapter 19 complements this with lamplighter walks: chains on the wreath-product state space of lamp configurations over a moving lamplighter, whose relaxation, mixing, and separation times are governed — beautifully — by the hitting and cover times of Missions VI. Both chapters are formalized in this mission.
A family of chains is a sequence on state spaces with stationary distributions ; all single-chain quantities acquire an index . As before, , , , and . The family has a cutoff when for every
and a cutoff at with window when and the distance at time tends (in the appropriate limsup/liminf sense) to as and to as . The separation distance from is (Mission III), , and a separation cutoff is defined by the same window template with in place of . From Mission VII, is the relaxation time; from Mission VI, and are the maximal hitting and cover times, and the pairwise distance is from Mission II.
The concrete chains: the lazy biased walk on holds with probability and otherwise steps up with probability , down with probability (reflecting at the endpoints); the lazy hypercube walk is the walk of Mission IV on . The lamplighter chain over a graph has states (lamp configuration in , lamplighter position in ); one step randomizes the current lamp, moves the lamplighter one step of the lazy walk on , and randomizes the new lamp. Its stationary distribution is uniform lamps times the walk's stationary distribution.
Theorem 18.3: the lazy hypercube walk has a cutoff at with window — the family's total variation distance undergoes its full collapse in a window of size around .
The results. Cutoff is the deepest phenomenon in the quantitative theory of Markov chains: it says mixing is a phase transition in time. The hypercube is the fundamental example where everything can be computed — the eigenvalue structure of Mission VII delivers the upper bound and a refined distinguishing-statistic argument (Mission IV) the lower — and the location with window is the sharpest statement of the coupon-collector heuristic. The product condition 18.4 is the basic sanity criterion in the ongoing research program of characterizing cutoff. The lamplighter theorems tie together the entire series: hitting times (Mission VI), cover times (Mission VI), relaxation times (Mission VII), and separation (Missions III, XI) all meet in one family of chains that furnishes counterexamples — for instance, families with total-variation cutoff but no separation cutoff.
Formalizing them. Nothing about cutoff exists in any proof assistant. The definitions themselves (families of chains, windows, limsup/liminf in a real parameter) are a formalization contribution: they force precision about quantifier order that informal texts elide. The hypercube cutoff is a landmark target — a sharp two-sided asymptotic statement, not an inequality.
The upper half of the hypercube cutoff needs the full eigenvalue decomposition of the walk ( with multiplicity , via Mission VII's spectral representation) and the bound summed over binomial coefficients; the lower half needs the Hamming-weight distinguishing statistic pushed to second-order precision (mean and variance at time ). Proposition 18.4 converts an eigenfunction with eigenvalue near into a quantitative anti-concentration statement — the formal content of "a bounded ratio forbids abrupt collapse". Theorem 18.2 rests on a central-limit-flavoured estimate for the biased walk's position, done with fourth-moment bounds rather than the CLT. The lamplighter theorems are the heaviest: the upper bounds couple lamp refreshment with the cover-time of the base walk, the lower bounds run separation-distance and eigenfunction arguments, and all four inequalities must hold with universal constants over an arbitrary growing graph family — the statements quantify over the family, so the proofs must too. The asymptotic language throughout (liminf/limsup over , limits in the window parameter ) exercises the filter library in earnest.
Families are dependent functions ∀ n, Matrix (V n) (V n) ℝ over a sequence of finite state-space types. Cutoff and windows are rendered exactly by the book's Eq. (18.3) and §18.1: the window definition uses Filter.liminf/limsup over composed with limits in the real parameter (through ⌊t n + α w n⌋₊, with the natural-floor convention on negative reals). The mixing-time ratio in the cutoff definition uses real division of the natural-valued mixing times (total division: the hypotheses keep denominators eventually positive). The biased walk's stationary distribution is passed as a hypothesis rather than a closed form. In the lamplighter theorems the comparability constants and the threshold are existentially quantified, with the graph family and its connectivity as hypotheses; the lamplighter matrix and its product stationary distribution are explicit definitions. Lemma 19.3 is stated for a single reversible chain at all times .
Every mixing bound in Missions II–IX ultimately leaned on either coupling or the spectrum, and the spectral route demanded reversibility. Chapter 17 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) opens a third route: martingales — processes whose conditional expected increment vanishes — and the beautiful evolving-set process of Morris and Peres built from them. The payoff theorem of the chapter bounds the mixing time of any lazy irreducible chain by its bottleneck constant, with no reversibility hypothesis anywhere — an honest strengthening of the spectral route through the Cheeger inequality, whose proof is a martingale analysis of a random sequence of sets growing and shrinking under the chain's flow. The same chapter proves the optional stopping theorem in the exact discrete form the rest of the series consumes, and applies the machinery to sharp return-probability estimates for lazy walks.
Throughout, is a chain on a finite state space with stationary distribution ; , , and as in the earlier missions; . The chain is lazy when at every state.
A martingale adapted to the chain is a family of functions of the trajectory up to time such that the conditional expectation of , given the trajectory so far, equals — for a finite chain, a pointwise finite-sum identity. A stopping time is a -valued stopping rule in the sense of Mission III: whether to stop at time depends only on the trajectory up to .
From Mission IV: the edge measure is , with , and the bottleneck constant is the minimum over sets with of . The evolving-set process is the Markov chain on subsets of in which, from the current set , one draws uniform on and passes to the superlevel set
— states currently receiving a large share of the flow out of are likely to join, states receiving little are likely to leave.
Theorem 17.10 (Morris–Peres), the capstone of Chapter 17: for any lazy irreducible chain — reversibility not assumed —
The results. The optional stopping theorem is the workhorse identity of discrete probability — the earlier missions' gambler's-ruin and hitting-time computations are all instances, and Missions XI–XII cite it again. The Morris–Peres theorem is the strongest known elementary relation between geometry and mixing: for reversible chains it recovers the Cheeger-based bound of Mission VII, but it needs no reversibility, and its proof technique — controlling the root as a supermartingale — introduced evolving sets as a tool that has since produced heat-kernel decay, isoperimetric mixing profiles, and bounds for non-reversible and time-inhomogeneous chains well beyond the book.
Formalizing them. Mathlib's martingale library lives in measure-theoretic generality; this mission's chain-adapted martingales are self-contained finite objects (families of functions on trajectory spaces), so the optional stopping theorem here is independent of, and complementary to, the measure-theoretic one. Evolving sets exist in no proof assistant; the process is a genuinely novel formalization target — a Markov chain whose states are Finsets, defined through interval lengths of a uniform variable.
The optional stopping theorem needs the dominated-convergence step (bounded martingale, a.s. finite time) rendered as an elementary tail estimate — the series must be shown summable and equal to by an exchange of finite sums with a limit. The evolving-set transition probabilities are interval lengths: the probability of passing from to is the length of the set of whose superlevel set is exactly , which the formalization encodes by explicit upper and lower thresholds (a min over and a max over of the clipped ratios ); establishing that these lengths sum to one over , and that the process has the two martingale properties, is delicate finite-order-statistics reasoning. The goal theorem then runs a supermartingale argument on : laziness keeps the thresholds in , an expansion estimate converts the bottleneck constant into a per-step multiplicative decay of , and Lemma 17.12 converts that decay into a total-variation bound. Theorem 17.17 composes the same machinery with a Cauchy–Schwarz step. None of this exists in any library; the auxiliary supermartingale lemmas are welcome as separate contributions.
Martingales, stopping times, and stopped expectations are the trajectory-calculus objects of Missions I and III: finite sums over paths weighted by , with expectations over the stopping time as tsums in (non-summable families sum to ; the a.s.-finiteness hypothesis is the statement that the stopping mass sums to ). The evolving-set matrix is defined by the clipped-threshold formula described above — an explicit real matrix on Finset V — and the goal and lemmas assume positive and lazy exactly where the book does. Theorem 17.17 is stated for the lazy walk on a connected graph with positive degrees, with written out. Real-valued bounds on the natural-valued are direct inequalities on the cast, with no hidden rounding.
The Ising model is statistical mechanics' fruit fly: spins on the vertices of a graph, neighbours preferring to agree, a single parameter — the inverse temperature — tuning the strength of that preference. Chapter 15 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) studies the Glauber dynamics for this model and exhibits, on concrete graphs, the phenomenon that made mixing times a subject: a dynamical phase transition. At high temperature (small ) the dynamics mixes in steps on any bounded-degree graph; on the complete graph the same dynamics passes, as crosses an explicit threshold, from mixing to exponentially slow mixing. The chapter also introduces two comparison tools of independent value — the sensitivity of the spectral gap to edge removal, and the block dynamics comparison — and the Kenyon–Mossel–Peres bound for trees, all formalized in this mission.
Spin configurations on a finite graph with vertex set of size and maximum degree are functions assigning to each vertex (encoded over Booleans, ). The Ising model at inverse temperature is the Gibbs distribution
each edge counted once, the normalizing partition function. The Glauber dynamics for picks a uniform vertex and re-samples its spin from conditioned on all other spins — concretely, the new spin at is with probability where is the sum of the neighbouring spins.
The yardsticks are as in the earlier missions: is the total variation distance, , and . From Mission VII: an eigenvalue of a chain is a real with for some nonzero ; is the largest eigenvalue , the spectral gap is , the largest over eigenvalues , and the relaxation time is .
Theorem 15.1, the high-temperature fast-mixing theorem: if then the Glauber dynamics on any graph satisfies
together with its refinement for graphs with all degrees even, where the condition relaxes to .
The results. Theorem 15.1 is the standard fast-mixing criterion for Glauber dynamics, and the model application of the path-coupling technique of Mission VIII. Theorem 15.3 exhibits, in the cleanest possible setting, the correspondence between the static phase transition of the mean-field Ising model and the dynamical transition of its Glauber dynamics — the phenomenon at the heart of Markov-chain approaches to statistical physics. The tree bound of Kenyon–Mossel–Peres and the block-dynamics comparison are the standard tools for spatially structured spin systems; block dynamics in particular is the engine of recursive gap bounds on trees and lattices.
Formalizing them. Nothing about the Ising model, Gibbs distributions, or Glauber dynamics exists in Mathlib. The Gibbs-distribution layer (weights, partition functions, conditional single-site laws with their closed forms) is foundational for any future formalization of statistical mechanics; the phase-transition theorem 15.3(ii) would be, to our knowledge, the first formalized instance of exponentially slow mixing driven by an energy barrier.
The high-temperature theorem is path coupling (Mission VIII) plus the tanh lemma: the one-site coupling of two adjacent configurations contracts the Hamming metric at rate , and every analytic input is in Lemma 15.2 — which is why that elementary lemma is a milestone of its own. The slow-mixing half of Theorem 15.3 runs through the bottleneck bound of Mission IV: the magnetization performs a one-dimensional walk in a double-well free-energy landscape, and the bottleneck at zero magnetization has exponentially small stationary mass — a large-deviations estimate carried out with binomial coefficients. The cycle's lower bound needs Wilson's method (Mission VII) with an explicit eigenfunction. The tree and block theorems are exercises in the comparison technology of Mission VII (Dirichlet forms, canonical paths through block updates); their constants are crude but the inductive structure is delicate. Everything sits on the subtlety that the state space has size , so all "polynomial" bounds are polynomial in , not in the size of the state space.
The Gibbs distribution is defined by explicit finite sums (weight over partition function, total division); no positivity side conditions are needed since the weights are exponentials. The Glauber dynamics is the generic single-site heat bath of Mission II applied to the Ising distribution, so the closed form is a provable lemma, not a definition. Asymptotic statements (, "for sufficiently large ") are rendered with explicit quantifiers and a free precision parameter ; the phase-transition constants are existentially quantified. The tree is encoded as words of length over an alphabet of size ; the block dynamics re-samples a uniformly chosen block from the conditional Gibbs distribution, with the convention that a conditioning of zero mass yields a zero row (total division), which the theorems' hypotheses exclude on the support. The even-degree refinement of the goal is stated as a second conjunct with its own hypothesis.
How many shuffles does a deck of cards need? The question created the modern theory of mixing times: Diaconis and Shahshahani's analysis of random transpositions (1981) and the Bayer–Diaconis "seven shuffles suffice" analysis of the riffle shuffle (1992) are its founding results. Chapters 8 and 16 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) treat the four standard shuffles: random transpositions (pick two cards, swap them), the riffle shuffle (cut and interleave, the Gilbert–Shannon–Reeds model), random adjacent transpositions, and the -reversal chain of segment reversals — the last motivated by genome rearrangement, where a chromosome evolves by reversing segments and the mixing time measures evolutionary distance ("from shuffling cards to shuffling genes").
All four chains are random walks on a symmetric group; decks are encoded as in Mission III, an arrangement being a permutation with position on top. Random transpositions have increment distribution , . The lazy adjacent-transposition walk puts mass on the identity and on each . One inverse riffle shuffle assigns each card an independent uniform bit and moves the cards labeled to the top, preserving relative order; the (forward) riffle shuffle is its time reversal, given by transposing the inverse-shuffle matrix (the stationary distribution being uniform). The -reversal chain on circular arrangements indexed by picks a position and a length uniformly and reverses the segment .
for random transpositions on cards (Corollary 8.10), formalized as: for every there is with for all .
Proposition 8.11 (random transpositions lower bound , via fixed points); Proposition 8.13 (riffle shuffle: ); Proposition 8.14 (riffle shuffle: for large , by the counting bound of Mission IV); the random adjacent transpositions upper bound for large (§16.1.2, display (16.4)) and lower bound (§16.1.3, by following a single card); and Proposition 16.2 (the -reversal chain with satisfies , via conserved adjacencies).
The results. Random transpositions at (the constant here is not sharp; the sharp constant is part of the celebrated Diaconis–Shahshahani cutoff) and riffle at are the emblematic mixing results outside of spin systems; the riffle bound is the mathematical content of "seven shuffles suffice" for . The adjacent-transposition walk at order is the basic example where geometry (diameter ) forces polynomial mixing. The -reversal lower bound is the quantitative starting point of the biological application.
Formalizing them. Random walks on symmetric groups and their mixing are entirely absent from Mathlib; so are the combinatorial devices these proofs run on — the Broder stopping time, rising sequences and the Eulerian-number analysis of riffle shuffles, single-card projections, conserved adjacencies. The riffle shuffle formalization via bit strings and the stable-sort permutation Tuple.sort gives a clean combinatorial model reusable for the cutoff analysis of Mission XI.
Corollary 8.10's route is the Broder strong stationary time: mark cards under a card-and-position scheme and prove that, conditioned on the marked set and its positions, the marked cards are uniformly ordered — an exchangeability induction on top of Mission III's stopping-rule framework; then the coupon-collector-style tail with an extra factor. Proposition 8.11 requires the fixed-point statistic: the expected number of untouched cards after transpositions and a second-moment bound, fed into Proposition 7.8. The riffle upper bound runs through inverse shuffles: after inverse shuffles the deck is a uniform stable sort of -bit labels, and mixing reduces to the birthday problem for labels; formalizing "distinct labels imply uniform order" is the crux. The -reversal lower bound needs a second-moment argument for the number of conserved adjacencies with the exact variance bookkeeping of the book. Throughout, the walk-on-group conventions (left vs right increments, forward vs inverse shuffle) are the classic source of silent errors; the formal statements pin them.
All chains are explicit matrices on Equiv.Perm (Fin n) (or Equiv.Perm (ZMod n) for the circular -reversal chain); increments act on the left, matching Mission I's group-walk convention. The riffle shuffle is defined as the transpose-reversal of the explicit inverse-riffle matrix — the two have equal distance to uniformity by Lemma 4.13 (Mission II), which a solver may use rather than re-derive. Asymptotic statements (, "for sufficiently large ") are spelled out with explicit quantifiers; upper bounds carry a where integer rounding requires it. The -reversal family takes the length function as a hypothesis-carrying parameter with , and its lower bound is a genuine limit statement (Tendsto, distance to stationarity tending to ).
Welcome contributions: exchangeability and projection lemmas for deck chains; Eulerian/rising-sequence counting; the single-card chain projection (reused for Mission XI's cutoff examples).
Why do interior-point methods solve convex programs in Newton steps? Nesterov and Nemirovskii's answer is self-concordance: a convex function whose third derivative is controlled by its second, along every line, admits a Newton analysis with absolute constants and no condition number — and the logarithmic barrier is self-concordant. This mission formalizes §9.6 and Chapter 11 of Boyd & Vandenberghe: the self-concordance calculus, the Newton-decrement analysis, the duality gap along the central path, the per-centering work bound , and the crown result — with the aggressive schedule the barrier method reaches duality gap after
centering steps, each of uniformly bounded Newton cost.
Determine the exact second-order term in the least possible largest factor in a factorization of into distinct integers exceeding , with the proposed rational constant .
The final step from bandits to reinforcement learning: actions now change the state of the world. Chapter 38 of Lattimore–Szepesvári studies online learning in an unknown Markov decision process with states, actions and rewards in . The optimism principle of Mission II scales up: UCRL2 maintains confidence sets over transition kernels, solves an extended MDP by extended value iteration, and recomputes only when a state-action count doubles. The goal theorem: with probability , , where is the diameter of the MDP — sublinear regret with no prior knowledge of the dynamics. The matching lower bound brackets the true complexity of tabular reinforcement learning up to .
Randomness appears to enlarge efficient computation, but the Sipser–Gács–Lautemann theorem places every bounded-error probabilistic polynomial-time language at the second level of the polynomial hierarchy, giving one of complexity theory’s foundational limits on the power of randomization.
How well can any algorithm possibly do? Chapters 13–17 of Lattimore–Szepesvári answer with three matching impossibility results. The divergence decomposition identifies the information a policy collects: . Feeding it into the Bretagnolle–Huber inequality of Mission VI yields the goal theorem — the minimax lower bound over Gaussian bandits, showing MOSS (Mission III) is optimal up to a constant. The same machinery gives the instance-dependent bound of Lai–Robbins type: every consistent policy suffers , certifying the asymptotic optimality of the UCB of Mission III and KL-UCB of Mission IV, and a high-probability lower bound showing the Exp3-IX guarantees of Mission V cannot be improved.
Graph theory began with a unicursal problem: Euler's question whether the bridges of Königsberg can be crossed in one closed walk using each bridge exactly once. For graphs whose arcs are all undirected, or all directed, the answer has been known since the nineteenth century: a connected graph has such a closed walk exactly when every node has even degree, respectively when every node has as many incoming as outgoing arcs. Street networks mix one-way and two-way streets, so routing problems such as the Chinese postman problem live on mixed graphs, where neither criterion applies.
Chapter II, §7 of Ford and Fulkerson's Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962) settles the mixed case with a necessary and sufficient condition read off from network flows. The same chapter treats, in §4 and §8, the other classical min–max theorems of combinatorics that flow theory reproves in a few lines: the König–Egerváry theorem on bipartite graphs, Menger's theorem on disjoint chains, and Dilworth's chain decomposition theorem for partially ordered sets.
A mixed graph has a finite set of nodes and a set of arcs. An arc is either directed, an ordered pair leading from to , or undirected, an unordered pair . No arc joins a node to itself, and there is at most one arc leading from one node to another: at most one directed arc , at most one undirected arc , and never both an undirected and a directed arc on the same pair. Directed arcs and may both be present.
A closed route is a sequence of nodes and arcs in which each leads from to : a directed arc is traversed with its direction, an undirected arc in either direction. Nodes may repeat, and a single node () is a closed route. The graph is unicursal if some closed route contains every arc of exactly once and every node of at least once.
is connected if is nonempty and any two nodes are joined by a path, arcs being allowed against their direction. The degree of a node counts the arcs incident with it, directed and undirected together. For with complement , write and for the numbers of directed arcs from to and from to , and for the number of undirected arcs joining and .
For §4, a chain in a directed graph is a sequence of at least two distinct nodes with consecutive pairs arcs, and an disconnecting set of nodes meets every chain from to . For §8, is partially ordered by , a decomposition partitions into chains , and the bipartite graph of has an arc whenever ; independent arcs are pairwise node disjoint, and a proper cover is a node set meeting every arc with no proper subset doing so.
The mixed graph is unicursal if and only if
MatousekLP.Integrality.konig.AppliedComb.Posets.dilworth.Theorem 7.1 contains both classical Euler criteria: for an undirected graph condition 3 is vacuous, and for a directed graph, applied to single nodes and their complements, it forces equal in- and out-degrees. In the mixed case, condition 3 is a cut condition over all node subsets, which is what makes unicursality decidable by one feasible-circulation computation. That computation is the first step of the Edmonds–Johnson treatment of the mixed Chinese postman problem (Edmonds & Johnson, 1973). Lemmas 8.1 and 8.2 are the bridge by which König's theorem gives Dilworth's theorem, and through it minimal chain decompositions that a bipartite matching algorithm can compute.
All results here are classical and proved; none of the book's statements has been formalized in this form. The platform has Proved formalizations of König's theorem and of Dilworth's theorem, used here as references. It also has an undirected set-to-set Menger theorem (Menger.menger_set), Euler's criterion for undirected multigraphs (AppliedComb.Graphs.eulerian_iff), and the existence of an Euler tour in a connected, even, symmetric mixed graph (ChinesePostman.Mixed.mixed_euler_tour). That last result is one step of the sufficiency direction of Theorem 7.1, not the theorem itself. The directed, node-disjoint, set-to-set Menger theorem and the mixed-graph criterion are new.
Necessity in Theorem 7.1 is a counting argument. Sufficiency is not: conditions 2 and 3 do not by themselves say which way to orient each undirected arc. A wrong local choice can leave a node unbalanced with no way to repair it, so a greedy orientation does not work. The global information is the cut condition over all subsets, and turning it into an orientation needs a feasibility theorem for circulations with integral solutions. Only then does the classical Euler argument apply, and that argument also needs an induction that splits off closed routes and reassembles connected pieces. For Lemma 8.2 it is showing that a proper cover never contains both copies and of an element; this uses transitivity, and finding F2 shows it fails without it.
Nodes are a Fintype with decidable equality. A mixed graph has directed arcs in a Finset (N × N) and undirected arcs in a Finset (Sym2 N); an arc is an element of (N × N) ⊕ Sym2 N. A closed route with arcs is a pair of maps Fin (m+1) → N and Fin m → MixedArc N, and "each arc exactly once" is injectivity plus surjectivity onto the arcs of . Unicursality is defined by the existence of such a route, never by conditions 1–3, and condition 3 is quantified over every subset with the difference taken in . These two choices rule out the trivializing formalization in which "unicursal" is defined by the theorem's own conditions or condition 3 is checked only at single nodes. Connectedness includes nonemptiness of , so the empty graph is neither unicursal nor connected.
For §4, chains are lists of distinct nodes, and Theorem 4.2 states the maximum and the minimum as attained (IsGreatest, IsLeast) with a common value. For §8, is Fin n with a relation carrying IsStrictOrder; the bipartite graph's nodes are Fin n ⊕ Fin n, and a decomposition is a Finpartition of Fin n into chains.
Beyond the paper. Two variant items stand beside the faithful statements. [Strengthened] Lemma 8.1 replaces the partial order by any relation without directed cycles. The book asserts this on p. 47, and the proof uses only that an independent arc set gives each element at most one successor and one predecessor (finding F1). [Sharpness probe] Lemma 8.2 makes the same weakening for Lemma 8.2 and is expected to be false: on five elements with , , , , , and no other relations, is a proper cover of size (finding F2).
A complete development needs Euler-tour infrastructure for mixed graphs, Hoffman's circulation theorem with integrality, and integral max-flow for Menger. Of these, the circulation theorem is the subject of a sibling mission (Flows in Networks III). Proofs of any item by any method are welcome, including direct combinatorial proofs that avoid flows.
Certify by specializing OpenAI's general seed theorem to and .
The construction gives
Here is block sensitivity at the all-zero input. The ratio is approximately . Prove the exact inequality , then reuse the foundation's finite-certificate theorem.
The goal uses the campaign's shared definitions and requires arbitrarily large sensitivity. This is a stronger specialization of the existing construction, not a claim of a new construction or global parameter optimality.
Value iteration and its policy-evaluation special case, value computation, are the basic algorithms of dynamic programming for Markov decision processes (MDPs). Both are fixed-point iterations of a -contraction, so they converge at the geometric rate , the discount factor. When is close to , which is the regime of long effective horizons in reinforcement learning ( or ) and in healthcare and operations applications, the number of iterations grows like .
Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) observe that behaves like the gradient of a function with smoothness constant and strong-convexity constant . This suggests importing the accelerated schemes of convex optimization: Nesterov's acceleration and Polyak's momentum (heavy-ball) method (Polyak 1964; Ghadimi, Feyzmahdavian, Johansson 2015). For the affine operator of a fixed policy, they prove that both schemes converge at a rate governed by rather than , with , provided the Markov chain of the policy is irreducible and reversible. This mission poses the momentum result, Theorem 5.5.
A finite MDP has a state set with , a finite action set , transition probabilities (from state to state under action ; each is a probability vector), rewards , and a discount factor . A policy is a matrix with nonnegative rows summing to ; it induces
The value function of is , the expected discounted reward from each starting state; it is the unique fixed point of .
Reversibility (Definition 2.1): the chain with transition matrix is irreducible, and it has a stationary probability distribution with for all .
Momentum Value Computation (M-VC) starts from arbitrary and iterates
with the constant step sizes (4.2)
The analysis runs through the matrix
which propagates the error of the pair , and its spectral radius , the largest modulus of a complex eigenvalue.
For a valid MDP and a policy whose chain is irreducible and reversible, the M-VC iterates with step sizes (4.2) converge to , and for every
The goal states the paper's three clauses as printed: convergence, the little-o rate for every , and the comparison with .
The rate is the optimal rate of the heavy-ball method on strongly convex quadratics with condition number . Theorem 5.5 shows that policy evaluation for reversible chains enjoys the same improvement over , so that an -approximation of needs a number of iterations scaling like rather than . The paper also shows that the reversibility assumption cannot simply be dropped: on a cyclic chain both accelerated schemes may diverge. Lemma B.2 is an exact spectral computation for a structured block matrix that reappears in any heavy-ball analysis driven by a matrix with real spectrum in .
The paper is a sibling series of four missions. This one poses Theorem 5.5; the others pose Theorem 5.1 (Accelerated Value Computation), Theorem 6.3 (a lower bound for first-order methods on a chain MDP) and Theorem 7.1 (Safe Accelerated Value Iteration). The results are proved on paper; none of them has a machine-checked proof. The work here is to formalize the known argument: the linear-recursion representation, the spectrum of , and the passage from spectral radius to a little-o rate.
The obvious argument bounds in some norm and iterates. No such bound by the rate holds in general: is not normal, and for eigenvalues of the two roots of (B.1) coincide, producing Jordan blocks. The rate must come from the spectral radius, and the gap between and is exactly what the absorbs. Computing needs two separate facts: the eigenvalues of are tied to those of through the quadratic (B.1), which needs a determinant identity for block matrices with commuting blocks; and the eigenvalues of are real and lie in , which needs reversibility together with irreducibility, used to make the stationary distribution positive. For non-real the modulus computation fails, which is why the hypothesis cannot be dropped.
States and actions are finite types. The MDP data is a plain structure, with validity (stochastic , ) a separate hypothesis; the paper's initial distribution plays no role and is omitted. The value function is the Neumann series . The norm on is the sup norm, and is with respect to it as . Spectra and spectral radii are those of the complexified matrices, so that the non-real eigenvalues of are seen. Reversibility uses the published mm_basic notions: irreducibility, a stationary probability distribution, and detailed balance with respect to it; detailed balance alone would be trivially satisfied by and is not used.
Three printed slips are corrected, and each milestone keeps the printed text verbatim. Lemma B.1 is printed with , but is undefined; the statement uses . Lemma B.2 prints , a negative number; its proof computes , the rate of Theorem 5.5, which is stated. On p. 22 the constant is printed as . The second step size, printed in (4.2), is the of (M-VC) and App. B.
A statement that holds only vacuously, for example one in which reversibility is replaced by detailed balance with an arbitrary vector or in which is unconstrained, is ruled out by the hypotheses above. Lemma B.2 is an equality and must not be weakened to an upper bound.
A complete development needs the determinant of a block matrix with commuting blocks, the reality of the spectrum of a reversible chain (implied by the published MarkovMixing.spectral_representation once the stationary distribution is shown positive), Gelfand's formula for matrices, and the convergence of the Neumann series. The spectral facts about reversible chains and the block-matrix spectrum are reusable beyond this mission. Proofs of any milestone are welcome independently.
Quantum communication and computation often require a receiver to infer which preparation was sent after it has passed through a noisy quantum process. When possible preparations are mixed states, their overlap makes exact identification impossible. A measurement is then judged by its average probability of a correct label. The pretty good measurement gives a concrete measurement from the ensemble itself, without first solving the optimization over all measurements. Barnum and Knill related it to a general reversal operation for noisy dynamics and bounded its error through pairwise state fidelities in their preprint, §V–VI. The bound is useful when the overlaps are easier to estimate than the measurement's success probability.
The present mission addresses the preprint's second main result. The source is arXiv:quant-ph/0004088v2, not the later journal pagination. The preprint also strengthens its Theorem 3 relative to the published text, as its acknowledgment explains; this mission concerns Theorem 5 and the calculation around it.
An ensemble is a finite family of output density matrices with probabilities satisfying . A density matrix is a positive semidefinite complex matrix with trace one. For each label , fix an orthonormal eigenbasis and nonnegative eigenvalues such that
The eigenpair index runs over a finite output basis ; zero eigenvalues are allowed. The input labels form a finite basis . A label distribution is represented by .
The paper's classicizing channel has Kraus operators . Acting on an input matrix , its value is . In particular, its output on is . The paper assumes has full support when it writes its reversal operation. For a general Kraus family , that operation has operators
The inverse square root is spectral: invert nonzero eigenvalues and leave zero eigenvalues at zero. With full support, it is the usual inverse square root.
For an input label , classical fidelity is the chance that the composite operation returns the same label. Averaging gives
The Bures–Uhlmann fidelity used here is the unsquared quantity . For the classicizing channel, the reversal operation realizes the pretty good measurement, as shown by equation (36) and the discussion after equation (37) in the preprint, p. 10.
The goal, in the reading established by the paper's proof, is
The sum is over ordered pairs; each unordered pair of distinct labels is counted twice. The coefficient is exactly one. The goal applies to every finite ensemble with the spectral data above and a full-support output. It does not fix the number of labels or the dimension of the output.
The milestones are the reversal formula (36), the classical-fidelity identities in (38), the unit squared Frobenius norm (40), the diagonal-block expression (41), the off-diagonal trace-norm identity following (42), and the two-block estimate of Lemma 6. They record the paper's mathematical statements and keep the attack path tied to the authors' displayed results.
The result bounds a measurement's probability of error using only pairwise similarities of the possible output states and their prior probabilities. For nearly distinguishable states, the weighted fidelity sum is small, so this particular measurement succeeds with high probability. The theorem therefore gives a usable guarantee for a specified recovery procedure, rather than only asserting that some procedure exists. In the preprint, §VII, Barnum and Knill describe quantum-information applications of such recovery bounds.
The mathematical result is already proved in the paper, subject to the correction explained below. The formalization work is to make the mixed-state channel, its recovery, the finite-dimensional spectral conventions, and the block-matrix norm estimate precise in Lean. The published Prove2Me definitions for Kraus updates and trace norm supply reusable starting points. A complete proof of this mission would add a checked mixed-state pretty-good-measurement bound; the local statements here compile as open theorems, and no proof is claimed.
The obvious pairwise-overlap estimate does not by itself express the error of the recovery channel. The recovery's classical fidelity is initially a channel evaluation on basis states, while the bound uses trace norms of blocks of a Gram matrix. The key obstacle is controlling the off-diagonal Frobenius mass of the positive square root of that Gram matrix by the trace norms of the corresponding blocks of the Gram matrix itself. Lemma 6 states the needed two-block comparison, including rectangular blocks. The matrix dimension and block labels must remain consistent when it is applied across a larger array.
All systems and index sets are finite, with matrices over and real probabilities. A general completely positive map is represented by an unbundled finite family of Kraus matrices. The classicizing family has rectangular matrices from the input-label space to the output space; the reversal has matrices in the opposite direction. Composite Kraus families are indexed by pairs. The classical fidelity is defined from the channel action in equation (10); the goal does not define it using the desired overlap bound. The reversal is defined by equation (12) for a general family, so its specialized formula remains a theorem.
The spectral hypotheses include nonnegative probabilities and eigenvalues, unit sums, and orthonormal eigenvectors. Full support of is an explicit hypothesis wherever the reversal appears, following page 7. Empty input or output types cannot satisfy the normalized data together with these hypotheses. The Bures–Uhlmann expression is the unsquared trace of a positive square root; using the squared fidelity would change the constant and is outside this mission. Lemma 6 is independent of the ensemble and can be reused for finite block-matrix estimates. Contributions to the spectral identities, the array equalities, and the block-norm argument are welcome.
Equation (39) prints the square of the optimal success probability on its left. The first line of (38) compares that quantity with the recovery fidelity in the opposite direction to Corollary 4. The proof on pages 12–13 concludes the displayed bound for . This mission states that proved conclusion and records the printed discrepancy in its item and audit notes.
Banks lend to one another, and the shape of the resulting network decides how a loss at one bank reaches the others. A long line of work, starting with Allen and Gale (2000) and continued by Acemoglu, Ozdaglar and Tahbaz-Salehi (2015), compares the ring network, where each bank is owed money by one neighbour, with the complete network, where every bank holds an equal share of every other bank's debt. That literature studies contagion after shocks hit and finds that the complete network spreads losses thinly and can absorb small shocks better.
Shu's paper (Management Science, doi:10.1287/mnsc.2022.01519) asks the ex-ante question: when banks choose how much risk to take, knowing the network they sit in, which network makes them take more? A successful bank subsidizes its failed counterparties through the clearing of interbank debt, and anticipating that subsidy pushes it toward riskier projects. Proposition 4 of the paper says that this effect is stronger in the complete network. This mission formalizes that proposition and the computation behind it.
There are banks. In a regular network with share matrix , bank owes bank the face value , every bank has total interbank liability , and every bank also owes a senior deposit . The two networks of Definition 3 are
Each bank chooses a project in a common interval . The project pays with probability and otherwise, independently across banks. Assumption 1 requires , decreasing, and concave. The standing assumption says a successful bank never defaults.
After the state is realized, interbank payments clear. A payment equilibrium is a vector with
where if bank succeeds and if it fails. Bank 's profit is . A risk-taking equilibrium is a profile in which each maximizes bank 's expected profit given . Equilibria need not be unique, and the paper selects the least one.
The key quantity is the network risk-taking distortion
which is bank 's expected net interbank payment to the other banks when its own project succeeds. In a regular network, expected profit equals , so acts like extra debt that the bank repays only when it succeeds. Superscripts and mark the complete and ring networks.
With the least equilibrium of the complete network and the least equilibrium of the ring,
The result. Proposition 4 reverses the conventional reading of the complete network as the safer structure. The co-insurance that makes it resilient after a shock is the same cross-subsidy that weakens incentives before the shock. Two networks with the same face-value liabilities therefore induce different equilibrium risk-taking. Liabilities alone are not a sufficient statistic for risk incentives, and the network topology matters in its own right. The same comparison is the template for the paper's later results on the number of banks and on central clearing.
Formalizing it. The proposition is proved in the paper, not open, and none of it is machine-checked yet. A formal proof must establish the two clearing vectors, the counting identity behind (I.15), and the two closed forms of the distortion. The printed argument also leaves a step to be supplied: its final appeal to "the monotone selection theorem" needs the distortion comparison at every profile of the other banks. It is proved only when they all choose the same project, and it is false in general. The goal is nevertheless stated for least equilibria exactly as in the paper, and its formal proof has to bridge that gap. The milestones are true as stated.
The distortion of the ring is not a function of the number of failures alone. What a successful bank receives depends on the length of the run of failed banks immediately upstream of it, so the closed form needs an exact count of the binary strings with a given number of failures and a given initial run length. The comparison of the two distortions is not termwise either: the positive part sits inside a sum on the ring side and outside it on the complete side.
The obvious final step is to say that the distortion is larger in the complete network, and that a larger distortion raises the optimal risk exposure. That step does not go through as stated. The equilibrium comparison needs control of the best-response maps at every profile, while the distortion comparison holds only on the diagonal, where all other banks choose the same project. Some further structure of the two games is needed to restrict attention to that diagonal.
Banks are Fin N with , and states are Fin N → Bool with true meaning success. The paper's general model is specialized to a regular network given by , which covers both networks of Definition 3. Every expectation is a finite sum over the states, so no measure theory is involved. The payment equilibrium is the greatest solution of the clearing system, because the paper asserts only generic uniqueness. Every bank's project lies in , and is a hypothesis of every statement.
The distortion milestones (2, 5 and 8) are stated at the constant profile in which every bank chooses the same , which is how the page's single reads. At , where every other bank fails, the printed ring binomial has lower index , and the weight is fixed explicitly to at . Proposition 4 is stated for least equilibria and weak inequality. It adds one hypothesis the page does not state, continuity of on , so that best responses and least equilibria exist. Without it the IsLeast hypotheses could be unsatisfiable and the goal vacuous.
Trivializing encodings are ruled out: is an actual solution of the clearing system, not a junk supremum, and the run length is only used in states where some bank succeeds.
A complete development needs Knaster–Tarski on the box , the clearing computations for the two networks, binomial identities, and a monotone comparative statics argument for the equilibria. Published Topkis results on supermodular games (existence of least equilibria, and monotonicity of least fixed points in a parameter) are included by reference as tools. The clearing and counting lemmas are reusable for the paper's other results on ring and complete networks. Proofs of any milestone, and of the goal, are welcome.
Not posed here: Proposition 1 (strategic complementarity in any network, a separate mission), Proposition 2 (existence), and the later comparative statics in the number of banks, central clearing and bailouts.
When every participant in a repeated game runs a no-regret learning algorithm, the time-averaged play converges to a coarse correlated equilibrium, and in smooth games the average welfare approaches the price-of-anarchy guarantee. These facts are a standard justification for equilibrium predictions in auctions, routing and markets, where agents learn rather than solve for equilibria. Against an adversary, the regret of any learning algorithm can grow like , which gives average regret of order . Syrgkanis, Agarwal, Luo and Schapire (arXiv:1507.00407, NIPS 2015) asked whether learning is faster when the opponents are themselves learning, and so their play changes slowly.
Timeline. Daskalakis, Deckelbaum and Kim (2011) gave a decentralized algorithm with regret in two-player zero-sum games. Rakhlin and Sridharan (2013) obtained the same rate in zero-sum games with optimistic mirror descent, which uses the last observed utility as a prediction of the next one. Syrgkanis et al. (2015) extended recency-biased learning to general multi-player normal-form games. They isolated the RVU property, proved that it gives constant total regret (Theorem 4, Corollary 8), and proved that each individual player's regret is (Theorem 11, Corollary 12). This mission formalizes the second result. Later work by Chen and Peng (2020) and by Daskalakis, Fishelson and Golowich (2021) improved the individual rate to polylogarithmic in .
A static game has players. Each player has a finite strategy set with , and a utility function . A mixed strategy is a point of the probability simplex , and the players randomize independently. The game is played at times . At time each player picks and then observes its utility vector
so its expected utility is . The regret of player after steps is
Strategies are measured in the norm . Utilities are measured in its dual, . A regularizer is 1-strongly convex if . The range is .
Optimistic follow the regularized leader (OFTRL) with step size and predictor sequence plays and
With one-step recency bias, . An algorithm has the RVU property (Regret bounded by Variation in Utilities) with parameters if its regret against every is at most . It has the stability property with constant if .
If , every player runs OFTRL with and , then for every player and every ,
The result. Corollary 12 shows that recency-biased regularized learning in a game guarantees each player average regret . The adversarial optimum is . The bound covers every player separately and needs no coordination beyond a common step size. Corollary 8, by contrast, bounds only the sum of the regrets. Theorem 11 isolates the two algorithmic properties responsible, RVU and stability. Any algorithm with both, including optimistic mirror descent and the other recency biases of the paper, inherits the bound.
Formalizing it. The result is proved in the paper, with the proofs of Proposition 7 and Lemma 20 in its supplementary material. No machine-checked version of optimistic FTRL, of the RVU property or of fast rates in games appears to exist. A formalization makes the following explicit: the strong-convexity form the proofs actually use, the convention for the first utility vector , and the exact range of times on which stability is needed. A later mission of this series formalizes the companion bound on total regret (Corollary 8) on the same objects.
The game-theoretic part is short. Once Proposition 7 and the stability bound are available, Theorem 11 is a summation and Corollary 12 is arithmetic with real powers. The weight lies in the single-player analysis of optimistic FTRL. The first idea, to compare consecutive argmax points through first-order optimality conditions, fails because the regularizer need not be differentiable and the maximizers can lie on the boundary of the simplex. The arguments must work with the optimality of argmax points over and with a quadratic-growth consequence of strong convexity. That consequence is not immediate from the midpoint condition in footnote 3. It needs continuity of the regularizer to pass from midpoints to the whole segment. Bounding the variation of utility vectors by the movement of the other players needs a total-variation estimate for product distributions.
Players are Fin n and strategies Fin d, both indexed from . Time keeps the paper's indices: is the initial play and sums run over . The vector is the utility vector against ; the paper never defines it. Mixed profiles and expectations use the published agt_games definitions. is and is Mathlib's sup norm. Optimistic FTRL and the leader sequence are predicates on trajectories, so every maximizer is a valid run. The goal quantifies over every run of the dynamics.
Standing assumptions and disclosed additions:
Trivializations are ruled out. The regularizer class is nonempty: satisfies it. Removing the bound on utilities would make the stability claim false. The goal fixes the paper's step size and constant, so it is not a statement about a chosen run, an unbounded supremum or a vacuous parameter range.
A complete development needs the following:
These are reusable well beyond this mission, for online learning and for learning in games, and contributions of each are welcome.
Ring learning with errors (ring-LWE) is the algebraic variant of the learning-with-errors problem on which most practical lattice-based cryptography is built, including the key-encapsulation scheme ML-KEM standardized by NIST in 2024. Its hardness rests on the paper of Lyubashevsky, Peikert and Regev, On ideal lattices and learning with errors over rings (J. ACM 60(6), 2013, doi:10.1145/2535925; conference version at EUROCRYPT 2010). The paper's main theorem (Theorem 3.6, p. 19) is a polynomial-time quantum reduction from worst-case approximate shortest-vector problems on ideal lattices to the ring-LWE decision problem. Statements about reductions, running times and negligible probabilities are outside the scope of this mission.
What this mission formalizes is the algebraic tool both of the paper's reductions rest on, which the authors list among their main technical contributions (p. 7): a Chinese-remainder technique for clearing an ideal. An arbitrary ideal of the ring of integers need not be principal, so a reduction that receives samples from a lattice cannot simply divide by a generator. Lemmas 2.14 and 2.15 show that, modulo an ideal such as , multiplication by a well-chosen identifies with , and more generally with for every fractional ideal . Steps 1–3 of the BDD-to-LWE reduction of §4.2 consist of exactly these identifications. The authors note that the lemmas are "probably standard for experts in computational number theory" (p. 16); the formulation used in lattice cryptography is theirs, and it is reused throughout the later literature on algebraic lattices.
Let be a number field of degree and its ring of integers. An integral ideal is a nonzero ideal (the paper excludes , footnote 2, p. 13). A fractional ideal is a set such that is an integral ideal for some nonzero ; the nonzero fractional ideals form a group under multiplication, and denotes the inverse. Two integral ideals are coprime when .
For the cleared ideal is . When it is an integral ideal, and " is coprime to " means
For a fractional ideal and , the map sends into , and therefore induces an -linear map
The dual of a fractional ideal is ; is the codifferent, and . For the cyclotomic field , a primitive -th root of unity, () is the automorphism with , and for a prime with a primitive -th root of unity the primes above are , . Calligraphic of the paper are written I, J, M in the milestone texts.
For nonzero ideals , with coprime to , and a nonzero fractional ideal ,
as -modules, via .
The isomorphism of Lemma 2.15 is what makes ideal lattices usable in worst-case to average-case reductions: it turns a discrete Gaussian sample from an arbitrary ideal into a uniform element of the fixed ring , and turns the ring-LWE secret in back into a coset of . Lemma 2.16 is the corresponding tool for the search-to-decision reductions of §5, which move between the CRT components of a completely split . Lemma 2.9 gives the scale of the lattices involved.
On the formal side, none of Lemmas 2.14–2.16 is stated on the platform or in Mathlib in this form. Mathlib has the Chinese remainder theorem for ideals, inverses of fractional ideals in Dedekind domains, trace duals with , and the isomorphism ; the mission connects these to the quotient modules and explicit primes that lattice cryptography works with. All statements are proved in the paper; what remains is the formal proof.
The obvious argument for Lemma 2.15 — both quotients have cardinality , so an injective map is bijective — needs the multiplicativity of the norm on fractional ideals and finiteness of the quotients, and still needs the kernel computation, which uses unique factorization: from one has to cancel and inside the group of fractional ideals and then use coprimality of and . Lemma 2.14 needs the factorization of along the primes of and a CRT choice of ; for it would assert that is principal, which is why the nonzero convention matters. In Lemma 2.16 the delicate point is the direction of the action: sends to , not .
NumberField, is 𝓞 K, fractional ideals are FractionalIdeal (𝓞 K)⁰ K, and integral ideals are coerced into them. Ideals are nonzero, per footnote 2: every statement carries I ≠ ⊥ (and J ≠ ⊥, M ≠ 0 where the paper's convention applies); I ≠ ⊥ is essential because Lean defines . Two kernel/surjectivity milestones drop the nonzero hypotheses on and , which only strengthens them.ClearedCoprime: and in the semiring of fractional ideals.FractionalIdeal.dual ℤ ℚ. is the inverse image of under IsCyclotomicExtension.Rat.galEquivZMod, acting on ideals by images; uses the representative of in . norms sum over all complex embeddings; bounds are phrased through nonzero elements of .When independent players repeatedly choose actions, a low-regret guarantee controls each player's performance against a fixed alternative. It does not directly control the social cost, the sum of all players' costs. For a class of games satisfying smoothness, however, the individual comparisons can imply a bound on the cost of the joint play. This connection makes learning guarantees useful for studying decentralized systems in which nobody selects the entire outcome. The paper uses the smooth-game framework for this purpose.
Syrgkanis, Agarwal, Luo, and Schapire study regularized learning in games and, in Appendix H, show a separate consequence for first-order regret in cost-minimization games. A first-order bound scales with the comparator's cumulative cost, rather than only with the number of rounds. Their Theorem 23 turns that guarantee into an average-cost estimate whose additive term falls as . The result is proved in the paper's supplementary material. This mission targets a machine-checked statement and proof of that known result.
There are players. Each player has pure strategies; a pure profile chooses one for each player. Player incurs a cost . The total cost is , and is the minimum over pure profiles. A mixed profile gives each player a probability distribution over its strategies. Players randomize independently, and is the expected total cost.
In round , player uses and sees a vector . Its coordinate is the expected cost of playing pure strategy against the other players' round- mixed strategies. Thus is that player's actual expected cost. Equation (21) assumes that, for every fixed pure strategy ,
The constants are the constants of the learning guarantee. The logarithm is natural.
A game is -smooth when one pure profile works against every pure profile :
Here replaces only player 's strategy in . This is the paper's cost-game smoothness condition (20). It concerns a single witness , rather than a different witness chosen for each .
The goal is Appendix H's Theorem 23. For and , if the game is -smooth and every player's realized play obeys (21), then
The constants are exactly those printed in the paper. The milestone list follows the displayed statements in its proof: the identity expressing social cost through cost-vector inner products, the aggregate first-order inequality (22), the expected smoothness inequality, the quadratic inequality for the auxiliary quantity , and the final root bound. Together they describe the intermediate claims available to solvers without changing the theorem's target.
The theorem says that the joint play of agents with individual first-order regret guarantees approaches an explicit benchmark in average social cost. The term separates the learning transient from the benchmark determined by , , and . It is a statement about arbitrary realized trajectories that meet the regret condition; the players need not coordinate on a common learning rule.
The paper already proves Theorem 23. The remaining work here is to formalize its cost model, the product-distribution expectations, the first-order bound, the smoothness transfer, and the real inequality behind the exact constants. A proof of this mission would give reusable finite-game definitions and a checked route from player-level cost comparisons to a social-cost statement. Its intermediate claims may also be useful when an alternative algorithm supplies the same first-order guarantee.
Summing the individual regret bounds leaves a sum of square roots of comparator costs. The cost benchmark in the conclusion is a single quantity, so the player-level terms cannot simply be replaced one at a time by . The cost-vector identity and smoothness condition must also agree on the same independent product distribution: changing only one player's pure action while keeping the opponents mixed is easy to encode with a different, unintended distribution. After those choices, the exact coefficient depends on the signs and domains in a quadratic bound. In particular, the intermediate Cauchy–Schwarz inequality uses , while the final theorem has no sign restriction on .
Players are Fin n, and each player's strategies are Fin d. The condition makes the pure optimum a minimum over a nonempty finite set. Mixed profiles are probability weights on each strategy set, with the players' choices independent. The published agt_games definition supplies product-profile probabilities and finite expectations; its expectedPayoff operation is used as an expectation of costs. The paper-specific layer defines pure and expected social cost, the pure optimum, cost vectors, smoothness, and the realized first-order regret condition.
Time has the paper's indices: every round sum runs from through , without shifting the sequence. The goal uses and so its divisions represent the paper's formula. Every cost is in ; every played profile is mixed; (21) is required for every player and every fixed pure comparator. The formulation does not restrict the game to a chosen example, assume the goal inequality, replace with a default-valued infimum, or allow an empty strategy set. The first-order condition is stated on the realized sequence, which follows from any algorithm that guarantees (21) for all sequences.
The intermediate inequality (22) and the quadratic milestone explicitly require , the sign used in their Cauchy–Schwarz step. Theorem 23 itself allows any real , as the paper's stated formula does. The source prints in (22); the Lean statement uses the intended round index . The source also switches between and ; both denote the natural logarithm. Contributions on finite product expectations, the mixed smoothness consequence, and the final real inequalities are all within scope.
Many stochastic optimization models contain an expected-value constraint
where is a random object with unknown law , is a decision and is a known loss. When is known only through an i.i.d. sample , data-driven distributionally robust optimization (DRO) replaces by the worst case over a ball of distributions around the data. H. Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization (arXiv:1605.09349v1, 2016; Operations Research 67(4), 2019), studies a ball of reweightings of the sample itself, measured by the Burg entropy, and links its radius to empirical likelihood (Owen 2001).
Lam's Theorem 2 shows that, for a fixed decision , the minimum and maximum of over this ball bracket with probability tending to when the radius is . Theorem 3, the goal of this mission, complements it: the two bounds also converge almost surely to . A confidence statement says the robust bounds are rarely wrong; consistency says they are eventually tight, so that the robust constraint does not stay conservative as data accumulate.
This mission is the second of a three-mission series on the pointwise theory of the paper (1: coverage, Theorem 2; 3: reduction to a Burg ball on a finite support, Proposition 1).
Let be i.i.d. random elements of a measurable space with law . Fix a decision and write .
The Burg generator is for and for . The empirical Burg-entropy divergence ball of radius is the set of weight vectors
On the simplex, , the -divergence of from the uniform weights.
Let and let be the -quantile of the distribution. The lower and upper empirical DRO values are
The proof works with the centred observations .
Under the conditions of Theorem 2 (, finite),
with the printed conventions at and for arguments outside the domain of the logarithm. 3. The elementary inequality (p. 34): for . 4. (77) (p. 34): if with , then
Milestones 2, 4 and 5 are deterministic statements about an arbitrary data vector; only Lemma 3 and the goal are probabilistic.
The result. Theorem 3 shows that the empirical DRO with the calibration is a consistent estimator of the constraint function at every fixed decision, not only a confidence bound. Together with Theorem 2 it places the empirical Burg-ball DRO on the same footing as the classical normal-approximation confidence interval: correct asymptotic coverage and shrinkage to the truth. The deterministic bounds (76)–(77) are also reusable on their own: they control the worst-case reweighting of any finite sample by its first two empirical moments.
Formalizing it. The theorem is proved in the paper; no machine-checked proof is known. The mission asks for a formal proof of the printed argument, specialized to one decision. A closely related open target exists on the platform: GenEmpLik.Expansion.lemma_1 (Duchi, Glynn and Namkoong) states the expansion of the robust mean, sample mean plus , for a smooth generator class under stationary ergodic data. Combined with the strong law it would give the upper half of Theorem 3, but it is a different statement with different hypotheses and is itself unproved, so it is not used as a milestone here.
The tempting argument, "the ball shrinks to the empirical distribution and the empirical mean converges", does not close by itself: is only square integrable, not bounded, and the maximizing weight shifts mass towards the largest observations, so the gap has to be controlled against the extremes of the sample rather than by the size of the ball alone. The printed proof routes this through the convex dual (76). That step needs a constraint qualification, the conjugate of the Burg generator with its boundary conventions (an infinite value outside the domain of the logarithm, and the degenerate multiplier ), and a choice of multiplier that dominates every centred observation while still letting all three terms of (77) vanish. The almost-sure statement then combines Lemma 3 with two strong laws on one event of full probability.
ξ 0, …, ξ (n-1): a sequence of measurable maps that is independent (iIndepFun) and identically distributed (IdentDistrib with ξ 0). is the Bochner integral of h x ∘ ξ 0, and the moment conditions are MemLp (h x ∘ ξ 0) 2 (finite mean and variance) together with positive variance, which makes the integral the true mean.EuclideanSpace ℝ (Fin m); plays no role in a pointwise statement and is dropped.GenEmpLik.Expansion.robustMean, whose ball has radius .robustMean burg (q/2); is robustLower burg (q/2) from the frozen shared EmpiricalDRO.Coverage.Setting module, a real infimum over the same published ball (PhiDivRobust.Counterpart.probUncertaintySet). For the value sets are nonempty and bounded, so the real sSup/sInf are the attained maximum and minimum.burg is valued in EReal with for , so a zero weight is excluded from the ball by an infinite divergence and never by a junk value of Real.log. The dual summand dualTerm is EReal-valued with the printed conventions: for ; or at .sSup/sInf of an empty value set, a free radius detached from the quantile, and a dropped variance condition are all excluded by the encoding above. The paper's printed (75) writes where its radius makes it ; at a single decision the two coincide.NumStochOpt.ListScheduling.lemma_8_1_i_max_over_sqrt_ae, included as a reference. Mathlib's ProbabilityTheory.strong_law_ae supplies the laws of large numbers. Contributions welcome: the duality (76) for general -divergence balls, and the deterministic bound (77).Newton's law of universal gravitation states that any two point masses attract each other with a force proportional to the product of their masses and inversely proportional to the square of their distance. It is the first quantitative law of gravity (Newton, Principia, 1687) and it remains the working model of gravity in celestial mechanics, geophysics and engineering whenever relativistic effects are negligible.
The law is stated for point masses, while planets, moons and apples are extended bodies. Newton delayed publication for about twenty years because he could not prove that the Earth attracts external bodies as if all its mass were concentrated at its centre. The result that closes this gap is the shell theorem: a spherically symmetric distribution of mass exerts, on every external point, the same gravitational attraction as a point mass at its centre carrying the total mass; and mass located at radii larger than that of the test point exerts no net force at all.
Timeline (as described in the source):
Space is with the Euclidean norm. The gravitational constant is .
If is a finite, spherically symmetric mass distribution carried by the closed ball , then for every with ,
The shell theorem is what licenses treating the Sun, planets and moons as point masses in the -body problem and in Kepler orbit computations, and it gives the linear growth of the gravitational field inside a uniform planet. The interior statement ("no net force inside a hollow shell") has an exact analogue in electrostatics (Coulomb's law is also inverse-square).
The results are classical and fully proved on paper. This mission asks for machine-checked proofs, together with the reusable infrastructure they require: vector-valued integrals against rotation-invariant measures, the surface measure of the sphere, and the Newtonian kernel .
Newton's argument (or the modern one via Gauss's law) is geometric: slice the shell into rings, or apply the divergence theorem to a sphere. Neither is directly available: Mathlib has no divergence theorem on spheres in the required form, and the ring-slicing computation requires explicit spherical coordinates for a surface measure that is defined abstractly. Using symmetry alone shows the field is radial, but its magnitude requires an actual computation of a singular integral (for the interior of a solid ball the integrand is unbounded).
EuclideanSpace ℝ (Fin 3). Mass distributions are Measures; the field is a Bochner integral. Because a non-integrable Bochner integral is defined to be , statements where integrability is not automatic either carry an explicit integrability hypothesis or are placed where the integrand is bounded (test point strictly outside the support).Space ≃ₗᵢ[ℝ] Space), centred at the origin.NNReal); radii are assumed strictly positive.Measure.toSphere (surface measure on the unit sphere) pushed forward by scaling.Contributions welcome: a general "radial field" lemma from spherical symmetry, the computation of the field of a uniform shell, and the disintegration of a spherically symmetric measure into shells.
Comparing histograms is a basic operation in statistics, computer vision and machine learning: a bag of image descriptors, a word-frequency vector, a discretized density. When the bins carry a geometry (colors that are close to one another, words with related meanings), a comparison that ignores the geometry, such as an norm between the histogram vectors, treats a small shift of mass to a neighboring bin as severely as a shift to a distant bin. Optimal transport compares two histograms by the cheapest way to move one onto the other, with costs read off a ground distance between bins. Rubner, Tomasi and Guibas introduced it to image retrieval as the earth mover's distance (Rubner et al. 2000), and it has since been used for document classification (Kusner et al. 2015) and as a training loss (Frogner et al. 2015).
These uses rely on the transport cost being a distance, so that nearest-neighbor search, clustering and the geometry of the space of histograms behave as expected. This mission formalizes the statement that it is one: Proposition 2.2 of Peyré and Cuturi, Computational Optimal Transport (2019), the discrete form of the classical fact that the -Wasserstein distance is a metric (Villani 2003, Theorem 7.3).
Fix and write . The probability simplex is
its elements are histograms. For the set of couplings (2.10) is
the nonnegative matrices with row sums and column sums ; is the mass sent from bin to bin . For a cost matrix , the Kantorovich problem (2.11) is
A matrix is a distance on if it is symmetric, exactly when , and for all . For , write for the entrywise power. The -Wasserstein distance (2.17) is
In the Lean development these are couplings a b, frob C P, otCost C a b, powCost D p and W D p a b in the namespace CompOT.Metric.
For a distance matrix and , for all ,
The case of the goal's attainment and triangle inequality is already proved on the platform, in another encoding (couplings as functions on for a finite metric space ): MarkovMixing.transport_metric, included here as a reference item. The goal for general is new.
The result. Proposition 2.2 makes a metric space whose metric depends on the ground distance . This is what entitles later chapters of the book to speak of Wasserstein barycenters, geodesics and Lipschitz properties of the transport cost, and it underlies the use of as a loss or a retrieval distance. Remark 2.15 of the same page records that for it is , not , that is a distance, so the restriction is substantive.
Formalizing it. The result is classical and fully proved in the book; it has not been machine-checked for general in this discrete matrix form. The platform's result uses a different encoding of couplings, so this mission supplies the matrix-form transportation polytope , the cost and shared with the other missions of this series, plus a discrete gluing lemma and a Minkowski step stated for arbitrary couplings, which are reusable in any finite transport argument.
Symmetry and definiteness are short once the minimum in is known to be attained, which needs compactness of ; strict positivity for fails for an infimum that is not attained. The triangle inequality is the substantial part. The direct idea of composing the two transport plans as does not give a coupling: the composition must be renormalized by the middle histogram , and may have zero entries, on which a naive is undefined. The renormalized matrix must then be shown to have the right marginals, which uses that wherever . The final step needs Minkowski's inequality for weighted sums together with the triangle inequality of and the monotonicity of ; for it fails.
Indices are Fin n (0-based). Histograms are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and is Mathlib's stdSimplex ℝ (Fin n); histograms may have zero entries. is a real infimum over the subtype , and every theorem assumes the histograms lie in , where is nonempty (it contains ) and compact. That attainment is part of what a solver proves; it is not a hypothesis. The exponent is a real number with , and all powers are real powers. The book's "positive" is read as ; strict positivity is the clause . The hypotheses of the goal are exactly those of the page: , (i)–(iii), and . The milestones carry the same setting, and milestones 5 and 6 are stated for all couplings instead of only optimal ones, since the proof does not use optimality there.
A trivializing formalization is ruled out: without the simplex hypotheses can be empty and the real infimum would be , making "" true for unrelated histograms; and the four claims are stated about itself, not about the glued coupling or about a minimum over a set assumed nonempty.
Needed infrastructure: compactness and nonemptiness of and attainment of ; transposition of couplings; the gluing construction; Minkowski's inequality for finite weighted sums (Mathlib has Real.Lp_add_le and its weighted variants). Proofs of any milestone are welcome, as are reusable lemmas on .
Optimal transport between two histograms is a linear program: move mass out of each source bin and deliver mass to each target bin at unit cost , as cheaply as possible. Its dual replaces the transport plan by a pair of price vectors and is the basis of most of the computational methods in G. Peyré and M. Cuturi's Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019, doi:10.1561/2200000073): the dual ascent and Hungarian methods, the auction algorithm, the semi-discrete solvers of Chapter 5, and the dual reading of Sinkhorn's algorithm in Chapter 4. The book states the duality as Proposition 2.4 and derives it from linear programming strong duality (Bertsimas and Tsitsiklis, Introduction to Linear Optimization, 1997, Theorem 4.4). Remark 2.21 gives it an economic reading: a vendor sets a collection price at each warehouse and a delivery price at each factory, and the best price the vendor can charge while staying below every shipping cost equals the optimal transport cost.
This is the third mission in a series on the book. It covers §2.5 (Dual Problem, pp. 382–385) and §3.1–3.3 (Kantorovich Linear Programs, C-Transforms, Complementary Slackness, pp. 400–405).
Indices run over and . A histogram is a vector in the probability simplex . Fix , and a cost matrix ; no sign or metric condition is imposed on .
In Lean these are couplings, frob, IsOptimalCoupling, dualFeasible, dualObj, IsDualOptimal, cTransform, cbarTransform and Complementary in the namespace CompOT.Duality.
Stated with both extrema attained: there are an optimal coupling and a dual optimal pair with .
Milestones 6 and 7 are consequences of the goal; milestones 1 and 5 do not need it.
Proposition 2.4 is the finite-dimensional form of Kantorovich duality. It turns the optimal cost into a maximum over price vectors, so that any admissible pair of prices certifies a lower bound on and an optimal pair certifies optimality of a plan through complementary slackness (Propositions 3.2 and 3.3). The -transform reduces the dual to a concave maximization in one vector (3.5), which is the form used for semi-discrete transport and for stochastic dual methods; Proposition 3.1 shows that alternating - and -transforms stalls after one round.
All of these results are classical and proved in the book or by direct reference to linear programming. General-form LP strong duality, weak duality and complementary slackness are already machine-checked on the platform (LinearOptimization.lp_strong_duality and its siblings, from the Bertsimas–Tsitsiklis series); measure-theoretic weak Kantorovich duality is also on the platform with integrability hypotheses. What this mission adds is the book's own discrete statements in the book's notation, as a base that later missions of the series (dual ascent, auction, entropic duality) can cite, with the -transform calculus of §3.2 formalized for real-valued finite costs.
Weak duality, the -transform facts and Proposition 3.3 are finite computations with sums and minima. The content of the mission is the equality in Proposition 2.4 together with attainment of both the minimum and the maximum. Attainment of the minimum needs compactness and nonemptiness of ; attainment of the maximum is not a compactness argument, since is unbounded (it is invariant under ). Reducing Proposition 2.4 to the general LP statement requires an explicit translation of and into the general-form primal–dual pair, including the sign conventions of equality-constrained primal variables and free dual variables. The Lagrangian argument on p. 382–383 exchanges a min and a max without justification beyond "always possible for linear programs", so it does not yield a proof by itself.
Indices are 0-based (Fin n, Fin m); matrices are Matrix (Fin n) (Fin m) ℝ; all quantities are real. Histograms are encoded as a ∈ stdSimplex ℝ (Fin n), the book's standing convention for , and every statement involving or carries it; this also forces . Zero entries in and are allowed. Optimality of a plan and of a dual pair are predicates quantifying over the whole feasible set, never real ⨅/⨆, so no junk value from an empty or unbounded set can enter. The -transforms are real infima over a finite index set; statements that use them without histograms assume (and where the -transform appears), because Lean's infimum over an empty index is .
The goal cannot be satisfied trivially: it asserts existence of a plan that is optimal against every coupling and a pair that is optimal against every admissible pair, with equal values; dropping either optimality clause, or the equal-mass hypotheses, changes the theorem.
Two printed slips are corrected and disclosed in the item notes: Proposition 3.2 prints where its proof uses , and Propositions 3.2 and 3.3 refer to the primal and dual as "(2.24)" and "(2.11)", meaning the discrete primal (2.11) and dual (2.20).
Useful infrastructure: the platform's general-form LP strong duality (included as a reference item), Mathlib's stdSimplex and finite infima. Contributions welcome: proofs of each milestone, a direct proof of Proposition 2.4 by reduction to the LP theorem, and alternative proofs of the goal.
Ordinary least squares and its robust relatives (least absolute deviations, Huber, -insensitive and quantile regression) fit a linear predictor by minimizing an average loss over the training sample. That average estimates the out-of-sample error poorly when the sample is small, and the usual fix is to add a regularization penalty such as a norm of the weights. Choosing that penalty is often a heuristic. Distributionally robust optimization gives one principled derivation of it: hedge against every data-generating distribution that is close to the empirical one in a Wasserstein distance, and minimize the worst-case expected loss.
S. Shafieezadeh-Abadeh, D. Kuhn and P. Mohajerin Esfahani, Regularization via Mass Transportation (arXiv:1710.10016v3, 2019; JMLR 20, 2019), show that for linear regression with a convex Lipschitz loss this worst-case problem is exactly a regularized empirical risk problem, with an explicit dual-norm penalty. The same identity appears for the logistic loss in Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn, Distributionally Robust Logistic Regression (NeurIPS 2015, arXiv:1509.09259). For a general convex loss it is Theorem 10 of the tutorial by Kuhn, Mohajerin Esfahani, Nguyen and Shafieezadeh-Abadeh (arXiv:1908.08729). Blanchet, Kang and Murthy (arXiv:1610.05627) obtain the square-root Lasso from a type-2 transport cost. This mission formalizes the regression theorem of the first paper, Theorem 3.1(ii) on p. 8. The source PDF is the arXiv preprint v3, and every page and label cited here refers to it.
Data. Inputs are and outputs are . A pair is written . The training samples are for , and is their empirical distribution (§2.1, p. 5).
Hypotheses and loss. A weight vector defines the linear hypothesis . A univariate convex loss defines the regression loss (§3.1, p. 8). The residual is the pairing of with the vector .
Norms. carries an arbitrary norm with dual norm (§1.1, p. 4). The Lipschitz modulus of is , and the convex conjugate is (§1.1).
Wasserstein ball. With transport cost , the Wasserstein distance (Definition 2.2, p. 7) is
where the infimum runs over couplings of and . The ball of radius is (3). The distributionally robust regression problem is
Let , , , and let be nonnegative, convex and Lipschitz continuous. Then for every
so (4) and the regularized problem (6) have the same optimal value.
WassersteinDRO.Duality.strong_duality_worst_case_risk_v2, which covers it for .The result. The theorem turns an infinite-dimensional min–max problem over distributions into a finite convex program over : an empirical average plus a norm penalty. The penalty is not but , because the transport cost moves outputs as well as inputs. It scales with the radius and with the Lipschitz modulus of the univariate loss. With the Huber, -insensitive and pinball losses it gives Corollaries 3.2–3.4 of the paper. It also gives a statistical reading of the regularization weight as a Wasserstein radius, which the paper's §4 turns into generalization bounds.
Formalizing it. The theorem is proved in the paper; none of its items is formalized yet except Lemma A.1. Lemma A.1 is available in a general form (any , any closed support set, ) as a proved platform theorem from the mission Wasserstein Distributionally Robust Optimization. The per- identity also follows from the proved WassersteinDRO.Duality.convex_loss_p1_v2 (Theorem 10 of the tutorial, also present as WassersteinDRO.Regularization.convex_loss_p1_v2; the public mission Wasserstein Distributionally Robust Optimization IV has it as goal) once one shows that . No platform item states that factorization. What this mission adds is the paper's explicit form of the penalty, Lemma A.3 (the inner supremum for an arbitrary convex Lipschitz loss and an arbitrary norm), and the conjugate description of the Lipschitz modulus. The last two are reusable in classification (mission I of this series states them again in its own namespace) and in every Wasserstein-regularization result with linear hypotheses.
The obvious argument is to write the worst case as a supremum over perturbations of the samples and bound each perturbed loss by its Lipschitz constant. That gives only the inequality "", and only for one Lipschitz constant. The identity needs two further steps that this bound does not supply. First, the bound must be attained: the supremum over distributions has to be shown to reach , a matching lower bound that a Lipschitz estimate cannot give. Second, must be the modulus, not any constant: an upper Lipschitz constant makes the identity false. In Lemma A.3 the case sits exactly on the boundary between a finite and an infinite supremum. A further point is that the duality of Lemma A.1 needs , while the theorem includes .
E with its Borel σ-algebra. A continuous linear isomorphism e : E ≃L[ℝ] (Fin n → ℝ) × ℝ reads off inputs and outputs. The theorem therefore covers every norm on ; fixing a concrete norm would prove it for that norm only. The functional is pairing e w, and is its operator norm.WassersteinDRO_Duality_ambiguitySet, _worstCaseRisk_v2, _empiricalDistribution and _lipschitzModulus. The worst case is taken in the extended reals, and expectations follow the convention of nominalRisk_v2 (no junk value for non-integrable losses). takes values in .A basic question of additive combinatorics asks how a set grows under repeated addition. If a finite set in an abelian group satisfies for some finite set , how large can the iterated sumsets be? Plünnecke's inequality gives the answer used throughout the subject: some nonempty part of grows by at most a factor per added copy of . Combined with Ruzsa's triangle inequality it becomes the Plünnecke–Ruzsa inequality , which underlies Freĭman-type structure theorems, sum–product estimates and the polynomial Freĭman–Ruzsa programme.
Timeline.
Let be a group with finite subsets , , . The product set is , and denotes cardinality. In an abelian group, written additively, the sumset is , and for the iterated sumset is with summands, . It is not the dilate .
A nonempty subset has minimal growth under if
Such an exists whenever is nonempty, since has finitely many subsets. In Lean, is a Group or AddCommGroup with decidable equality, the sets are Finset G with the pointwise operations of Mathlib (A * B, A + B, h • B), and cardinalities are #A cast to ℝ.
For finite , in an abelian group with nonempty and , there is a nonempty with
The point is the order of quantifiers: one serves all .
FamousTheorems.pluennecke_petridis (additive notation, cross-multiplied), and enters the mission as a reference.Theorem 3.1 is the form of Plünnecke's inequality used in applications. Two consequences follow directly. Taking gives whenever . Combining one for all with Ruzsa's triangle inequality gives (Theorem 1.2 of the paper). With a separate for each , the second step would need the same set for and , and that is exactly what Theorem 3.1 provides. Theorem 1.5 is the non-abelian ingredient: missions 2 and 3 of this series apply it to obtain explicit Plünnecke-type bounds for and in arbitrary groups.
Formalizing it. The results are proved and classical. Mathlib already contains Proposition 2.1 (Finset.pluennecke_petridis_inequality_mul) and the Plünnecke–Ruzsa inequality Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add. Its proof runs through a private lemma that bounds for one fixed minimiser, but no public statement in Mathlib or on the platform asserts Theorem 3.1 or Theorem 1.5 in the form "there exists a nonempty for all " (respectively "for all "). This mission adds those statements as reusable, citable nodes in the paper's numbering.
A first attempt iterates the hypothesis directly: would follow if again grew by a factor under , but nothing controls the growth of . The ratio is not monotone in , and passing to subsets of can only help if the subset is chosen correctly. Choosing a different good subset for each gives Theorem 1.1 but loses the uniformity. The work is to show that one fixed subset controls all the products simultaneously, and in the non-abelian Theorem 1.5 to keep the order of the factors , , throughout.
AddCommGroup with DecidableEq. Theorem 1.5 is stated in a Group, with no commutativity, as on the page. The factor order is preserved.h • B (the -fold sumset; 0 • B = {0}), and "for all " ranges over all natural numbers, including the true case .ℝ. No hypothesis is added: it follows from the hypotheses once and are nonempty (with empty they force only , and every conclusion is still true).Finset.ruzsa_covering_mul, Finset.ruzsa_triangle_inequality_mul_mulInv_mul) and are not items of this mission.