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?
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.
Engineers deciding whether a pipe flow will be smooth or turbulent, whether a wind-tunnel model at 1/20 scale reproduces the flow over a full-size wing, or how fast a sand grain settles in water, all reduce the question to a single number. The Reynolds number is that number: the ratio of inertial to viscous forces in a flow. It was introduced as a similarity parameter by George Stokes in 1851, popularised by Osborne Reynolds's 1883 pipe experiments, and named by Arnold Sommerfeld in 1908.
What makes more than a convenient abbreviation is a mathematical fact: among the four quantities that describe a simple viscous flow — density, velocity, a characteristic length and viscosity — the Reynolds number is the only dimensionless combination, up to taking powers. Everything a dimensional analysis can say about such a flow is therefore a statement about alone. This mission formalises that uniqueness claim, together with the standard algebraic identities that surround it in engineering practice.
Work with four real parameters of a flow:
The Reynolds number is
and the kinematic viscosity is , so that .
For duct flow one further needs the hydraulic diameter , where is the cross-sectional area of the duct and its wetted perimeter — the part of the boundary in contact with the fluid.
Dimensional analysis is modelled explicitly. In the mass–length–time system the four parameters carry the dimensions
For real exponents the monomial therefore has dimension with
and the monomial is called dimensionless when . These
three linear forms are what the mission's dimExponents and Dimensionless record.
The goal theorem is the uniqueness of the Reynolds number as a dimensionless group. For positive and real exponents :
The milestones are the supporting statements, ordered as they appear in the source:
The result itself. The uniqueness statement is the reason dynamic similitude works at all: two geometrically similar flows of a Newtonian, incompressible fluid that share a Reynolds number cannot be distinguished by any dimensionless monomial in , which is why a scale model in a wind tunnel is informative about the full-size object. It also explains the shape of engineering correlations: drag coefficients, friction factors and settling laws are tabulated as functions of a single variable, , rather than of four. The pipe-flow and hydraulic-diameter milestones are the bookkeeping that lets the same number be computed from whatever data a practitioner actually has — volumetric or mass flow rate, circular or annular cross section.
Formalizing it. None of these statements is open mathematics; each is a short computation, and the mission's value is in fixing a faithful formal model of dimensional analysis for this system and checking that the textbook identities hold in it exactly as stated, with the boundary conditions (, , ) made explicit rather than assumed silently. The mission is therefore suitable as an entry point: it produces a small reusable layer — a dimension-exponent model and the Reynolds number itself — on which sharper fluid-dynamical formalizations can build. It does not attempt any part of the physics of transition to turbulence; the critical values and quoted in the source are experimental observations, not theorems, and are deliberately excluded.
The mathematical content is elementary linear algebra and field arithmetic; the difficulty is entirely in the modelling. Two traps are worth naming. First, division in Lean is total: , so a statement about that omits may still be provable while asserting nothing physical. Every statement here carries its positivity hypotheses explicitly for that reason. Second, the uniqueness claim is only true for monomials: an arbitrary dimensionless function of the four parameters is a function of , but the formal statement quantifies over exponent vectors, and the equivalence with uses real powers of positive reals.
All quantities are real numbers, not elements of a dimensioned type; the dimensional
content is carried by the explicit exponent map dimExponents, which returns the triple of
mass, length and time exponents in that order. Dimensionless a b c d is the proposition
that this triple is — a linear condition on the exponents, with no positivity
hypothesis on the parameters.
In the goal theorem the powers and are
real powers (Real.rpow), which is why are all assumed strictly
positive there. The milestone statements use ordinary arithmetic and assume only the
positivity each identity needs.
A trivializing reading is ruled out as follows: the goal is an iff whose right-hand side
pins the exponent vector and the value of the monomial, so it cannot be satisfied
vacuously; and the unit-rescaling milestone quantifies over all positive , so it
is not a statement about one convenient choice of units.
A complete development needs only Mathlib's real arithmetic and Real.rpow API. The
definition file is reusable: the Reynolds number, kinematic viscosity and hydraulic
diameter are the standard entry points for any later formalization of duct flow,
similitude or drag correlations. Contributions extending the model — other dimensionless
groups (Prandtl, Nusselt, Froude) expressed in the same exponent framework, or a general
Buckingham theorem for an arbitrary dimension matrix — are welcome.
Polynomial equations are the special case of root finding where algebra says a great deal before analysis is needed: the number of roots is known, the roots of a real polynomial come in conjugate pairs, the rational candidates can be listed, and the whole complex plane can be narrowed down to an annulus that must contain every root. A numerical method that exploits this information starts closer to the answer and needs fewer evaluations; and each evaluation itself can be made cheaper by Horner's scheme, which also delivers the deflated quotient for free.
This mission is the second in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 4, Zeros de Polinômios.
Throughout, a polynomial is written in the book's convention
so the index names the coefficient of and is the leading coefficient. The coefficients are real (integral, in the rational-root milestone) and ranges over unless stated otherwise.
Horner's algorithm computes by the recurrence , , so that , using multiplications and additions. The same numbers are the coefficients of the deflated polynomial with .
With and , the chapter's two localization results confine the roots to the annulus
The goal theorem is the outer bound (Proposição 4.2.1): every complex root of satisfies , where is the largest absolute value among the non-leading coefficients.
The milestones are the companion results of the chapter: the inner bound (Proposição 4.2.2), the fact that non-real roots of a real polynomial occur in conjugate pairs (Proposição 4.1.1), the existence of a real root in odd degree (Proposição 4.1.2), the correctness of Horner's evaluation scheme, and the deflation identity that accompanies it.
The two localization bounds are what makes a search for complex roots finite: they give an explicit compact region to sweep, and they give scale information that prevents an iteration from wandering off. The conjugate-pair statement halves the work for real polynomials and is the reason odd-degree real polynomials always have a real root. The rational-root test turns exact factorization into a finite search. Horner's scheme is the standard way a polynomial is evaluated inside every root finder, and its deflation identity is what lets a method remove a root that has already been found and continue with a polynomial of lower degree.
Mathlib already contains general results close to some of these (a polynomial over a real closed field of odd degree has a root; rational-root divisibility), so those milestones are accessible; the two localization bounds and the Horner statements in the book's index convention are the substantive new work.
The localization proofs in the source are short but rest on a geometric-series estimate that is only valid for ; the boundary cases have to be treated separately in a formal proof, and the degenerate situations (, coefficients all zero except the leading one) must be checked rather than waved through. The inner bound is obtained from the outer one by the substitution , which requires knowing that is a root of if and only if is a root of the reversed polynomial — an argument that has to be made explicit. The Horner statements look computational but need a careful induction because the exponents are natural-number subtractions.
Coefficients are given as a function together with a degree , and the polynomial is the finite sum ; two versions are provided, one evaluated at a real point and one at a complex point, with the coefficients coerced into . Only indices are read, so the values of beyond are irrelevant to every statement. The exponent is natural-number subtraction, which is harmless in this range. No hypothesis says that the family describes a polynomial of exact degree beyond the explicit assumptions or where they appear. The constants and are given as hypotheses equating them to the maximum of the relevant finite family of absolute values, rather than being defined separately. The rational-root and odd-degree milestones are stated with Mathlib's polynomial type instead of the coefficient-family encoding, since their statements involve no index convention.
The most precisely measured property of an elementary particle is the magnetic moment of the electron. The 2022 Northwestern measurement of Fan, Myers, Sukra and Gabrielse (arXiv:2209.13084) reports , and, combined with the Standard-Model prediction, . Those numbers are experimental results, not theorems, and nothing in this mission asserts them.
What is a theorem is the piece of mathematics the measurement rests on. A single electron is held in a Penning trap: a uniform magnetic field plus an electrostatic quadrupole potential. The quantity the experiment needs is the free-space cyclotron frequency , but what a trap lets you observe are its three normal-mode frequencies — the trap-modified cyclotron frequency , the axial frequency , and the magnetron frequency . A real apparatus is never perfect: the magnetic field is tilted relative to the axis of the potential, and the potential is elliptically distorted. The invariance theorem of Brown and Gabrielse (Phys. Rev. A 25, 2423 (1982)), quoted as Eq. (4) of the measurement paper, says that a particular combination of the three observed frequencies is completely insensitive to both imperfections:
This is what makes a part-per-trillion measurement possible with an imperfect trap, and it is the object of this mission.
Work in . A particle of charge and mass sits in a uniform magnetic field with a unit vector, and in the static field of a quadratic electrostatic potential. Dividing the Hessian of that potential by the mass gives a real matrix , and the equation of motion of the particle is linear:
Two properties of carry all the physics of the trap: is symmetric, because it is a Hessian, and traceless, because the potential satisfies Laplace's equation in the vacuum region where the particle moves. Beyond that, is arbitrary — an arbitrary is exactly what "the axis of the potential is tilted relative to , and the potential is elliptically distorted" means, so no separate tilt angle or ellipticity parameter appears anywhere.
Substituting the ansatz with turns the equation of motion into the linear system , where
is the matrix of . A frequency is a normal mode of the trap precisely when . The three eigenfrequencies of the trap, written (angular versions of ), are the non-negative solutions of that equation.
The goal is the invariance theorem in the form: if the three numbers are the eigenfrequencies of the trap, in the sense that
then, for every symmetric traceless and every unit vector ,
The milestones are the three steps of the argument, in increasing order of dependence:
The result. The invariance theorem is why the electron magnetic moment can be measured to parts per trillion in an apparatus whose magnetic field and electrode axis are not, and cannot be, exactly aligned. Without it, every misalignment and every elliptic distortion would enter the extracted as a systematic error, and the frequency ratio that gives would have to be corrected with a model of the imperfections rather than being invariant under them.
Formalizing it. The theorem is a short, completely classical piece of linear algebra — the point of formalizing it is to have the frequency-metrology identity available as a machine-checked statement, together with a reusable model of linear motion in crossed electric and magnetic fields (the mode matrix, its characteristic cubic, and the correspondence between the exponential ansatz and the kernel of the mode matrix).
Status — please read before treating this as open. All four statements in this proposal have been proved by the drafting agent on a local Lean 4.28 / Mathlib installation; the proofs are deliberately not uploaded, so the platform statements are genuinely open here, but this is a formalization-transfer mission, not an open research problem. Milestone 3 is included precisely so that the goal's factorization hypothesis is known to be satisfiable and the goal is not vacuously true. The statements themselves were additionally compiled in this platform's default Lean environment before this proposal was assembled.
The obvious first idea — solve and add up the roots — is exactly the thing not to do: for a tilted, elliptically distorted trap the three eigenfrequencies have no usable closed form. The whole content of the theorem is that the sum of their squares is the coefficient of in the characteristic polynomial and therefore needs no root formula at all: it is Vieta plus the two structural facts and . The work in Lean is consequently not analysis but bookkeeping: computing a determinant with complex off-diagonal entries and extracting one coefficient of the resulting cubic in . The one place real care is needed is the mode-equation milestone, where derivatives of complex-valued functions of a real variable must be handled honestly.
Conventions fixed by the Lean statements, and not visible in the prose:
Only Mathlib is needed: matrices over and , determinants of matrices, the cross product, and derivatives of complex-valued functions of a real variable. The definitions are reusable for any linear-motion-in-a-magnetic-field problem.
Experimental data are not exact, and forcing a curve through every measured point reproduces the noise rather than the law behind it. Curve fitting replaces interpolation by approximation: choose a family of shapes — a straight line, a polynomial of low degree, a combination of prescribed base functions — and pick the member of the family that is closest to the data in the least-squares sense. The resulting minimization is the numerical method most often used outside numerical analysis itself, from calibration curves to regression in statistics.
This mission is the fourth in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 6, Ajuste de Curvas.
Data are pairs , . Fix base functions and look for coefficients making
close to the data. The least-squares functional is
Setting the partial derivatives to zero gives the normal system
whose matrix is the Gram matrix .
The goal theorem is the necessity direction of §6.3: a coefficient vector that minimizes satisfies the normal system.
The milestones complete the picture the source leaves informal. First, the converse: any solution of the normal system is a global minimizer, so the normal system characterizes the least-squares fit rather than merely constraining it. Second, existence and uniqueness of the minimizer when the Gram matrix is invertible — the source assumes a minimum exists on geometric grounds, and this milestone supplies the hypothesis under which the assumption is a theorem. Third, the classical linear case , , where the normal system is the familiar pair of equations in the sums , , , .
The normal equations are the computational content of least squares: they turn an optimization over into one linear system, which the previous mission's methods can solve. The converse direction matters in practice because it is what licenses stopping at a stationary point, and the invertibility criterion is what tells a practitioner when the fit is determined by the data rather than under-determined by a badly chosen family of base functions.
The source differentiates formally and reads off the necessary condition; a formal proof must either differentiate rigorously or argue directly with the quadratic expansion
which also gives the converse at once. The existence-and-uniqueness milestone is where the real work is: invertibility of the Gram matrix has to be converted into positive definiteness of the quadratic form, and that into the existence of a unique global minimum.
The data are indexed by a finite type with elements and the coefficients by one with elements, so both families are nonempty; the number of data points is not assumed to exceed the number of base functions, and the degenerate cases (repeated nodes, linearly dependent base functions) are allowed except where the Gram hypothesis excludes them. The base functions are arbitrary real functions given as a family , evaluated only at the nodes . Minimality is stated globally — the coefficient vector is compared with every other coefficient vector — not as a local or stationary condition, which avoids any appeal to differentiability in the statement. The Gram matrix hypothesis is that its determinant is a unit of , i.e. nonzero. In the linear case the base functions are supplied together with the equations identifying them as the constant function and the identity, so that the statement's two displayed equations are exactly the classical normal system.
Many definite integrals cannot be evaluated in closed form — the normal distribution function is the standard example in the source — and many others are integrals of functions known only through a table of values. Numerical quadrature replaces the integrand by an interpolating polynomial on each subinterval and integrates that instead. The two classical rules obtained this way, the trapezoidal rule (linear interpolation) and Simpson's rule (quadratic interpolation), come with error terms proportional to and respectively, and it is those error terms that tell the user how fine the subdivision has to be.
This mission is the sixth in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 8, Integração Numérica.
Let be defined on and subdivide the interval into equal parts of length , with nodes .
The composite trapezoidal rule is
and the composite Simpson rule, defined when the number of subintervals is even, , is
The chapter derives, for each rule, an exact error term containing a derivative of at an unspecified intermediate point.
The goal theorem is the composite Simpson error formula, equation (8.3): if is four times continuously differentiable on and with , then there is with
The milestones are the three error formulas the derivation passes through: the simple trapezoidal error on one subinterval, its composite version , and the simple Simpson error on a pair of subintervals.
The two composite error formulas are what turn a quadrature rule into a method with an accuracy guarantee: bounding or by a constant on converts them into the bounds and , from which the number of subintervals needed for a prescribed tolerance is read off directly. The rate is also the standard illustration of why a higher-order rule is worth its extra function evaluations, and why Simpson's rule is exact for cubics despite being built from quadratic interpolation.
Both composite formulas are obtained from the per-subinterval error by summing and then invoking the intermediate value theorem to replace a sum of derivative values at unknown points by times the derivative at a single unknown point. That step needs continuity of the relevant derivative on the whole interval and a genuine intermediate-value argument, which is the part that a formal proof cannot wave through. The simple Simpson error itself is not a one-line Taylor estimate: the source integrates a remainder three times, and the standard alternative is a Peano-kernel argument.
Integrals are the interval integral of a real-valued function with respect to Lebesgue measure. Smoothness is stated as continuous differentiability of order (trapezoid) or (Simpson) on the relevant closed interval, and the derivative in the error term is the iterated derivative computed within that closed interval; on the interior this coincides with the ordinary derivative. The quadrature rules are defined for arbitrary , and subdivision count, with computed by total division, so the definitions also make sense for ; the theorems assume and a positive number of subintervals. Simpson's rule is parameterised by the half-count , so the number of subintervals is and is even by construction. The intermediate point is asserted to exist in the open interval, with no uniqueness and no relation to the subdivision.
Every numerical computation is performed in a finite arithmetic: a real number is stored with a fixed number of decimal digits, and each stored value carries an error. Before any method is analysed, a course in numerical methods has to say how large that error can be and how it grows when approximate values are combined. The answers are the two rounding bounds — for truncation and for symmetric rounding with digits — and the propagation formulas for sums, products and quotients.
This mission is the eighth in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 2, Erros.
Every nonzero real can be written in normalized decimal form with retained digits,
where is the decimal exponent of and its normalized mantissa.
Truncated rounding keeps , discarding the tail; the error is .
Symmetric rounding keeps when and when ; this is the familiar school rule of rounding the -st digit up when it is at least .
If approximates and approximates , the absolute errors are and , and the chapter computes the error of the four arithmetic operations in terms of them.
The goal theorem is Proposição 2.4.3: with symmetric rounding to digits, the relative error of a stored positive number satisfies
The milestones are the companion bound for truncated rounding, (Proposição 2.4.2), and the propagation identities of §2.5.1 for the sum and difference, for the product and for the quotient.
These bounds are the unit of account for every later error analysis: the machine epsilon of a -digit decimal arithmetic is exactly the constant appearing in the goal, and the factor two between truncation and symmetric rounding is the reason the latter is the default. The propagation identities explain the two classical failure modes of floating-point computation — cancellation in a difference of nearly equal numbers, where the absolute errors survive while the result shrinks, and the amplification of a relative error by division by a small number.
The difficulty is entirely in the normalization. The bounds follow from two facts about the decimal decomposition — that the discarded part is at most one unit in the last retained place, and that the retained part is at least — and both have to be derived from the definition of the decimal exponent through the floor function and the logarithm, including the boundary case where is an exact power of ten and the case where symmetric rounding carries into a new leading digit. The propagation statements, by contrast, are algebraic identities.
The decimal exponent is defined as , and the two roundings are defined by scaling by , applying the floor function (with an added in the symmetric case, so that halves round up) and scaling back. This is a total definition for every real number; the theorems are stated for and , which is the situation the source describes, and no claim is made about negative arguments or about .
Two points of deviation should be checked by the auditor. First, the source states both bounds with a strict inequality; for symmetric rounding equality is attained when the discarded tail is exactly one half unit in the last place, so the formal statement uses a non-strict inequality, while the truncation bound remains strict. Second, the propagation formulas for the product and the quotient are stated here as exact identities: the source's versions drop the second-order term and the higher terms of a geometric series, which is a legitimate approximation but not an equality.
In 1982 Yoshio Koide, searching for an empirical formula for the Cabibbo angle, noticed that the three charged-lepton masses satisfy
With the present-day values MeV, MeV and MeV, the dimensionless ratio on the left over the bracket on the right equals — the value to five digits. Whether this is numerology or a shadow of flavour physics beyond the Standard Model is an open physics question; what is not open, and what this mission is about, is the exact mathematical content of the relation: which triples of nonnegative reals satisfy it, what its polynomial (square-root-free) consequences are, and what its geometric reading is.
The material formalized here is Chapter 3 ("A Mass Relation") of F. Goffinet's 2008 doctoral thesis A bottom-up approach to fermion masses (Université catholique de Louvain), which collects the algebraic and geometric properties of the relation and proposes a mixing-matrix generalization. None of the statements below depends on any physics input: they are elementary real-algebraic facts about the function defined next. The physics enters only in which numbers one plugs in.
For a family of nonnegative "masses" , not all zero, define the Koide splitting parameter
In Lean this is koideRatio, defined by exactly this quotient for m : Fin n → ℝ (with Lean's
convention that for and , so the definition is total; every statement in
the mission carries the nonnegativity and nondegeneracy hypotheses that make it meaningful).
Two further objects from the chapter are formalized alongside it.
koideCos is
the cosine written out as a
quotient of sums, and koideAngle is its .pseudoMass).Koide's relation is the statement ; the value corresponds to exact degeneracy and to maximal hierarchy.
The goal theorem is the exact solution of the relation for the third mass. For , writing and ,
This is equation (3.25) of the source, made precise: the "" branch of (3.25) is a genuine solution exactly when , and is a spurious root of the squared equation otherwise (for instance at , where the "" value is positive but fails the relation).
The milestones cover, in the source's order: the range and its two equality cases (Table 3.1); the geometric reading and the equivalence (eq. (3.5)–(3.6), Fig. 3.1); the square-root-free polynomial consequence (eq. (3.24)) and its matrix form (eq. (3.30)); the failure of the converse (eqs. (3.26)–(3.28)); the reformulation in the composite-model parametrization (eqs. (3.18)–(3.22)); the -mass prediction (eq. (3.4)); and the fact that the pseudo-mass extension (3.31)–(3.32) reduces to the original relation at .
The result itself. The goal theorem turns an empirical numerical coincidence into a complete description of its solution set: given any two masses, it says exactly which third masses are admissible, and it separates the two roots by an explicit inequality. This is what licenses the standard use of the relation as a prediction: fixing and and the normal hierarchy singles out one root, giving MeV, a number two orders of magnitude more precise than the direct measurement (milestone on eq. (3.4)). The bound with its equality cases explains why the relation can never hold for the neutrinos in a near-degenerate spectrum, and why the up-quark family sits near the opposite boundary. The square-root-free form (3.24)/(3.30) is what any Lagrangian-level model must reproduce, since square roots of masses do not appear in a mass matrix; the failure of its converse is the price paid for removing them, and the mission pins that failure down with an explicit witness.
Formalizing it. All the statements here are classical-strength real algebra, and none is
formalized in Mathlib: there is no koideRatio, no Cauchy–Schwarz-style equality analysis for the
vs. pair, and no treatment of the geometry. The mission
produces a small reusable development — the parameter, its sharp bounds with equality cases, and its
angle formulation — that any later formalization of mass-relation phenomenology can import. It also
records, machine-checked, where the source text is imprecise: the "" discussion after (3.25)
and the claim that (3.1) has exactly two solutions for the third mass.
Nothing here needs heavy machinery, and everything here needs care with square roots.
The bounds are Cauchy–Schwarz in one direction and in the other, but the equality cases are where the work is: the upper bound saturates exactly when at most one mass is nonzero, and a proof must handle the mixed terms without assuming positivity of all entries. The goal theorem is a quadratic in — with , — so the difficulty is not solving it but keeping the equivalence exact in both directions: passing from back to requires , which is precisely where the "" branch survives or dies, and the discriminant has to be recognized as a perfect square times . The obvious route of squaring the relation twice, as the source does to reach (3.24), is not reversible; a solver who squares must come back and discharge the sign conditions, and the counterexample milestone shows that the lost information is real.
Masses are real numbers, not physical quantities with units, and are indexed by Fin n (Fin 3 for
the three-generation statements); the mixing matrix in the pseudo-mass definition is complex, as in
the source. koideRatio, koideCos, koideAngle and pseudoMass are total functions and rely on
Lean's junk conventions outside their intended domain, so each statement carries its own
hypotheses — nonnegativity of every entry and the existence of a strictly positive entry — rather
than delegating them to the definitions. No statement is vacuous: every hypothesis set is satisfied
by the physical charged-lepton triple, and the degenerate configurations the quantifiers admit
(all-zero families, the family) are excluded by those hypotheses rather than by a side
condition that can never hold.
The angle statements use Real.arccos and are stated for the cosine written out as an explicit
quotient of sums, not through an inner-product-space instance; a solver is free to route the proof
through EuclideanSpace if that is convenient. The matrix milestone uses
Matrix.IsHermitian.eigenvalues for a complex Hermitian matrix and states the conclusion
as an identity in between , and
. Contributions of general- versions of the three-generation statements, and of the
equality analysis as standalone lemmas, are welcome.
High-dimensional data is often computationally expensive to work with and hard to visualize. The Johnson-Lindenstrauss lemma answers a striking question in this setting: can any finite set of points, no matter how high-dimensional the ambient space, be squeezed into a space of dimension depending only on the number of points (logarithmically) and the desired accuracy, while barely disturbing the distances between them? The answer is yes, and — remarkably — a single, data-independent random construction (a random Gaussian matrix) achieves it with positive probability for any point set. This mission formalizes the lemma and the two probabilistic results its proof is built from.
For a set of points in , a map is a -distance-preserving embedding of if for every . The book's proof constructs from a random matrix with i.i.d. standard normal () entries, and argues by the probabilistic method: for a fixed pair of points, Lemma 15.3 shows preserves their squared distance up to with probability at least , because the ratio (for the difference of the two points) is exactly a random variable, whose two-sided concentration around its mean is Lemma 15.2. A union bound over the pairs in then shows the probability that every pair is simultaneously preserved is still strictly positive — so a map with the desired property must exist, even though no single fixed matrix is exhibited.
Lemma 15.2 (Chi-squared concentration, milestone). If , then for , .
Lemma 15.3 (Gaussian random projection distortion, milestone). For , , and with i.i.d. entries,
Lemma 15.4 — the mission's goal (Johnson-Lindenstrauss). For , integer , and , any set of points in admits a map with for all .
This is one of the cleanest instances in the book of the probabilistic method: existence is
proved without exhibiting the object, by showing a random construction succeeds with positive
probability. The target dimension is independent of the ambient
dimension — the embedding works no matter how large the original feature space is, which
is exactly why the lemma has inspired random-projection methods throughout dimensionality
reduction, streaming algorithms, and compressed sensing. Prior art on the Prove2Me platform is
not faithful here: HighDimProb.Isoperimetry.johnson_lindenstrauss (Vershynin series) proves a
Johnson-Lindenstrauss-type bound, but via a uniformly-random -dimensional subspace and its
orthogonal projection, rescaled by — a genuinely different construction from this
book's explicit i.i.d.-Gaussian-matrix map , and with different (existentially
quantified, unspecified) constants rather than this book's explicit .
The two are classically known to give essentially the same qualitative guarantee, but showing
them equivalent would require an independent equivalence proof neither platform item nor this
mission undertakes; per the chunk's own brief, the Vershynin theorem is cited here only as
related work, not reused as a kind: reference item.
Not formalized here: Theorem 15.1 (the PCA solution), the chapter's other headline result.
BRIEF.md explicitly flags PCA and JL as the chapter's two independent capstones, not a
proof chain, and recommends dropping PCA if the mission focuses purely on JL. Theorem 15.1's
proof is an Eckart-Young-type Frobenius-norm optimization argument over the set of rank-
orthogonal projection matrices — sharing no definitions, hypotheses, or proof technique with
the probabilistic-method argument this mission's three items are built from. Formalizing it
would mean standing up a second, unrelated piece of mathematics (constrained matrix
optimization, singular value decomposition) from scratch for a single additional item; per the
captain brief's guidance to leave out, rather than approximate, material disproportionate to
the time budget, it is omitted. §15.2 (kernel PCA) and §15.3 (Isomap, LLE, Laplacian
eigenmaps) are likewise out of scope, per BRIEF.md's own page-range restriction — applications-
heavy manifold-learning material with no numbered result feeding Lemma 15.4's proof.
Lemma 15.2's proof is a genuine Chernoff-bound argument: apply Markov's inequality to , substitute the chi-squared distribution's own moment-generating function , and optimize the resulting bound over by calculus (the book's own choice is exactly the minimizer) — not a one-line union of tail bounds, and the same argument must be repeated (with a sign flip) for the lower tail before combining via a union bound. Lemma 15.3's proof needs the non-obvious observation that (for ) are themselves i.i.d. standard normal — a consequence of 's i.i.d. Gaussian entries and , not immediate from the definitions alone — before the sum of their squares can be recognized as exactly a variable and Lemma 15.2 applied. Lemma 15.4's own proof, while conceptually simple (a single union bound), needs the specific numerical accounting at the chosen and to conclude the success probability is strictly positive — a formalization that merely asserted "the union bound gives a positive probability" without this exact accounting would not establish the book's specific, tight constant .
SqNorm is the coordinate-wise squared Euclidean norm (∑ᵢ vᵢ²), used in place of Mathlib's
EuclideanSpace/PiLp norm typeclass machinery to keep the statements close to the book's own
concrete ℝ^N/ℝ^k-coordinate notation. IsChiSquaredMGF states the moment-generating-function
characterization of a chi-squared distribution that the proof of Lemma 15.2 itself cites
(Eq. C.25), rather than restating the book's own Definition C.7, which sits in an out-of-chapter
appendix not read for this mission; this is checked (in SELF_REVIEW.md) to be a faithful,
uniquely-determining substitute, since a real random variable's law is determined by its MGF
wherever it is finite near 0. IsIIDStandardGaussianMatrix states "i.i.d. standard normal
entries" via Mathlib's gaussianReal 0 1 (marginal law) together with iIndepFun (joint
independence). The goal theorem's target dimension k is taken as ⌈20 log(m)/ε²⌉ (Nat.ceil)
rather than the book's real-valued 20 log(m)/ε², since a map's codomain dimension must be a
natural number; this rounding only strengthens (never weakens) the existential conclusion, since
the union-bound success probability is monotonically increasing in k. No numerical constant in
any of the three items is otherwise altered from the book's own displayed form. A trivializing
formalization this mission avoids: stating Lemma 15.4 with an unspecified k = O(log m/ε²)
(an asymptotic, not an explicit constant) — per BRIEF.md's own naming of this as one of the
series' "explicit-constant" results, k's exact formula 20 log(m)/ε² (up to the ceiling
needed for well-typedness) is stated directly.
The Standard Model of particle physics assigns to each elementary fermion a vector in a representation of the compact Lie group . The pattern of hypercharges this forces on quarks and leptons looks arbitrary. Three grand unified theories from the mid 1970s explain the pattern by enlarging the symmetry group: Georgi and Glashow's theory, Georgi's theory, and the Pati-Salam model based on .
Baez and Huerta, The Algebra of Grand Unified Theories (2011), isolates the part of this story that is pure algebra: homomorphisms out of , their kernels and images, and the way the three unified groups sit inside one another. This mission formalizes that group theoretic core. It deliberately leaves out the representation theoretic half of the paper (the exterior algebra , the binary codes, the Dirac spinor representations), which is a natural follow-up mission.
Write for the group of complex numbers of modulus one, and for the complex matrices with and . The Standard Model gauge group is the product
Fix the splitting and write matrices in in the corresponding block form. The Georgi-Glashow homomorphism is
where means the scalar times the matrix . Fixing instead the splitting (colour plus lepton number), the Pati-Salam homomorphism is
Finally, forgetting the complex structure of gives a real inner product space , and every complex-linear map becomes a real-linear one. Writing each complex coordinate as a pair of real coordinates turns a complex matrix into a real matrix , built from the blocks . Under , the splitting becomes .
Concretely: a real matrix is simultaneously (i) the realification of some and (ii) block diagonal with blocks in and , if and only if for some . The image of is a copy of , which is why this is the statement of Theorem 8; the quotient itself never has to be formed.
The milestones establish, in order: that is a homomorphism into ; that its kernel is exactly , a group of order six; that its image is the subgroup of preserving the splitting; the same programme for the Pati-Salam homomorphism , whose kernel turns out to have order three; that realification is an injective homomorphism carrying into ; and the diagram chase by which Theorem 9 (p. 69) upgrades Theorem 8 from to .
The kernel computation is what makes the theory testable at the level of algebra: because is nontrivial, no representation coming from can distinguish the six elements of that kernel, so the Standard Model representation must be trivial on them — a nontrivial relation between hypercharge, isospin and colour that the observed fermions do satisfy. The intersection theorem says the Standard Model group is not merely contained in both unified theories: inside it is precisely their intersection, so the two routes to unification determine it exactly.
Formalizing this produces reusable Lean infrastructure for classical matrix groups: block decompositions of , the subgroup , and the realification homomorphism with its determinant and orthogonality properties, none of which is currently available off the shelf. The mathematics is classical and fully proved in the source; what is open here is only the formalization.
The obvious first move — " is visibly a homomorphism, so quotient by its kernel and apply the first isomorphism theorem" — settles the milestones but not the goal. The goal compares two subgroups of that are defined by different structures: one by preserving a complex structure and a volume form, the other by preserving a splitting of the real space. Showing the intersection is no larger than the image of requires knowing that a real matrix commuting with the complex structure and respecting the real splitting must respect the complex splitting, and that the determinant conditions then match up exactly; the surjectivity half needs a sixth root of the determinant of the block to exist inside .
Theorem 9 is a second, independent difficulty: and its double cover of are not available in the current Lean library, so the milestone states the diagram chase of the published proof with the covering data as hypotheses rather than constructing .
The Lean development commits to the following conventions.
fromBlocks. Likewise is indexed by .No statement is vacuous: every milestone is universally quantified over the whole group, the goal is an equivalence between two nonempty subsets of (both contain the identity), and the hypotheses of the Theorem 9 milestone are satisfied by the real data of the source.
Contributions welcome beyond the milestones: constructing and its covering map so Theorem 9 can be stated unconditionally, and the representation theoretic half of the paper (Theorems 1-7), which needs and the Dirac spinor representations.
Chapter 9 asks whether the support vector machine — a regularized empirical risk minimizer over an RKHS — is a statistically consistent estimator for regression: does as the sample size , for a suitable regularization schedule ? The chapter's main theorem (Theorem 9.1) answers yes, under an explicit polynomial rate condition on . Its proof reduces the question to bounding how far the empirical regularized solution can be from the population regularized solution, and that reduction bottoms out in a single concentration-of-measure fact: how tightly does an empirical mean of i.i.d. Hilbert-space-valued random variables concentrate around its true mean, given only a bound on one -th moment (no exponential-moment assumption at all)? That fact is Lemma 9.2, "the following lemma to bound the probability of for " — the technical core the whole chapter's consistency argument rests on, and this mission's goal.
Fix a measurable space , a distribution on , a separable Hilbert space , and a measurable . Its -th moment norm, for , is — the direct Hilbert-space analogue of an ordinary norm. The proof machinery behind concentration results of this kind is symmetrization: replacing a centered i.i.d. sum by a Rademacher-randomized sum , where a Rademacher sequence is a family of independent -valued random variables, each taking each sign with probability . Once randomized, the sum's -norms (for different ) become comparable to each other via Kahane's inequality, with a universal constant depending only on the two exponents involved — never on the sample size or the ambient Banach space.
for a universal constant depending only on , every and every . This is a genuine generalization of Chebyshev's inequality to Hilbert-space-valued means, sharp enough (via the explicit rate ) to drive Theorem 9.1's own polynomial regularization condition .
Theorem 9.1 itself (BRIEF.md's recommended goal — the full SVM-regression consistency theorem)
was not attempted this session; see STATUS.md for the reason and the fallback taken instead.
Lemma 9.2 is stated and proved once, in the Appendix's general Rademacher-sequence toolkit and this chapter, and then used directly to obtain Theorem 9.1's consistency guarantee: substituting the pointwise SVM "difference process" into Lemma 9.2 converts a purely probabilistic concentration fact into a statement about how close the empirical SVM solution's risk is to the population solution's risk, for every sample size. Because the bound depends on nothing but a single moment — no boundedness, no sub-Gaussian tail — it is what lets Theorem 9.1 avoid assuming the loss or the label distribution has any exponential tail control, which is essential for regression (where need not be bounded, unlike the classification setting of this series' earlier chapters). Symmetrization and Kahane's inequality are themselves standard, reusable tools of empirical process theory (used throughout Chapter 7's entropy-number program, excluded from this series, and Chapter 6's classification oracle inequality).
The published proof of Lemma 9.2 is a short but dense computation: Markov's inequality reduces the tail bound to bounding for the centered mean ; Theorem A.8.1 symmetrizes; for , Theorem A.8.3 (Kahane) converts the -th moment of the Rademacher sum to its second moment, which an explicit orthogonality computation (the book's Eq. (9.4), for any fixed , an immediate consequence of the Rademacher signs' independence and the Hilbert space's parallelogram identity) reduces to a sum of individual second moments; the case argues analogously with a different exponent split. None of this computation is captured by this mission's two milestones alone — they supply the two cited theorems, not the connecting algebra — so a complete proof of the goal from the milestones as stated still requires reconstructing this argument, exactly as the captain brief's milestones are meant to be (the book's own attack path, not a fully mechanized proof outline).
and (the Rademacher sequence's own probability space) are arbitrary measurable
spaces; is [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] [BorelSpace H] [SeparableSpace H] (a separable real Hilbert space with its Borel
-algebra), matching " be a separable Hilbert space" without narrowing to a concrete
space (e.g. ) the book itself does not assume. IsRademacherSequence states independence
via Mathlib's iIndepFun and the -probability- condition directly, since no ready-made
"Rademacher distribution" object exists in this Mathlib revision (checked by search). is substituted algebraically rather than introducing a separate conjugate
exponent , since pins down uniquely — not a change of content. In Theorem
A.8.3, "for all Banach spaces " quantifies over E : Type (the Type 0 universe) rather than
every universe Type*, a disclosed minor restriction with no effect on this mission's own use of
the theorem (with instantiated to a Type* Hilbert space that is, in every actual
application, itself at the Type level).
A trivializing formalization here would drop the "independent" half of IsRademacherSequence
(leaving only the marginal -probability- condition, true even for perfectly correlated
signs) or drop the "i.i.d." qualifier on in Theorem A.8.1 (both symmetrization
and Kahane's inequality are false, or at least unproven by the book's own argument, without
independence) — both are ruled out here by stating iIndepFun explicitly rather than only the
marginal distribution conditions.
IsRademacherSequence is reusable beyond this mission: any future formalization of Chapter 7's
entropy-number/Rademacher-complexity program, or of Chapter 6's oracle inequality's own use of
Rademacher averages, would restate it locally (per Hard Rule 9) from the same book definition.
Contributions completing the three sorrys are welcome; Theorem 9.1 itself remains a natural,
substantially larger follow-up mission built on top of this one's two milestones together with
the RKHS/regularized-risk-minimizer apparatus already available in this series' 04-representer
mission (restated locally, per Hard Rule 9).
Chapters III and IV formalize what it means for one random variable to be "more spread out" or "larger and more spread out" than another. Chapter VIII asks a different kind of question: if the number of terms in a sum of i.i.d. random variables is itself random, and one count is larger than another in one of these orders, does the resulting random sum inherit the comparison? This mission formalizes the chapter's own answer — Theorem 8.A.13 — a clean, self-contained closure result that needs only the icx/icv/cx orders from Chunks 03/04 (restated locally) and one nonnegative-integer-valued index, without the heavier parametric-family apparatus (SICX, SICV, SIL, and the stochastic-convexity-of-a-family notions) that occupies most of the rest of the chapter.
This chapter restates the univariate increasing convex, increasing concave and convex orders (Chunks 04 and 03's own subjects) locally, since drafts cannot import another mission's definitions: for random variables , [] if for every increasing convex [concave] for which the expectations exist, and if the same holds for every convex (dropping "increasing"). Theorem 8.A.13 applies these same three orders to nonnegative-integer-valued random variables — a special case of the real-valued order (after the coercion ), not a separate discrete order, per this chapter's own pitfall 1.
Let be i.i.d. nonnegative random variables, independent of the two nonnegative discrete random variables and . Then
Comparing the number of terms propagates to a comparison of the resulting random sums. This is
"an application of these notions in establishing a stochastic inequality," in the book's own
words right before the theorem — the formal content behind Example 8.A.2's claim that a
homogeneous Poisson process is SIL, via the semigroup property of Example 8.A.7 (neither a
numbered theorem, so neither is drafted as a milestone here — cited as background only, per
CAPTAIN_BRIEF.md rule 5).
The book's proof defines for an increasing convex [concave] and observes (via the unnumbered Example 8.A.4) that is itself increasing and convex [concave] in ; the icx/icv order on then transfers directly to vs. , giving part (a). Part (b) follows from part (a) together with the equal-means fact under (Theorem 4.A.35, a Chapter 4 result not restated in this mission).
Random sums are the natural model for aggregate risk, total service time, or total demand when the number of contributing terms is itself uncertain — the number of claims in an insurance period, the number of customers served, the number of jobs in a batch. Theorem 8.A.13 is the tool that lets an analyst reduce a comparison of two such aggregates to a comparison of the (often much simpler) counting processes that generate them, without having to reason about the joint distribution of the sums directly. It is also the concrete instance, stripped of the rest of the chapter's parametric-family machinery, of a pattern that recurs throughout the book: an order on an index set (here, the count vs. ) transferring through a monotone/convex construction (here, summation) to an order on the resulting random variables — the same shape Chunk 06's Theorem 6.B.16(b) and Chunk 07's Theorem 7.A.9 each illustrate in their own settings.
No platform prior art exists: GET /theorems?q=random+sum, q=compound+distribution,
q=Poisson+process, and q=renewal return nothing usable (the last returns only
MarkovMixing/CLT-adjacent hits, not classical renewal or compound-sum results, confirmed at
triage time and re-checked this session). This mission restates the icx/icv/cx orders and their
random-sum closure as a self-contained result, independently drafted since drafts cannot import
Chunks 03/04's Lean.
The chief formalization risk is treating as a separate "discrete" order rather than
the same real-valued order applied to -valued random variables after coercion — this
chapter's own pitfall 1. A second risk is drafting as a fixed-length sum with
substituted in afterward, rather than a genuine random (randomly-stopped) sum where is
itself random and independent of the sequence — this chapter's own pitfall 2; the
independence hypothesis has to be carried explicitly, not left as an unstated convention. A third
risk, common to every bracketed theorem in this series, is conflating the icx and icv cases of
part (a) into a single Or-joined statement rather than two clearly distinguished conjuncts —
this chapter's own pitfall 3.
A different kind of risk, specific to this chapter, is scope creep into the parametric-family
apparatus (SI, SCX, SICX, SIL, and the "family indexed by " definitions) that
occupies most of Chapter 8: as BRIEF.md's own Setup note observes, that apparatus is heavier
than the rest of the book (a family, a parameter set, and several bracketed cases per
definition), and a trivializing risk specific to it — flagged in this chapter's pitfall 4 — is a
family predicate that is vacuously true for a degenerate parametrization (e.g. a
singleton). This mission avoids that risk entirely by choosing the one clean, self-contained
closure theorem in the chapter that needs none of it.
The icx/icv/cx orders are restated locally (IcxOrder, IcvOrder, ConvexOrder, univariate,
real-valued), exactly matching Chunks 04 and 03's own shapes, since drafts cannot import another
mission's definitions. are nonnegative-integer-valued; the orders are
applied to them via the coercion fun ω => (M ω : ℝ) (resp. N), matching pitfall 1 exactly —
no separate discrete-order predicate is introduced. The i.i.d. sequence is drafted as
Y : ℕ → Ω → ℝ (indexing Y 0, Y 1, … for the book's Y_1, Y_2, …, a one-step reindexing noted
explicitly rather than left implicit), with iIndepFun Y μ for mutual independence and
IdentDistrib (Y j) (Y k) μ μ for every j, k for identical distribution, plus 0 ≤ᵐ[μ] Y k for
nonnegativity. The random sum itself is ∑ k ∈ Finset.range (M ω), Y k ω — a genuine
randomly-stopped sum, per pitfall 2 — and independence of from jointly is
IndepFun (fun ω => (M ω, N ω)) (fun ω k => Y k ω) μ, treating the whole sequence as one
ℕ → ℝ-valued random element, stated as an explicit hypothesis rather than an implicit
convention. The theorem's three conjuncts (icx, icv, cx) mirror the book's own single Theorem
8.A.13, whose part (a) bundles the icx/icv brackets and whose part (b) states the cx case
separately, per pitfall 3.
A trivializing formalization this mission rules out: substituting M into a fixed-length
Finset.range n sum after the fact (erasing the random-stopping structure that makes this a
random-sum theorem at all) rather than genuinely summing over Finset.range (M ω), and treating
M ≤icx N as anything other than the same real-valued order Chunks 03/04 define, applied after
coercion. This mission draws on no platform prior art (searches for "random sum", "compound
distribution", "Poisson process" and "renewal" as of 2026-09-18 return nothing usable). Unlike
every other chapter in this series so far, this mission has no milestone theorems: every
other numbered result near the goal in this chapter needs the parametric-family apparatus this
mission deliberately avoids, and the un-numbered facts the goal's own proof cites (Example
8.A.4's potential-function monotonicity, Example 8.A.7's semigroup property) cannot be milestones
per CAPTAIN_BRIEF.md rule 5 — see STATUS.md for the full accounting.
StochasticOrders.Convex) and Chunk 04 (StochasticOrders.MonotoneConvex),
for the univariate convex and increasing convex/concave orders this chapter restates locally.Compressed sensing asks a question that looks impossible at first: can a signal be reconstructed exactly from far fewer than linear measurements , ? Classical linear algebra says no — an underdetermined system has infinitely many solutions. But if is known in advance to be sparse (most of its coordinates are zero), the extra structure makes recovery possible: solving the convex program that minimizes the norm of a candidate solution, subject to matching the measurements, recovers exactly, for a measurement matrix with a suitable geometric property. This idea, developed by Candès, Romberg, Tao and Donoho in the mid-2000s, underlies modern MRI acceleration, single-pixel cameras, and sparse signal processing generally.
The chapter isolates the exact geometric property a measurement matrix needs — the restricted isometry property (RIP) — and proves, purely by linear algebra with no probability involved, that RIP alone is sufficient for exact recovery by minimization. (A companion result, outside this mission, shows random sub-gaussian matrices satisfy RIP with high probability once is large enough, which is what makes the deterministic guarantee here practically useful; this mission formalizes the deterministic half.)
For a vector indexed by a finite set, write for its number of non-zero coordinates (so is -sparse if ), for its norm, and for its Euclidean norm.
An matrix satisfies the restricted isometry property (RIP) with parameters if
i.e. acts as an approximate isometry on every -sparse vector — equivalently (the book's own Exercise 10.5.9), the singular values of every column-submatrix of lie in .
Given a matrix and measurements for an unknown sparse , the exact-recovery program is
precisely: suppose satisfies RIP with parameters where ; then for every -sparse , every that is feasible () and -optimal among feasible vectors satisfies . No constant here is hard-coded beyond the book's own explicit threshold — the weakest stable form of the claim.
RIP isolates exactly the geometric mechanism that makes -minimization work for sparse recovery: once a matrix is known to satisfy it, exact recovery is a deterministic, provable consequence with no appeal to randomness, no failure probability, and no measurement-count formula to verify beyond the RIP parameters themselves. This clean separation — a purely geometric sufficient condition (RIP), proved separately (in the book's Theorem 10.5.11, outside this mission) to hold with high probability for random sub-gaussian matrices — is the template compressed sensing theory follows throughout: geometric/deterministic guarantee first, probabilistic verification that random constructions meet it second. The theorem is one of the two standard routes (with the direct probabilistic argument of Theorem 10.5.1) to the chapter's central claim that measurements suffice to recover any -sparse signal in — exponentially fewer than the measurements a naive linear-algebraic argument would need.
The result itself, and the RIP framework, are classical and well-established (Candès-Tao 2005). This mission formalizes the deterministic linear-algebra core of the argument — the statement infrastructure (RIP, sparsity, the exact-recovery program stated as an explicit optimization problem) and the goal theorem — for a solver to close with a proof.
The natural first idea for showing is to try to bound the recovery error directly using (which vanishes, since both and are feasible) together with RIP applied to itself — but need not be sparse at all: it is the difference of two sparse-ish vectors and can have full support. The actual argument decomposes 's support into blocks by descending magnitude (the support of , then the largest remaining coordinates , then the next , and so on), applies RIP only to the leading block (which genuinely has bounded sparsity ), and separately bounds the contribution of every later block using the fact that is -optimal (so , the "cone constraint"): each later block's norm is controlled by the mass of the previous block divided by its size. This is a genuinely multi-step argument combining a purely geometric fact (RIP on one bounded-sparsity block) with a purely combinatorial one (the magnitude-sorted decomposition), and the "obvious" idea of applying RIP to as a whole does not typecheck, since RIP says nothing about vectors with more than non-zero entries.
Vectors are plain functions ι → ℝ on a finite index type, not EuclideanSpace ℝ ι: the latter's
fixed norm instance cannot also host the norm the program's objective needs, so
both norms (L2Norm, L1Norm) are defined directly by their defining sums on the same underlying
type. Sparsity (Sparsity) takes a real-valued threshold s : ℝ, matching that the RIP parameter
used by the goal theorem is a real number even at integer base sparsity. A solution
"of the program" is formalized as an explicit argmin membership — feasibility
(A.mulVec xhat = A.mulVec x) conjoined with optimality over the exact feasible set
(∀ x', A.mulVec x' = A.mulVec x → l1Norm xhat ≤ l1Norm x') — never "there exists an estimator
such that", the trivialization risk this chapter's own triage brief flags explicitly (shared with
Chapter 3's Max-Cut): an existential reading would prove a different, strictly weaker statement.
The conclusion is stated for every such , not one witness, matching that RIP forces
uniqueness.
This mission covers Theorem 10.5.10 only, as the sole item; the probabilistic goal Theorem 10.5.1
(exact recovery for random sub-gaussian measurement matrices, which needs Theorem 10.5.10 together
with a separate probabilistic argument, Theorem 10.5.11, that random matrices satisfy RIP), and the
Lasso guarantee (Theorem 10.6.1), are both left out for lack of session time: each would need a
fresh probabilistic apparatus (independent isotropic sub-gaussian random rows, a failure-probability
bound) built from scratch in this chapter's own sub-namespace, with no reusable published
definition from an earlier chunk. L2Norm, L1Norm, Sparsity and RIP are reusable by any
later chapter or mission needing sparse vectors or the restricted isometry property; solvers'
contributions are welcome on completing the proof of Theorem 10.5.10 itself (the magnitude-sorted
support decomposition sketched under Difficulty above), and, beyond this mission's current scope,
on Theorem 10.5.11 and Theorem 10.5.1.
A cooperative game with side payments models a set of economic agents who can form coalitions and split the proceeds. The central question is stability: is there a way to split the total payoff among all the players so that no subset of them would do better by breaking away and acting on its own? The set of such stable splits is the core, introduced by Gillies [1959] and studied extensively since (Shapley [1971], Shapley [1953]). Sharkey [1982c] surveys the core's role in the economics of natural monopoly, where "no coalition wants to secede" is exactly the condition that a cost-sharing scheme is defensible against any subgroup of customers.
The core of an arbitrary cooperative game can be empty — there may be no split that satisfies every coalition simultaneously — and even when nonempty it can be hard to exhibit a point in it, since it is cut out by linear inequalities. Shapley [1971] identified a large and economically natural class, the convex games (characteristic functions that are supermodular in the coalition), for which the core is always nonempty, and for which an explicit family of core points — one per ordering of the players — can be written down directly. This mission formalizes Shapley's theorem and its later sharpening: this book's central result of Chapter 5, together with a genuine converse (Moulin [1990], sharpening an observation of Sharkey [1982a]) and comparative-statics theorem (Topkis [1987]) showing how these core points move as the underlying economics changes.
Fix a finite set of players . A characteristic function assigns a real number to every coalition , with ; is the net return a coalition could earn on its own. The pair is a cooperative game, and throughout this chapter is assumed superadditive: for disjoint . A payoff vector is feasible if , and acceptable if for every coalition . The core is the set of payoff vectors that are both:
is a convex game if is supermodular on the Boolean lattice of coalitions: for all . ("Convex" is the game-theory literature's name for this supermodularity property; it has no relation to convexity of sets or of real functions, a collision the book itself flags.) Equivalently, by Theorem 2.6.1/2.6.4, a game is convex exactly when the marginal value of any player to any coalition not containing increases as grows — the more players already committed to a project, the more valuable one more player is to it.
Given a permutation of , let . The greedy algorithm builds the payoff vector by paying each player its marginal contribution when added in the order : . The Shapley value pays player the average of over all permutations , equivalently .
A core is large if every acceptable payoff vector is dominated, coordinatewise, by one in the core; a subgame restricts to subsets of ; a core is totally large if the core of every subgame is large.
The weakest stable statement here is already the union of these three claims: nonemptiness of the core (b) is a formal consequence of (a) for any single permutation, and (c) is a genuinely separate fact about the average of the 's, not implied by (a) and (b) alone.
Theorem 5.2.1 is the reason convex games are the tractable case of cooperative game theory: it turns an existence question about linear inequalities into an explicit construction (any ordering of the players gives a point in the core), and it identifies the Shapley value — an axiomatically motivated but a priori only feasible payoff rule — as one that always respects every coalition's participation constraint on this class. Theorem 5.2.6 shows this is not an accident of the sufficient condition: total largeness of the core is a genuine characterization of convexity, so "does every subgame's core dominate every acceptable vector" is an equivalent, purely core-theoretic way to test convexity. Theorem 5.2.7 gives the comparative statics that make convex games useful in applied models (Chapter 5's later sections build monopoly, surplus sharing, and procurement games on exactly this apparatus): as a game's characteristic function improves in a complementary way with some parameter (a price, a technology level, a capacity), every player's greedy payoff and Shapley value improve monotonically, with no separate argument needed for each application.
Formalizing this mission produces, for the first time on the platform, machine-checked statements of the core, convex games, the greedy algorithm and the Shapley value — definitions that later missions in this series's own polyhedral-structure sections, and any future cooperative-game-theory mission, can reuse rather than re-derive. All three results already have a complete proof in the literature; this mission's remaining work is formalizing that known argument, not any open mathematics.
The routine first idea — check acceptability for the greedy vector one subset at a time using only the definition of supermodularity — does not directly work: Theorem 5.2.1(a)'s proof needs to compare a subset against the initial coalitions built by the particular permutation , splitting by the first and last time one of its elements appears in 's order and applying supermodularity along the resulting chain, not a single inequality. Theorem 5.2.6's converse direction is the harder half: showing a totally large core forces supermodularity requires constructing an auxiliary characteristic function from an arbitrary acceptable vector and showing is itself supermodular (via Theorem 2.6.4 and Theorem 2.7.6, results from the earlier monotone-comparative-statics chapter this mission depends on) before the argument closes.
Players are modeled as Fin n and a characteristic function as f : Finset (Fin n) → ℝ; a
payoff vector is y : Fin n → ℝ, and the core's feasibility and acceptability conditions are
stated with respect to Finset.univ (the whole player set) or a coalition U : Finset (Fin n)
for a subgame, never approximated by a finite sample of coalitions or by feasibility alone — the
acceptability condition genuinely quantifies over every subset. The Shapley value's coefficient
is the exact rational weight S.card.factorial * (n - S.card - 1).factorial / n.factorial cast
to ℝ, not a placeholder constant. The greedy algorithm's InitialCoalition σ j uses Lean's
0-indexed Equiv.Perm (Fin n) throughout, with the book's 1-indexed absorbed into
the definition rather than into the index j, so the definition and the goal read the same j
consistently. Theorem 5.2.7(c), which needs Theorem 5.2.4's convex-combination-of-extreme-points
machinery beyond this section, is out of scope for this mission.
A trivializing formalization would state acceptability only on singleton coalitions, or would
let n = 0/an empty player set stand in for the general case; neither is used here — every
Core/IsLargeCore statement quantifies over arbitrary subsets, and none of the theorems
restrict n.
This mission reuses Supermodularity.Monotonicity.SupermodularOn and
Supermodularity.Monotonicity.IncreasingDifferencesOn from this series's chunk II
(02-monotonicity) rather than restating supermodularity or increasing differences for
coalitions from scratch. InitialCoalition, Core, GreedyPayoff, IsConvexGame,
IsLargeCore, IsTotallyLargeCore and ShapleyValue are new to this mission and reusable by
any later mission on cooperative games, polymatroids, or the polyhedral structure of the core
(Section 5.2.3 of this chapter). Contributions completing the sorrys — Theorem 5.2.1(a)'s
chain-splitting argument, Theorem 5.2.6's auxiliary-function construction, and Theorem
5.2.7(a,b)'s direct comparison — are all welcome.
Many of the central questions of high-dimensional statistics reduce to bounding the expected supremum of a stochastic process: the maximum correlation of noise with a family of candidate signals, the operator norm of a random matrix, the uniform deviation of an empirical process from its mean. Whenever the index set of the process is infinite or exponentially large, a naive union bound over "all" indices is either vacuous or requires re-deriving a tail bound from scratch for every new problem. Chaining is the general-purpose technique that removes this need: it bounds the expected supremum of a process purely in terms of the geometry of its index set, measured by how many balls of a given radius are needed to cover it. The classical form of this bound is due to Dudley (1967), building on ideas that trace to Kolmogorov; the exposition here follows Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 5.
Fix an index set and a collection of zero-mean random variables . Say this collection is a sub-Gaussian process with respect to a (pseudo)metric on (Definition 5.16) if
This single condition covers, as special cases, the canonical Gaussian process for a standard Gaussian vector (with the Euclidean metric) and the Rademacher process built from i.i.d. Rademacher signs.
A -cover of with respect to a metric is a finite set such that every lies within -distance of some ; the -covering number is the size of the smallest such cover (Definition 5.1). The quantity is the metric entropy of at scale . Writing for the diameter of , the -truncated Dudley entropy integral is
The bound holds for every zero-mean sub-Gaussian process, with no further structure on beyond its metric entropy — this is what makes it a general-purpose tool rather than a bound tailored to one model.
The same conclusion with replaced by the cruder single-scale term , under the extra technical hypothesis . This is the one-step precursor whose refinement — iterating the discretization over a geometric sequence of scales instead of applying it once — is exactly what chaining improves.
A general comparison principle for pairs of centered Gaussian random vectors whose pairwise covariances are ordered coordinatewise and tested against a function with matching sign conditions on its mixed second partial derivatives: . This is the source, by specializing and the covariance-ordering sets, of both Slepian's inequality and the Sudakov–Fernique comparison, the two workhorse tools of Gaussian process theory used elsewhere in the chapter to obtain sharper, Gaussian-specific bounds than the sub-Gaussian chaining bound above.
Dudley's bound is the single most-used tool for controlling suprema of stochastic processes in high-dimensional statistics and empirical process theory: Gaussian complexity bounds for convex bodies, operator-norm bounds for random matrices, and uniform laws of large numbers for function classes are all obtained by computing a covering-number bound for the relevant index set and substituting it into Theorem 5.22 (see, for instance, Examples 5.18–5.21 later in the same chapter, and Chapters 13–14 of the book). Its significance is exactly its generality: it converts a purely geometric quantity — how "big" a set is under a metric — into a probabilistic bound, uniformly over every sub-Gaussian process on that set.
Formalizing it. The mathematical proof (interpolation-free, based on chaining and repeated
union bounds) is well understood and not itself in question; what this mission produces is a
faithful Lean statement of the theorem, its immediate one-step precursor, and the general Gaussian
comparison principle that underlies the chapter's complementary (Gaussian-specific) results, each
against Mathlib's own measure-theoretic and Gaussian-process infrastructure. All three theorems are
currently stated as open goals (:= by sorry); no claim is made here that they are already
formalized elsewhere on the platform (a fresh prior-art search for "Dudley," "chaining," "Slepian,"
"Sudakov," and "Gaussian comparison" returned no faithful matches).
The naive approach — apply Proposition 5.17's one-step discretization once, at whatever scale seems best — cannot see improvement past the cruder scaling of the metric entropy at a single resolution. The chaining argument that proves Theorem 5.22 instead telescopes the supremum across a geometric ladder of covers at scales , paying for each scale's approximation with a union bound over its own (much smaller, for a small ) covering number, and only then summing the resulting terms into an integral. The difficulty is not any single step of this argument — each step is an elementary sub-Gaussian tail bound — but bookkeeping the composition correctly: the recursive "best approximation at level of the best approximation at level " chain (Eq. (5.47)) must be built explicitly, and the telescoping sum of union bounds, each over a set that itself depends on the level , is what converts into an integral only in the limit as the covers refine to itself.
The index set is formalized as a nonempty Fintype, rather than the book's general totally
bounded metric space: this keeps every covering number, diameter, and supremum in this mission a
genuine maximum over a finite, nonempty family (realized via ⨆/sInf over finite index types),
rather than requiring the full apparatus of totally bounded infinite metric spaces to state the
covering-number definition (Definition 5.1) faithfully without risking a vacuous or ill-defined
infimum. This is a genuine narrowing of the book's stated generality, disclosed here rather than
left implicit — the underlying mathematics of the proof does not depend on finiteness, but a
faithful formalization of a general totally bounded space's covering number was judged out of
scope for this mission's budget.
The constant in the goal theorem is kept exactly as stated; the book's own remark that "there
is no particular significance to the constant 32, which could be improved with a more careful
analysis" is not license to substitute a sharper constant, since doing so would no longer match
what this particular proof establishes. Expectations are Bochner integrals against an explicit
probability measure Prob, with integrability required as an explicit hypothesis in the
sub-Gaussian process definition (SubGaussianProcess) rather than left implicit, since Mathlib's
Bochner integral silently returns for a non-integrable function — a trivializing formalization
this mission's definitions and hypotheses rule out.
Theorem 5.25's "centered Gaussian random vector" is formalized using Mathlib's own
ProbabilityTheory.HasGaussianLaw predicate (a genuine multivariate Gaussian law, not merely
Gaussian marginals) together with an explicit coordinatewise mean-zero hypothesis, and its mixed
second partial derivative condition is formalized via iteratedFDeriv ℝ 2 F applied to the
relevant pair of standard basis vectors, keeping the sign pattern over the disjoint index sets
and exact rather than collapsing it to a global convexity assumption on .
Out of scope for this mission: Sudakov's minoration (the complementary lower bound on the expected supremum of a genuinely Gaussian process, Theorem 5.30, misidentified as "Theorem 5.36" in this mission's planning brief — the correct Sudakov minoration statement is Theorem 5.30, p. 148; Theorem 5.36 is instead a tail-bound generalization of Dudley's bound to -Orlicz processes) and the Slepian/Sudakov–Fernique corollaries of Theorem 5.25 (Corollary 5.26, Theorem 5.27) — both natural follow-on work for a later contribution, once the Gaussian comparison principle formalized here is in place.
A Gaussian process is a family of jointly Gaussian real random variables indexed by an arbitrary set — not necessarily time. The canonical example is for ranging over a subset and a standard Gaussian vector in ; this single family already encodes questions as varied as the operator norm of a random matrix, the size of a random projection, and the metric complexity of a convex body. In every one of these applications the object of interest reduces to the same quantity: , the expected supremum of the process.
Bounding directly is hard — computing it exactly is possible only in special cases, such as the reflection principle for Brownian motion. Slepian's inequality (David Slepian, 1962) sidesteps this by comparison: if a second Gaussian process has matching variances and at-least-as-large pairwise increments as , then 's supremum stochastically dominates 's. This turns a hard direct estimate into a search for a simpler comparison process — the technique that Sudakov and Fernique later sharpened by dropping the equal-variance hypothesis (Theorem 7.2.11), and that Sudakov used to derive a purely geometric lower bound on from the covering numbers of (Theorem 7.4.1, Sudakov's minoration inequality). Together these results are the entry point to the theory of Gaussian width and generic chaining that occupies the rest of the book (Chapters 7–9, 11), and they underlie sharp bounds on random matrices (Section 7.3), random projections (Chapter 9), and high-dimensional geometry more broadly (Adler and Taylor, Random Fields and Geometry, Springer, 2007; Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014).
Fix a probability space . A random process indexed by a set is a family of real random variables on . It is a Gaussian process if every finite linear combination ( finite, ) is a (possibly degenerate) normal random variable — equivalently, every finite marginal is a multivariate Gaussian vector. A process is mean zero if for every .
For a mean zero process, the increments always define a (pseudo)metric on — the canonical metric — turning the otherwise unstructured index set into a metric space. For a metric space and $\varepsilon
0N(T,d,\varepsilon)N\subseteq TT\varepsilonN\varepsilonN(T,d,\varepsilon) := \infty$ if no finite net exists.
Because need not be countable, need not be a measurable function of . Following the book's own convention, every quantity built from this supremum — and — is instead defined through the process's finite-dimensional marginals: as the supremum, over finite nonempty , of (respectively ). This sidesteps the measurability question entirely, at the cost of the quantity possibly being .
Let and be mean zero Gaussian processes with and for all . Then for every ,
and consequently .
Under only the increment hypothesis (no equal-variance hypothesis),
This is the weaker-hypothesis, strictly more applicable form: it is what Sudakov's minoration inequality and the sharp Gaussian random matrix bound of Section 7.3 both invoke.
Let be a mean zero Gaussian process with canonical metric . For every at which is finite,
for an absolute constant . This is the weakest, most stable form of the bound: it names no numerical value for , so it survives any later sharpening of the constant.
The vector-indexed special case of Theorem 7.2.1 ( finite), proved first by Gaussian interpolation and then extended to the general index set.
The results themselves. Slepian's inequality is the founding comparison theorem for Gaussian processes; Sudakov-Fernique's inequality is its practically indispensable generalization, used routinely to bound suprema of Gaussian processes without needing to track variances explicitly. Sudakov's minoration inequality is the first bridge from the probability of a Gaussian process to the metric geometry of its index set, complementing Dudley's upper bound (Chapter 8) and together giving matching bounds — up to a logarithmic factor, and exactly in many cases of interest — on purely from the covering numbers of . Downstream, this machinery gives the sharp bound on Gaussian random matrices (Section 7.3), underlies the Gaussian width used throughout convex geometry and compressed sensing (Chapters 9, 11), and bounds the covering numbers of polytopes and other convex sets (Corollary 7.4.4).
Formalizing it. All three inequalities are proved by the book (Gaussian interpolation and integration by parts for Slepian/Sudakov-Fernique; a direct application of Sudakov-Fernique to a well-chosen comparison process for Sudakov's minoration), so this mission's work is formalizing the statements faithfully and precisely — including the finite-marginal convention needed to make and meaningful for an uncountable index set without begging the underlying measurability question. The Gaussian interpolation technique itself (Lemmas 7.2.3, 7.2.5, 7.2.7) is not part of this mission's formalization scope; it is the proof method for the milestones and belongs to solvers closing them.
The obvious first idea — bound by controlling each separately, e.g. via a union bound over a net — throws away exactly the structure Slepian-type comparisons exploit: the joint Gaussianity across , not marginal tail behavior at each fixed . A union bound needs a net and a modulus of continuity to begin with; Slepian's and Sudakov-Fernique's inequalities need neither — they compare two processes directly through their covariance structure, which is what makes the technique (Gaussian interpolation: continuously deform the covariance of one process into the other's, and track how a smooth, nearly-indicator functional behaves along the path) work with no assumption on beyond the two hypotheses stated. The genuine difficulty is the smooth-interpolation argument itself — showing that is monotone in for the right choice of test function — which is exactly the part left as a milestone for solvers to formalize, not sketched here per the mission format's own rule against proof ideas.
(ProcessESup) is valued in EReal, not ℝ: the finite-marginal supremum a
real-valued definition would silently default to the junk value when the set of finite-marginal
expectations is unbounded above — exactly the case the book itself records as (Exercise 7.4.2, a non-relatively-compact index set). P\{\sup_{t\in T}X_t\ge\tau\}
(ProcessTailProb) stays real-valued, since it is always bounded in and so carries no
such risk. Both are defined through finite nonempty subsets of , per the book's own footnote
to Section 7.2; no separability, continuity, or countability assumption is placed on itself.
Gaussianity is Mathlib's ProbabilityTheory.IsGaussianProcess — every finite restriction of the
process has a Gaussian law — which is definitionally the book's Definition 7.1.10 ("every finite
linear combination is Gaussian"); mean-zero is stated as an explicit hypothesis alongside it.
Integrability of every quantity appearing under an expectation is not stated as a separate
hypothesis: Fernique's theorem (already in Mathlib for general Gaussian measures) guarantees a
Gaussian process has finite moments of every order, exactly as the book takes for granted.
Sudakov's minoration inequality (Theorem 7.4.1) is formalized for the case the book's own proof
actually covers — finite, taken as a hypothesis = (N : ℕ) rather than as a
case split inside the conclusion — since the book itself defers the infinite-covering-number case
to a separate, unproved exercise (7.4.2). This keeps fully general (still possibly
uncountable) at every fixed where the net is finite, which rules out a trivializing
reading of the theorem: nothing here forces itself to be finite or countable, only the
covering number at the scale in play, which is the book's own hypothesis.
Definitions reusable beyond this mission: ProcessESup, ProcessTailProb, CanonicalMetric,
and CoveringNumber are exactly the substrate Chapters 8 ("Dudley's Integral Inequality"), 9
("The Matrix Deviation Inequality"), and 11 ("Dvoretzky-Milman's Theorem") need for Gaussian
width and generic chaining; per this series' plan those missions restate them locally (drafts
cannot import another draft's definitions), using this chunk's forms as the faithful reference.
Contributions closing the Gaussian-interpolation machinery (Lemmas 7.2.3–7.2.8) as a reusable
definitions layer, beyond what any one milestone needs, are welcome.
A gas of interacting particles is described exactly by coordinates, and by no useful equation. Kinetic theory replaces that description by a single scalar field, the one-particle distribution function , whose evolution is governed by the Boltzmann equation. The price is the collision operator: the true Boltzmann collision integral is quadratic and five-dimensional, and almost every statement about it is hard. The BGK operator (Bhatnagar, Gross and Krook, 1954) replaces it by simple relaxation of towards the local Maxwellian at a fixed rate . It is the standard first model for rarefied gas dynamics, the basis of lattice-Boltzmann numerics, and the model in which the structural features of kinetic theory — conserved moments, an -theorem, hydrodynamic closure — can be exhibited in closed form.
This mission formalizes the BGK material as it is posed in Question 1 of the Oxford MMathPhys Kinetic Theory examination paper of Hilary Term 2019: the conservation of the hydrodynamic moments by the collision operator, the sign of the entropy production together with the characterisation of equality, the slab-geometry reduction to a closed two-field system, and the vanishing of the resulting stress and heat-flux corrections at equilibrium.
Velocities and positions range over . A distribution function is a map on velocity space (at a fixed position and time), assumed everywhere positive, integrable, and with finite second velocity moment. Particles have unit mass and the Boltzmann constant is set to . Its moments are
the mass density, the bulk velocity and the temperature. The Maxwellian with parameters is
and the local Maxwellian of is : the Maxwellian carrying the same three moments as . The BGK collision operator with relaxation time is
and the Boltzmann equation with this operator is
In the slab geometry of parts (c)-(d) of the source, , , with , and is independent of and ; the reduced fields are and .
This is part (b) of the source question, including the answer to "under what conditions does equality hold". It is stated for every admissible and every ; it fixes no rate and no constant, so it is not invalidated by sharper quantitative versions.
The three conservation identities say that the BGK operator, however crude as a model of binary collisions, respects the exact conservation laws of the gas: they are what makes the moment hierarchy of the BGK equation reduce to the Euler equations at leading order. The entropy inequality is the model's -theorem: it forces the entropy to be non-decreasing under collisions and singles out the Maxwellians as the only collisional equilibria, which is the statement that fixes the direction of time in the model. The slab reduction of part (c) is the standard device by which a three-dimensional kinetic problem is reduced to a pair of one-dimensional kinetic equations, used throughout computational rarefied gas dynamics; part (d) identifies exactly which moments of the reduced fields carry the non-equilibrium stress and heat flux.
Formalizing this material requires building the moment calculus of Gaussians on against Lebesgue measure — normalisation, first and central second moments, and the partial integration over two of the three velocity components — none of which exists in Mathlib in a form adapted to kinetic theory. The mathematics is classical and the proofs are known; the work is in the analysis bookkeeping: integrability of moments, dominated convergence, and the a.e. equality case of a strict pointwise inequality.
The obvious computation for the -theorem — expand and integrate term by term — does not by itself give a sign: has no sign, and neither does . The argument needs the conservation identities as an input, because they are what allows , which is a quadratic polynomial in , to be subtracted for free. Only then is the integrand pointwise of one sign. Formally, the obstacle is that none of the pieces of the integrand is separately integrable in general: the statements are formulated with the integrability of the entropy-production integrand as an explicit hypothesis, and any splitting of it must be justified.
The equality case adds a second difficulty. Vanishing of the integral of a non-negative integrable function gives vanishing only almost everywhere, so the conclusion is an a.e. identity , and the strictness of for must be used pointwise.
Velocity space is EuclideanSpace ℝ (Fin 3) with its Lebesgue (volume) measure, and
integrals are Bochner integrals; vector-valued moments are integrals of
EuclideanSpace-valued functions. Distribution functions are total functions
with no measurability packaged into the type, so every statement
carries its own integrability hypotheses; admissibility (positivity everywhere, integrability,
finite second moment) is bundled in a predicate. The Maxwellian prefactor is written with a
real power , so is required wherever it appears. The relaxation
time satisfies .
Two traps are worth naming. First, in Lean the integral of a non-integrable function is by convention, so an entropy inequality stated without an integrability hypothesis would be satisfiable for trivial reasons; the goal therefore assumes the entropy-production integrand is integrable, and states the equality case as an iff, which is not satisfiable by a degenerate reading. Second, the local Maxwellian is defined from the moments of itself, not from externally supplied parameters, so none of the conservation statements can be discharged by choosing convenient parameters.
The slab-geometry part of the mission is developed in its own definition file, with the
perpendicular velocity in EuclideanSpace ℝ (Fin 2) and the reduced fields as functions
. The Gaussian moment lemmas produced here are reusable for any
Maxwellian-based kinetic model; contributions that add Mathlib-level lemmas on Gaussian moments
in , rather than ad-hoc computations, are especially welcome.
The rise and fall of the ocean surface under the gravitational pull of the moon and the sun is the oldest quantitative problem in physical oceanography, and it is still a working one: satellite altimetry can only see ocean circulation after the tidal signal has been removed, and the removal is done with a numerical solution of Laplace's tidal equations (LTE) constrained by tide-gauge and altimeter data (Le Provost et al., J. Geophys. Res. 99 (1994) 24777). The same equations carry the global tidal energy budget: an estimate of where the roughly 3.5 TW of tidal energy is dissipated — shallow-sea bottom drag versus conversion into internal tides over deep-ocean topography — is obtained by integrating the energy identity of these equations against observed elevation data (Egbert and Ray, Nature 405 (2000) 775).
The material formalized here is M. Hendershott, Lecture 3: Solutions to Laplace's Tidal Equations (Woods Hole Oceanographic Institution, Geophysical Fluid Dynamics Program lecture notes, pp. 34–44), notes taken by V. Birman and E. Williams Frajka. The lecture states the separable normal-mode solutions of the stratified problem, the solid Earth tide and the Love number decomposition, models of dissipation, coastal boundary conditions, and finally the energy equation of the tides, both ignoring and including the yielding of the solid Earth.
Write and for the two components of the depth-independent horizontal velocity, for the free-surface elevation, for the solid Earth tide (the elastic displacement of the crust under the tidal load), and for the observed, geocentric tide. The ocean has resting depth , constant density , gravity , and constant Coriolis parameter . The astronomical forcing enters through the tide generating potential and the dissipation through a force per unit area .
Laplace's tidal equations are the two momentum equations
together with the continuity equation, which in the presence of the solid Earth tide reads
For a stratified ocean the same system arises mode by mode after separation of variables, with replaced by the equivalent depth of the -th mode and the vertical structure solving , where is the buoyancy frequency.
with
This is a pointwise identity, valid at every for every solution of the equations above, with variable depth and no assumption on the form of the dissipation.
The milestone list covers the corresponding identity with the solid Earth tide ignored (eqs. (29)–(30)), the two normal-mode facts of §2 — the vertical structure equation with the equivalent depth (eq. (4)) and the nonrotating barotropic plane wave with its dispersion relation (§2.1) — and the two averaging statements of §6: that the period mean of the time derivative of a periodic energy density vanishes (eq. (31)) and the resulting period-averaged balance (eq. (32)).
The energy identity is what converts elevation observations into a dissipation estimate: averaged over a tidal period and integrated over a basin with no flux through its boundary, the flux divergence drops out and the work done by the tide generating potential equals the dissipation, so is computable from alone. Every term in that chain — which terms are exact, which vanish only on average, which require the Love numbers to be real — is a hypothesis that a formal statement has to carry explicitly, and the lecture is explicit that the identity holds "provided that the Love numbers are real", i.e. provided the solid Earth tide is dissipation-free.
Formalizing this material produces a reusable model of a rotating shallow-water system with forcing, dissipation and an elastic bottom boundary, together with the calculus lemmas needed to differentiate products of fields of several variables. Nothing here is an open problem: the results are classical, and the contribution is a machine-checked derivation from a precisely stated model, including the bookkeeping that textbook derivations compress.
The obstacle is not depth of argument but faithfulness of the model. The derivation multiplies the two momentum equations by and , the continuity equation by , and adds; every step needs a product rule for a field of three variables, and the Coriolis terms must cancel exactly rather than approximately. Two places in the source require care before they can be formalized: equation (29) prints the surface term with coefficient , and the printed in §6.1 has signs that do not follow from the printed ; the identities are true with and respectively. The potential energy (37) also differs from by a term independent of time, which is invisible in and therefore harmless. A naive formalization that copies the printed formulas without checking these will state something false.
Fields are real-valued functions of , and ; partial derivatives are Lean's
one-dimensional deriv applied slot-wise, and differentiability is imposed as an explicit
hypothesis in each variable separately, rather than through Fréchet derivatives. Depth is a
function that does not depend on time, and positivity of and is assumed
where the momentum equations are divided by . The equations themselves are packaged
as a structure with three fields, one per equation, so that a solution is an explicit witness
rather than an assumption schema; this rules out a vacuous reading, since constant fields with
zero forcing satisfy the structure. The barotropic plane wave of §2.1 is stated with
complex-valued and and the physical normalization , , and is
an equivalence: the wave solves the system exactly when . The
vertical mode statement uses the rigid-lid conditions ; the lecture's
free-surface condition at is satisfied by the sine modes only
in the limit of small equivalent depth, and is not claimed. Period averaging is formalized as
of an interval integral at a fixed horizontal position, with periodicity and
continuity of the relevant time derivative as hypotheses.
Contributions extending this mission are welcome in three directions: the derivation of the equations from the linearized Euler equations of Lecture 2, the solid Earth tide of §3 with the Love number decomposition (17)–(20), and the basin-integrated form of the energy budget (33), which needs a divergence theorem for the flux term.
Graphene is a single sheet of carbon atoms arranged on a honeycomb lattice. Its electrons are described, to a first approximation that is quantitatively good near the Fermi level, by a nearest-neighbour tight-binding model: a hopping amplitude between adjacent carbon sites and nothing else. What makes the model worth studying is that this two-parameter lattice problem produces a band structure with two bands that touch at isolated points of the Brillouin zone and disperse linearly around them, so that low-energy electrons obey a two-dimensional massless Dirac equation rather than a Schrödinger equation with an effective mass. That observation organises the standard review literature on graphene (Castro Neto, Guinea, Peres, Novoselov, Geim, The electronic properties of graphene, Rev. Mod. Phys. 81 (2009) 109), and goes back to Wallace's 1947 band theory of graphite.
This mission formalises a self-contained set of lecture notes that carries the computation out in full: F. Utermohlen, Tight-Binding Model for Graphene (2018). It is the two-dimensional, two-sublattice counterpart of the tight-binding chain: the chain gives a single band with no band touching, while the honeycomb lattice, whose unit cell contains two inequivalent sites, produces a Bloch matrix and the conical band touchings targeted here.
Fix a carbon–carbon distance and a hopping amplitude . The honeycomb lattice is two interpenetrating triangular lattices, the and sublattices, with lattice unit vectors , and nearest-neighbour vectors
each joining an site to one of its three neighbours. The corners of the first Brillouin zone — the Dirac points — are
Fourier transforming the second-quantised hopping Hamiltonian gives with and the Bloch Hamiltonian
where is called the structure factor. The mission takes this matrix as its starting point: the second-quantised derivation (Eqs. 2–8 of the notes) is not formalised, and together with is defined by the displayed formulas. The band energies are the eigenvalues of , and is the quantity the statements are written in terms of. The Fermi velocity is (units with ).
with , and . The three clauses say, in order, that really are the eigenvalues of the Bloch Hamiltonian, that the two bands touch at the Brillouin-zone corner , and that they disperse linearly and isotropically around it. The goal deliberately asserts the shape of the low-energy dispersion — a first-order expansion, with no quantitative remainder — so it is not invalidated by sharper error estimates.
The milestone list follows the notes equation by equation: the closed form of (Eq. 11), the characteristic polynomial of (Eq. 9), the two explicit forms of the dispersion (Eqs. 12 and 13–14), the Pauli-matrix form of (Eq. 18), the vanishing of at and , the first-order expansions at both Dirac points (Eqs. 22–23 and 30), the spectrum of the linearised Hamiltonians (Eq. 32), and the gap opened by a mass term (Eqs. 33–34).
The three clauses of the goal are what turn a lattice hopping problem into the massless-Dirac-fermion picture used throughout graphene physics: they are the precise sense in which "graphene has Dirac cones at and with Fermi velocity ". Downstream, the same objects carry the valley structure — the two expansions are complex conjugates of one another — and the mass milestone shows how a sublattice-asymmetric on-site potential (boron nitride rather than graphene) opens a gap , the standard model of a gapped Dirac material.
The mathematics is classical and the physics literature regards it as settled; what this mission adds is a machine-checked development in which the honeycomb geometry, the Bloch matrix, its spectrum and the Dirac-point expansions are reusable definitions and lemmas rather than a computation redone by hand. No part of the development is claimed to be new mathematics.
The obstacles are in the analysis, not the algebra. The first two clauses of the goal are a trigonometric identity and a determinant. The third is a genuine differentiability statement, and the naive route — expand , cancel the zeroth-order terms, read off the linear term — has to be carried out uniformly in the direction of ; moreover the quantity being expanded is , a modulus, which is not differentiable at a zero of . The linear behaviour of survives only because the modulus of a function with a nonzero complex-linear differential at a zero is asymptotically the modulus of that differential, and the elementary estimate is what lets the error be transported through the modulus. Note also that itself is not differentiable at — the cone has a vertex there — so no Taylor theorem applies to directly.
Wave vectors and lattice vectors are pairs of reals, . Because that product type carries the sup norm, the Euclidean length is introduced as a separate definition and is the one used in every statement; the little-o statements are taken with respect to the neighbourhood filter of the origin, for which the two norms agree up to constants. is a finite sum over a three-element index set, is a concrete complex matrix, and "eigenvalues" are always expressed through the characteristic polynomial rather than through an eigenvector predicate. Lattice constant and hopping amplitude are real parameters; the standing hypotheses of the goal are exactly and , and several milestones need less. Units are , so .
Two things the formalization deliberately does not do: it does not derive the Bloch Hamiltonian from the second-quantised hopping Hamiltonian (Eqs. 2–8), which would require a Fock-space development, and it does not claim that and are the only zeros of . No statement is vacuous: every hypothesis is satisfiable (take ), and the goal's third clause is a nontrivial asymptotic rather than an identity.
Contributions welcome beyond the milestone list: the second-quantised derivation, the identification of the full zero set of modulo the reciprocal lattice, eigenvector-level (pseudospin) statements, the density of states, and the extension to next-nearest-neighbour hopping.
Which workers end up at which firms, and does higher quality always land at the more productive employer? This is the question of assortative matching: whether an efficient assignment pairs the best workers with the best firms, the second-best with the second-best, and so on down the line. The question has a long history in labor economics. Becker [1973] showed, for the simplest case of two-sided homogeneous firms and a single worker characteristic, that profit maximization under complementarity forces exactly this kind of sorting. Kremer [1993] extended the analysis to firms with many workers of a single type, under a specific Cobb–Douglas production function. What was missing was a general theory: one that covers firms hiring several types of workers simultaneously, firms that differ in efficiency, and labor markets of any degree of tightness, while still deriving sorting from a single primitive economic condition rather than from functional-form assumptions.
Topkis's Chapter 3, §3.2 supplies exactly that theory, as an application of the book's central tool — supermodularity — to the assignment problem. The condition that drives every result in this mission is a single complementarity hypothesis on the firms' profit functions: no concavity, no differentiability, no specific functional form. That a purely order-theoretic hypothesis pins down the qualitative shape of an optimal assignment is the mission's central content, and the platform currently has no lattice-theoretic treatment of matching at all — its one matching result formalizes Gale–Shapley two-sided stable matching by preference, an entirely different mechanism (see Formalization scope below).
Fix worker types, indexed , each with a lattice of available worker qualities, and firms, indexed . A matching assigns to each firm a vector of qualities — one worker of each type hired by that firm (a firm that hires no worker of some type, or several, is accommodated by adjoining an artificial "no worker" element to , or by splitting a type into several, as Topkis notes on p. 97; the model itself needs neither device). If firm hires the quality vector , it earns profit ; the dependence on reflects differences among firms such as technology or management efficiency. A matching is optimal if it maximizes the total profit over every matching.
A matching is increasing if — a single chain, firm by firm, under the pointwise order on — and ordered if every two of its firm-assignments are comparable (a weaker, only pairwise, condition). The labor market is loose if each firm's hiring problem can be solved by unconstrained maximization over the whole quality space , without regard to the other firms' decisions, and tight if the supply of each worker type is exactly , so a feasible matching must assign every available worker to exactly one firm.
The hypothesis common to every result is that is supermodular in the joint variable on : for every and , . By Theorem 2.6.1 of Chapter 2, this is equivalent to having increasing differences both between any two worker types' qualities (complementarity among the worker types) and between each worker type's quality and the firm index (complementarity between quality and firm efficiency).
Existence of an increasing optimal matching, with no loose-market hypothesis — the general case, and the harder of this mission's results to formalize, since its proof is a non-constructive lexicographic-minimization argument rather than a direct reduction to per-firm optimization.
The result gives a clean, hypothesis-light account of assortative matching: sorting by quality is a structural consequence of complementarity in the profit function, not an artifact of a particular production technology. It generalizes Becker's and Kremer's special cases to arbitrarily many worker types, heterogeneous firms, and any degree of labor-market tightness, identifying supermodularity in as the single condition doing all the work. Formalizing it contributes a genuinely new object to the platform: a firm-quality matching model driven by lattice-theoretic complementarity rather than by preference orderings, together with the four distinct comparative-statics conclusions (loose-market optimality, general existence, orderedness, increasingness) that the strength of the supermodularity hypothesis buys. No prior formalized proof of any of these four theorems exists on the platform or, to the author's knowledge, in any other proof assistant library.
The obvious approach — prove the goal (Theorem 3.2.3) by reducing to the loose case, firm by firm, as in Theorem 3.2.1 — does not work, because the loose-market argument crucially uses that each firm's decision does not constrain any other's; without that, a locally optimal per-firm choice need not combine into a globally optimal matching. Topkis's actual proof is non-constructive: among all optimal matchings, pick one that lexicographically minimizes the "latest" failure of the increasing property (a well-ordering argument over the finite but unbounded set of optimal matchings, not an inequality chase), then show that if it still fails to be increasing, exchanging the two offending firms' assignments via strictly increases total profit — contradicting optimality by supermodularity. Formalizing this requires setting up the lexicographic minimization (over pairs ordered by then ) as a well-founded induction, not merely restating the inequality (3.2.3) at the end of the proof.
Worker-type quality spaces are modeled as finite, nonempty lattices (Lattice,
Fintype, Nonempty); firms are indexed by Fin m. A matching is Fin m → ∀ i, X i with no
constraint beyond membership — the general matching problem (3.2.1) imposes no injectivity or
supply constraint on its own, a modeling choice Topkis's own text supports (p. 96: the
"" representation of a matching "may not distinguish between
all distinct assignments of workers to firms if the qualities of different workers of any given
type are not all distinct, but that ambiguity is inconsequential"). Tightness is instead
formalized as an explicit feasibility predicate (a bijection between firms and the available
workers of each type) supplied as a hypothesis exactly where a tight-market theorem needs it,
never folded into the general optimality predicate.
A trivializing formalization to avoid: collapsing Theorem 3.2.4's "ordered" conclusion and
Theorem 3.2.5's "increasing" conclusion into the same statement, or conflating their two
distinct supermodularity hypotheses (joint-non-strict-plus-per-firm-strict versus jointly
strict) — the mission's four milestones are kept as four genuinely different claims with their
own hypotheses, not variations proved once and restated. AGT.stable_matching_exists
(Gale–Shapley) is not reused here, despite the shared word "matching": it produces a
two-sided, preference-based stable matching with no notion of aggregate profit, a mechanism
unrelated to this mission's profit-maximizing, supermodularity-driven assignment.
Reused from earlier missions in this series: the induced set ordering InducedSetOrder
(mission I) and joint supermodularity SupermodularOn (mission II), both published platform
definitions. Contributions most welcome on the goal theorem's lexicographic-minimization
argument, the mission's hardest step.