Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Periodic signals are the basic objects of audio processing, electrical engineering and the analytic study of partial differential equations, and the standard first-course tool for handling them is the Fourier series: a decomposition of a -periodic signal into sinusoids of frequencies . The identity that makes the decomposition quantitatively useful is Parseval's theorem: the average power of the signal equals the sum of the squared moduli of its Fourier coefficients, so energy can be accounted for frequency by frequency.
This mission formalizes the chain of results leading to that identity exactly as it is presented in the open-access undergraduate textbook Análise de Fourier — Um Livro Colaborativo (Esequia Sauter and Fabio Souto de Azevedo, orgs., UFRGS/REAMAT, 2022): the orthogonality relations of the trigonometric system (Teorema 3.2.1), the coefficient formulas (Teorema 3.2.2), the passage to the exponential form (§4.2), and the Parseval identity itself (Teorema 5.1.1).
Fix a period and write
For a real-valued integrable on the book defines the trigonometric Fourier coefficients (eq. 3.23)
and for a complex-valued the exponential coefficients (§4.2, eq. 4.8)
which for real satisfy . The average power of a -periodic signal is (Definição 5.1.1)
A trigonometric polynomial of degree (Definição 3.2.1) is
For and continuous and -periodic,
The book states the identity for a periodic function "representable by a Fourier series"; the mission fixes continuity as the concrete sufficient regularity hypothesis, which keeps the statement non-vacuous and true, and leaves the sum as an unordered sum over so that no summation order is smuggled in.
Parseval's identity converts an integral estimate into a coefficientwise one: it is the bridge between the time domain and the frequency domain, underlies the RMS computations of the book's own electrical-engineering examples (Exemplo 5.1.2), and yields closed-form evaluations of numerical series (the book's Exemplo 5.1.3 computes a series of reciprocal odd squares this way).
Mathlib already contains the abstract Hilbert-space form of the identity for the Fourier
basis on the circle AddCircle T. What this mission adds is the concrete, classroom-level
layer that an engineering or physics reader recognizes: coefficients written as interval
integrals of a function on with an explicit period , the real
form, the exponential form and the dictionary between them, and the orthogonality
relations as free-standing computations. That layer is reusable by any later mission in
this series (transformada de Fourier, equação do calor, equação da onda).
The obvious route — expand , substitute the Fourier series, and integrate term by term — is exactly the book's proof, and it is the step that a formal development cannot take for granted: interchanging the integral with an infinite sum requires a convergence theorem that the book explicitly places outside its scope (the remark after Definição 3.2.3), and pointwise convergence of the Fourier series of a merely continuous function is false in general. A complete proof must run through convergence rather than pointwise convergence, so the central task is to connect the interval-integral coefficients on with the Hilbert-space machinery for the circle, including the change of variables and the normalization of Haar measure.
The development commits to the following conventions, all fixed in the definition bundle so that every statement shares them:
The goal is not trivializable: the hypotheses (a positive period, a continuous periodic function) are satisfiable, and both sides of the identity are non-degenerate already for .
Useful infrastructure beyond the mission: the dictionary between the interval-integral
coefficients on and Mathlib's fourierCoeff on AddCircle T, and the
orthogonality relations as standalone integral computations.
The discrete Fourier transform (DFT) is the basic spectral tool of digital signal processing, numerical analysis and computational number theory: it turns a finite sample of a signal into its frequency content, converts convolution into pointwise multiplication, and underlies fast integer and polynomial multiplication. Computed straight from its defining sum, a transform of length costs arithmetic operations. The fast Fourier transform (FFT) is any method that computes the same values in operations, and the radix-2 Cooley–Tukey algorithm is the most widely used of them.
The history is long and worth stating precisely. Gauss used an equivalent divide-and-conquer scheme in unpublished work of 1805 on the orbits of Pallas and Juno, without any complexity analysis. Danielson and Lanczos (1942) published the doubling step — the even/odd splitting identity that the recursion rests on — for x-ray crystallography. Good (1958) gave the prime-factor algorithm for coprime factorizations. Cooley and Tukey (1965) published the general composite-size algorithm together with the analysis that made the method famous. What is not known is a matching lower bound: whether a DFT of length can be computed in arithmetic operations is open.
Fix a length and a sequence of complex samples , modelled as a function . The DFT of length evaluated at frequency index is
and the inverse transform of a spectrum is
Only the first samples enter the sum; the frequency index is an arbitrary natural number, and the transform is -periodic in it.
The radix-2 Cooley–Tukey algorithm is the recursion on the exponent , with :
where is the transform of the even-indexed subsequence and that of the odd-indexed one. The factor is the twiddle factor of the merge stage.
The arithmetic cost of that recursion is modelled by two counters. At the merge stage of a transform of points there are butterflies; each butterfly performs one twiddle-factor multiplication and two complex additions, and the two recursive calls are on points each:
The goal fixes no operation count and no rate: it asserts only that the recursion computes exactly the transform it is supposed to compute, at every frequency index, for every input. That is the statement an implementation's correctness rests on, and it stays true whatever the cost analysis of the algorithm turns out to be.
The milestones are the intermediate statements the source separates out: -periodicity of the transform in the frequency index; the Danielson–Lanczos even/odd splitting
Fourier inversion for ; the conjugate symmetry of the spectrum of a real input; and the closed forms and of the two cost recursions, with .
Fourier inversion and the splitting identity are the two facts that make the transform usable at all: the first says no information is lost, the second is the single algebraic step from which every Cooley–Tukey variant — mixed radix, split radix, iterative bit-reversed implementations — is assembled. The operation counts are what justify the claim that the algorithm is rather than : for they are the difference between roughly and roughly complex multiplications.
None of this is open mathematics; all of it is classical. What this mission produces is a self-contained machine-checked development of the radix-2 algorithm against an explicit definition of the DFT: a recursive algorithm, a proof that it agrees with the defining sum at every index, and a proof of its arithmetic cost. Mathlib carries Fourier theory for characters of finite abelian groups and for , but the mission is stated against the elementary sum above so that the statements can be read, and audited, without that background.
The obvious induction on does not close by itself. Unfolding the recursion gives the even and odd sub-transforms evaluated at the reduced index , while the splitting identity produces them at . Closing the gap needs periodicity of the length- transform in its frequency index — which is why periodicity is a milestone rather than a step inside the main proof. The second recurring obstacle is bookkeeping with the exponential: and are the only analytic inputs, but they must be applied under a finite sum with natural-number casts, where -subtraction and division by a cast that may be zero are easy to get wrong.
Sequences are total functions , not vectors of a fixed length: the length appears only as the range of the defining sum, so the transform of length ignores for . The frequency index ranges over all of , and the goal is asserted for every such index, not only for — the periodicity of both sides makes this the stronger, and cleaner, statement.
Degenerate inputs are inside the statements, not excluded by hypothesis. The length- transform is the empty sum ; division by the cast follows Lean's convention , which is why inversion carries the hypothesis and the splitting identity carries . The real-input symmetry is stated for , with -subtraction in .
There is no trivializing reading: the FFT recursion is defined without ever mentioning the DFT, the cost counters are defined by their own recursions, and every hypothesis in the list above is satisfiable.
A complete development needs: the geometric-sum evaluation of for an -th root of unity (for inversion), the even/odd reindexing of a sum over , and the periodicity computations above. All of these are reusable beyond this mission; the splitting identity in particular is the entry point for a mixed-radix or split-radix sequel.
The NRL Plasma Formulary is a standard desk reference of the plasma-physics community: a compilation of the formulas, constants and unit conversions used in daily practice. Its opening section, "Numerical and Algebraic" (p. 3 of the 2013 edition), collects the few purely mathematical identities the rest of the handbook leans on. Two of them are exact summation formulas rather than approximations, and the first is the Rothe–Hagen identity, quoted there as valid "for all complex , , except when singular" and attributed to H. W. Gould's work on binomial coefficient summations.
Unlike the handbook's numerical entries, this identity is a theorem with a precise hypothesis set, and it is exactly the kind of entry a reader takes on trust. It generalizes the Vandermonde convolution, it is the coefficient identity underlying the generalized binomial series, and it specializes to Abel's binomial theorem. Formalizing it turns one line of a reference handbook into a machine-checked statement and produces, as a by-product, a reusable Lean development of binomial coefficients with an arbitrary complex upper index.
For a complex number and a natural number , the generalized binomial coefficient is the falling factorial divided by a factorial,
with the empty-product convention . It is a polynomial in of degree , and it agrees with the usual binomial coefficient when is a natural number.
Fix complex parameters , , and, for , consider the Rothe factor
which is defined whenever . The factor in the denominator cancels against the leading factor of the falling factorial, so extends to a polynomial in and : and, for ,
Both forms occur in the literature; the mission carries both and asks for the comparison between them, because the quotient form is the one printed in the handbook while the polynomial form is the one that carries no side condition.
For complex and , provided and for every , and ,
This is the handbook's line, with its "except when singular" proviso made explicit as the three non-vanishing hypotheses.
in terms of the polynomial form above. This version holds for all complex , with no exceptional locus, and implies the printed form wherever the latter's denominators are non-zero.
The first is Pascal's rule for a complex upper index; the second is the Vandermonde convolution over , which is the case of the goal.
The identity is the convolution law of the generalized binomial series: the formal power series solving satisfies , so the goal is the statement read off coefficientwise (Graham–Knuth–Patashnik, Concrete Mathematics, §5.4). Consequences include Abel's binomial theorem, the Lagrange-inversion count of -ary trees, and ballot-type identities in lattice-path enumeration.
Mathlib provides the Vandermonde convolution for natural-number arguments (Nat.add_choose_eq), the ascending and descending Pochhammer polynomials, and Ring.choose for binomial rings; it does not contain the Rothe–Hagen identity in any form. The four statements of this mission are therefore new formal content, and the complex-upper-index binomial API they force is reusable well beyond the mission.
The identity is classical and has been proved many times since Rothe (1793) and Hagen (1891), with the modern treatment in Gould's papers; nothing here is open mathematics. What is missing is a machine-checked proof.
The obvious attack — induction on using Pascal's rule — does not close as stated: the summand is not Pascal-stable, since shifting by moves for every at once, and the induction hypothesis is about a different family. The standard proofs instead treat both sides as polynomials in and for fixed and , verify the identity on an infinite set of points where a combinatorial reading is available, and conclude by the identity theorem for polynomials; or they extract coefficients from the generalized binomial series via Lagrange inversion. Either route needs infrastructure: a two-variable polynomial-identity argument over , or a formal-power-series compositional inverse.
A second, more prosaic difficulty is the singular locus. The printed identity divides by for every , and in Lean division by zero returns zero rather than failing, so a formalization that drops the non-vanishing hypotheses states a different — and in general false — claim.
All statements are over . The generalized binomial coefficient is defined as an explicit product over Finset.range k divided by (k ! : ℂ), so holds definitionally and no Nat.choose coercion enters. Sums run over Finset.range (n+1), with the complementary index written as the truncated natural subtraction n - k; inside that range this is the ordinary , so the truncation convention is never exercised.
The proviso "except when singular" is formalized as three explicit hypotheses — for all , for all , and — rather than by relying on Lean's junk value for division by zero. These hypotheses are satisfiable (for instance , ), so the goal is not vacuous, and they constrain only denominators, so they do not trivialize the sum.
The singularity-free milestone commits to a total function rotheA defined by cases on , with value at ; the comparison milestone pins that function to the quotient form under the non-vanishing hypothesis, so the mission cannot be satisfied by proving facts about a differently normalized object.
Contributions welcome beyond the milestones: complex-upper-index binomial API (symmetry, negation , polynomiality in the upper index), and any formal-power-series development supporting Lagrange inversion.
This mission formalizes the group theory of J. A. Wolf's Growth of finitely generated solvable groups and curvature of Riemannian manifolds, J. Differential Geometry 2 (1968) 421–446 (doi:10.4310/jdg/1214428658), namely its §3 and §4. Wolf opens with the object of study: "If a group is generated by a finite subset , then one has the 'growth function' , where is the number of distinct elements of expressible as words of length on " (p. 421). Section 3 proves that a group with a finitely generated nilpotent subgroup of finite index "is of polynomial growth, and in fact "; section 4 proves that "a polycyclic group, either has a finitely generated nilpotent subgroup of finite index and thus is of polynomial growth, or has no such subgroup and is of exponential growth" (p. 421).
Applying Milnor's companion note, which is the complete mission Milnor: growth of finitely generated solvable groups on this platform, Wolf concludes "that a finitely generated solvable group, either is polycyclic and has a nilpotent subgroup of finite index and is thus of polynomial growth, or has no nilpotent subgroup of finite index and is of exponential growth" (p. 421). That is the Milnor–Wolf theorem, the goal here, and Wolf's Theorem 4.8. It prompted the question Wolf asks on p. 422, "whether every finitely generated group , which is not of exponential growth, necessarily has a nilpotent subgroup of finite index"; Grigorchuk's groups of intermediate growth (1984) answered it in the negative, and Gromov (1981) proved that polynomial growth alone does force a nilpotent subgroup of finite index.
Growth. For a finite subset of a group , the growth function counts
the elements expressible as words of length on , a word
having length (p. 426). The published MilnorWolf.growthFunction S m takes
this as the size of the ball Chou.wordBall S m, the set of products of at most factors from
. Wolf's two kinds of bound (p. 421) are polynomial growth of degree ,
, and exponential growth, with ; the
published predicates are MilnorWolf.HasPolynomialGrowthOfDegreeLE and
Chou.HasExponentialGrowth, the latter with , which is what Theorem 4.3 actually produces.
Both quantify over some finite generating set, and Wolf shows (p. 427, p. 434) that neither depends
on which one.
Growth exponents. For a finitely generated nilpotent with lower central series
, each factor
is finitely generated abelian with free part of rank ; Wolf's (3.3)
sets and . These are
MilnorWolf.growthExponentOne and MilnorWolf.growthExponentTwo.
Polycyclic groups. A solvable group is polycyclic if it satisfies condition (1) of
Proposition 4.1: "There is a normal series
with every quotient
finite or infinite cyclic" (p. 433), where a normal series, as in Kurosh, has each term normal in
the preceding one. This is MilnorWolf.IsPolycyclic. Solvable is Mathlib's
Group.IsSolvable.
The goal is Wolf's Theorem 4.8 (p. 438): "Let be a finitely generated solvable group. If has a nilpotent subgroup of finite index, then is polycyclic and of polynomial growth of degree . If does not have a nilpotent subgroup of finite index, then is of exponential growth."
The milestones are the results it rests on, in the paper's order. Section 3 climbs from two rescaling lemmas (3.4, 3.5) and the growth function of a free abelian group (3.6) through generating sets adapted to the lower central series (3.7) to the polynomial bounds for a finitely generated nilpotent group (3.2), then passes them to a group with a finite-index subgroup (3.11). Section 4 characterises polycyclic groups (4.1, whose one hard input is Hirsch's theorem, a milestone of its own) and proves the polycyclic dichotomy (4.3). Milnor's Theorem, already proved on this platform, appears as a reference milestone: it is what carries 4.3 from polycyclic to solvable, and Wolf notes on p. 437 that "J. Milnor extended the scope of Theorem 4.3 by proving [10] that a finitely generated nonpolycyclic solvable group must be of exponential growth."
Theorem 4.8 is the first growth dichotomy: within finitely generated solvable groups there is nothing between polynomial and exponential, and the polynomial side is exactly the almost nilpotent one. It is the result Gromov's theorem generalises in one direction and Grigorchuk's groups bound in the other, and the reason a group of intermediate growth can be neither solvable nor elementary amenable, which is how those groups were first placed outside both classes. Chou's Theorem 3.2, in the mission Chou: elementary amenable groups, extends exactly this statement to elementary amenable groups and cites both halves.
Section 3 also has independent value. The polynomial bounds with the explicit exponents and from the lower central series are sharper than the usual textbook statement that a finitely generated nilpotent group has polynomial growth, and the pieces along the way are reusable: the growth function of in closed form, and the fact that polynomial growth of a given degree is inherited from a finite-index subgroup.
The hard milestone is the second half of Theorem 4.3, that a polycyclic group with no nilpotent subgroup of finite index has exponential growth. Wolf proves it through Proposition 4.4, which passes to a Malcev completion and reads the eigenvalues of the induced Lie algebra automorphisms; that machinery is not in Mathlib and is not part of this mission. A route that avoids it: a polycyclic group acts on a free abelian factor of its chain by integer matrices, so either some element has an eigenvalue off the unit circle, and then the separation argument of Wolf's p. 437 applies verbatim with that factor in place of the Lie algebra, or every eigenvalue of every element lies on the unit circle, and then Kronecker's theorem, which Mathlib has, makes them all roots of unity, so a finite-index subgroup acts unipotently and is nilpotent. Wolf records in the "Added in Proof" (p. 445) that "B. Hartley recently sent me a manuscript consisting of an alternate proof that a polycyclic group without nilpotent subgroups of finite index is of exponential growth."
Theorem 3.2 is long rather than deep: the lower bound (3.8) and the upper bound (3.9), (3.10) are two inductions along the lower central series, each carrying explicit word-length bookkeeping, and both need the adapted generating sets of Lemma 3.7, in the corrected form stated here: as printed, the lemma fails when a lower-central factor has torsion. Mathlib has no polycyclic groups, so Proposition 4.1 starts from nothing; it also lacks Hirsch's theorem and P. Hall's finite presentability results, which is why Hirsch is stated here as its own milestone rather than assumed.
No new definitions: every notion is taken from the published bundles Chou_Growth and
MilnorWolf_Growth, so the statements here are directly comparable with those of the Chou and
Milnor missions. Growth is measured on closed balls, Chou.wordBall S m being the products of at
most letters from and its cardinality, finite because is a
Finset. "Not of exponential growth" is the negation of an existential, so it is a statement about
every finite generating set.
Conditions (8) to (11) of Proposition 4.1, Proposition 4.4 and the Lie-theoretic apparatus of §4, and the Riemannian geometry of §2, §5 and §6, are outside this mission; Proposition 4.1 is stated here with its first seven conditions, which are the ones §4 uses. Hirsch's theorem is cited, not proved, by Wolf, and appears as a milestone under its own source (Proc. London Math. Soc. 44 (1938) 53–60) rather than as an omission. Cheeger's and Hartley's sharpenings, recorded in Wolf's "Added in Proof", are not included.
No hypothesis is vacuous: the free abelian groups witness Proposition 3.6 and Theorem 3.2, a polycyclic group with no nilpotent subgroup of finite index exists (the semidirect product for a hyperbolic , which is Wolf's own example of the exponential case), and the lamplighter group is finitely generated solvable and not polycyclic, so Theorem 4.8's second alternative is not empty either. Contributions welcome: proofs of any milestone, and the general library results they need, such as polycyclic groups and Hirsch's theorem.
The Schrödinger equation is the equation of motion of non-relativistic quantum mechanics: it determines how the state of an isolated quantum system evolves in time. Its time-independent form is an eigenvalue equation whose eigenvalues are the energies the system can have. The single most elementary illustration that this eigenvalue problem forces energies to be discrete is the particle in a one-dimensional box, also called the infinite potential well: a particle of mass confined to an interval by walls of infinite potential energy. It is the first worked example in essentially every introduction to quantum mechanics, and it is the model in which "quantization" can be derived in a few lines from a boundary-value problem for an ordinary differential equation.
This mission is the first in a series formalizing the mathematical content of the Schrödinger equation. It targets exactly the particle-in-a-box computation: that the admissible energies are for positive integers , and nothing else.
Fix three positive real constants: the reduced Planck constant , the mass , and the width of the box. A stationary state of energy is a function such that
together with the regularity needed to state it — is continuous on and twice differentiable at every interior point — and the Dirichlet boundary conditions imposed by the infinite walls,
Inside the box the potential vanishes, which is why only the kinetic term appears; outside the box the potential is infinite and the wave function is identically zero, which is what forces the two boundary values. A stationary state is non-trivial if for at least one ; the trivial solution is excluded because a physical state must be normalizable to unit probability.
Write for , and for the corresponding unnormalized eigenfunction.
This is the weakest statement that carries the physical content: it fixes no eigenfunction, no normalization and no phase, only the set of admissible energies.
The last two give the converse direction — every really occurs — and the normalization constant that turns into a unit vector of .
The result itself is the standard textbook derivation: confinement plus the time-independent Schrödinger equation yields a discrete spectrum, with a strictly positive ground-state energy (no state of zero energy exists) and level spacing growing like . As a piece of mathematics it is the computation of the Dirichlet spectrum of the one-dimensional Laplacian on an interval, which is the model case for spectral theory on domains.
What the mission adds is a machine-checked version of both halves of that derivation, in a form that later missions in this series can import: a reusable predicate for "stationary state with Dirichlet boundary conditions", the classification of the solutions of with one boundary zero, and the quantization step. Mathlib contains the ordinary-differential-equation uniqueness results and the trigonometric API needed, but does not contain this boundary-value classification.
The physics derivation writes down the general solution and is done. Formally, that step is the whole problem: one must prove that every twice-differentiable solution of on an interval has this form, rather than assume it. The usual route is a uniqueness theorem for the associated first-order system applied to the difference of and an explicit sine solution, which requires converting the second-order scalar equation into a system and supplying a Lipschitz estimate. Two further traps: the sign case must be excluded separately (hyperbolic solutions with two zeros are identically zero), and the equation is assumed only on the open interval, so the values at the walls are reached by continuity rather than by evaluating the equation there.
Wave functions are complex-valued functions of a real variable, ; energies, , , are real. Derivatives are the ordinary derivative of a complex-valued function of a real variable, the second derivative being the derivative of the derivative. The equation is imposed pointwise on the open interval only, with continuity on the closed interval and differentiability at interior points; nothing is assumed about outside , so the junk values of the derivative outside the box never enter a statement. The constants are hypothesized strictly positive, so no division by zero occurs in .
The goal is not vacuous: the supporting target exhibiting shows that its hypotheses are satisfiable for every , so the mission cannot be closed by proving that no non-trivial stationary state exists. Conversely the non-triviality hypothesis cannot be dropped: solves the boundary value problem for every real .
Contributions welcome: the ODE classification lemma (solutions of on an interval), orthogonality of the in , and the finite-well and harmonic-oscillator analogues, which are planned as later missions in this series.
A convex combination expresses a point as a weighted average of other points. Such representations connect geometric sets with finite lists of coordinates and coefficients. A point in a convex hull may initially be described using many generators, even when the ambient space has small dimension. Carathéodory's theorem gives a bound depending only on that dimension. Grünbaum presents this result as a basic theorem of convexity in Convex Polytopes, §2.3, Theorem 5, printed page 15 (the supplied source PDF, page 33).
Fix a natural number . Real -space consists of vectors with real coordinates. Let be any subset of this space. A convex combination of points of is a finite sum of those points multiplied by nonnegative real coefficients, with the coefficients adding to one. The convex hull is the set of all such combinations; equivalently, it is the smallest convex set containing .
The generating set can be finite or infinite. It need not be closed, bounded, or convex. Membership of a point in its convex hull is the sole geometric assumption. The theorem concerns exact equality of vectors, so the representation is not an approximation or a limiting expression.
For every , find points and real numbers satisfying
This is the complete target of Theorem 2.3.5. The witnesses may depend on , , and . No single selection of points must work for every point of the hull. Repeated points are permitted, and some coefficients may be zero. Thus the fixed list of positions can express a combination that uses fewer distinct points.
The result gives a finite certificate for membership in a convex hull whose length is controlled by dimension rather than by the size of the generating set. In the plane it gives three positions, and in three-dimensional space it gives four. Infinite generating sets remain within the same statement: once a particular hull point is chosen, only finitely many generators are needed for its certificate.
The mission asks for a formal proof of this known mathematical result in its fixed-length formulation. Its content is the existence of points and normalized coefficients together. Supplying coefficients without ensuring that their points lie in , or supplying a finite representation without the dimension bound, would leave part of the target unestablished.
The definition of the convex hull guarantees a finite representation but does not directly fix its length at . The dimension bound must hold while preserving nonnegativity, normalization, membership in the original generating set, and exact equality with the selected point. None of these constraints can be replaced by a condition on nearby points or on the closure of .
The coordinate model is Fin d → ℝ. Both the point list and the coefficient list are indexed by Fin (d + 1), corresponding to the source indices from zero through . The convex hull, finite sums, and real scalar multiplication have their standard mathematical meanings. No additional geometric definition is needed.
Dimension zero has one position in the representation. If is empty, its convex hull is empty, so there is no hull point to represent. A singleton generating set and sets contained in a proper affine subspace are allowed. Neither strict positivity of the weights nor affine independence of the selected points is required. The target does not assert uniqueness of a representation.
Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, Chapter 2, §2.3, Theorem 5, printed page 15; supplied source.pdf, page 33.
A convex set contains the segment joining any two of its points. For a bounded closed convex set in finite-dimensional real space, extreme points describe the set through convex combinations. An extreme point cannot lie strictly between two distinct points of the set. Allowing unbounded sets introduces a second ingredient: directions in which one can move indefinitely while remaining in the set.
This mission concerns that second ingredient and its interaction with extreme points. A closed convex set is line-free if it contains no entire straight line. It may nevertheless contain rays and be unbounded. Its characteristic cone consists of directions v for which x + t v stays in the set whenever x belongs to the set and t is nonnegative. For a nonempty closed convex set, checking one basepoint gives the same cone as checking every basepoint. Thus the cone records the directions of recession without singling out an origin inside the set.
The goal is Grünbaum’s Theorem 2.5.6:
for every line-free, closed convex set K in real d-dimensional space. The plus sign denotes Minkowski addition: all sums of one point from each set. The equation says that every point of K is a recession vector plus a finite convex combination of extreme points. Conversely, each such sum belongs to K. There is no topological closure around the convex hull in this equation.
A ray illustrates the two ingredients. Its endpoint is its only extreme point, while its characteristic cone supplies every nonnegative displacement along the ray. A singleton has only itself as an extreme point and has zero characteristic cone. A whole straight line shows why the line-free hypothesis matters: it has no extreme points and cannot be recovered from their convex hull by this formula.
The ambient dimension is arbitrary and finite; the set need not be full-dimensional or polyhedral. The characteristic cone is defined using all basepoints, so its value on the empty set is the whole ambient space. Since the empty set has no extreme points, its convex hull and the displayed Minkowski sum are empty, and the equation remains valid. This convention extends the formula without asserting that the book defines a characteristic cone at an absent basepoint.
The source is Branko Grünbaum, Convex Polytopes, second edition (2003), §2.5, Theorem 6, printed page 25 (PDF page 43). The characteristic cone and line-free condition appear on printed page 24 (PDF page 42); extreme points are defined in §2.4 on printed page 17 (PDF page 35). These definitions supply the vocabulary for the single representation goal.
A quantum computer manipulates superpositions of many degrees of freedom, and every gate it applies is imperfect. Before 1996 it was widely argued that this fragility is fatal: the accuracy demanded of each elementary operation appeared to grow with the length of the computation, so that arbitrarily long computations would require arbitrarily perfect hardware. The discovery of quantum error-correcting codes, of fault tolerant syndrome extraction, and of transversally encoded operations changed that picture, but the first fault tolerant schemes still required the error per operation to shrink as the computation grew.
Knill, Laflamme and Zurek, Resilient Quantum Computation: Error Models and Thresholds (arXiv:quant-ph/9702058), together with the independent work of Kitaev and of Aharonov and Ben-Or, removed that requirement: they exhibited a fixed threshold value such that any physical error rate below it permits arbitrarily accurate encoded computation, at an overhead that is only polylogarithmic in the length of the computation. Their paper is also the one that pushes past independent stochastic noise: its thresholds are proved for quasi-independent error models, which accommodate coherent over-rotation and weak residual couplings between neighbouring qubits.
This mission formalizes the quantitative engine of that paper: the concatenation recursion, the error-model bounds it is applied to, the threshold it produces, and the resulting overhead.
Fix a physical implementation in which each gate, state preparation and idle memory step carries an error location. A noisy network with error locations indexed by a finite set is described through an error expansion; each summand fails at a set of locations, and the model constrains how probable simultaneous failures are.
Write for the underlying probability measure and for the event that location has failed. Two models from Section I.B of the paper are used here.
The fault tolerant construction of Section I turns physical qubits into encoded qubits: each encoded gate is a transversal operation preceded by fault tolerant recovery networks built from the -qubit Steane code. The analysis of Section II declares an encoded gate failed according to an explicit combinatorial rule, and shows that a failure requires two failures among a set of minimal pairs of physical error locations. Consequently one level of encoding maps a failure parameter to .
Iterating this reduction is concatenation. Define the level- failure parameter by
written in the Lean development. Let bound the number of qubits and time steps at the level below that are consumed by one encoded gate, so that one computational gate at level costs physical resources.
For , , , and every gate count and target failure probability with , there exists a level with
The first clause is resilience: a computation of encoded gates can be made to fail with probability below any prescribed . The second is the cost: the overhead per computational gate is polylogarithmic in , with exponent . The threshold itself is the hypothesis ; no numerical value is hard-coded, so the statement survives any improvement of the paper's count and of the resulting bounds and .
The milestone list covers the closed form of the concatenation recursion and its threshold form ; convergence below threshold; the failure bounds and for a network under the two error models; the criterion under which ; and the overhead estimate .
The threshold theorem is the reason large-scale quantum computation is regarded as a physically meaningful goal rather than an idealization: it converts an engineering requirement that scales with the problem size into a fixed, size-independent accuracy target, and it fixes the currency — threshold value and overhead exponent — in which every later architecture is compared. The quasi-independent models matter separately: they show the conclusion does not depend on noise being stochastic, which is what rules out the objection that coherent over-rotations invalidate the stochastic analysis.
The paper's own argument is a physics-style derivation: a circuit-level construction, a combinatorial count of failure-inducing pairs of error locations, and a recursion. This mission formalizes the recursion, the probabilistic bounds and the resulting threshold and overhead statements. It does not formalize the circuit-level content — the -qubit code, the cat-state syndrome extraction networks, transversality, or the count itself; these enter the formal statements as the parameters and . No machine-checked proof of the full threshold theorem, in the sense of a verified fault tolerant circuit construction, is known to the author of this proposal; formalizing the quantitative layer is a prerequisite for one.
The obvious route to "errors vanish under concatenation" is to iterate the bound and observe the doubly exponential decay. That step is the easy half, and the milestone list makes it explicit. What the naive argument silently assumes is exactly what Section II must establish: that the level- failure events again obey a quasi-independent bound, with simultaneous encoded failures bounded by rather than merely each single failure bounded by . This is why the paper's failure declaration is defined backwards in time and demands disjoint pairs of contributing locations. A formalization that bounds only single-gate failure probabilities cannot close the induction.
The second difficulty is bookkeeping at the edges: the recursion is stated for a failure parameter that is a probability in one model and an operator strength in the other, and the overhead bound involves a real exponent and a ceiling, whose interaction with the degenerate cases and has to be handled rather than assumed away.
All parameters are real numbers: , and the gate count is a natural number cast to . levelError is defined by recursion on the level and is total, so it is meaningful for every real ; the threshold hypothesis appears explicitly as where it is needed.
The two error models are predicates on a measure on a measurable space, a Finset of error locations, and a family of failure events, with values in ENNReal; they quantify over all subsets of the location set, matching the paper's "at a given many error locations". The network failure bounds are stated for , the probability that some location fails.
The goal is not vacuous: the hypotheses , , , are simultaneously satisfiable (for instance , , , , ), and the conclusion asserts a strict inequality together with a quantitative overhead bound, so it cannot be discharged by a degenerate reading. Degenerate inputs are inside the statement rather than excluded: , and the case , are covered by the and must be handled.
A complete development needs only Mathlib's real analysis (Real.log, Real.logb, Real.rpow, Nat.ceil) and the measure-theoretic union bound; nothing quantum is required by the formal statements. Contributions strengthening the milestone list towards the circuit level — a formal model of error locations in a network, of the induced next-level error model, or of stabilizer-code recovery — are welcome as further targets.
Quantum computations are performed on physical devices whose elementary operations are never exact: every gate, every idle qubit, every time step is subject to decoherence, damping and systematic inaccuracy. Without protection these errors accumulate and destroy the computation. In 1997 Dorit Aharonov and Michael Ben-Or proved that this can be overcome: as long as the error rate — the probability, per location per time step, that a fault occurs — is below a fixed positive threshold, an arbitrary quantum circuit can be simulated reliably with only polylogarithmic overhead (arXiv:quant-ph/9906129). This threshold theorem is the reason large-scale quantum computing is regarded as physically possible in principle, and the number it produces is the target every hardware programme is measured against.
The engine of the proof is not quantum mechanical but combinatorial. A circuit is encoded, then the encoded circuit is encoded again, times over. The locations of the resulting circuit are organised into a tree of nested rectangles, and the computation survives precisely when the set of faulty locations is sparse in a recursive sense. The mission formalizes that engine: the recursive sparseness calculus of §7.4–7.6 and §8.2 of the paper, which converts a constant error rate below the threshold into a doubly exponentially small failure probability.
Fix two natural numbers: , the number of locations in a rectangle, and , the number of faulty sub-rectangles a rectangle tolerates (in the paper , where is the number of errors the code corrects and is the spread of a fault). A -rectangle is a single location of the circuit, and an -rectangle consists of many -rectangles. A fault pattern of an -rectangle records, for each of its locations, whether a fault occurred there.
Following Definition 18 of the paper, a fault pattern is -sparse by recursion on : at level it is sparse when the location carries no fault; at level it is sparse when at most of the constituent -rectangles carry a pattern that is not -sparse. Under independent probabilistic noise of rate each location is faulty with probability , independently; write for the probability that the pattern of an -rectangle is -sparse, and for the probability that it is not.
Two thresholds appear. The threshold condition for probabilistic noise (Definition 19) is
and the threshold condition for general noise (Definition 21) is
The corresponding thresholds are and : every positive below them satisfies the respective condition.
The goal is the quantitative core of Theorem 10. Below the threshold there are constants such that for every circuit size and every accuracy some recursion depth satisfies both
The first inequality says that, over all rectangles of the simulated circuit, the probability that any of them carries a non-sparse fault pattern is below ; the second says that the overhead per simulated location, , is polylogarithmic in — the cost claimed in Theorem 10.
The milestones build up to it: the two threshold conditions hold below the respective thresholds, the exponent gap of equation 7.5 exists, the base case , the union-bound recursion , Lemma 10 itself (), and the analogous recursion 8.8–8.10 governing the bad part in the general-noise analysis.
Lemma 10 is where a constant error rate becomes a vanishing one. Each level of concatenation only has to improve reliability slightly, because the improvement compounds doubly exponentially in the number of levels; this is exactly why constant-rate noise can be tolerated while Shor's earlier scheme needed a polylogarithmically small rate. The same recursion, with in place of and an extra factor of , controls the trace norm of the bad part of the fault-path expansion in the general-noise model (§8.2), which is how the result is extended from probabilistic errors to decoherence, damping and systematic inaccuracy.
Formalizing this part of the paper yields a reusable, model-independent statement: nothing in the milestones mentions density matrices, so the sparseness calculus can later be plugged into a formal model of noisy quantum circuits, or reused for classical concatenated fault tolerance. What this mission does not do is formalize the circuit-level statement of Theorem 10 — that requires a full Lean model of quantum circuits with mixed states, fault-tolerant procedures, and the code constructions of §3–§6, and is deliberately out of scope here.
The obvious approach — bound the failure probability by a union bound over all fault sets of size and iterate — is exactly right, but the iteration is where the work is. The recursion only produces the doubly exponential decay once the threshold condition is converted into the strict exponent gap of equation 7.5, and the induction has to keep alive to reuse that gap at every level. In the general-noise recursion there is a second trap: the factor exceeds , so the recursion is not contracting termwise, and one needs to bound it by .
On the probabilistic side, the statements are about a genuine product distribution on an exponentially large sample space, not a recursively defined real number: the union-bound step must be carried out over the actual set of fault patterns, where independence across the sub-rectangles is what makes the product bound valid.
Fault patterns are a type defined by recursion on the level: is the booleans and is the functions from the sub-rectangles to ; every level is a finite type with decidable equality. Sparseness is a decidable predicate following Definition 18 verbatim. The noise distribution is given by the weight of a pattern, the product over all locations of (faulty) or (clean), and the sparseness probability is the sum of these weights over the sparse patterns — an honest finite product measure, so no hypothesis is built into the definitions and each statement carries the range hypotheses it needs.
Two conventions are worth flagging. First, the thresholds are formalized as and ; the paper prints the exponent as in equations 7.4 and 8.6, which is inconsistent with its own threshold conditions 7.3 and 8.5, and is the exponent for which the paper's claim "any satisfies the threshold condition" is true. Second, Lemma 10 is stated with rather than the paper's strict , because at the two sides are equal.
Nothing here is vacuous: all hypotheses are satisfiable — for instance , , satisfies every hypothesis of the goal — and the goal quantifies over all circuit sizes and all accuracies, so it cannot be discharged by a degenerate choice. A complete development needs only real analysis, finite sums and binomial counting from Mathlib. Contributions that generalise the branching factor to a per-rectangle bound , or that connect the calculus to a formal model of noisy circuits, are welcome.
A Padé approximant is the "best" approximation of a function near a point by a rational function of prescribed numerator and denominator degrees. The idea goes back to Georg Frobenius (1881), who studied relations among the convergents of a power series, and was developed systematically by Henri Padé in his 1892 thesis. Unlike a truncated Taylor polynomial, a rational approximant can reproduce poles, and it often converges where the Taylor series does not; this is why Padé approximants are standard tools in numerical computation, in the resummation of divergent perturbation series in physics, and — through the "ad hoc methods inspired by Padé theory" — in Diophantine approximation and transcendence proofs.
The theory rests on one structural fact, stated in the source as a single sentence: when it exists, the Padé approximant is unique as a formal power series for the given and . That sentence hides the two theorems this mission asks for — that a suitable pair of polynomials always exists, and that any two such pairs define the same rational function.
Fix a field and a formal power series
Given integers and , one looks for a rational function
whose Maclaurin expansion agrees with that of through order , i.e.
This is denoted .
Written this way the condition is nonlinear in the unknowns and presupposes . The classical device, due to Frobenius, is to linearize: instead of asking that vanish to order , one asks that
A pair satisfying these three conditions is what this mission calls a Padé pair of type for ; it is the predicate every statement below is phrased with. The linearized problem is a homogeneous linear system, so it is always solvable, whereas the original ratio problem is not: the linearized solution may have , in which case no normalized of the displayed shape exists (the " entry of the Padé table is defect"). The two formulations coincide exactly when .
The goal theorem is the conjunction of existence and uniqueness for the linearized problem, over an arbitrary field , for all :
Statement (U) is the precise content of "the Padé approximant is unique": the two pairs need not be equal — they may differ by a common polynomial factor — but they determine the same element of , and hence the same formal power series wherever the quotient is defined.
The milestones are: existence (E); uniqueness (U); the equivalence between the linearized condition and agreement of Maclaurin expansions when ; the Bézout form used by the extended-Euclidean computation of the approximant; the normalization of the denominator to constant term ; and the two worked examples given in the source, namely for and for .
The result itself. Existence and uniqueness are what make the Padé table — the doubly indexed array — a well-defined object, and therefore what make every identity among its entries (the block structure of the table, the Frobenius identities, Wynn's -algorithm and the cross rules) meaningful. Every computational route to the approximant, including the extended-Euclidean route recorded in the source, computes the approximant only because of (U).
Formalizing it. Mathlib has formal power series, polynomials, truncation, and the inverse of a power series with invertible constant term, but no Padé theory: there is no predicate for the condition and no existence or uniqueness statement. This mission adds the linearized predicate and the two structural theorems, which is the minimum foundation on which the Padé table, the block theorem, and convergence results such as Nuttall–Pommerenke could later be built. The results are classical and have textbook proofs; the contribution here is the machine-checked development, not new mathematics.
Neither theorem is deep, but both have a specific step where the obvious approach fails.
For existence, the naive route — solve for , then read off — requires knowing that the homogeneous system for the coefficients of given by the equations "coefficients of of vanish" has a nonzero solution. That is a rank argument about a rectangular Toeplitz-like matrix, and the work in Lean is in packaging it as a linear-algebra statement rather than in the mathematics.
For uniqueness, the one-line argument is to divide: from and conclude . This is invalid, because need not be invertible modulo (its constant term may vanish) and is not a domain. The correct argument compares , whose left side is divisible by while its right side has degree at most ; the difficulty is the degree bookkeeping, not the algebra.
A solver should also note that (U) is not the claim , which is false — rescaling, or a common factor, gives distinct pairs.
The development is over an arbitrary field F (the definition itself only needs a commutative ring), with f : PowerSeries F, and P Q : Polynomial F. Conventions fixed in Lean, and worth reading before starting:
Polynomial.degree ≤ (m : WithBot ℕ), so the zero polynomial satisfies every bound; in particular is allowed and is excluded by an explicit hypothesis.PowerSeries F through the canonical coercion.PowerSeries.exp ℚ and supplied as an explicit series .Contributions of further Padé material — the Padé table, defect entries, the block structure, or the -algorithm — are welcome as follow-up missions built on this predicate.
An exclusion system models particles moving among sites under the rule that each site is either vacant or occupied. A move exchanges the occupation variables at two sites, so particle number is conserved. On a countably infinite site set, however, the formal sum of all possible exchanges need not automatically determine a well-defined Markov evolution. Individual rates can be continuous and bounded while infinitely many potential exchanges remain active. Chapter 8, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, gives conditions under which this formal operator closes to the generator of a conservative Feller semigroup Ethier--Kurtz, Theorem 3.6.
This mission states that theorem with its complete weighted two-site domain and its finite-coordinate core. It does not replace the countable system by a finite Markov chain, collapse the ordered-pair generator sum, or substitute the neighboring spin-flip theorem. Spin flips change particle number one coordinate at a time; exclusion moves exchange two coordinates and conserve it.
Let S be a countable type of sites. A configuration is a function η : S → Bool, where false and true relabel vacancy and occupation. The product topology is induced by the discrete topology on Bool. The Lean space C(S → Bool, ℝ) consists of continuous real-valued observables on this compact configuration space and carries the uniform norm.
For sites i and j, exclusionExchange i j η swaps η i and η j and leaves every other coordinate unchanged. When i = j, the exchange is the identity. For an observable f, its two-site exchange variation is
The theorem assigns a continuous nonnegative rate c i j to every ordered pair and a nonnegative real dominating weight γ i j. Both families are symmetric, the diagonal rates vanish, and c i j η ≤ γ i j. The rows of γ are summable with one uniform upper bound, which is the Lean form of equation (3.27).
Rate dependence on the configuration is controlled through a different operation. spinFlip k η toggles the single coordinate k, and spinVariation (c i j) k measures the resulting uniform change in the rate. Equation (3.28) requires these single-site influences to be summable and bounded by K * γ i j, with one constant K for all pairs. The influence condition therefore deliberately uses single-site flips even though the dynamics itself uses two-site exchanges.
The pre-generator graph implements equation (3.29). Its domain is exactly the continuous observables satisfying
where the sum is over ordered pairs and has no factor of one half. For (f,g) in the graph, the continuous output satisfies
The goal is Theorem 3.6 in full. Every observable in the weighted domain has a continuous image in the graph. The graph closure in the product uniform-norm topology is single-valued and equals the derivative graph of a strongly continuous contraction semigroup. The semigroup preserves nonnegative functions and the constant function one, expressing the conservative Feller conclusion.
The last clause retains the source's cylinder core. Restrict the initial graph to observables determined by finitely many coordinates: there is a finite set F such that configurations agreeing on F receive the same value. The closure of that restricted graph equals the entire closed generator graph. Generation, the full weighted domain, and the core remain one target because they are conclusions of the same source theorem.
The theorem turns an infinite formal exchange sum into a closed Markov generator on continuous observables. The conclusion is stronger than pointwise convergence of the series: it identifies the whole generator domain through a derivative biconditional, provides positivity and conservativity, and establishes a finite-coordinate class from which the closed graph can be recovered.
The result is proved in the textbook. The formalization target is its precise Lean statement, including symmetry, zero diagonal, domination, the uniform row bound, the single-site influence bound, the weighted ordered-pair domain, graph closure, Feller generation, and cylinder core. Reusable infrastructure consists of the book-wide contraction-semigroup predicate and the already shared single-site flip and variation definitions; the exchange, exchange variation, and weighted graph are specific to this model.
A naive finite-state jump-process argument does not apply. Countability and a uniform row bound do not turn the full ordered-pair collection into a finite set of moves. Pointwise notation for the exchange series also does not by itself prove that the result is continuous, that the graph closure is single-valued, or that finite-coordinate observables form a core. The weighted two-site domain and the configuration-influence condition are therefore essential parts of the theorem rather than optional regularity assumptions.
The spin-flip and exclusion models cannot be interchanged. A coordinate flip creates or removes occupation and is measured by a one-site domain. An exclusion move conserves occupation by swapping two coordinates and requires the γ-weighted two-site variation domain. Only the rate-influence hypothesis uses the shared one-site variation.
The Lean statement allows empty, finite, and countably infinite S, matching the source's countability assumption without adding nonemptiness. Bool is an exact two-state encoding of {0,1}. Real suprema define both one-site and two-site uniform variations over the nonempty compact configuration space. Explicit Summable hypotheses prevent divergent real tsum expressions from being silently totalized.
The graph records a continuous output equal to the actual pointwise ordered-pair series. Its first conclusion ensures that this representation does not shrink the stated weighted domain. Closure is taken in C(S → Bool, ℝ) × C(S → Bool, ℝ). The semigroup is real-time indexed, while its laws and bounds are imposed for nonnegative times. No finite-site restriction, finite-total-rate replacement, factor of one half, exchange-based substitute for the influence bound, or weakened core statement is admitted.
Chapter 4's framework (formalized in this series' 04-framework mission) solves the online
covering-packing pair only in the restricted setting a(i,j) ∈ {0,1}, b(j) = 1 — every
constraint is an unweighted "cover me with at least one of these" condition. Chapter 14 delivers
the promise made at the very start of the survey (p. 115: "we show how to extend the ideas we
present here to handle general (non-negative) values of a(i,j) and b(j)"): fully general
non-negative coefficients, normalized so every constraint reads ∑_i a(i,j)x(i) ≥ 1. This
mission formalizes both halves of that generalization — the packing scheme (Theorem 14.1, with a
matching lower bound, Lemma 14.2, showing an extra additive term is unavoidable) and the covering
scheme (Theorem 14.3, the goal).
Fix a finite set I of primal (covering) variables with positive costs c(i), and a finite set
J of dual (packing) variables/covering constraints, with a(i,j) ≥ 0 for every pair (Fig. 14.1).
The packing scheme (Section 14.1) is parameterized by a target competitive ratio B > 0: on each
new dual variable y(j) and its coefficients a(i,j), the algorithm increases y(j) continuously
and each x(i) by an explicit exponential increment function until the new primal constraint is
satisfied, achieving B-competitiveness for the packing objective at the cost of an additive
O(log(a_i(max)/a_i(min))) term (beyond the multiplicative O(log n)) in how much each dual
constraint can be violated — qualitatively different from Chapter 4's purely multiplicative
O(log d) bound, and Lemma 14.2 proves this additive term cannot be removed. The covering scheme
(Section 14.2) instead works in phases: each phase assumes a doubling lower bound α(r) on OPT
and "forgets" its primal/dual variables once the primal cost exceeds α(r), restarting with
α(r+1) = 2α(r) — a structurally different mechanism from Chapter 4's direct algorithms, needed
because with general coefficients a single monotone run can no longer be analyzed via one
potential function alone.
Theorem 14.3 (the goal, p. 253): for any B > 0, the phase-based covering scheme (each
constraint normalized to ∑_i a(i,j)x(i) ≥ 1/B) is competitive with an explicit ratio
8 log(2n)/B, taken directly from the proof's own final displayed chain,
2α(r) ≤ 4α(r-1) ≤ (8 log(2n)/B) Y(r-1) ≤ (8 log(2n)/B) OPT (p. 253-254) — the theorem's own
statement only gives O(log n/B), so this explicit constant is this mission's own
instantiation from the proof, not an independent derivation and not a transcription of a
displayed theorem-level formula (flagged, per this series' explicit-constants rule).
Two milestones, in attack order:
B-competitive, and violates each dual
constraint by at most the book's own exact displayed bound
c(i)·2log(1 + n·a_i(max)/a_i(min))/B (Claim (3) — the exact constant the proof establishes,
not the theorem headline's O(·) simplification).log(a(max)/a(min)) term of Theorem 14.1 is necessary.This chapter is the survey's demonstration that the primal-dual framework's core technique survives its most natural generalization, at the price of an explicit extra term the chapter also proves is unavoidable — a tight characterization, not merely an upper bound. Every other online covering/packing chapter in this survey (set cover, routing, ad-auctions, bounded allocation) is technically a special case of this chapter's general model; Chapter 4's restricted framework is the pedagogical entry point, and this chapter is where the general theory actually lives. No formal development of the general packing-covering problem was found on the platform as of 2026-09-20; this mission is the first.
Two distinct obstacles, mirroring this chapter's own two schemes. First, Theorem 14.1's proof
(p. 249-251) establishes its per-round primal/dual derivative inequality via a direct calculus
argument (differentiating the explicit increment function) — formalized here as a hypothesis
(hX_le_BY) standing for that calculation, not reproduced, since the goal is a faithful
statement of the resulting competitive ratio, and the increment function's own exponential form
is transcribed in the theorem's docstring but the differentiation itself is out of scope. Second,
Theorem 14.3's phase-based mechanism is genuinely stateful across an unbounded number of phases
(each phase resets its own primal/dual variables while the LP's actual variables retain the
running maximum) — modeling this process explicitly is comparable in complexity to Chapter 13's
level-based algorithm, and this mission makes the same scope choice: the mechanism's output
(the resulting cost/profit relationship, hX_le_ratio) is taken as a hypothesis standing for the
book's own Claims (1) and (3) combined, rather than constructed phase-by-phase.
GeneralInstance I J bundles Fig. 14.1's fully general LP data (a(i,j) ≥ 0, c(i) > 0) —
restated locally (not importing 04-framework's CoveringInstance) per this series' rule against
cross-draft imports, even though this chapter is the direct generalization of that one.
aMax/aMin are the per-variable (not per-instance) maximum and minimum-non-zero coefficients
Theorem 14.1 needs. harmonicNum is restated locally (duplicated from 13-bounded-allocation's
own definition, for the same no-cross-draft-import reason). Both goal-adjacent theorems use this
series' weak-duality "competitive against any feasible comparison solution" pattern
(04-framework, reused as a convention, not re-derived): Theorem 14.1 against any feasible
packing comparison (matching that it concerns the packing side), Theorem 14.3 against any
feasible covering comparison (matching the covering side). Welcome contributions: completing
the three sorrys (Theorem 14.1's calculus argument, Theorem 14.3's phase-based mechanism
constructed explicitly, and Lemma 14.2's direct summation argument, which is the most tractable of
the three to actually prove), and formalizing the sanity check that both schemes reduce to
Chapter 4's Algorithm 1/2/3 when a(i,j) ∈ {0,1}, b(j) = 1 (checked by hand in SELF_REVIEW.md,
not as a Lean lemma).
The classical online allocation (AdWords) problem has a tight 1 - 1/e competitive ratio in
general, achieved by the water-level algorithm and matched by a lower bound in which the number
of buyers interested in each item can be as large as the total number of buyers. Buchbinder and
Naor's Chapter 13 observes that in many realistic settings each item's interested-buyer set is
much smaller than the total buyer population, and shows this structural fact — an explicit bound
d on interested buyers per item — provably beats 1 - 1/e for every finite d, via a
deliberately non-water-level algorithm. This mission formalizes that algorithm's competitive
ratio and its matching lower bound.
A seller offers items to n buyers one at a time; buyer i has budget B(i) > 0. Each item j
has a fixed price b(j) > 0 and a set S(j) of interested buyers with |S(j)| ≤ d. The
fractional LP relaxation (Fig. 13.1) allocates y(i,j) ∈ [0,1] of item j to buyer i, subject
to each item being sold at most once in total and each buyer's spending never exceeding budget;
the seller's objective is to maximize total revenue ∑_j ∑_{i∈S(j)} b(j)y(i,j). Buyers are
partitioned into d+1 levels by the fraction of budget spent so far (level k = spent between
k/d and (k+1)/d); on each new item, the allocation algorithm splits it equally among the
interested buyers in the lowest non-empty level, moving to the next level once that level's
buyers are exhausted or saturated — deliberately not the naive "water-level" rule of splitting
among the least-spent buyers, which the book shows cannot beat 1-1/e even for small d. The
analysis tracks a piecewise-linear trade-off potential function f_d, built from a geometric
sequence, that relates each buyer's level to their contribution to a feasible primal (covering)
solution.
Theorem 13.1 (the goal, p. 240): the allocation algorithm is C(d)-competitive, with the
book's own explicit closed form C(d) = 1 - (d-1)/(d(1+1/(d-1))^{d-1}) — strictly better than
1 - 1/e for every finite d, approaching it as d → ∞ (Table 13.1). Formalized via the
survey's standard weak-duality pattern (as in 04-framework's Theorem 4.3): given the algorithm's
per-item primal/dual cost changes satisfying the book's core inequality
ΔX(j) ≤ (1/C(d))ΔY(j) (established there by a potential-function case analysis, not reproduced
here), the algorithm's realized profit is C(d)-competitive against any feasible comparison
allocation.
Lemma 13.2 (milestone, p. 244): a matching lower bound,
C(d) ≤ 1 - (k - kH(d) + ∑_{i=1}^k H(d-i))/d, where H is the harmonic number and k is the
largest value with H(d) - H(d-k) ≤ 1.
This chapter is the survey's demonstration that a structural restriction invisible to the
classical 1-1/e lower bound — a bound on demand concentration, not on budgets or prices — can be
exploited algorithmically, and the exploiting algorithm is not the naive generalization of the
water-level rule but a genuinely different level-based, "who's-behind" allocation rule. No formal
development of the bounded allocation problem was found on the platform as of 2026-09-20; this
mission is the first.
The chapter's own proof of Theorem 13.1 (p. 241-244) is a page-and-a-half case analysis on how an
item's fractional allocation crosses level boundaries, bookkeeping the change in both the primal
potential-function value and the dual profit through several sub-cases (an item fully absorbed by
one level; an item that empties a level and continues into the next; a level exhausting every
interested buyer's budget). This mission formalizes the resulting per-item inequality
ΔX(j) ≤ (1/C(d))ΔY(j) as a hypothesis (the theorem's own headline claim, not a case-by-case
re-derivation) rather than modeling the stateful, order-dependent level-allocation process itself
— the same scope choice this series makes for Chapter 11's randomized rounding process, where the
book similarly omits (there, entirely; here, gives but does not ask this mission to reproduce) the
underlying case analysis. The potential function f_d and its connection to the algorithm's
primal variable (allocX) are formalized precisely, since they are what the goal's proof and
Lemma 13.2 both depend on structurally, even though the case analysis linking them to ΔX/ΔY
is left as the theorem's sorry.
AllocationInstance I J bundles the LP data of Fig. 13.1 (S, B, b, d ≥ 2,
∀j, |S(j)|≤d) — restated locally per this series' rule that concurrent drafts cannot import each
other, even though the problem is a special case of Chapter 10's ad-auctions model (the two
chapters' algorithms differ: Chapter 10's is proportional-to-remaining-budget, this chapter's is
level-based). geomSeq/potential transcribe the geometric sequence a_t and the potential
function f_d at its level grid points exactly (not extended to non-grid-point reals, since
Theorem 13.1's and Lemma 13.2's own statements only need the grid values). allocX connects the
potential function to the algorithm's primal variable via each buyer's final level t(i).
packingFeasible/packingValue transcribe Fig. 13.1's dual/packing LP with a genuine two-index
allocation y : I → J → ℝ (not collapsed to a single per-item variable, unlike Chapter 4's
simpler 0/1-coefficient framework). harmonicNum is the ordinary harmonic number. The level-based
algorithm's literal stateful per-item update rule (which buyers move between which levels, in
what order, within a single item's allocation) is not modeled directly — a documented scope
reduction (STATUS.md), not a substitution of the "water-level" algorithm the book explicitly
warns against (this mission's theorem13_1 commits to neither algorithm's literal rule, only to
the resulting invariant the book's own proof establishes for the level-based one). Welcome
contributions: completing the two sorrys, and modeling the level-allocation process explicitly
enough to derive hinvariant from first principles.
1-1/e lower bound).Network routing is one of the paradigmatic applications of the online primal-dual method:
requests for bandwidth between a source and target arrive one at a time, and the algorithm must
commit bandwidth to paths without knowing future requests. Chapter 4 already gave a simple
(3, O(log n))-competitive routing algorithm as an illustration of the general framework. This
chapter asks for something qualitatively stronger: a uni-criteria (1, O(log n))-competitive
algorithm — one that routes the full optimal bandwidth (no loss on the throughput side at all),
paying only in a bounded edge-capacity violation. The chapter shows this exact-throughput
guarantee is achievable, and is moreover the key building block for several other routing
objectives (fair routing, max-min fairness) built on top of it in Section 9.2 — a (1, O(log n))-competitive algorithm composes into those richer objectives in a way a merely
constant-factor-lossy algorithm does not.
Fix a graph , , , with integer edge capacities . Routing requests arrive online, each demanding one unit of bandwidth between a source and target; in the splittable model (this chapter's comparison class), a request's bandwidth may be divided across multiple paths. A -competitive algorithm routes at least of the maximum possible bandwidth while guaranteeing every edge's load (bandwidth allocated divided by capacity) is at most . The chapter's generic algorithm (Section 9.1) maintains, for each of copies of the graph (copy keeping only edges of capacity at least , each capped at ), a primal-dual pair matching Chapter 4's own routing LP (Fig. 9.1, identical to Fig. 4.2): a request is routed on the shortest path (by the copy's current primal edge-lengths ) if that length is below , multiplicatively updating on the path's edges; otherwise, subject to a capacity-limited fallback rule, on an arbitrary feasible path.
Theorem 9.2 (goal, p. 204): the algorithm is (1, O(log n))-competitive with respect to all
splittable routing solutions — exact throughput (ratio 1), edge load at most O(log n).
Lemma 9.1 (milestone, p. 202-204): a single copy 's own guarantee, which Theorem 9.2's proof composes across all copies: the algorithm accepts at least (the maximum splittable bandwidth achievable in , out of the requests introduced to it) and incurs load on every edge of .
This is the survey's demonstration that the online primal-dual method, in its most basic form (a single accumulating dual sum driving a multiplicative primal update, exactly Chapter 4's framework), scales to a genuinely harder bicriterion objective once composed across a carefully constructed family of graph copies — the copies are what let the algorithm avoid ever needing to reason about which of the exponentially many - paths to consider, reducing routing to a sequence of independent shortest-path computations. The chapter's own Section 9.2 builds a coordinate-wise-competitive fair-routing algorithm directly on top of Theorem 9.2 (not formalized here), and its Notes section places -competitiveness as "a crucial non-trivial step" the chapter needed before those richer objectives became tractable at all. No prior formalization of online routing, splittable or otherwise, was found on the platform as of 2026-09-20 (search below).
This is the most algorithmically intricate chapter in this series: the algorithm processes each
request against every one of graph copies, each copy running its own instance of the
Chapter-4-style primal-dual update, and Theorem 9.2's own proof composes Lemma 9.1's per-copy
guarantee via a combinatorial backward induction (partitioning the offline-optimal solution's
paths into groups by bottleneck capacity, and showing group by group that the algorithm's
cumulative routed bandwidth across the top levels dominates the cumulative optimal bandwidth in
those groups) together with a separate geometric argument bounding how many copies any single
edge can meaningfully appear in. Fully modeling the copy construction, the request-routing
process, and both composition arguments from first principles was judged to exceed this mission's
time budget without sacrificing the faithfulness of what does get stated (per CAPTAIN_BRIEF.md
rule 6). Instead: Lemma 9.1 is formalized via the two facts its own proof isolates as doing the
real work — a weak-duality contradiction bound (stepB ≥ M − uMin) and the step-(1c) fallback's
own greedy-fill rule for part (i); the multiplicative-update invariant x(e,j) ≤ 2 for part (ii),
whose consequence — the exact constant 2 + 6·log₂n — is re-derived from scratch in this mission
(the displayed equation this derivation depends on was garbled by the PDF's text extraction; it
was confirmed against the actual typeset page image before drafting, see SELF_REVIEW.md).
Theorem 9.2 then composes Lemma 9.1 across copies via two explicit, clearly-labeled hypotheses
standing for the book's own backward-induction accounting and edge-multiplicity argument,
respectively — genuine mathematical content this mission does not re-derive, named honestly as
hypotheses rather than silently assumed away or approximated by a weaker statement.
No shared data structure was introduced: every quantity in both theorems (bandwidths, capacities,
loads) is a plain real-number hypothesis-level parameter, since neither theorem's own content
needs a reusable instance record (unlike the packing/covering CoveringInstance of
04-framework, this chapter's per-copy quantities are consumed once each, not threaded through a
family of algorithms). per_copy_guarantee (Lemma 9.1) takes the weak-duality bound, the
step-(1c) fill rule, and the x(e,j)≤2 invariant as hypotheses and derives both parts of the
lemma's conclusion by real algebra (a sign case-split for part (i); Real.logb/rpow manipulation
for part (ii)). routing_competitive (Theorem 9.2) takes Lemma 9.1's guarantee (universally
quantified over the copy index J, a general Fintype) plus the two composition hypotheses
described above, and derives the bicriterion conclusion by summation, transitivity, and scaling.
This correctly rules out the trivializing formalization in which the composition hypotheses are
strengthened to directly assert the theorem's own conclusion (each is a strictly weaker,
independently-motivated fact — the backward-induction accounting identity and the geometric
edge-multiplicity bound — checked in MODERATION_NOTES.md against this exact failure mode).
Reals throughout; Real.logb 2 for log₂. Welcome contributions: completing the two sorrys
(Lemma 9.1's part (i) is short algebra; part (ii) needs Real.rpow/Real.logb lemmas; Theorem
9.2's is transitivity/summation once its hypotheses are in hand), and — the natural follow-on —
formalizing the copy construction and the backward-induction/edge-multiplicity arguments
hquota/hload_aggregation currently stand in for, which would upgrade them from hypotheses to
theorems in their own right; Section 9.2's coordinate-wise-competitive fair-routing algorithm
(Theorem 9.3) and the matching lower bound (Lemma 9.5) are further natural follow-ons.
Caching is a two-level memory-management problem — the fast level (cache) can hold only
items, and the algorithm must decide, online, which item to evict whenever the current request
misses — that is normally analyzed through the competitive ratio of ad hoc marking or LRU-style
rules. Buchbinder and Naor's survey [1] instead recasts weighted caching (non-uniform fetching
costs) as an instance of the covering/packing linear program, and derives a fractional online
algorithm through the same primal-dual recipe formalized in this series' 04-framework mission
(Chapter 4), but for a genuinely different LP shape: the caching LP's right-hand side varies from
constraint to constraint, unlike Chapter 4's uniform . This mission covers Sections
7.1-7.2 of Chapter 7, "Generalized Caching": the fractional weighted-caching algorithm and its
-competitive analysis. Sections 7.3-7.4, which further generalize to non-uniform page
sizes (not just costs), are out of scope — a natural follow-on mission, not attempted here (see
Formalization scope).
Fix a finite set of primal variables — one per page and each of its eviction intervals between its -th and -th request — with fetching cost (the book's standing weighted-caching assumption), and a finite set of online constraints, one per request time , revealed in the order enumerated by . The eviction-charged LP formulation (the book charges for evicting pages rather than fetching them, an equivalent reformulation up to an additive constant independent of the request sequence) constrains, at each time : , where is the set of currently-active eviction variables for pages present until (excluding the page just requested) and is the amount of cache space those pages must collectively vacate. The Lagrangian dual has a variable per request time and a variable per eviction interval, with dual constraint . As in Chapter 4, primal variables may only increase and the algorithm sees each constraint only upon its arrival.
The Fractional Caching algorithm (p. 153-154) sets each to jump from to the first time its dual constraint tightens, then increases continuously according to an exponential function of the accumulated dual sum until it saturates at (at which point begins absorbing further dual increase at the same rate, freezing ). This is a genuinely different LP shape from Chapter 4's framework (non-uniform, time-varying right-hand side) reusing the same complementary-slackness design pattern as that chapter's Algorithm 3.
Theorem 7.1 (the goal, p. 154), given the algorithm's final dual values , and primal feasibility:
i.e. the algorithm is -competitive, with the constant taken verbatim from the book's
own theorem statement (no instantiation needed here, unlike most goals in this series).
The antecedent is itself Eq. (7.2) (p. 155), formalized as the milestone
dual_near_feasible: the algorithm's dual solution, scaled down by , is feasible — the
book's own intermediate step, derived from the fact that every cachingX value is capped at .
Chapter 7 is the first chapter in this survey to apply the online primal-dual method to an LP
whose right-hand side is not uniformly (unlike Chapters 4 and 5), demonstrating the method's
reach beyond the "simplified" 0/1-coefficient covering LP that 04-framework formalizes. The
fractional guarantee is also the analytical core of the chapter's randomized rounding
result (Theorem 7.3, not part of this mission — see Formalization scope), which converts it into
an actual -competitive randomized algorithm against an adaptive adversary, and of the
chapter's further generalization to non-uniform page sizes (Theorem 7.5, Sections 7.3-7.4). No
formal development of weighted or generalized caching was found on the platform as of 2026-09-20
(searches below); the existing KServer.* namespace formalizes a different, unweighted, uniform
-server model and shares no substrate with this mission. This mission is the first.
As with 04-framework's Algorithm 3, the central obstacle is characterizing an online process
by its final output alone: cachingX is defined as the algorithm's own closed-form update rule
(threshold-then-exponential, capped once ), evaluated at the run's final accumulated
dual values, rather than as an independently-constrained free variable — the latter would let
and be chosen to satisfy the conclusion's inequalities directly, trivializing the claim
that a specific online algorithm achieves this ratio. Establishing that the capped closed form
is faithful (not merely an invented convention) requires the same monotonicity argument
04-framework's alg3X uses, adapted to this chapter's extra term inside the exponent
(present here; absent from Chapter 4's Algorithm 3). The proof's own structure — splitting the
primal cost into a contribution () bounded via complementary slackness and a
contribution () bounded via a derivative/telescoping argument over the continuous
accumulation process (Eqs. (7.6)-(7.10), p. 155-157) — is, as in Chapter 4, a genuinely dynamic
fact about the trajectory, not encoded as a hypothesis; the mission states the theorem faithfully
and leaves the sorry for that argument, per this series' documented-simplification convention.
CachingInstance V Time bundles S : Time → Finset V, rhs : Time → ℝ (unlike
04-framework's CoveringInstance, whose right-hand side is fixed at throughout), c : V → ℝ with hc_pos : ∀v, 1 ≤ c v (the book's own literal cp ≥ 1, not a strengthening), and k : ℕ
with hk_pos : 0 < k. dualSum inst y v := ∑_{t \mid v \in S(t)} y_t, matching 04-framework's
pattern. cachingX inst y z v is a noncomputable def: 0 before activation, otherwise
min 1 ((1/k) exp((dualSum - z - c v)/c v)), so "the algorithm's output" is genuinely a function
of its dual trajectory. Reals throughout; Real.log for the book's natural log . Explicitly
out of scope: Section 7.3's rounding apparatus (Theorem 7.3, the map from fractional to
randomized-integral cache states) and Section 7.4's non-uniform-page-size generalization
(Theorem 7.5) — both are natural follow-on missions building on this one's CachingInstance and
cachingX, not attempted here per this chunk's own BRIEF.md, which flags Theorem 7.1 alone as
"a complete, self-contained mission goal" when the rounding apparatus proves too heavy for a
single pass. Welcome contributions: completing the two sorrys, and the Section 7.3-7.4 follow-on
mission.
The metrical task system (MTS) problem is one of the earliest and most general online models: a server occupies a state in a metric space, requests arrive with per-state service costs, and the server may change state (paying the metric's transition cost) before serving each request. On a general metric, competitive algorithms are hard to design directly. Chapter 6 shows that on a weighted star metric — the simplest genuinely non-uniform metric, a hub with leaves at varying distances — the online primal-dual framework of Chapter 4 becomes applicable, but only after a change of rules: the chapter defines a new MTS model, in which the server may change state only at the boundary of a "phase" (an interval during which its accumulated service cost reaches the state's own transition charge), and shows this new model is cost-equivalent, up to a constant factor, to the standard model. This equivalence is what licenses recasting the (new-model) problem as a covering linear program with the online primal-dual framework directly applicable — the chapter's actual algorithmic payoff (an unnumbered -competitive result, Section 6.2) rests entirely on it.
Fix a set of leaves (the book's finite ) of a weighted star, each leaf at distance from the center. The chapter immediately collapses the full star metric to a single per-state transition charge , since on a star every transition costs at most , and charging the doubled source leaf's distance alone (never charging for arriving) upper-bounds every transition cost independent of destination. A standard-model solution is a finite sequence of runs, each specifying a state occupied and the service cost accumulated while in that state, ending with a transition (cost ) to the next run's state; its total cost is . A new-model solution is a finite sequence of phases, each specifying a state visited; a phase's cost is exactly regardless of how much service actually occurred during it (a state change is only permitted once a phase's accumulated service reaches the phase's own -value), so the new model's total cost is .
Lemma 6.1 (goal, p. 144): any standard-model solution's runs transform into a new-model solution whose cost is at most ; in particular .
Lemma 6.2 (milestone, p. 145): any new-model solution's phases , with each phase's actual service , are simultaneously a legal standard-model solution (the same trajectory, recosted) whose standard-model cost is at most .
Together (stated in the book but not separately numbered, hence not a formalization target here): a -competitive algorithm in the new model implies a -competitive algorithm in the standard model.
This is a model-equivalence result, a distinct and recurring pattern in online algorithm design
from the competitive-ratio bounds formalized elsewhere in this series: rather than analyzing an
algorithm directly, the chapter first shows that solving an easier, more restricted version of
the problem (state changes only at phase boundaries) loses only a constant factor, and only then
designs an algorithm for the restricted version. The technique generalizes (the chapter's own
Notes section places it in the context of Borodin et al.'s original MTS bounds, and of later work
on hierarchically well-separated trees for general metrics), but this chapter gives its cleanest,
self-contained instance: two short, tight (factor-2 each direction) transformations between two
formally distinct online cost models. No prior formalization of metrical task systems on a
weighted star, or of this new/standard model equivalence, was found on the platform as of
2026-09-20 (search below); the platform's existing KServer.* campaign formalizes a different
online problem (uniform-metric -server) with a different metric structure and is not adjacent
substrate for this chapter's weighted-star MTS model.
The central obstacle is representing "a solution" at a level of abstraction faithful to the
book's own proof without committing to a full continuous-time process model (states as functions
of a real time variable, phases as recursively-defined stopping times, requests as an explicit
arriving sequence) that neither lemma's own proof actually needs. Both proofs work entirely at
the granularity of a solution's runs (standard model) or phases (new model) — finite
sequences of (state, cost) data — never referencing continuous time except to justify that this
decomposition exists. This mission formalizes both lemmas at exactly that granularity: a run/phase
sequence indexed by Fin k, with costStandard/costNewPhases the book's own displayed cost
formulas. Lemma 6.1's proof genuinely constructs a new object (the delayed-transition solution
) and only bounds its cost, never gives a closed form — formalized here as an existential
over a per-segment cost witness w', bounded above and below exactly as the proof's own argument
does (with the lower bound d(s i) ≤ w' i serving as the guard against the vacuous witness
w' = 0, since without it the existential is trivially satisfiable and asserts nothing). Lemma
6.2's proof, by contrast, reuses the same trajectory in both models with no construction at all,
formalized directly as a cost comparison between costStandard and costNewPhases applied to
the identical (s, w) data.
WeightedStar V bundles centerDist : V → ℝ (the book's ) with non-negativity;
WeightedStar.d is the collapsed charge . costStandard/costNewPhases are
literal transcriptions of the two models' displayed cost formulas over a Fin k-indexed run/phase
sequence. standard_to_new (Lemma 6.1) is the existential described above; new_to_standard
(Lemma 6.2) is the direct cost comparison. Reals throughout; V is left a general Type* (not
assumed Fintype) since neither lemma's own statement needs the chapter's finiteness assumption
— that assumption only matters for the unnumbered -competitive claim of
Section 6.2, out of scope per BRIEF.md's explicit instruction (no numbered theorem to formalize
it against). This correctly rules out the trivializing formalization in which "new-model
solution" is left as an unconstrained free variable satisfying only the conclusion's own
inequality, or in which the star structure is dropped entirely in favor of an arbitrary metric
(the chapter's own reduction to a per-state charge , rather than a full metric
, is precisely what the star's structure licenses, and is preserved
here via WeightedStar.d rather than a bare hypothesis-level function). Welcome contributions:
completing the two sorrys (Lemma 6.1's needs an explicit construction of and its
per-segment cost bound; Lemma 6.2's is a short termwise algebraic argument), and formalizing the
Section 6.2 covering-LP algorithm and its -competitive claim as a follow-on mission
once it can be stated against a numbered result.
A polytope can be represented not only by vertices or supporting inequalities, but also as a section of a simplex in a higher-dimensional space. Perles's prescribed-point theorem strengthens this representation: the cutting flat can be required to pass through an interior point selected in advance. This is Theorem 5.1.10 in Branko Grünbaum's Convex Polytopes, second edition, §5.1, printed p. 74. The result isolates how a bound on the number of facets controls the dimension of a universal simplex while retaining freedom to prescribe a point in the section.
Fix natural numbers and . A -polytope is represented here as a nonempty convex hull of finitely many points whose affine span is all of . A face is the complete maximizing locus of a supporting linear functional, and a facet is a nonempty face of affine dimension . The quantity used in the target counts geometric faces, not the number of inequalities in a chosen description.
A -simplex is the convex hull of affinely independent points in . Write this simplex as . Affine independence makes full-dimensional, so is its ordinary ambient interior. No regularity, coordinate normalization, or metric condition is imposed on . A -flat is a translate of a -dimensional linear subspace. Its section of is the whole intersection .
Two subsets are affinely equivalent when an affine bijection between their affine spans maps one set exactly onto the other. Distances and angles need not be preserved. In the formal statement this equivalence is witnessed by an injective affine map whose range is and whose image of equals .
The single target is the prescribed-point section theorem:
Grünbaum writes the number of allowed facets as and uses an -simplex in . The Lean statement sets . Every input, including the simplex and its interior point, is universally quantified before and are chosen. Thus the witnesses may depend on all the input data, but neither the simplex nor the prescribed point may be chosen to suit .
The theorem gives a controlled simplex-section representation for every polytope with a bounded number of facets. Its prescribed-point clause is stronger than merely asserting that some section somewhere is affinely equivalent to : it permits the ambient simplex and any one of its interior points to be fixed first. The equality also covers the entire section, excluding a weaker containment statement.
This is a known theorem, not an open conjecture. The package supplies a source-reviewed, compiling Lean statement with a proof placeholder. A complete contribution would replace that placeholder by a machine-checked proof while preserving the facet bound, the arbitrary-simplex quantifier, the prescribed point, the flat dimension, and the exact affine-equivalence conclusion.
A flat chosen only to pass through may cut out the wrong affine shape, while a flat producing the correct shape need not contain the prescribed point. The theorem requires both conditions simultaneously for every allowed simplex and every interior point. Restricting to a regular simplex, moving the chosen point, or proving only an unrestricted section representation would lose essential quantifiers from the source statement.
The facet allowance also refers to geometric facets rather than a particular inequality presentation. A formal proof must therefore connect the combinatorial boundary data of with the geometry of the simplex section without replacing the source hypothesis by a representation-dependent count.
Lean represents by Fin d → ℝ. Grunbaum2003.IsDPolytope requires a finite nonempty convex-hull presentation and full affine span. Grunbaum2003.faceCount P r is the finite cardinality of nonempty exposed faces whose affine-span direction has dimension . For , the hypothesis uses faceCount P (d - 1). For , the formal statement makes the facet allowance automatic; this avoids natural-number underflow while retaining the zero-dimensional source case.
The simplex is convexHull ℝ (Set.range v) under AffineIndependent ℝ v, and interior is ambient interior. The witness L is an affine subspace containing with direction dimension . The affine map is injective, has range exactly , and maps all of onto the full intersection. These conventions rule out degenerate simplices, lower-dimensional input polytopes, containment-only conclusions, and vacuous facet counts.
The two definition files are expression-essential and shared with other missions in this textbook series. No proof-only theorem is packaged, and there is no separate reviewed source lemma to list as a milestone.
The cosmological constant entered physics in 1917, when Einstein added a term to his field equations in order to allow a spatially homogeneous universe that neither expands nor contracts (Einstein, Kosmologische Betrachtungen zur allgemeinen Relativitätstheorie, 1917). The resulting Einstein static universe is the unique balance in which the attraction of pressureless matter, the repulsion carried by , and a positive spatial curvature cancel exactly. Two facts about that balance shaped the next century of cosmology:
After Hubble's 1929 observations Einstein dropped the term; it returned in 1998, when the supernova measurements of the Supernova Cosmology Project and the High- Supernova Search Team required . Interpreting as a vacuum energy density with equation of state then produced the cosmological constant problem: the measured value, about , is roughly in Planck units, tens of orders of magnitude below the scale that effective quantum field theory suggests (Wikipedia, Cosmological constant problem).
This mission formalizes the classical ordinary-differential-equation content of that story: the static solution, its uniqueness, its instability, the vacuum-energy reading of , the density-parameter bookkeeping, and the numerical size of the discrepancy.
A homogeneous isotropic universe is described by a positive scale factor on a set of times . Matter is pressureless dust, whose density dilutes with volume,
where and are reference values. Units are geometrized, , so has dimension (length); is Newton's constant and the curvature constant.
The dynamics are the two Friedmann equations. The first Friedmann equation is the constraint
and the acceleration equation for dust is
The Hubble parameter is , the critical density is , and the density parameters are
For , the constant function satisfies both Friedmann equations if and only if
in which case , , , and the equilibrium is unstable in the following exact sense: every solution of on with and is strictly increasing and satisfies ; and every positive solution on with and is strictly decreasing.
is exactly a perfect fluid of constant density and pressure ; the density parameters satisfy ; the acceleration equation is a consequence of the first Friedmann equation along a solution with ; and the observed is smaller than in Planck units.
The static solution is the historical origin of , and its instability is the reason the static model was never a viable cosmology even before the expansion was observed: the balance point is a local maximum of the effective potential, not a minimum, so the equilibrium cannot be maintained. The same function and the same linearization govern the late-time behaviour of the standard CDM model, where the growing mode becomes the de Sitter expansion .
What the mission produces on top of the textbook statements: a machine-checked ODE treatment of a dust-plus- cosmology that does not stop at the linearized equation. The classical physics argument computes and calls the equilibrium unstable; the formal statements here ask for the nonlinear conclusion — monotone escape to infinity on one side and strict collapse on the other — which is what "unstable" has to mean for the exact equations. Mathlib contains neither the Friedmann equations nor a general instability criterion for second-order autonomous scalar ODEs, so both have to be built here.
The linearized step is routine calculus. The nonlinear instability is not: from with and strictly increasing on , one must run a bootstrapping argument in which the sign of controls , which in turn controls whether stays in the region where the sign of was known. The obvious approach — solve the ODE explicitly — is not available: the dust-plus- equation with the static value of has no elementary closed-form solution through the static point, and the first Friedmann equation, which is the conserved energy of the second, degenerates exactly at , where . Divergence additionally requires ruling out that stalls, i.e. a quantitative lower bound on once the solution has left a neighbourhood of .
Everything is stated for real-valued functions of a real time variable; derivatives are the usual derivative of a real function, and each equation is asserted pointwise on an explicit set of times (, , , or a general open set), never globally by fiat. Dust density, the Friedmann equations, the acceleration function , the Hubble parameter, the critical density and the three density parameters are all fixed in one definition file shared by every statement, so all items commit to the same conventions: , curvature entering as in the equation for , and as fixed reference constants rather than the value of the density at a particular time.
Two trivializing readings are ruled out explicitly. First, the contracting-side statement is posed on a bounded interval with positivity of assumed there, because a collapsing solution reaches in finite time; posing it on would make its hypotheses unsatisfiable and the statement vacuous. Second, the escape statement asks for , not merely , so it cannot be satisfied by a solution that converges to a finite limit.
Useful contributions beyond the listed items: a reusable instability criterion for at a zero of with , and the corresponding stability criterion, both of which are independent of cosmology.
Convex hulls are often defined using arbitrary finite convex combinations. In finite dimensional geometry, Carathéodory's theorem gives a uniform bound on how many points are needed to represent any one point of the hull. This is the finite representation result stated in Branko Grünbaum's Convex Polytopes, second edition (2003), §2.3, Theorem 2.3.5, printed page 15 (PDF page 33). It matters when one wants a description whose number of witnesses depends on the ambient dimension rather than on the size of the generating set. The mission concerns that exact textbook statement for an arbitrary subset of real coordinate space.
Fix a natural number . The ambient space is represented in Lean as Fin d → ℝ: a point assigns a real coordinate to each of the indices. Let be any set of such points. Its convex hull, written in the book and convexHull ℝ A in Lean, is the smallest convex set containing . A convex combination is a finite weighted sum of points of whose real weights are nonnegative and total one. No finiteness, closedness, boundedness, convexity, or nonemptiness assumption is imposed on .
The witnesses in the target are indexed by Fin (d + 1), which has exactly elements, corresponding to the book's indices . Repeated points and zero weights are permitted. They allow a representation that uses fewer than distinct points to be written with the same fixed index type.
For every , find points and real numbers such that
The Lean goal is Grunbaum2003.caratheodory_convex_representation. It quantifies over every natural dimension, every set in that real coordinate space, and every point of its convex hull. The existential witnesses and all four required clauses are part of one theorem. This is the sole goal and sole source obligation in the frozen mission grouping; there is no separate supporting milestone to attest.
The result turns membership in a convex hull into a representation with a dimension controlled number of generators. The bound is independent of the cardinality of , which may even be infinite. In the textbook's chapter, this is the finite representation model from which other discussions of convex sets can proceed. It does not itself claim a separation theorem, a compactness statement about closures, or a representation of unbounded closed convex sets using recession directions; those are distinct statements with different hypotheses and conclusions.
A formal proof of this statement would establish the textbook result in Lean for the exact source quantifiers and index bound. The present proposal contains a statement with sorry, not a proof. The original statement compiled in the local Lean workspace and passed source aware moderation; successful compilation verifies that its expression is well formed but does not settle the theorem. The open work in this mission is to replace the placeholder with a machine checked proof of the stated result.
The definition of convexHull ℝ A establishes membership by finite convex combinations, but such a combination can have arbitrarily many terms. The target asks for a bound of terms, uniformly for every point and every generating set. Merely unfolding convex hull membership therefore does not deliver the claimed index bound. The witness must also keep membership in , nonnegative coefficients, normalization, and the exact vector equality simultaneously. These constraints explain why a general finite combination cannot simply be relabelled as a Fin (d + 1) family.
The representation uses real scalars and the coordinate space Fin d → ℝ. The Lean statement uses convexHull ℝ A for the hull, Fin (d + 1) for both point and weight families, and a finite sum for normalization and the represented point. d = 0 is included. When is empty, the hypothesis has no instance; no artificial nonemptiness premise is added. There is no extra affine independence or strict positivity condition on the witnesses.
The only expression dependencies are Mathlib's convex hull, real numbers, finite indexing, finite sums, and scalar multiplication. The proposal does not introduce a duplicate convex hull definition or a book specific representation predicate. A complete proof may use Mathlib's existing convexity library, but the theorem statement and its source obligations remain fixed. Contributions that prove the exact quantified statement are within scope; variants with a restricted , a changed ambient space, or fewer clauses would answer a different question.
source.pdf in the book record; SHA-256 070befaa8c47f043ef9da1df0705910480eb692f044d1843c9f048f3e61fecac.Minimum mean square error (MMSE) estimation — predicting a signal from a noisy observation by minimizing expected squared prediction error — underlies linear systems theory, linear regression, Kalman filtering, and multiple-input multiple-output signal processing. Its classical solution assumes the joint distribution of is known exactly; in practice it is estimated from data, and the estimator inherits sampling error and model risk. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter shows that hedging the MMSE objective against every distribution in a Wasserstein ball around the empirical distribution — an infinite-dimensional worst case over an intractable set of measures, a priori — collapses to a tractable, finite-dimensional convex semidefinite program (Theorem 25, p. 29), building on the Gelbrich-hull machinery of Section 2.3. This mission formalizes that reduction.
Fix and let be a random vector: the signal to be estimated, the observation. An estimator is a measurable function ; write for the family of all estimators. The distribution of is only known to lie in a type-2 Wasserstein ball centered at an elliptical nominal distribution with nominal mean (), nominal covariance , and density generator . The distributionally robust MMSE estimation problem is
Writing blockwise, the nonlinear convex SDP
is the finite-dimensional relaxation the chapter builds toward.
Goal (Theorem 25, distributionally robust MMSE estimator). If , then the optimal value of problem (35) equals the optimal value of SDP (36). Moreover, if is optimal in (36) with invertible, then the affine function
attains the outer infimum of (35) — it is a distributionally robust MMSE estimator, exhibited in closed form from an SDP optimizer.
Theorem 25 reduces an a priori infinite-dimensional, worst-case functional optimization problem (an infimum over all measurable estimators of a supremum over all distributions within a Wasserstein ball) to a finite convex program with one linear matrix inequality, one Loewner-order lower bound, and one trace/matrix-square-root constraint — solvable in polynomial time, with the optimal estimator recovered in closed form from the SDP's optimal block matrix. It shows that robustifying MMSE estimation against distributional ambiguity does not sacrifice tractability: the resulting estimator remains affine, the same functional form as the classical (non-robust) best linear unbiased estimator, only with its coefficients drawn from a regularized covariance estimate rather than the raw sample covariance. Formalizing it fixes, machine-checkably, the exact shape of that regularization — which SDP constraints are load-bearing (the Loewner lower bound in particular rules out a numerically unstable near-singular ) and which conditions (, invertible) the closed-form estimator formula actually needs.
The paper's own remark (p. 29) names the two nontrivial steps: first, "establishing a minimax theorem for (35) and exploiting the properties of elliptical distributions" to show the outer infimum is attained by an affine estimator — a priori (35) ranges over all measurable , and there is no obvious reason the worst case forces linearity. Second, "combining this structural insight with Theorem 16" (the SDP-representability result for indefinite quadratic losses under an elliptical nominal distribution, itself a nontrivial closed-form reduction of an infinite-dimensional worst-case risk) to convert the now-restricted problem over affine estimators into the finite SDP (36). Neither step is a routine consequence of the ambiguity-set definitions alone; each requires structural facts about elliptical distributions and quadratic losses proved earlier in the chapter.
The signal-observation space is EuclideanSpace ℝ (Fin mx ⊕ Fin my), with and recovered
as the two summand projections; the block matrix is Matrix (Fin mx ⊕ Fin my) (Fin mx ⊕ Fin my) ℝ, and Matrix.toBlocks₁₁/toBlocks₁₂/toBlocks₂₁/toBlocks₂₂ give its four blocks. The
constraint "" is not stated as a separate hypothesis: it follows
automatically once is symmetric (implied by S.PosSemidef), so encoding the feasible set from
a single symmetric S rather than four independently-quantified blocks makes it structurally
impossible to drop — see pitfall 4 of BRIEF.md. The outer infimum of problem (35) ranges only
over measurable (Measurable ψ on the binder), matching the paper's own definition of
as "the family of all possible measurable estimators" (p. 29) exactly. λ_min(Σ̂) is taken
as a hypothesis parameter
characterized by the two properties that make it the minimum ("≤ every eigenvalue of Σ̂, and
attained by some eigenvalue"), rather than invoking a specific Mathlib min-eigenvalue API by name.
S_{yy}⁻¹ uses the ordinary matrix inverse (junk zero matrix when singular), matching the paper's
literal notation; S^\star_{yy} invertible is stated as an added hypothesis, not present
verbatim on the page, because the paper leaves the formula's well-definedness implicit — disclosed
per pitfall 5 rather than silently assumed away. The paper's own "which is always solvable"
clause is not asserted: Theorem 25 states, as part of itself, that SDP (36) attains its maximum
(an unconditional existence claim for an optimal ); this formalization states only the
conditional consequences of such an existing, not that one does — proving or asserting
solvability is out of this mission's scope, so the Lean statement is strictly weaker than Theorem
25's own conclusion on this point, disclosed rather than silently dropped. All risk-style suprema
are EReal-valued and
Integrable-guarded, matching the series' convention. No milestone theorem is included: the
paper's own proof sketch derives (33)'s and by extension (36)'s SDP "via Theorem 16", but Theorem
16 (indefinite quadratic loss and , eq. 23) was itself judged too heavy to state faithfully
in 02-gelbrich's time budget and is not redefined here either — see STATUS.md. Theorem 24 (the
Wasserstein shrinkage estimator, this chapter's originally recommended goal) is out of scope: its
closed-form eigenvalue transformation (eq. 34a/34b) requires transcribing nested square roots from
a rendered PDF page that this session's time budget did not allow verifying to the standard the
brief demands (pitfall 1); the brief's own documented fallback to Theorem 25 was taken instead.
Distributionally robust optimization (DRO) hedges a decision against every distribution within some ambiguity set around an estimated (nominal) distribution, rather than trusting the estimate exactly. When the ambiguity set is a ball of radius around the empirical distribution in the type- Wasserstein metric, the resulting worst-case risk problem inherits attractive statistical guarantees (Mohajerin Esfahani & Kuhn 2018) but is, in general, an optimization problem over an infinite-dimensional space of measures. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter surveys when this problem becomes computationally tractable. One route — the subject of this mission — discards everything about the nominal distribution except its mean vector and covariance matrix and replaces the Wasserstein ball with a set built only from these two moments, the Gelbrich hull. The construction is due to Gelbrich (1990), who first bounded the Wasserstein distance between two distributions using only their means and covariances.
Fix , a nominal distribution , a radius and an exponent . The type- Wasserstein distance between two probability measures on is
the infimum over couplings (probability measures on with marginals and ) of the -th root of the expected -th power of Euclidean distance. The Wasserstein ambiguity set is , and the worst-case risk of a loss function is .
Suppose has mean vector and covariance matrix (the positive semidefinite matrices). The mean-covariance uncertainty set is
where is the positive-semidefinite square root. The Gelbrich hull is : the distributions on whose own mean and covariance lie in . An elliptical distribution has density for a density generator and normalizing constant ; two elliptical distributions "have the same density generator" when their coincide (e.g. both Gaussian, both Student- for the same ).
Goal (Theorem 13, Gelbrich hull). For every ,
This is an outer approximation: every distribution within of in Wasserstein distance has a mean and covariance inside , so optimizing over the Gelbrich hull instead of the Wasserstein ball can only enlarge the feasible set, never shrink it below the truth.
Supporting results. Theorem 4 (Gelbrich bound) gives the moment-only lower bound on that Theorem 13 is built from, with equality for elliptical distributions sharing a generator. Proposition 1 sharpens the goal's containment to an equality on the mean-covariance projection itself, under the same two conditions (, elliptical). Corollary 1 propagates the goal's set containment to the risk level: for every , where is the Gelbrich risk.
Theorem 13 is the hinge between an intractable infinite-dimensional worst-case-risk problem and a tractable one: the paper goes on (Theorem 16, outside this mission's scope) to show that for quadratic loss functions and elliptical nominal distributions the Gelbrich risk itself equals the optimal value of a semidefinite program with two linear matrix inequality constraints — and that, under those same conditions, the Wasserstein worst-case risk, the Gelbrich risk and the SDP value all coincide. Corollary 1 is what makes the Gelbrich risk usable as a conservative surrogate even outside that special case: it upper-bounds the true worst-case risk for any loss function and any , at the cost of discarding all but first- and second-order information about the nominal distribution. Formalizing the goal and Corollary 1 gives the exact scope in which this moment-relaxation is licensed — the restriction and the outer-approximation direction are both easy to get backwards, and this mission's Lean encoding fixes both irreversibly.
The obvious first argument is to prove containment pointwise: fix and show its mean and covariance land in . That reduces Theorem 13 to Proposition 1's containment half, which in turn reduces to the Gelbrich bound (Theorem 4) applied to the pair — the inequality direction of Theorem 4 suffices for containment; only the sharper equality direction (needed for Proposition 1's own equality clause) requires the elliptical hypothesis. The non-obvious step is Theorem 4 itself: bounding below by a closed-form expression in the two distributions' first two moments only, for arbitrary with those moments, requires an argument that survives every coupling — the paper's proof goes through a lower bound on the coupling's cross-covariance term via the eigenvalues of , not a direct manipulation of 's definition.
is EuclideanSpace ℝ (Fin m); a "distribution" is a MeasureTheory.Measure on it
constrained by Q Set.univ = 1 (probability) and Q Ξᶜ = 0 (support in Ξ). The Wasserstein
distance is ENNReal-valued (Definition 1's infimum over couplings, matching 01-duality's
convention); the worst-case and Gelbrich risks are EReal-valued suprema restricted to loss
functions integrable under the candidate distribution, avoiding Mathlib's junk value for a
non-integrable Bochner integral. is the positive-semidefinite matrix square root,
picked by choice from its defining existential and applied in this mission only to matrices
hypothesized (or, per Section 2.3's standing assumption, given) positive semidefinite. Elliptical
distributions (IsElliptical) are represented by the paper's own density formula (a measure
equal to volume.withDensity of C·det(Σ)⁻¹·g((ξ-μ)ᵀΣ⁻¹(ξ-μ)) for some C>0), together with
the mean/covariance facts every theorem in this chunk reads off directly; an earlier draft kept
only the latter, under which "same density generator" held vacuously for any moment-matched
pair — corrected after moderation flagged it (see STATUS.md).
Because 01-duality (Wasserstein distance, ambiguity set, worst-case risk) is not yet a published
mission, this chunk redefines those objects locally in its own namespace rather than importing an
unpublished draft, per the series' definition-reuse policy; a future upload can retire the
duplication once 01-duality is live. A formalization that dropped Theorem 4's "same density
generator" condition from its equality clause, or that stated the goal's containment for all rather than , would be trivializing or simply false — both are explicit hypotheses in
the Lean statements. Matrix.PosSemidef and its Loewner order carry the constraints; no
elliptical-distribution or Gelbrich-hull infrastructure exists elsewhere on the platform, so this
mission's definitions are original contributions reusable by any later extension (Theorem 16/17,
Lemma 1/2's SDP representations) of this series.
A system of natural units fixes the size of the base units not by reference to an artefact or a historical convention, but by declaring that certain universal constants have numerical value . The oldest and most widely used such system is the one Max Planck proposed in 1899, at the end of Über irreversible Strahlungsvorgänge, built from the speed of light , the gravitational constant , the quantum of action (today ) and the Boltzmann constant . Planck's claim for these units was that they are "independent of special bodies or substances" and therefore retain their meaning "for all times and for all civilizations, including extraterrestrial and non-human ones".
The claim that gives the system its force is a uniqueness claim: there is one and only one choice of base length, mass, time and temperature for which all four constants read . Textbooks and reference works state the resulting expressions , , , as the Planck units, but the accompanying argument is usually a dimensional-analysis sketch rather than a proof that the defining system of equations has exactly one positive solution. This mission formalizes the statement and its standard consequences.
Fix four positive real numbers , , , — the numerical values of the four constants in some reference system of units (SI, say).
A unit system is a quadruple of positive reals: the size of the chosen unit of length, mass, time and temperature, measured in the reference system. Changing to divides every quantity by the appropriate product of . Concretely, a speed is divided by , a quantity of dimension (the dimension of ) by , an action by , and a heat capacity by .
Say that normalizes when each of the four constants has numerical value in , i.e. when
The Planck system is the quadruple
together with the identification of that unique solution as the Planck system above. The statement is asserted for arbitrary positive , so it does not depend on the SI values of the constants, and it fixes nothing beyond positivity.
The milestones record the standard relations among the Planck units: ; the reduced Compton wavelength of the Planck mass equals ; the Schwarzschild radius of the Planck mass equals ; the coherent derived units of Table 2 of the source (energy, momentum, force, density, acceleration, frequency) have the stated closed forms; Newton's law of gravitation takes the constant-free form when every quantity is replaced by its ratio to the corresponding Planck unit; and normalizing in place of yields the rationalized Planck units.
The uniqueness statement is what licenses the everyday practice of "setting ": it says that the convention determines the units completely, so that a dimensionless equation written in Planck units can be translated back into a dimensional one in exactly one way. It also makes precise the sense in which the Planck scale is defined rather than measured: the quantities , , are consequences of the SI values of four constants and of nothing else.
What formalization adds here is not a new theorem — the algebra is elementary and the result is classical — but a machine-checked statement of a claim that is normally left implicit, together with a reusable Lean model of "system of base units" and "constant normalized to " in which variant conventions can be stated and compared. The rationalized-units milestone is included precisely to exercise that generality: it is the same theorem applied to instead of , and it shows that the formalization does not secretly hard-code the Planck convention.
The obvious argument — "count dimensions, invert a exponent matrix" — proves uniqueness of
the exponents in a monomial ansatz , not uniqueness of the solution among all
positive quadruples, which is what the claim asserts. The formal statement therefore has to be proved
directly from the four equations: eliminate and , reduce to with
, and cancel a positive factor . The remaining friction is Lean-side rather than
mathematical: the four defining equations are stated with division, so every step carries a
non-vanishing side condition, and the closed forms are square roots, so equalities are proved by
comparing squares of non-negative reals rather than by ring alone.
The development is over ℝ. A unit system is a structure with four real fields, positivity is a
separate predicate rather than a subtype, and "normalizes" is the conjunction of the four displayed
equations as written with division — for a positive unit system this is equivalent to the
product form, but the division form is what the statements use. All four constants are universally
quantified positive reals; no SI numerals appear anywhere in the development, and the milestones
about the derived units state closed forms (e.g. force , density ) rather
than decimal approximations.
Two trivialization risks are ruled out explicitly. The hypotheses are satisfiable — the Planck system itself is exhibited as a positive solution in the first milestone — so the uniqueness statement is not vacuous. And the goal is not merely "the Planck system normalizes the constants": it also asserts that every positive normalizing system equals it.
Infrastructure needed beyond Mathlib is minimal: Real.sqrt and its interaction with squaring and
positivity. The unit-system model is reusable for other natural-unit conventions (Stoney units,
reduced Planck units with , Hartree atomic units), and contributions extending it in that
direction are welcome.
A coupling constant is the number that fixes the strength of an interaction: it is the coefficient that multiplies the interaction term of a Lagrangian relative to its kinetic term, and in a perturbative treatment it is the parameter the expansion is organised in. The central structural fact about such a coupling in a quantum field theory is that it is not constant: once quantum corrections are resummed, the coupling depends on the energy scale at which the theory is probed. This scale dependence — the running of the coupling — is what distinguishes quantum electrodynamics, whose coupling grows with energy until perturbation theory breaks down (the Landau pole), from quantum chromodynamics, whose coupling decreases logarithmically at high energy (asymptotic freedom, Gross–Politzer–Wilczek, Nobel Prize in Physics 2004).
This mission formalizes the elementary mathematics behind those statements: the one-loop renormalization-group equation, its exact solution, and the two qualitatively different behaviours it produces depending on the sign of the one-loop coefficient. The source is the Wikipedia article Coupling constant (sections Beta functions, QED and the Landau pole, QCD and asymptotic freedom), which states these facts in prose and in the single displayed formula for the running QCD coupling.
Write for a single real coupling and for the logarithm of the energy scale. The beta function is defined by
and at one loop is a cubic monomial,
with a scheme- and theory-dependent real coefficient . Saying that runs at one loop on a set of scales means that is differentiable at every with .
For QCD the article records the one-loop form of the strong coupling directly in terms of the process energy and the QCD scale :
The goal theorem is the dichotomy governed by the sign of , for an initial condition at the reference scale :
i.e. : the coupling dies off logarithmically in the energy.
the flow cannot be continued up to the finite scale , which is the Landau pole of the one-loop approximation.
Both follow from the exact one-loop solution, which is itself a milestone:
The dichotomy above is the mathematical content of the two headline claims made about running couplings: that a positive one-loop coefficient drives the coupling to infinity at a finite energy, and that a negative one makes it vanish logarithmically at high energy. The milestones also isolate the statement that a vanishing beta function means the coupling does not run at all (scale invariance), and record the elementary analytic properties of the explicit QCD formula : it is strictly decreasing above , tends to as , and satisfies the one-loop flow equation .
Nothing here is open mathematics: these are exercises in the theory of a separable scalar ODE. What the mission produces is a machine-checked, reusable Lean development of the one-loop renormalization-group flow — a small piece of formalized physics infrastructure that later missions on renormalization or dimensional transmutation can import.
The only real subtlety is that the exact solution is obtained by differentiating , which requires knowing in advance that the solution never vanishes. Positivity is not assumed: it is a separate milestone, and must be derived from the initial condition together with the flow equation (if reached at a first time , the identity on forces to have a strictly positive limit). The Landau-pole statement is a non-existence claim and has no analytic content beyond this, but it does depend on the positivity step.
Scales are parametrised logarithmically: the independent variable is , the coupling is a function , and the flow hypothesis is imposed pointwise as a two-sided derivative at each point of the given set (at an endpoint of a closed interval this is slightly stronger than a one-sided derivative, which only strengthens the hypotheses of the positive results and weakens the non-existence claim — the Landau pole statement is therefore the conservative reading). No uniqueness or existence theory for ODEs is assumed; the statements quantify over arbitrary functions satisfying the flow equation. The QCD formula is taken with real arguments and no constraint tying or to a particular number of flavours; the numerical values quoted in the source (, MeV) are measurements and are deliberately not formalized.
Degenerate cases are visible in the statements rather than hidden: appears as its own milestone (constant coupling), and the value of for , where the logarithm is non-positive or zero, is never asserted.
Every quantitative statement of special relativity — how much a moving clock slows, how much a moving rod shortens, how the momentum and energy of a fast particle grow — is controlled by a single dimensionless number, the Lorentz factor . It is the factor by which the time, length, and inertia of a body in uniform motion differ from their rest values, and it is the quantity that makes relativistic kinematics quantitative rather than qualitative. Its consequences are measured routinely: cosmic-ray muons with a mean lifetime of reach the ground from an altitude of about in numbers explained by their large , and the standard model of long gamma-ray bursts requires ejecta with initial to resolve the compactness problem.
The material formalized here is textbook kinematics rather than open research: the definition of , the identities relating it to its reciprocal, to momentum, and to rapidity, its numerical and asymptotic behaviour, and the composition law of the boosts it parametrizes. The value of the mission is a reusable, machine-checked treatment of that material in Lean 4 — a small, self-contained piece of relativistic kinematics that later formalizations of Minkowski geometry or relativistic dynamics can build on.
Fix an inertial frame and a relative velocity along a single spatial axis, and let be the speed of light in vacuum. Write for the dimensionless velocity ratio. All statements in this mission are in units where , so is the only kinematic parameter and takes values in the interval for a massive body.
The Lorentz factor is
and its reciprocal is , the quantity tabulated alongside in the source article.
Two derived objects appear throughout. Relativistic velocity addition is
and the Lorentz boost of velocity , acting on the coordinate pair by and , is the symmetric matrix
Finally, the rapidity of a motion is the hyperbolic angle with .
for all subluminal . The goal asserts only the shape of the composition law — that the boosts are closed under composition and that the composed velocity is the relativistic sum — and fixes no numerical constants, so it is stable under any later refinement of the surrounding development.
The milestones cover, in the order of the source article: the bound with equality exactly at rest; the reciprocal identity ; strict monotonicity of on and its divergence as ; the rapidity identities and ; additivity of rapidity, ; the momentum form ; the Newtonian limit as ; the exact table entries , , ; and the inversion on .
The composition law is what turns the Lorentz factor from a formula into a group structure: closure of the boosts under composition, with velocities combining by , is the reason rapidity is additive and the reason the velocity of light is the same in every inertial frame, since stays inside . The supporting milestones are the facts a downstream development actually consumes — positivity and monotonicity of , the reciprocal identity, the momentum and rapidity representations, and the low-speed limit that recovers Newtonian kinetic energy.
None of these statements is mathematically open; all are standard. What the mission produces is their machine-checked form in Lean 4, stated against one fixed set of definitions so that the results compose with each other, together with a boost model usable by later work on Minkowski space. Mathlib supplies the analytic infrastructure (real square roots, hyperbolic functions, filters and limits, matrices) but carries no development of relativistic kinematics built on it.
The individual statements are elementary; the friction is in the analysis, not the physics. Three specific places are where a naive attempt stalls.
First, the real square root is a total function returning on negative inputs, so is defined — and useless — outside . Every algebraic step needs the positivity of in hand before dividing, and the hypothesis must be propagated to each intermediate expression, including to the composed velocity in the goal.
Second, the goal's matrix identity does not follow from entrywise algebra alone: the
entries of contain , a nested
square root, and the composition law only becomes polynomial after the identity
has
been proved. Attempting field_simp on the raw matrix equation, before establishing that
identity, produces a goal with three independent radicals.
Third, the two asymptotic milestones are statements about filters, not pointwise bounds. The divergence at is a one-sided limit that must be routed through the positivity of on a left neighbourhood of , and the Newtonian limit is stated on the punctured neighbourhood of , where the quotient has to be rewritten as a function continuous at before any limit theorem applies.
Everything is over the real numbers in units ; the definitions bundle fixes , , , and as total functions, and the boost is the matrix acting on with the sign convention . Subluminality is never built into the types: it appears as an explicit hypothesis on each statement that needs it, so the statements are about the physical regime and not about the junk values the definitions take elsewhere. Those junk values are the one trivialization risk worth naming: for the square root is and , so a statement that omitted the hypothesis would be false rather than vacuous, and a statement that replaced it by an unsatisfiable condition would be vacuous — every milestone here carries hypotheses that are satisfiable and that exclude only the unphysical range.
A complete development needs Mathlib's real square root, hyperbolic functions, filter and limit API, and matrix notation; nothing beyond Mathlib is assumed. The boost model and the velocity-addition operation are the reusable parts: extensions to boosts in dimensions, to the invariance of the Minkowski quadratic form, to time dilation and length contraction as corollaries of the goal, and to the energy–momentum relation are all welcome as follow-up contributions.
The proton-to-electron mass ratio is a dimensionless constant of nature; the CODATA 2022 recommended value is
the parenthesised digits being the standard uncertainty on the last two places, i.e. a relative standard uncertainty of (NIST CODATA).
In a two-sentence note in Physical Review in 1951, Friedrich Lenz observed that the then best experimental value, , is matched almost exactly by the closed-form expression . The observation is regarded as a numerical coincidence rather than a physical relation: measurement precision has improved by roughly nine orders of magnitude since 1951, and at today's precision the two numbers are close but demonstrably different. This mission fixes that statement as a machine-checked one — it asks for rational enclosures of sharp enough to decide the comparison in both directions: agreement with the 1951 datum, disagreement with the modern one.
The mathematics is elementary. The content is entirely in the rigour of the numerics: certified rational enclosures of a transcendental quantity rather than floating-point evaluations.
Throughout, all quantities are real numbers.
lenzExpression in the formal development), with the usual circle constant.codataValue), and its standard uncertainty (codataUncertainty), the "(32)" attached to the last two digits.lenz1951Measurement) and its quoted uncertainty (lenz1951Uncertainty).These five constants are exactly the numbers appearing in the source; no physical model, no unit system and no dimensional analysis enters the mission. A "mass ratio" is modelled simply as a quotient of two reals.
For all reals with :
while at the same time
The goal deliberately packages both halves of the historical statement: Lenz's expression is inside the 1951 error bar and outside the 2022 one by more than a million standard uncertainties. The constants , and are stated with slack — the true values are about and — so the goal does not depend on the last digits quoted by any one source.
Note that the second window must be narrower than : an enclosure of of width is not sharp enough to imply the relative-deviation bounds of the goal, whose window has absolute width about but is centred away from .
The result itself. The claim "" is quoted in reference works but is normally supported only by decimal expansions computed in floating point. What this mission produces is a certified version: enclosures of and with rational endpoints, verified by the kernel, separating Lenz's expression from the measured constant by more than a million standard uncertainties, together with the complementary fact that the same number is consistent with the 1951 datum — which is why the coincidence was reported in the first place.
Formalizing it. Status honesty: none of this is open mathematics, and the numerical facts are standard. Mathlib already provides 20-digit bounds for (Real.pi_gt_d20, Real.pi_lt_d20) as well as the Real.pi_gt_sqrtTwoAddSeries / Real.pi_lt_sqrtTwoAddSeries machinery behind them, so the enclosures are reachable by monotonicity of on the nonnegative reals plus rational arithmetic. The mission's value is a clean, reusable formal record of a frequently quoted numerical comparison, not a new theorem. Contributions that go beyond a first proof — sharper enclosures, a general lemma bounding , or comparisons against other quoted values of the ratio — are welcome.
This is an easy mission by design; the one place a first attempt goes wrong is precision bookkeeping.
All statements are over ℝ. The constants are published as a single definition file; lenzExpression is noncomputable since it mentions Real.pi. Decimal literals such as 1836.152673426 denote exact real numbers (the corresponding rationals), not floating-point approximations. Inequalities are strict throughout, and comparisons are stated with absolute values so that no sign convention is hidden.
The goal quantifies over two reals subject only to ; no positivity is assumed, since the hypothesis already pins the quotient, and the hypothesis is satisfiable (e.g. ), so the statement is not vacuous. No measurement-theoretic notion of "uncertainty" is formalized: and are plain real constants appearing in the stated inequalities.
A complete development needs only Mathlib's Real.pi bound API and norm_num/linarith. The enclosure of is the one piece reusable beyond this mission.