All missions

Motivation

In 1982 Yoshio Koide, searching for an empirical formula for the Cabibbo angle, noticed that the three charged-lepton masses satisfy

$$m_e + m_\mu + m_\tau \;=\; \frac{2}{3}\left(\sqrt{m_e}+\sqrt{m_\mu}+\sqrt{m_\tau}\right)^2 .$$

With the present-day values $m_e = 0.510998910 \pm 0.000000013$ MeV, $m_\mu = 105.6583663 \pm 0.0000038$ MeV and $m_\tau = 1776.99 \pm 0.29$ MeV, the dimensionless ratio on the left over the bracket on the right equals $0.666667 \pm 0.000016$ — the value $\tfrac{2}{3}$ 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 $q$ defined next. The physics enters only in which numbers one plugs in.

Setting

For a family of $n$ nonnegative "masses" $m = (m_1,\dots,m_n)$, not all zero, define the Koide splitting parameter

$$q(m) \;=\; \frac{\sum_{i} m_i}{\bigl(\sum_i \sqrt{m_i}\bigr)^{2}} .$$

In Lean this is koideRatio, defined by exactly this quotient for m : Fin n → ℝ (with Lean's convention that $\sqrt{x}=0$ for $x<0$ and $x/0 = 0$, 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.

• The degeneracy angle. Put $S = (\sqrt{m_1},\dots,\sqrt{m_n})$ in "generation space" and let $\psi$ be the angle between $S$ and the democratic direction $(1,\dots,1)$. In Lean, koideCos is the cosine $\langle S,\mathbf 1\rangle/(\lVert S\rVert\,\lVert\mathbf 1\rVert)$ written out as a quotient of sums, and koideAngle is its $\arccos$.
• The pseudo-masses of the chapter's generalization: given a mixing matrix $U \in \mathbb{C}^{n\times n}$, $\tilde m_i = \bigl|\sum_j U_{ij} m_j\bigr|$ (pseudoMass).

Koide's relation is the statement $q(m_e,m_\mu,m_\tau) = \tfrac{2}{3}$; the value $q=\tfrac13$ corresponds to exact degeneracy $m_1=m_2=m_3$ and $q=1$ to maximal hierarchy.

Target

The goal theorem is the exact solution of the relation for the third mass. For $m_1,m_2,m_3>0$, writing $P = \sqrt{m_1 m_2}$ and $R = \sqrt{m_1 + 4P + m_2}$,

$$q(m_1,m_2,m_3) = \tfrac{2}{3} \iff m_3 = 7(m_1+m_2) + 20P + 4\sqrt3\,(\sqrt{m_1}+\sqrt{m_2})R$$ $$\textrm{or}\quad \bigl(\, 4P < m_1+m_2 \ \textrm{ and }\ m_3 = 7(m_1+m_2) + 20P - 4\sqrt3\,(\sqrt{m_1}+\sqrt{m_2})R \,\bigr).$$

This is equation (3.25) of the source, made precise: the "$-$" branch of (3.25) is a genuine solution exactly when $4\sqrt{m_1m_2} < m_1+m_2$, and is a spurious root of the squared equation otherwise (for instance at $m_1=m_2$, where the "$-$" value is positive but fails the relation).

The milestones cover, in the source's order: the range $\tfrac1n \le q \le 1$ and its two equality cases (Table 3.1); the geometric reading $\cos\psi = 1/\sqrt{n\,q}$ and the equivalence $\psi = 45^\circ \iff q = \tfrac23$ (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 $\sum_i z_i = 0$ reformulation in the composite-model parametrization (eqs. (3.18)–(3.22)); the $\tau$-mass prediction (eq. (3.4)); and the fact that the pseudo-mass extension (3.31)–(3.32) reduces to the original relation at $U = \mathrm{Id}$.

Significance

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 $m_e$ and $m_\mu$ and the normal hierarchy $m_\tau > m_\mu$ singles out one root, giving $m_\tau = 1776.968874$ MeV, a number two orders of magnitude more precise than the direct measurement (milestone on eq. (3.4)). The bound $\tfrac13 \le q \le 1$ 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 $\sum m$ vs. $(\sum\sqrt m)^2$ pair, and no treatment of the $45^\circ$ 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 "$\pm$" discussion after (3.25) and the claim that (3.1) has exactly two solutions for the third mass.

Difficulty

Nothing here needs heavy machinery, and everything here needs care with square roots.

The bounds are Cauchy–Schwarz in one direction and $\bigl(\sum\sqrt{m_i}\bigr)^2 \ge \sum m_i$ 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 $z = \sqrt{m_3}$ — $z^2 - 4(x+y)z + (x^2+y^2-4xy) = 0$ with $x=\sqrt{m_1}$, $y=\sqrt{m_2}$ — so the difficulty is not solving it but keeping the equivalence exact in both directions: passing from $m_3$ back to $z$ requires $z \ge 0$, which is precisely where the "$-$" branch survives or dies, and the discriminant has to be recognized as a perfect square times $3$. 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.

Formalization scope

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 $n=0$ 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 $3\times3$ complex Hermitian matrix and states the conclusion as an identity in $\mathbb{C}$ between $\operatorname{tr} M$, $\operatorname{tr} M^2$ and $\det M$. Contributions of general-$n$ versions of the three-generation statements, and of the equality analysis as standalone lemmas, are welcome.

Selected references

• F. Goffinet, A bottom-up approach to fermion masses, PhD thesis, Université catholique de Louvain, December 2008. Chapter 3, pp. 59–86. http://hdl.handle.net/2078.1/20873
• Y. Koide, A fermion–boson composite model of quarks and leptons, Phys. Lett. B 120 (1983) 161–165. https://doi.org/10.1016/0370-2693(83)90644-5
• Y. Koide, Challenge to the mystery of the charged lepton mass formula, https://arxiv.org/abs/hep-ph/0506247
• R. Foot, A note on Koide's lepton mass relation, https://arxiv.org/abs/hep-ph/9402242 (the $45^\circ$ geometric reading).
• J.-M. Gérard, F. Goffinet, M. Herquet, A new look at an old mass relation, Phys. Lett. B 633 (2006) 563–566. https://arxiv.org/abs/hep-ph/0510289 (the pseudo-mass extension).

Motivation

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.

Setting

For a set $V$ of $m$ points in $\mathbb R^N$, a map $f:\mathbb R^N\to\mathbb R^k$ is a $(1\pm\epsilon)$-distance-preserving embedding of $V$ if $(1-\epsilon)\|u-v\|^2\le\|f(u)-f(v)\|^2\le(1+\epsilon)\|u-v\|^2$ for every $u,v\in V$. The book's proof constructs $f=A/\sqrt k$ from a random matrix $A\in\mathbb R^{k\times N}$ with i.i.d. standard normal ($N(0,1)$) entries, and argues by the probabilistic method: for a fixed pair of points, Lemma 15.3 shows $f$ preserves their squared distance up to $(1\pm\epsilon)$ with probability at least $1-2e^{-(\epsilon^2-\epsilon^3)k/4}$, because the ratio $\|f(x)\|^2/\|x\|^2$ (for $x$ the difference of the two points) is exactly a $\chi^2_k$ random variable, whose two-sided concentration around its mean $k$ is Lemma 15.2. A union bound over the $O(m^2)$ pairs in $V$ 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.

Formalization targets

Lemma 15.2 (Chi-squared concentration, milestone). If $Q\sim\chi^2_k$, then for $0<\epsilon<1/2$, $P[(1-\epsilon)k\le Q\le(1+\epsilon)k]\ge1-2e^{-(\epsilon^2-\epsilon^3)k/4}$.

Lemma 15.3 (Gaussian random projection distortion, milestone). For $x\in\mathbb R^N$, $k<N$, and $A\in\mathbb R^{k\times N}$ with i.i.d. $N(0,1)$ entries,

$$P\Big[(1-\epsilon)\|x\|^2\le\big\|\tfrac1{\sqrt k}Ax\big\|^2\le(1+\epsilon)\|x\|^2\Big] \ge1-2e^{-(\epsilon^2-\epsilon^3)k/4}.$$

Lemma 15.4 — the mission's goal (Johnson-Lindenstrauss). For $0<\epsilon<1/2$, integer $m>4$, and $k=20\log(m)/\epsilon^2$, any set $V$ of $m$ points in $\mathbb R^N$ admits a map $f:\mathbb R^N\to\mathbb R^k$ with $(1-\epsilon)\|u-v\|^2\le\|f(u)-f(v)\|^2\le(1+\epsilon) \|u-v\|^2$ for all $u,v\in V$.

Significance

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 $k=O(\log m/\epsilon^2)$ is independent of the ambient dimension $N$ — 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 $m$-dimensional subspace and its orthogonal projection, rescaled by $\sqrt{n/m}$ — a genuinely different construction from this book's explicit i.i.d.-Gaussian-matrix map $f=A/\sqrt k$, and with different (existentially quantified, unspecified) constants rather than this book's explicit $k=20\log(m)/\epsilon^2$. 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-$k$ 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.

Difficulty

Lemma 15.2's proof is a genuine Chernoff-bound argument: apply Markov's inequality to $\exp(\lambda Q)$, substitute the chi-squared distribution's own moment-generating function $(1-2\lambda)^{-k/2}$, and optimize the resulting bound over $\lambda\in(0,1/2)$ by calculus (the book's own choice $\lambda=\epsilon/(2(1+\epsilon))$ 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 $T_j=\widehat x_j/\|x\|$ (for $\widehat x=Ax$) are themselves i.i.d. standard normal — a consequence of $A$'s i.i.d. Gaussian entries and $\mathbb E[\widehat x_j^2]=\|x\|^2$, not immediate from the definitions alone — before the sum of their squares can be recognized as exactly a $\chi^2_k$ variable and Lemma 15.2 applied. Lemma 15.4's own proof, while conceptually simple (a single union bound), needs the specific numerical accounting $2m^2e^{-(\epsilon^2-\epsilon^3)k/4}=2m^{5\epsilon-3}<2m^{-1/2}$ at the chosen $k=20\log(m)/\epsilon^2$ and $\epsilon\le1/2$ 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 $k=20\log(m)/\epsilon^2$.

Formalization scope

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.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 15, §15.4.
• W. B. Johnson, J. Lindenstrauss, "Extensions of Lipschitz mappings into a Hilbert space," Contemporary Mathematics 26, 1984, 189-206.
• S. Vempala, The Random Projection Method, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 2004.

Motivation

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 $m$ confined to a circle of radius $R$ 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 $\pi$ electrons of an aromatic ring, such as benzene, as particles on a circular waveguide; filling all levels up to index $n$ takes $2\times(2n+1) = 4n+2$ 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 $n \neq 0$, the count of $2n+1$ states up to level $n$, and — as the goal — the statement that the admissible energies are exactly the quantized values.

Setting

Write $\theta$ for the angular coordinate on the ring of radius $R$. A state is a function $\psi : \mathbb{R} \to \mathbb{C}$ of $\theta$ alone. Since the Laplacian on the ring is $\nabla^2 = R^{-2}\,\partial^2/\partial\theta^2$, the time-independent Schrödinger equation $-\frac{\hbar^2}{2m}\nabla^2\psi = E\psi$ becomes

$$-\frac{\hbar^{2}}{2mR^{2}}\,\psi''(\theta) \;=\; E\,\psi(\theta), \qquad \theta \in \mathbb{R},$$

and single-valuedness on the circle is imposed as the periodic boundary condition

$$\psi(\theta + 2\pi) = \psi(\theta), \qquad \theta \in \mathbb{R}.$$

A stationary state of energy $E$ is a function $\psi$ that is twice continuously differentiable on $\mathbb{R}$, satisfies the periodic boundary condition, and solves the displayed equation. Normalization is over one period,

$$\int_0^{2\pi} |\psi(\theta)|^{2}\, d\theta = 1 .$$

For each integer $n$ put

$$\psi_n(\theta) \;=\; \frac{1}{\sqrt{2\pi}}\, e^{i n \theta}, \qquad E_n \;=\; \frac{n^{2}\hbar^{2}}{2mR^{2}} .$$

Here $\hbar, m, R$ are real parameters, taken positive where positivity matters.

Formalization targets

Goal — the spectrum is exactly the quantized set

For $\hbar, m, R > 0$ and $E \in \mathbb{R}$:

$$\Bigl(\exists\, \psi \not\equiv 0 \ \text{of class } C^{2},\ 2\pi\text{-periodic},\ -\tfrac{\hbar^{2}}{2mR^{2}}\psi'' = E\psi \Bigr) \iff \exists\, n \in \mathbb{Z},\ E = \frac{n^{2}\hbar^{2}}{2mR^{2}} .$$

The right-to-left direction is the construction of $\psi_n$; the left-to-right direction is the quantization statement proper, and it must rule out every $E$ that is not of this form, including all $E < 0$ and every positive $E$ whose associated wave number is not an integer.

Supporting targets

The milestones cover, in order: the periodicity of $\psi_n$; its normalization; the identity $\psi_n'' = -n^{2}\psi_n$; the resulting fact that $\psi_n$ is a stationary state of energy $E_n$; the orthonormality relation $\int_0^{2\pi}\overline{\psi_j}\,\psi_n\,d\theta = \delta_{jn}$; the two-fold degeneracy $E_{-n} = E_n$ with $\psi_n, \psi_{-n}$ linearly independent for $n \neq 0$; and the level count, that exactly $2N+1$ integers $n$ satisfy $E_n \le E_N$.

Significance

The result itself fixes the spectrum of the free Hamiltonian on the circle, with the degeneracy pattern $1, 2, 2, 2, \dots$ and the $2N+1$ level count that underlies the $4N+2$ electron count of Hückel's rule. The orthonormality relation is the statement that the eigenfunctions form the classical Fourier system on $[0, 2\pi]$; the assertion that every ring wave function is a superposition of the $\psi_n$ 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 $L^2$, but the pointwise, $C^2$, 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.

Difficulty

The naive argument — "write the general solution as $A e^{ik\theta} + B e^{-ik\theta}$ with $k = R\sqrt{2mE}/\hbar$, then impose periodicity" — assumes the classification of solutions of $\psi'' = -k^{2}\psi$, which must itself be established over $\mathbb{C}$ for a $C^{2}$, not a priori analytic, function. Three regimes must be treated separately and none may be skipped: $E > 0$, where periodicity forces $k \in \mathbb{Z}$ and hence $E = E_k$; $E = 0$, where the solutions are affine in $\theta$ and periodicity kills the linear term, leaving $n = 0$; and $E < 0$, where the solutions are real exponentials and periodicity forces $\psi \equiv 0$, contradicting nontriviality. The third case is where a careless proof quietly assumes what it should prove.

Formalization scope

Wave functions are total functions $\mathbb{R} \to \mathbb{C}$ 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 $\mathbb{C}$, holding at every real $\theta$. The energy $E$ ranges over $\mathbb{R}$, not $\mathbb{C}$: the mission does not address non-self-adjoint or complex-eigenvalue variants. The parameters $\hbar, m, R$ 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 $\hbar, m, R > 0$. Integrals are interval integrals over $[0, 2\pi]$ with respect to Lebesgue measure.

The goal cannot be satisfied vacuously: the right-hand side of the equivalence is satisfiable (take $n = 0$), and the left-hand side explicitly requires a $\psi$ with $\psi(\theta) \neq 0$ at some point, so the trivial solution is excluded. Contributions that build reusable infrastructure — a classification of $C^{2}$ solutions of $\psi'' = c\,\psi$ over $\mathbb{C}$, 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.

Selected references

• Wikipedia, Particle in a ring, revision 1318339663, https://en.wikipedia.org/wiki/Particle_in_a_ring — the source text for this mission's statements.
• H. Cox, Problems and Solutions to accompany Physical Chemistry: a Molecular Approach, University Science Books, p. 141, ISBN 978-0935702439 — the reference cited by the source for the angular reduction of the Laplacian.
• Wikipedia, Hückel's rule, https://en.wikipedia.org/wiki/H%C3%BCckel%27s_rule — the $4n+2$ electron count obtained from the level count formalized here.

Motivation

The Standard Model of particle physics assigns to each elementary fermion a vector in a representation of the compact Lie group $G_{\mathrm{SM}} = \mathrm{U}(1)\times \mathrm{SU}(2)\times \mathrm{SU}(3)$. 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 $\mathrm{SU}(5)$ theory, Georgi's $\mathrm{Spin}(10)$ theory, and the Pati-Salam model based on $\mathrm{SU}(2)\times \mathrm{SU}(2)\times \mathrm{SU}(4)$.

Baez and Huerta, The Algebra of Grand Unified Theories (2011), isolates the part of this story that is pure algebra: homomorphisms out of $G_{\mathrm{SM}}$, 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 $\Lambda\mathbb{C}^5$, the binary codes, the Dirac spinor representations), which is a natural follow-up mission.

Setting

Write $\mathrm{U}(1)$ for the group of complex numbers of modulus one, and $\mathrm{SU}(n)$ for the $n\times n$ complex matrices $A$ with $A^{*}A = I$ and $\det A = 1$. The Standard Model gauge group is the product

$$G_{\mathrm{SM}} \;=\; \mathrm{U}(1)\times \mathrm{SU}(2)\times \mathrm{SU}(3).$$

Fix the splitting $\mathbb{C}^5 \cong \mathbb{C}^2\oplus\mathbb{C}^3$ and write matrices in $\mathrm{SU}(5)$ in the corresponding $2+3$ block form. The Georgi-Glashow homomorphism is

$$\varphi(\alpha, g, h) \;=\; \begin{pmatrix}\alpha^{3} g & 0\\ 0 & \alpha^{-2} h\end{pmatrix}, \qquad (\alpha, g, h)\in G_{\mathrm{SM}},$$

where $\alpha^{3}g$ means the scalar $\alpha^3$ times the $2\times2$ matrix $g$. Fixing instead the splitting $\mathbb{C}^4\cong\mathbb{C}^3\oplus\mathbb{C}$ (colour plus lepton number), the Pati-Salam homomorphism is

$$\beta(\alpha, g, h) \;=\; \left(g,\; \begin{pmatrix}\alpha^{3} & 0\\ 0& \alpha^{-3}\end{pmatrix},\; \begin{pmatrix}\alpha h & 0\\ 0 & \alpha^{-3}\end{pmatrix}\right) \in \mathrm{SU}(2)\times \mathrm{SU}(2)\times \mathrm{SU}(4).$$

Finally, forgetting the complex structure of $\mathbb{C}^5$ gives a real inner product space $\mathbb{R}^{10}$, and every complex-linear map becomes a real-linear one. Writing each complex coordinate as a pair of real coordinates turns a complex $5\times5$ matrix $A$ into a real $10\times 10$ matrix $\rho(A)$, built from the $2\times 2$ blocks $\begin{pmatrix}\operatorname{Re} A_{ij} & -\operatorname{Im} A_{ij}\\ \operatorname{Im} A_{ij} & \operatorname{Re} A_{ij}\end{pmatrix}$. Under $\rho$, the splitting $\mathbb{C}^2\oplus\mathbb{C}^3$ becomes $\mathbb{R}^4\oplus\mathbb{R}^6$.

Formalization targets

Goal — Theorem 8 (p. 68): the true gauge group as an intersection

$$G_{\mathrm{SM}}/\mathbb{Z}_6 \;=\; \mathrm{SU}(5)\,\cap\,\bigl(\mathrm{SO}(4)\times \mathrm{SO}(6)\bigr)\;\subseteq\;\mathrm{SO}(10).$$

Concretely: a real $10\times10$ matrix $M$ is simultaneously (i) the realification $\rho(A)$ of some $A\in \mathrm{SU}(5)$ and (ii) block diagonal with blocks in $\mathrm{SO}(4)$ and $\mathrm{SO}(6)$, if and only if $M = \rho(\varphi(x))$ for some $x\in G_{\mathrm{SM}}$. The image of $\varphi$ is a copy of $G_{\mathrm{SM}}/\mathbb{Z}_6$, which is why this is the statement of Theorem 8; the quotient itself never has to be formed.

Supporting targets

The milestones establish, in order: that $\varphi$ is a homomorphism into $\mathrm{SU}(5)$; that its kernel is exactly $\{(\alpha, \alpha^{-3}I,\alpha^{2}I): \alpha^6=1\}$, a group of order six; that its image is the subgroup $S(\mathrm{U}(2)\times \mathrm{U}(3))$ of $\mathrm{SU}(5)$ preserving the $2+3$ splitting; the same programme for the Pati-Salam homomorphism $\beta$, whose kernel turns out to have order three; that realification is an injective homomorphism carrying $\mathrm{SU}(5)$ into $\mathrm{SO}(10)$; and the diagram chase by which Theorem 9 (p. 69) upgrades Theorem 8 from $\mathrm{SO}(10)$ to $\mathrm{Spin}(10)$.

Significance

The kernel computation is what makes the $\mathrm{SU}(5)$ theory testable at the level of algebra: because $\ker\varphi \cong \mathbb{Z}_6$ is nontrivial, no representation coming from $\mathrm{SU}(5)$ 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 $\mathrm{Spin}(10)$ 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 $\mathrm{SU}(n)$, the subgroup $S(\mathrm{U}(p)\times \mathrm{U}(q))$, and the realification homomorphism $\mathrm{U}(n)\to \mathrm{SO}(2n)$ 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.

Difficulty

The obvious first move — "$\varphi$ is visibly a homomorphism, so quotient by its kernel and apply the first isomorphism theorem" — settles the $\mathrm{SU}(5)$ milestones but not the goal. The goal compares two subgroups of $\mathrm{SO}(10)$ that are defined by different structures: one by preserving a complex structure and a volume form, the other by preserving a $4+6$ splitting of the real space. Showing the intersection is no larger than the image of $\varphi$ 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 $\mathrm{U}(2)$ block to exist inside $\mathrm{U}(1)$.

Theorem 9 is a second, independent difficulty: $\mathrm{Spin}(10)$ and its double cover of $\mathrm{SO}(10)$ 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 $\mathrm{Spin}(10)$.

Formalization scope

The Lean development commits to the following conventions.

1. $\mathbb{C}^5$ is indexed by the disjoint union $\{0,1\}\sqcup\{0,1,2\}$, so the $2+3$ splitting is built into the index type and $\mathrm{SU}(5)$ elements are written with fromBlocks. Likewise $\mathbb{C}^4$ is indexed by $\{0,1,2\}\sqcup\{0\}$.
2. $\mathbb{R}^{10}$ is indexed by $(\{0,1\}\times\{0,1\})\sqcup(\{0,1,2\}\times\{0,1\})$, the second factor being the real/imaginary coordinate; the $4+6$ splitting is likewise built in.
3. $\mathrm{SO}(n)$ means the real special orthogonal group, i.e. real matrices $M$ with $M^{\mathsf T}M = I$ and $\det M = 1$, and $\mathrm{SO}(4)\times\mathrm{SO}(6)$ means block diagonal matrices whose two diagonal blocks lie in $\mathrm{SO}(4)$ and $\mathrm{SO}(6)$ — the identity component of $S(\mathrm{O}(4)\times \mathrm{O}(6))$, as in the source.
4. $\varphi$ and $\beta$ are given as matrix-valued functions on $G_{\mathrm{SM}}$; that they land in the special unitary groups and are multiplicative are milestones, not definitional assumptions. Quotient groups are never formed: $G_{\mathrm{SM}}/\mathbb{Z}_6$ appears as the image of $\varphi$, and the order of the kernel is stated separately.

No statement is vacuous: every milestone is universally quantified over the whole group, the goal is an equivalence between two nonempty subsets of $\mathrm{SO}(10)$ (both contain the identity), and the hypotheses of the Theorem 9 milestone are satisfied by the real $\mathrm{Spin}$ data of the source.

Contributions welcome beyond the milestones: constructing $\mathrm{Spin}(10)$ and its covering map so Theorem 9 can be stated unconditionally, and the representation theoretic half of the paper (Theorems 1-7), which needs $\Lambda\mathbb{C}^5$ and the Dirac spinor representations.

Selected references

• John Baez and John Huerta, The Algebra of Grand Unified Theories, Bulletin of the American Mathematical Society 47 (2010), 483-552. https://math.ucr.edu/home/baez/guts.pdf
• Howard Georgi and Sheldon Glashow, Unity of All Elementary-Particle Forces, Physical Review Letters 32 (1974), 438-441. https://doi.org/10.1103/PhysRevLett.32.438
• Jogesh Pati and Abdus Salam, Lepton number as the fourth "color", Physical Review D 10 (1974), 275-289. https://doi.org/10.1103/PhysRevD.10.275

Motivation

Chapter 9 asks whether the support vector machine — a regularized empirical risk minimizer $f_{D,\lambda}$ over an RKHS $H$ — is a statistically consistent estimator for regression: does $R_{L,P}(f_{D,\lambda_n}) \to R^*_{L,P}$ as the sample size $n \to \infty$, for a suitable regularization schedule $\lambda_n \to 0$? The chapter's main theorem (Theorem 9.1) answers yes, under an explicit polynomial rate condition on $\lambda_n$. 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 $q$-th moment (no exponential-moment assumption at all)? That fact is Lemma 9.2, "the following lemma to bound the probability of $|R_{L,P}(f_{D,\lambda}) - R_{L,P}(f_{P,\lambda})| \le \varepsilon$ for $|D| \to \infty$" — the technical core the whole chapter's consistency argument rests on, and this mission's goal.

Setting

Fix a measurable space $Z$, a distribution $P$ on $Z$, a separable Hilbert space $H$, and a measurable $g : Z \to H$. Its $q$-th moment norm, for $q \in (1,\infty)$, is $\|g\|_q := (\mathbb E_P\|g\|_H^q)^{1/q}$ — the direct Hilbert-space analogue of an ordinary $L^q$ norm. The proof machinery behind concentration results of this kind is symmetrization: replacing a centered i.i.d. sum $\frac1n\sum_i(\xi_i - \mathbb E_P\xi_i)$ by a Rademacher-randomized sum $\frac1n\sum_i \varepsilon_i \xi_i$, where a Rademacher sequence $\varepsilon_1,\dots,\varepsilon_n$ is a family of independent $\pm1$-valued random variables, each taking each sign with probability $1/2$. Once randomized, the sum's $L^p$-norms (for different $p$) 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.

Formalization targets

Goal: Lemma 9.2 (concentration of Hilbert-space-valued sample means)

$$P^n\!\left(\left\{(z_1,\dots,z_n) \in Z^n : \left\|\frac1n\sum_{i=1}^n g(z_i) - \mathbb E_P g\right\|_H \ge \varepsilon\right\}\right) \le c_q\left(\frac{\|g\|_q}{\varepsilon\, n^{q^*}}\right)^{q}, \qquad q^* := \min\{1/2,\,1-1/q\}$$

for a universal constant $c_q>0$ depending only on $q$, every $\varepsilon>0$ and every $n \ge 1$. This is a genuine generalization of Chebyshev's inequality to Hilbert-space-valued means, sharp enough (via the explicit rate $n^{-q^*}$) to drive Theorem 9.1's own polynomial regularization condition $\lambda_n^{p^*} n \to \infty$.

Milestones (attack order)

1. Theorem A.8.1 (Symmetrization) — $\mathbb E_P\Psi(\|\frac1n\sum_i(\xi_i-\mathbb E_P\xi_i)\|) \le \mathbb E_P\mathbb E_\nu\Psi(2\|\frac1n\sum_i\varepsilon_i\xi_i\|)$ for convex non-decreasing $\Psi$, i.i.d. $P$-integrable $\xi_i$ valued in a separable Banach space, and a Rademacher sequence $\varepsilon_i$. Directly cited in Lemma 9.2's proof ("Using the symmetrization argument given in Theorem A.8.1...").
2. Theorem A.8.3 (Kahane's inequality) — for a Rademacher sequence, every two $L^p(\nu)$ and $L^q(\nu)$ norms of $\|\sum_i\varepsilon_ix_i\|$ are comparable via a universal constant $K_{p,q}$, independent of $n$ and the Banach space $E$. Directly cited in Lemma 9.2's proof ("If $q\in(1,2]$, we obtain with Kahane's inequality, see Theorem A.8.3, that...").

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.

Significance

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 $g :=$ 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 $\|g\|_q$ — 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 $Y \subset \mathbb R$ 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).

Difficulty

The published proof of Lemma 9.2 is a short but dense computation: Markov's inequality reduces the tail bound to bounding $\mathbb E_{P^n}\|h\|_H^q$ for the centered mean $h$; Theorem A.8.1 symmetrizes; for $q \in (1,2]$, Theorem A.8.3 (Kahane) converts the $q$-th moment of the Rademacher sum to its second moment, which an explicit orthogonality computation (the book's Eq. (9.4), $\mathbb E_{\nu^n}\|\sum_i\varepsilon_ix_i\|^2 = \sum_i\|x_i\|^2$ for any fixed $x_1,\dots,x_n$, 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 $q>2$ 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).

Formalization scope

$Z$ and $\Theta$ (the Rademacher sequence's own probability space) are arbitrary measurable spaces; $H$ is [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] [BorelSpace H] [SeparableSpace H] (a separable real Hilbert space with its Borel $\sigma$-algebra), matching "$H$ be a separable Hilbert space" without narrowing to a concrete space (e.g. $\ell^2$) the book itself does not assume. IsRademacherSequence states independence via Mathlib's iIndepFun and the $\pm1$-probability-$1/2$ condition directly, since no ready-made "Rademacher distribution" object exists in this Mathlib revision (checked by search). $q^* := \min\{1/2, 1-1/q\}$ is substituted algebraically rather than introducing a separate conjugate exponent $q'$, since $1/q+1/q'=1$ pins $q'$ down uniquely — not a change of content. In Theorem A.8.3, "for all Banach spaces $E$" 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 $E$ instantiated to a Type* Hilbert space $H$ 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 $\pm1$-probability-$1/2$ condition, true even for perfectly correlated signs) or drop the "i.i.d." qualifier on $\xi_1,\dots,\xi_n$ 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).

Selected references

• I. Steinwart & A. Christmann, Support Vector Machines, Springer, Information Science and Statistics, 2008. https://doi.org/10.1007/978-0-387-77242-4 (Chapter 9, §§9.1-9.2, pp. 333-337, and Appendix §A.8, pp. 535-537).
• J.-P. Kahane, Some Random Series of Functions, 2nd ed., Cambridge University Press, 1985 (Kahane's inequality, Theorem A.8.3's original source).
• A. W. van der Vaart & J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996 (Lemma 2.3.1, the source of Theorem A.8.1's proof technique).

Counting terms and comparing the resulting sums

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.

The icx/icv/cx orders, restated for this 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 $X,Y$, $X\le_{icx}Y$ [$X\le_{icv}Y$] if $E[\varphi(X)]\le E[\varphi(Y)]$ for every increasing convex [concave] $\varphi:\mathbb{R}\to\mathbb{R}$ for which the expectations exist, and $X\le_{cx}Y$ if the same holds for every convex $\varphi$ (dropping "increasing"). Theorem 8.A.13 applies these same three orders to nonnegative-integer-valued random variables $M,N$ — a special case of the real-valued order (after the coercion $\mathbb{N}\to\mathbb{R}$), not a separate discrete order, per this chapter's own pitfall 1.

Formalization target

Goal: closure of the icx/icv/cx orders under random sums (Theorem 8.A.13)

Let $\{Y_k, k\in\mathbb{N}_{++}\}$ be i.i.d. nonnegative random variables, independent of the two nonnegative discrete random variables $M$ and $N$. Then

$$M\le_{icx}[\le_{icv}]\,N \implies \sum_{k=1}^{M}Y_k \le_{icx}[\le_{icv}]\sum_{k=1}^{N}Y_k, \qquad M\le_{cx}N \implies \sum_{k=1}^{M}Y_k \le_{cx}\sum_{k=1}^{N}Y_k.$$

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 $\psi(n) = E[\varphi(\sum_{k=1}^n Y_k)]$ for an increasing convex [concave] $\varphi$ and observes (via the unnumbered Example 8.A.4) that $\psi$ is itself increasing and convex [concave] in $n$; the icx/icv order on $M,N$ then transfers directly to $\psi(M)$ vs. $\psi(N)$, giving part (a). Part (b) follows from part (a) together with the equal-means fact $E[\sum_{k=1}^M Y_k]=E[\sum_{k=1}^N Y_k]$ under $M\le_{cx}N$ (Theorem 4.A.35, a Chapter 4 result not restated in this mission).

Significance

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 $M$ vs. $N$) 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.

Difficulty

The chief formalization risk is treating $M\le_{icx}N$ as a separate "discrete" order rather than the same real-valued order applied to $\mathbb{N}$-valued random variables after coercion — this chapter's own pitfall 1. A second risk is drafting $\sum_{k=1}^{M}Y_k$ as a fixed-length sum with $M$ substituted in afterward, rather than a genuine random (randomly-stopped) sum where $M$ is itself random and independent of the $\{Y_k\}$ 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 $\theta\in\Theta$" 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. $\Theta$ 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.

Formalization scope

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. $M,N:\Omega\to\mathbb{N}$ 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 $\{Y_k\}$ from $(M,N)$ 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.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Chapter 8 (Stochastic Convexity and Concavity), §8.A.1–8.A.2. https://doi.org/10.1007/978-0-387-34675-5
• This series' Chunk 03 (StochasticOrders.Convex) and Chunk 04 (StochasticOrders.MonotoneConvex), for the univariate convex and increasing convex/concave orders this chapter restates locally.

Motivation

Compressed sensing asks a question that looks impossible at first: can a signal $x\in\mathbb R^n$ be reconstructed exactly from far fewer than $n$ linear measurements $y=Ax\in\mathbb R^m$, $m\ll n$? Classical linear algebra says no — an underdetermined system has infinitely many solutions. But if $x$ 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 $\ell_1$ norm of a candidate solution, subject to matching the measurements, recovers $x$ exactly, for a measurement matrix $A$ 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 $\ell_1$ minimization. (A companion result, outside this mission, shows random sub-gaussian matrices satisfy RIP with high probability once $m$ is large enough, which is what makes the deterministic guarantee here practically useful; this mission formalizes the deterministic half.)

Setting

For a vector $v$ indexed by a finite set, write $\|v\|_0$ for its number of non-zero coordinates (so $v$ is $s$-sparse if $\|v\|_0\le s$), $\|v\|_1:=\sum_i|v_i|$ for its $\ell_1$ norm, and $\|v\|_2:=\sqrt{\sum_i v_i^2}$ for its Euclidean norm.

An $m\times n$ matrix $A$ satisfies the restricted isometry property (RIP) with parameters $\alpha,\beta,s$ if

$$\alpha\|v\|_2 \;\le\; \|Av\|_2 \;\le\; \beta\|v\|_2 \qquad\text{for every } s\text{-sparse } v\in\mathbb R^n,$$

i.e. $A$ acts as an approximate isometry on every $s$-sparse vector — equivalently (the book's own Exercise 10.5.9), the singular values of every $m\times s$ column-submatrix of $A$ lie in $[\alpha,\beta]$.

Given a matrix $A$ and measurements $y=Ax$ for an unknown sparse $x$, the exact-recovery program is

$$\text{minimize } \|x'\|_1 \quad\text{subject to}\quad y = Ax'.$$

Formalization targets

Goal (Theorem 10.5.10, RIP implies exact recovery)

$$\exists\,\hat x = x \quad\text{whenever}\quad \hat x \text{ solves the exact-recovery program for } y=Ax,$$

precisely: suppose $A$ satisfies RIP with parameters $\alpha,\beta,(1+\lambda)s$ where $\lambda>(\beta/\alpha)^2$; then for every $s$-sparse $x$, every $\hat x$ that is feasible ($A\hat x=Ax$) and $\ell_1$-optimal among feasible vectors satisfies $\hat x=x$. No constant here is hard-coded beyond the book's own explicit threshold $\lambda>(\beta/\alpha)^2$ — the weakest stable form of the claim.

Significance

RIP isolates exactly the geometric mechanism that makes $\ell_1$-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 $m=O(s\log n)$ measurements suffice to recover any $s$-sparse signal in $\mathbb R^n$ — exponentially fewer than the $n$ 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.

Difficulty

The natural first idea for showing $\hat x=x$ is to try to bound the recovery error $h:=\hat x-x$ directly using $\|Ah\|_2$ (which vanishes, since both $x$ and $\hat x$ are feasible) together with RIP applied to $h$ itself — but $h$ need not be sparse at all: it is the difference of two sparse-ish vectors and can have full support. The actual argument decomposes $h$'s support into blocks by descending magnitude (the support $I_0$ of $x$, then the $\lambda s$ largest remaining coordinates $I_1$, then the next $\lambda s$, and so on), applies RIP only to the leading block $I_{0,1}=I_0\cup I_1$ (which genuinely has bounded sparsity $\le(1+\lambda)s$), and separately bounds the contribution of every later block using the fact that $\hat x$ is $\ell_1$-optimal (so $\|h_{I_0^c}\|_1\le\|h_{I_0}\|_1$, the "cone constraint"): each later block's $\ell_2$ norm is controlled by the $\ell_1$ 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 $h$ as a whole does not typecheck, since RIP says nothing about vectors with more than $(1+\lambda)s$ non-zero entries.

Formalization scope

Vectors are plain functions ι → ℝ on a finite index type, not EuclideanSpace ℝ ι: the latter's fixed $\ell_2$ norm instance cannot also host the $\ell_1$ 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 $(1+\lambda)s$ used by the goal theorem is a real number even at integer base sparsity. A solution $\hat x$ "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 $\hat x$, 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.

Selected references

• E. J. Candès, T. Tao, Decoding by linear programming, IEEE Transactions on Information Theory 51 (2005), 4203–4215. https://doi.org/10.1109/TIT.2005.858979
• D. L. Donoho, Compressed sensing, IEEE Transactions on Information Theory 52 (2006), 1289–1306. https://doi.org/10.1109/TIT.2006.871582
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 10. https://doi.org/10.1017/9781108231596

Motivation

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 $2^n$ 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.

Setting

Fix a finite set of players $N = \{1,\dots,n\}$. A characteristic function $f$ assigns a real number $f(S)$ to every coalition $S \subseteq N$, with $f(\emptyset) = 0$; $f(S)$ is the net return a coalition $S$ could earn on its own. The pair $(N,f)$ is a cooperative game, and throughout this chapter $f$ is assumed superadditive: $f(S') + f(S'') \le f(S' \cup S'')$ for disjoint $S', S''$. A payoff vector $y \in \mathbb{R}^N$ is feasible if $\sum_{i \in N} y_i = f(N)$, and acceptable if $\sum_{i \in S} y_i \ge f(S)$ for every coalition $S$. The core is the set of payoff vectors that are both:

$$\mathrm{Core}(N,f) = \Big\{ y \in \mathbb{R}^N : \sum_{i \in N} y_i = f(N) \text{ and } f(S) \le \sum_{i \in S} y_i \ \forall S \subseteq N \Big\}.$$

$(N,f)$ is a convex game if $f$ is supermodular on the Boolean lattice of coalitions: $f(S) + f(S') \le f(S \cup S') + f(S \cap S')$ for all $S, S'$. ("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 $f(S \cup \{i\}) - f(S)$ of any player $i$ to any coalition $S$ not containing $i$ increases as $S$ grows — the more players already committed to a project, the more valuable one more player is to it.

Given a permutation $\pi$ of $N$, let $S_\pi(j) = \{\pi(1),\dots,\pi(j)\}$. The greedy algorithm builds the payoff vector $y^\pi$ by paying each player its marginal contribution when added in the order $\pi$: $y^\pi_{\pi(j)} = f(S_\pi(j)) - f(S_\pi(j-1))$. The Shapley value pays player $i$ the average of $y^\pi_i$ over all $n!$ permutations $\pi$, equivalently $\sum_{S \subseteq N\setminus\{i\}} \frac{|S|!(n-|S|-1)!}{n!}(f(S\cup\{i\}) - f(S))$.

A core is large if every acceptable payoff vector is dominated, coordinatewise, by one in the core; a subgame $(N',f)$ restricts $f$ to subsets of $N' \subseteq N$; a core is totally large if the core of every subgame is large.

Formalization targets

Goal — Theorem 5.2.1 (Shapley [1971])

$$\text{if } (N,f) \text{ is a convex game, then for every permutation } \pi,\ y^\pi \in \mathrm{Core}(N,f); \quad \mathrm{Core}(N,f) \ne \emptyset; \quad \text{Shapley value} \in \mathrm{Core}(N,f).$$

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 $y^\pi$'s, not implied by (a) and (b) alone.

Milestones

• Lemma 5.2.1(a): $\sum_{i \in S_\pi(j)} y^\pi_i = f(S_\pi(j))$ for every $j = 1,\dots,n$ — the partial-sum identity the goal's proof of acceptability is built on.
• Theorem 5.2.6 (Moulin [1990]): a cooperative game is convex if and only if its core is totally large — the converse direction that a large core alone (Theorem 5.2.1's easy corollary) does not give.
• Theorem 5.2.7(a,b) (Topkis [1987]): if the characteristic function $f^t$ of a family of games has increasing differences in a parameter $t$ (a complementary parameter), the greedy payoff vector and the Shapley value both increase in $t$.

Significance

Theorem 5.2.1 is the reason convex games are the tractable case of cooperative game theory: it turns an existence question about $2^n$ 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.

Difficulty

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 $S'$ against the initial coalitions $S_\pi(j)$ built by the particular permutation $\pi$, splitting $S'$ by the first and last time one of its elements appears in $\pi$'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 $g(S) = \max_{S \subseteq S' \subseteq N} \big(f(S') - \sum_{i \in S'} y''_i\big)$ from an arbitrary acceptable vector $y''$ and showing $g$ 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.

Formalization scope

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 $S_\pi(j)$ 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.

Selected references

• L. S. Shapley, "Cores of convex games," International Journal of Game Theory, 1(1), 1971, 11–26. https://doi.org/10.1007/BF01753431
• L. S. Shapley, "A value for n-person games," in Contributions to the Theory of Games II, Princeton University Press, 1953, 307–317.
• H. Moulin, "Cores and large cores when population varies," International Journal of Game Theory, 19(3), 1990, 219–232. https://doi.org/10.1007/BF01766437
• W. W. Sharkey, "Cooperative games with large cores," International Journal of Game Theory, 11(3-4), 1982, 175–182. https://doi.org/10.1007/BF01766193
• D. M. Topkis, "Activity optimization games with complementarity," European Journal of Operational Research, 28(3), 1987, 358–368. https://doi.org/10.1016/0377-2217(87)90232-5
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 2011, Chapter 5. https://doi.org/10.1515/9781400822539