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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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 particle in a ring is the simplest quantum system in which a boundary condition of purely topological origin — single-valuedness of the wave function on a circle — forces the energy spectrum to be discrete. A free particle of mass confined to a circle of radius has no potential well and no classical turning points; nothing about the differential equation alone selects a discrete set of energies. Quantization arises solely from the requirement that the solution close up after one revolution. For that reason the model is the standard first illustration of angular-momentum quantization in quantum mechanics courses, and the azimuthal factor of the hydrogen-atom eigenfunctions is exactly the eigenfunction family derived here.
The model is also used quantitatively. In organic chemistry the free-electron model treats the electrons of an aromatic ring, such as benzene, as particles on a circular waveguide; filling all levels up to index takes electrons once electron spin is counted, which is the counting behind Hückel's rule for aromatic stability. In rotational spectroscopy the same spectrum approximates the rotational levels of a rigid rotor.
This mission formalizes the model as presented in the Wikipedia article Particle in a ring (revision 1318339663): the eigenfunctions, the eigenenergies, the normalization and orthogonality relations, the two-fold degeneracy of every level with , the count of states up to level , and — as the goal — the statement that the admissible energies are exactly the quantized values.
Write for the angular coordinate on the ring of radius . A state is a function of alone. Since the Laplacian on the ring is , the time-independent Schrödinger equation becomes
and single-valuedness on the circle is imposed as the periodic boundary condition
A stationary state of energy is a function that is twice continuously differentiable on , satisfies the periodic boundary condition, and solves the displayed equation. Normalization is over one period,
For each integer put
Here are real parameters, taken positive where positivity matters.
For and :
The right-to-left direction is the construction of ; the left-to-right direction is the quantization statement proper, and it must rule out every that is not of this form, including all and every positive whose associated wave number is not an integer.
The milestones cover, in order: the periodicity of ; its normalization; the identity ; the resulting fact that is a stationary state of energy ; the orthonormality relation ; the two-fold degeneracy with linearly independent for ; and the level count, that exactly integers satisfy .
The result itself fixes the spectrum of the free Hamiltonian on the circle, with the degeneracy pattern and the level count that underlies the electron count of Hückel's rule. The orthonormality relation is the statement that the eigenfunctions form the classical Fourier system on ; the assertion that every ring wave function is a superposition of the is precisely the Fourier expansion theorem for periodic functions.
Formalizing it produces a small, reusable Lean development: a periodic-boundary-condition predicate, a second-order eigenvalue problem stated through iteratedDeriv, and a complete spectral determination for that problem. Mathlib supplies the Fourier exponentials on AddCircle and their orthonormality in , but the pointwise, , real-eigenvalue formulation used here is not present as such, and no formalization of this spectral statement currently exists on the platform. The supporting milestones are routine analysis; the goal theorem is where the content sits.
The physics is standard textbook material and is not in question; what this mission adds is the machine-checked proof.
The naive argument — "write the general solution as with , then impose periodicity" — assumes the classification of solutions of , which must itself be established over for a , not a priori analytic, function. Three regimes must be treated separately and none may be skipped: , where periodicity forces and hence ; , where the solutions are affine in and periodicity kills the linear term, leaving ; and , where the solutions are real exponentials and periodicity forces , contradicting nontriviality. The third case is where a careless proof quietly assumes what it should prove.
Wave functions are total functions of the angular variable, not functions on a quotient or on AddCircle; periodicity is an explicit hypothesis. Smoothness is ContDiff ℝ 2, and the second derivative is iteratedDeriv 2, so the Schrödinger equation is a pointwise identity in , holding at every real . The energy ranges over , not : the mission does not address non-self-adjoint or complex-eigenvalue variants. The parameters are explicit real arguments rather than fixed constants, and positivity is assumed exactly where it is needed; note that under Lean's convention for division by zero, degenerate parameter values make both sides of the equation vanish, which is why the goal theorem carries . Integrals are interval integrals over with respect to Lebesgue measure.
The goal cannot be satisfied vacuously: the right-hand side of the equivalence is satisfiable (take ), and the left-hand side explicitly requires a with at some point, so the trivial solution is excluded. Contributions that build reusable infrastructure — a classification of solutions of over , or a bridge between this pointwise formulation and Mathlib's AddCircle Fourier basis — are welcome, and would serve any later mission on one-dimensional periodic Schrödinger operators.
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.
Two-stage stochastic programs with recourse are already hard to optimize when the recourse problem is a linear program: Chapters 4–6 of this series show how the L-shaped method exploits the recourse function's convexity and polyhedrality to converge finitely by cutting planes. Adding integrality restrictions destroys both properties. Birge and Louveaux open Chapter 7 by naming the consequence directly: "properties of stochastic integer programs are scarce," duality is lost, and the recourse value for even a single first-stage point may itself require solving an integer program from scratch, with no warm start available across scenarios (Birge & Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer 2011, p. 290).
Section 7.2 isolates the one structural feature that still buys finite convergence: first-stage variables restricted to . Laporte and Louveaux's Integer L-shaped method (1993) exploits this by combining a branch-and-bound search over the finitely many binary first-stage points with a new family of optimality cuts, valid wherever a finite lower bound on the recourse value is available. This mission formalizes that method's specification and its finite-convergence guarantee, together with the two propositions its proof rests on.
A stochastic integer program (SIP) extends a two-stage stochastic linear program with fixed
recourse (Chapter 3's Recourse.Instance: first-stage data , fixed recourse matrix ,
and scenarios of with probabilities ) by two further restrictions:
where restricts the first stage and restricts the recourse variable — typically requiring
integrality of . Section 7.2's standing hypothesis narrows further: every coordinate of
is binary. Write for the resulting recourse value (a possibly-infinite expectation, by
the same convention as the continuous case) and for the value of the continuous
relaxation, obtained by dropping the restriction and keeping only — exactly the
recourse value Chapter 3's Recourse.Instance already computes.
The method needs one further hypothesis, Assumption 2: a finite lower bound with , not required to be tight. For a subset of the first-stage index set, write , and let be the binary point with for , otherwise — measures how far a binary point is from matching exactly, reaching its maximum only at .
Any L-shaped optimality cut valid for the continuous relaxation's value remains valid for the true, integrality-restricted recourse value, since pointwise.
is a valid lower bound on for every binary first-stage-feasible , given a binary feasible point with true recourse value and a lower bound satisfying Assumption 2.
Under Assumption 2, the Integer L-shaped method — the branch-and-bound search over binary first-stage points, tightened at each iteration by a fresh cut of the Proposition 3 form — finitely converges to an optimal solution of an SIP with relatively complete recourse and binary first-stage variables, when one exists. "Finitely" is quantified explicitly: a bound of on the number of iterations, the number of distinct binary first-stage points.
Proposition 4 is the chapter's payoff: it turns "solve an SIP with binary first-stage variables" from an open-ended search into a procedure with a certified stopping point, at the cost of one additional hypothesis (a computable lower bound ) that is often easy to obtain by relaxing the second-stage integrality restriction, as the book's Example 1 illustrates directly. Propositions 1 and 3 are the two soundness facts the method's cuts rest on: Proposition 1 lets an implementation reuse the continuous L-shaped method's own optimality cuts as valid (if weaker) constraints, and Proposition 3 supplies the chapter's genuinely new cut, tailored to the binary structure and strong enough by itself to guarantee termination.
Formalizing this mission fixes, machine-checkably, the exact hypotheses under which the method is correct — in particular, that "binary" is load-bearing (the finiteness bound is literally ) and that "relatively complete recourse" cannot be dropped, since it is what keeps the recourse value from becoming at a feasible point. No result here has, to the mission's knowledge, been formalized elsewhere; the propositions and the method's specification are drafted fresh.
The recourse function is neither convex nor polyhedral once is integer-restricted, so the argument cannot follow the continuous L-shaped method's proof line for line — that proof leans on 's convexity to certify a cut from finitely many bases. Proposition 3's cut instead argues purely combinatorially: for every binary , with equality forcing , so the cut's right-hand side collapses to the true value exactly there and falls to at most everywhere else — a fact about the finitely many binary points of , not about 's analytic structure. The natural first idea, adapting a continuous L-shaped cut by simply restricting its domain to binary , fails: nothing forces such a cut to be tight at the current iterate, so it need not exclude a revisited point, and finite convergence (the content Proposition 4 actually asserts, not just "an optimum exists") would be lost.
The mission represents first-stage points as Fin n1 → ℝ with a Binary predicate
(∀ i, x i = 0 ∨ x i = 1) rather than a Fin n1 → Bool type, so that the master problem's
feasible region and its binary-restricted subset share one ambient space, matching how the book
moves between and its binary points. The second-stage restriction is left an arbitrary
Set (Fin n2 → ℝ); taking it to be all of recovers exactly Chapter 3's continuous
recourse value, without a second definition. Flagged (moderator review, 2026-09-19):
Proposition 1's own is the book's -based continuous/LP-relaxation of
(Eq. (1.3)-(1.4)), which can retain bounds imposes beyond integrality — the book's own
worked example on the same page gives binary , so , not
alone. This mission's prop1_cuts_valid_for_sip uses the dropped- relaxation
(only ) rather than , which coincides with the book's only when
is itself an unbounded integrality restriction; the theorem is a narrower result than the
book's Proposition 1 whenever carries additional structure, though it remains true as
stated because the dropped- value is unconditionally the book's -based
, which is itself — see the item's own Formalization Note for the full
argument. The existential lower bound of Assumption 2 is kept a bare existentially-quantified real, never
sharpened to a formula, matching the book's own "no requirement is made that the bound should
be tight."
The Integer L-shaped method's branch-and-bound bookkeeping (Steps 0, 1, 3, 4: pendant-node list management, bound-based fathoming, and branching on a violated integrality restriction) is abstracted into a direct optimization over the binary first-stage feasible set at each iteration, since Proposition 3's cut is proved valid there without appeal to any specific branching order — the same level of abstraction the Chapter 5 mission uses for the continuous L-shaped method's own master-problem bookkeeping. What is retained explicitly is the part the finiteness bound actually depends on: Step 5's recourse-value computation and Step 6's binary choice between fathoming and adding a fresh cut, modeled as a state machine whose state is the finite set of binary points already excluded by a cut. A formalization that dropped this state machine — asserting only "if Assumption 2 and relatively complete recourse hold, an optimal solution exists" — would trivialize the proposition's actual content, the finite bound on the number of steps; this mission keeps that bound as an explicit, checkable part of the goal statement.
Definitions reused from earlier missions in this series: StochasticProg.Recourse.Instance
(Chapter 3) for the underlying two-stage recourse data and its continuous-relaxation value.
Contributions welcome on strengthening Proposition 4's proof to also derive Proposition 3 as a
lemma, and on formalizing the improved cuts of Propositions 5–7 (out of scope here, left for a
possible follow-up mission).
Sequential planning problems — inventory replenishment, hydro-thermal power scheduling, asset-liability management — routinely span more than two decision epochs, with information about the future revealed gradually as each period unfolds. A two-stage recourse model (decide now, observe once, recourse once) is too coarse for these: it either collapses the whole horizon into a single "wait and see" observation or forces an ad-hoc rolling-horizon heuristic with no optimality guarantee. The multistage stochastic program is the natural model that keeps the full sequence of decisions and observations, and Benders (L-shaped) decomposition is the workhorse algorithm the field has used to solve it since Van Slyke and Wets [1969] introduced it for the two-stage case. Ho and Manne [1974] and Glassey [1973] first proposed nested decomposition for deterministic multistage models; Louveaux [1980] extended it to multistage quadratic stochastic programs, and Birge [1985] gave the linear multistage generalization this mission formalizes, later implemented at scale by Pereira and Pinto [1985] and Gassmann [1990] and still the basis of production stochastic-programming solvers today.
A multistage stochastic linear program unfolds over stages . At each stage, uncertainty resolves into one of finitely many realizations, so the whole process of realizations forms a scenario tree: a single scenario at (the root), branching into finitely many scenarios at , each of those again branching at , and so on. Write for a scenario (a tree node) and for its ancestor, the scenario at stage that descends from; is the set of scenario 's descendants at the next stage. Each scenario at stage carries its own decision vector , bounded above (, coordinatewise), subject to the linear constraint
where the recourse matrix depends only on the stage (fixed recourse) while the transition matrix and right-hand side may vary scenario by scenario. Stacking every scenario's constraint over the whole tree gives the deterministic equivalent linear program, minimizing the probability-weighted total cost over this feasible region — problem (3.4.1) in the source.
The nested L-shaped method solves (3.4.1) by decomposition rather than forming this (typically enormous) single LP directly. Each scenario owns a small subproblem, , that looks exactly like a two-stage L-shaped subproblem: it has 's own constraint and bound, plus a running set of feasibility cuts and optimality cuts accumulated so far, plus, if has descendants, an approximation variable standing in for the (unknown, convex, piecewise-linear) future cost of everything downstream of . Solving either finds it infeasible — in which case a feasibility cut is derived from the infeasibility certificate and sent up to 's parent — or finds an optimal dual solution, whose aggregate over all of 's children (weighted by conditional probability) becomes a candidate optimality cut for . The method sweeps forward and backward across the tree, feasibility and optimality cuts accumulating at every internal node, until no node's subproblem produces a fresh cut.
This is the chapter's only numbered result and the weakest faithful statement of "the method works": it makes no claim about the number of iterations beyond finiteness, and none about which sequencing protocol (forward-forward-back, or any other) is used to choose which subproblem to solve next.
Finite convergence is what separates an algorithm from a heuristic: without it, nothing rules out an infinite sequence of ever-finer cuts that never certifies optimality or infeasibility. Birge's 1985 result is the reason nested Benders decomposition can be used as an exact method rather than an approximation, and every later refinement (bunching, sifting, multicuts, parallel implementations, all mentioned in the source text) modifies how cuts are generated or which subproblem is solved next without touching this finiteness guarantee — they are all still instances of the same cut-generation mechanism this mission formalizes. The two-stage case (Chapter 5, Theorem 2) is the special case of this theorem; the mission's tree-indexed state and transition relation are written to specialize to the two-stage development directly when the tree has one branching level, though the two developments are not connected by an import (see Formalization scope). No machine-checked proof of either the two-stage or multistage case appears to exist prior to this series; formalizing it here produces the first Lean statement of the mechanism nested Benders decomposition rests on.
The obvious first idea — prove finiteness by bounding the total number of cuts a node can ever receive, the way a flat scenario set bounds the two-stage method's cut count by its number of LP bases — fails because a node's own subproblem is not a fixed-size LP: every cut recorded at node becomes a new row of 's own constraint set, so the "number of possible bases" at keeps changing as the algorithm runs, and the bound at depends recursively on how many cuts 's own children could ever produce. The book's actual argument (p. 290) is a genuine induction on the stage index, from the last stage backward: assume the bound holds for every node at stage , then combinatorially bound the finite number of extended bases at stage that this permits, then take the finite union over every possible extension size. This mission's Lean development commits to a scope that keeps a node's basis a fixed-size object (see below) rather than re-deriving that combinatorial bound.
Every stage shares one decision dimension and one constraint dimension (Fin n,
Fin m); the book allows these to vary by stage but nothing in Theorem 1's statement
needs that generality. Scenario probabilities p are the unconditional probability of
reaching a node, required strictly positive and summing to within each stage
(Instance.hp_pos, Instance.hp_sum); the aggregation formulas use only the ratio
for a child of , which reads the same whether p is unconditional or
conditional, so this is a normalization choice, not a substantive restriction. The upper
bound ub is ℝ-valued rather than extended-real-valued, which is Theorem 1's own
hypothesis ("finite upper bounds"), not an added convention.
The one deliberate scope-narrowing choice, flagged here and in MODERATION_NOTES.md, and
strengthened in this revision after moderator review (2026-09-19,
CHANGES_REQUESTED.md #2): a node 's dual witness (Basis, FeasBasis) is read off
's original constraint (1.2) alone — the fixed-size recourse matrix
— never off the extended constraint set (1.2)-(1.4). The gap this
leaves is broader than "accumulated cuts are ignored": 's own continuation variable
— present in (1.1)'s objective, and fixed to from Step 0 onward, not
merely absent until cuts accumulate — has no representation at all in Basis,
multiplier, basisValue, or the optimality-cut coefficients optCutCoeffs computes
for a parent of . Consequently, whenever a child used in an optimality cut is
itself an interior node ( has children of its own, i.e. ,
which happens for every tree), the mechanized cut coefficients are not the
book's of Eq. (1.1) and are not the printed algorithm's
mechanism at that node — they are the dual of 's plain sub-LP alone, omitting 's
own contribution to the recourse value entirely, not only the portion contributed by
's accumulated cuts. This gap is inert exactly when every child aggregated in a cut is
a last-stage node (, where the mechanism coincides with the already-published
two-stage sibling 05-two-stage-methods) and active for every deeper cut, which is most
of what a general Tree H actually exercises. Concretely: as mechanized, the
optimality-cut half of Step (Bases.optCutCoeffs, Step.opt) is faithful to the
printed nested L-shaped method's cut-generation step only when every child it
aggregates over is a last-stage node; for an interior child it computes a value that
omits that child's own term rather than the book's recursive one. The
feasibility-cut half (Bases.feasCutCoeffs, Step.feas) has no such gap — feasibility
does not involve at any stage — and the tree/instance layer (Tree, Instance)
and the goal theorem's own outer shape are unaffected: thm1_finite_convergence's
statement (existence of a finite, Step-reachable state that is infeasible-certified
or globally optimal) is not weakened, but the reader should treat the mechanized Step
relation itself, for H ≥ 3, as a documented variant of Steps 1-2 rather than a literal
transcription of them at every node — see STATUS.md's Revision section for the
moderator exchange this responds to. Reworking cut generation to consume each child's own
current witness directly, so that an interior child's continuation
value is no longer dropped, is left to a future revision; it is a materially larger
change (the child's local optimum is then piecewise-linear rather than linear in its own
parent's decision, so the duality argument needs a genuinely different — not merely
extended — basis notion) than this session's time budget allows. This keeps every basis
type a fixed-size Fin m → Fin n object, exactly as in the two-stage method, and keeps
the algorithm's finite-step bound an explicit, provable cardinality
(|Node × FeasBasis| + |Node → Basis|) rather than the book's own implicit,
recursively-defined one. The trivializing formalization this scope choice must not fall
into — declaring victory by proving the plain two-stage case is what convergence
"reduces to" without ever quantifying over the tree — is avoided because every definition
and the goal statement itself are stated for a general Tree H with unrestricted
branching, not merely ; what is disclosed above is a gap in how faithfully Step
models the book's own cut-generation mechanism at depth, not a restriction of the
statement to .
Reusable beyond this mission: Def_StochasticProg_Multistage_Tree (the finite scenario
tree) is a natural building block for 07-integer-programs (an integer restriction of
the same two-stage subproblem) and 10-multistage-approximations (multistage Jensen
bounds, which need the same tree). Contributions welcome: a faithful account of the
extended-basis induction sketched above, and a formalization of Chapter 6, Theorem 3
(finite termination of the quadratic nested decomposition of Section 6.2), which this
mission omits for time (see STATUS.md).
A micron-sized bead suspended in water and held by an optical tweezer is one of the standard measuring instruments of soft-matter physics: the bead's fluctuating position reports on the viscosity of the medium, on the stiffness of the trap, and on the forces exerted by whatever is attached to the bead. The quantity that experiments record is the mean-squared displacement (MSD) of the bead. Interpreting such data rests on a single classical calculation, due to Paul Langevin (1908): write Newton's second law for the bead including the drag of the fluid, the trap force and the fluctuating force of the molecular environment, multiply the equation by the position, and average over realizations. What comes out is a closed, deterministic, second-order ordinary differential equation for — no stochastic calculus required. This mission formalizes exactly that derivation, and the solution of the resulting equation, for a particle in a harmonic trap.
A particle of mass moves in Cartesian dimensions. Its position at time is the vector with components , ; its velocity components are and its acceleration components . The particle feels three forces: a hydrodynamic drag with drag coefficient ; a harmonic trap force with spring constant ; and a random force exerted by the surrounding medium, which is held at temperature . Newton's second law then reads
A single solution of this equation, for one realization of the random force, is called a path. An ensemble is a probability space of such paths, and the ensemble average of a quantity is . Two physical inputs single out a thermal environment: the random force is uncorrelated with the instantaneous position, , and the velocity obeys equipartition, with Boltzmann's constant. The mean-squared displacement is .
This is the weakest stable form of the result: it fixes no initial condition, no sign convention on the roots, and no regime (inertial or overdamped), and every later statement about the MSD of a trapped Brownian particle is a consequence of it.
For each realization, with ,
which is Newton's equation contracted with and rewritten using and .
With the two distinct roots of ,
solves the goal equation with , and in the inertialess (overdamped) case the solution reduces to , which grows as at short times and saturates at the equipartition plateau .
The MSD equation is what converts a measured displacement trace into physical numbers: its plateau calibrates trap stiffness, its short-time slope gives the diffusion coefficient , and the crossover between the two identifies the relaxation time . The derivation is also the historical template for treating noisy dynamics without a theory of stochastic integrals: Langevin's move of averaging the equation multiplied by is what makes the noise term drop out.
Formalizing it produces a machine-checked statement of the classical calculation together with the assumptions it actually needs, each of which is carried explicitly as a hypothesis rather than left implicit in the prose: interchange of ensemble averaging with time differentiation, integrability of the averaged quantities, decorrelation of the random force from the position, and equipartition. The pathwise identity and the solution-verification statements are elementary calculus; the substance of the mission is that the physical derivation is faithful once those hypotheses are written down.
The obvious route — solve the stochastic equation for and then square and average — requires a theory of stochastic integration against the random force, whose statistics the problem never specifies beyond the two averaged facts above. Langevin's derivation avoids this entirely, but the step "average the equation" hides two real assumptions: that commutes with (so that is the second derivative of ), and that vanishes at every time. Neither follows from the equation of motion; both must be hypotheses, and stating them precisely without weakening the theorem into vacuity is the formalization problem.
Paths are represented in components: position, velocity, acceleration and force are families , and the model predicate records that is the derivative of , that is the derivative of , and that Newton's law holds at every time, so no differentiability is smuggled in. Euclidean contractions are the single helper , so that , , and are all instances of one definition. Ensembles are an arbitrary probability space with the integral as average, and paths are indexed by the sample point; the averaging assumptions appear as hypotheses relating and its derivatives to integrals of the pathwise quantities. Dimension is arbitrary, the source's being a special case.
No hypothesis of the goal is vacuous: a deterministic ensemble (one path, a Dirac measure) with and a particle at rest satisfies all of them when , and nondegenerate instances exist for every choice of parameters, so the statement is not satisfied only in an empty context. All statements target real-valued time and real coefficients; no positivity of , , is assumed except where a milestone needs it for an asymptotic claim.