Mathematical Physics

Motivation

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 $\gamma$. 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 $2.2\,\mu\mathrm{s}$ reach the ground from an altitude of about $10\ \mathrm{km}$ in numbers explained by their large $\gamma$, and the standard model of long gamma-ray bursts requires ejecta with initial $\gamma \gtrsim 100$ to resolve the compactness problem.

The material formalized here is textbook kinematics rather than open research: the definition of $\gamma$, 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.

Setting

Fix an inertial frame and a relative velocity $v$ along a single spatial axis, and let $c$ be the speed of light in vacuum. Write $\beta = v/c$ for the dimensionless velocity ratio. All statements in this mission are in units where $c = 1$, so $\beta$ is the only kinematic parameter and takes values in the interval $(-1, 1)$ for a massive body.

The Lorentz factor is

$$\gamma(\beta) = \frac{1}{\sqrt{1 - \beta^{2}}},$$

and its reciprocal is $\alpha(\beta) = \sqrt{1 - \beta^{2}} = 1/\gamma(\beta)$, the quantity tabulated alongside $\gamma$ in the source article.

Two derived objects appear throughout. Relativistic velocity addition is

$$\beta_1 \oplus \beta_2 = \frac{\beta_1 + \beta_2}{1 + \beta_1 \beta_2},$$

and the Lorentz boost of velocity $\beta$, acting on the coordinate pair $(t, x)$ by $t' = \gamma(t - \beta x)$ and $x' = \gamma(x - \beta t)$, is the symmetric matrix

$$B(\beta) = \begin{pmatrix} \gamma(\beta) & -\gamma(\beta)\beta \\ -\gamma(\beta)\beta & \gamma(\beta) \end{pmatrix}.$$

Finally, the rapidity $w$ of a motion is the hyperbolic angle with $\beta = \tanh w$.

Formalization targets

Goal — boosts compose by relativistic velocity addition

$$B(\beta_1)\,B(\beta_2) = B(\beta_1 \oplus \beta_2), \qquad \gamma(\beta_1 \oplus \beta_2) = \gamma(\beta_1)\gamma(\beta_2)(1 + \beta_1\beta_2), \qquad |\beta_1 \oplus \beta_2| < 1,$$

for all subluminal $\beta_1, \beta_2$. 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.

Supporting targets

The milestones cover, in the order of the source article: the bound $\gamma \ge 1$ with equality exactly at rest; the reciprocal identity $\alpha = 1/\gamma$; strict monotonicity of $\gamma$ on $[0,1)$ and its divergence as $\beta \to 1^{-}$; the rapidity identities $\gamma(\tanh w) = \cosh w$ and $\gamma(\tanh w)\tanh w = \sinh w$; additivity of rapidity, $\tanh w_1 \oplus \tanh w_2 = \tanh(w_1 + w_2)$; the momentum form $\gamma = \sqrt{1 + (p/m)^2}$; the Newtonian limit $(\gamma - 1)/\beta^{2} \to \tfrac12$ as $\beta \to 0$; the exact table entries $\gamma(3/5) = 5/4$, $\gamma(4/5) = 5/3$, $\gamma(\sqrt3/2) = 2$; and the inversion $\sqrt{1 - 1/\gamma^{2}} = \beta$ on $[0,1)$.

Significance

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 $\oplus$, is the reason rapidity is additive and the reason the velocity of light is the same in every inertial frame, since $\beta_1 \oplus \beta_2$ stays inside $(-1,1)$. The supporting milestones are the facts a downstream development actually consumes — positivity and monotonicity of $\gamma$, 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, $2 \times 2$ matrices) but carries no development of relativistic kinematics built on it.

Difficulty

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 $0$ on negative inputs, so $\gamma$ is defined — and useless — outside $|\beta| < 1$. Every algebraic step needs the positivity of $\sqrt{1-\beta^{2}}$ in hand before dividing, and the hypothesis $|\beta| < 1$ must be propagated to each intermediate expression, including to the composed velocity $\beta_1 \oplus \beta_2$ in the goal.

Second, the goal's matrix identity does not follow from entrywise algebra alone: the entries of $B(\beta_1 \oplus \beta_2)$ contain $\gamma(\beta_1 \oplus \beta_2)$, a nested square root, and the composition law only becomes polynomial after the identity $\gamma(\beta_1 \oplus \beta_2) = \gamma(\beta_1)\gamma(\beta_2)(1 + \beta_1\beta_2)$ 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 $\beta \to 1^{-}$ is a one-sided limit that must be routed through the positivity of $\sqrt{1 - \beta^{2}}$ on a left neighbourhood of $1$, and the Newtonian limit is stated on the punctured neighbourhood of $0$, where the quotient $(\gamma - 1)/\beta^{2}$ has to be rewritten as a function continuous at $0$ before any limit theorem applies.

Formalization scope

Everything is over the real numbers in units $c = 1$; the definitions bundle fixes $\gamma$, $\alpha$, $\oplus$, and $B$ as total functions, and the boost is the $2 \times 2$ matrix acting on $(t, x)$ with the sign convention $t' = \gamma(t - \beta x)$. Subluminality is never built into the types: it appears as an explicit hypothesis $|\beta| < 1$ 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 $|\beta| \ge 1$ the square root is $0$ and $\gamma(\beta) = 0$, 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 $3{+}1$ 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.

Selected references

• Lorentz factor, Wikipedia (revision oldid=1355686906). https://en.wikipedia.org/w/index.php?title=Lorentz_factor&oldid=1355686906
• J. Forshaw and G. Smith, Dynamics and Relativity, John Wiley & Sons, 2014, p. 118.
• J. D. Jackson, Kinematics, Particle Data Group review, 2005 (rapidity, p. 7). https://pdg.lbl.gov/2005/reviews/kinemarpp.pdf

Motivation

The proton-to-electron mass ratio $\mu = m_p/m_e$ is a dimensionless constant of nature; the CODATA 2022 recommended value is

$$\mu = 1836.152673426(32),$$

the parenthesised digits being the standard uncertainty on the last two places, i.e. a relative standard uncertainty of $1.7\times10^{-11}$ (NIST CODATA).

In a two-sentence note in Physical Review in 1951, Friedrich Lenz observed that the then best experimental value, $1836.12 \pm 0.05$, is matched almost exactly by the closed-form expression $6\pi^5$. 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 $6\pi^5$ 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.

Setting

Throughout, all quantities are real numbers.

• $L := 6\pi^5$ is Lenz's expression (lenzExpression in the formal development), with $\pi$ the usual circle constant.
• $\mu_{2022} := 1836.152673426$ is the CODATA 2022 value of the mass ratio (codataValue), and $u_{2022} := 3.2\times10^{-8}$ its standard uncertainty (codataUncertainty), the "(32)" attached to the last two digits.
• $\mu_{1951} := 1836.12$ is the experimental value available to Lenz (lenz1951Measurement) and $u_{1951} := 0.05$ 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 $m_p/m_e$ of two reals.

Formalization targets

Goal

For all reals $m_p, m_e$ with $m_p/m_e = \mu_{2022}$:

$$m_p/m_e \neq L,\qquad |m_p/m_e - L| > 10^6\,u_{2022},\qquad 1.88\times10^{-5} < \frac{m_p/m_e - L}{m_p/m_e} < 1.89\times10^{-5},$$

while at the same time

$$|L - \mu_{1951}| < u_{1951}.$$

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 $10^6$, $1.88\times10^{-5}$ and $1.89\times10^{-5}$ are stated with slack — the true values are about $1.08\times10^6$ and $1.8825\times10^{-5}$ — so the goal does not depend on the last digits quoted by any one source.

Supporting levels

$$306.019684 < \pi^5 < 306.019685, \qquad 1836.1181 < 6\pi^5 < 1836.11811.$$

Note that the second window must be narrower than $10^{-4}$: an enclosure of $6\pi^5$ of width $10^{-4}$ is not sharp enough to imply the relative-deviation bounds of the goal, whose window has absolute width about $1.8\times10^{-3}$ but is centred $0.0346$ away from $\mu_{2022}$.

Significance

The result itself. The claim "$6\pi^5 \ne \mu$" 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 $\pi^5$ and $6\pi^5$ 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 $\pi$ (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 $x \mapsto x^5$ 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 $\pi^n$, or comparisons against other quoted values of the ratio — are welcome.

Difficulty

This is an easy mission by design; the one place a first attempt goes wrong is precision bookkeeping.

• The commonly used six-digit bounds $3.141592 < \pi < 3.141593$ propagate to an uncertainty of about $\pm 1.5\times10^{-3}$ in $6\pi^5$, which decides the comparison with $\mu_{1951}$ but is two orders of magnitude too coarse for the goal's relative-deviation window. The 20-digit bounds are needed.
• The relative-deviation bounds are the binding constraint: they require an enclosure of $6\pi^5$ of width about $10^{-5}$, not the $10^{-4}$ that a first draft naturally writes down.
• Raising an enclosure of $\pi$ to the fifth power multiplies the relative error by about $5$; the input enclosure must be tighter than the target by that factor.

Formalization scope

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 $m_p, m_e$ subject only to $m_p/m_e = \mu_{2022}$; no positivity is assumed, since the hypothesis already pins the quotient, and the hypothesis is satisfiable (e.g. $m_e = 1$), so the statement is not vacuous. No measurement-theoretic notion of "uncertainty" is formalized: $u_{2022}$ and $u_{1951}$ 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 $\pi^5$ is the one piece reusable beyond this mission.

Selected references

• F. Lenz, The Ratio of Proton and Electron Masses, Physical Review 82 (1951) 554. doi:10.1103/PhysRev.82.554.2
• CODATA 2022, proton-electron mass ratio, NIST Reference on Constants, Units, and Uncertainty. physics.nist.gov
• Wikipedia, Proton-to-electron mass ratio, revision 1371273020. link

Motivation

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 $\mathrm{Re}$ 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 $\mathrm{Re}$ 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 $\mathrm{Re}$ alone. This mission formalises that uniqueness claim, together with the standard algebraic identities that surround it in engineering practice.

Setting

Work with four real parameters of a flow:

• $\rho > 0$, the density of the fluid (SI: $\mathrm{kg\,m^{-3}}$);
• $u$, the flow velocity ($\mathrm{m\,s^{-1}}$);
• $L > 0$, a characteristic length ($\mathrm{m}$);
• $\mu > 0$, the dynamic viscosity ($\mathrm{Pa\,s} = \mathrm{kg\,m^{-1}s^{-1}}$).

The Reynolds number is

$$\mathrm{Re}(\rho,u,L,\mu) \;=\; \frac{\rho u L}{\mu},$$

and the kinematic viscosity is $\nu = \mu/\rho$, so that $\mathrm{Re} = uL/\nu$.

For duct flow one further needs the hydraulic diameter $D_H = 4A/P$, where $A$ is the cross-sectional area of the duct and $P$ 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

$$[\rho] = ML^{-3},\quad [u] = LT^{-1},\quad [L] = L,\quad [\mu] = ML^{-1}T^{-1}.$$

For real exponents $a,b,c,d$ the monomial $\rho^{a}u^{b}L^{c}\mu^{d}$ therefore has dimension $M^{\alpha}L^{\beta}T^{\gamma}$ with

$$\alpha = a+d,\qquad \beta = -3a+b+c-d,\qquad \gamma = -b-d,$$

and the monomial is called dimensionless when $(\alpha,\beta,\gamma) = (0,0,0)$. These three linear forms are what the mission's dimExponents and Dimensionless record.

Target

The goal theorem is the uniqueness of the Reynolds number as a dimensionless group. For positive $\rho, u, L, \mu$ and real exponents $a,b,c,d$:

$$\rho^{a}u^{b}L^{c}\mu^{d} \text{ is dimensionless} \iff \exists\, s\in\mathbb{R}: (a,b,c,d) = s\,(1,1,1,-1) \ \text{ and }\ \rho^{a}u^{b}L^{c}\mu^{d} = \mathrm{Re}(\rho,u,L,\mu)^{s}.$$

The milestones are the supporting statements, ordered as they appear in the source:

1. $\mathrm{Re}$ is invariant under a change of the mass, length and time units: $\mathrm{Re}(\rho m l^{-3},\, u l t^{-1},\, L l,\, \mu m l^{-1} t^{-1}) = \mathrm{Re}(\rho,u,L,\mu)$ for all $m,l,t>0$.
2. $\mathrm{Re} = uL/\nu$ with $\nu = \mu/\rho$.
3. Buckingham $\pi$: the exponent vectors of dimensionless monomials form the line spanned by $(1,1,1,-1)$.
4. Pipe flow: with mean velocity $u = Q/A$, one has $\mathrm{Re} = QD_H/(\nu A) = W D_H/(\mu A)$, where $Q$ is the volumetric flow rate and $W = \rho Q$ the mass flow rate.
5. Circular pipe: $4A/P = D$ when $A = \pi D^{2}/4$ and $P = \pi D$.
6. Annular duct: $4A/P = D_o - D_i$ when $A = \pi(D_o^{2}-D_i^{2})/4$ and $P = \pi(D_o+D_i)$.
7. Nondimensionalised Navier–Stokes: the viscous term's coefficient satisfies $\mu/(\rho L V) = 1/\mathrm{Re}(\rho,V,L,\mu)$.

Significance

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 $\rho, u, L, \mu$, 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, $\mathrm{Re}$, 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 ($\mu \neq 0$, $P \neq 0$, $D_i < D_o$) 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 $\mathrm{Re}_D \approx 2300$ and $\mathrm{Re}_x \approx 5\times 10^{5}$ quoted in the source are experimental observations, not theorems, and are deliberately excluded.

Difficulty

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: $x/0 = 0$, so a statement about $\mathrm{Re}$ that omits $\mu > 0$ 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 $\mathrm{Re}$, but the formal statement quantifies over exponent vectors, and the equivalence with $\mathrm{Re}^{s}$ uses real powers of positive reals.

Formalization scope

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 $(0,0,0)$ — a linear condition on the exponents, with no positivity hypothesis on the parameters.

In the goal theorem the powers $\rho^{a}, u^{b}, L^{c}, \mu^{d}$ and $\mathrm{Re}^{s}$ are real powers (Real.rpow), which is why $\rho, u, L, \mu$ 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 $m, l, t$, 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 $\pi$ theorem for an arbitrary dimension matrix — are welcome.

Selected references

• Osborne Reynolds, "An experimental investigation of the circumstances which determine whether the motion of water shall be direct or sinuous, and of the law of resistance in parallel channels", Philosophical Transactions of the Royal Society 174 (1883), 935–982. DOI: 10.1098/rstl.1883.0029
• Edgar Buckingham, "On physically similar systems; illustrations of the use of dimensional equations", Physical Review 4 (1914), 345–376. DOI: 10.1103/PhysRev.4.345
• "Reynolds number", Wikipedia — the source text this mission formalises: https://en.wikipedia.org/wiki/Reynolds_number

Motivation

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 $-\mu/\mu_B=g/2=1.001\,159\,652\,180\,59\,(13)$, and, combined with the Standard-Model prediction, $\alpha^{-1}=137.035\,999\,166\,(15)$. 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 $\nu_c=eB/(2\pi m)$, but what a trap lets you observe are its three normal-mode frequencies — the trap-modified cyclotron frequency $\bar\nu_c$, the axial frequency $\bar\nu_z$, and the magnetron frequency $\bar\nu_m$. 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:

$$\nu_c=\sqrt{\bar\nu_c^{2}+\bar\nu_z^{2}+\bar\nu_m^{2}}.$$

This is what makes a part-per-trillion measurement possible with an imperfect trap, and it is the object of this mission.

Setting

Work in $\mathbb{R}^3$. A particle of charge $q$ and mass $m$ sits in a uniform magnetic field $\mathbf B=B\,b$ with $b$ 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 $3\times3$ matrix $K$, and the equation of motion of the particle is linear:

$$r''(t)\;=\;-K\,r(t)\;+\;\omega_c\,\big(r'(t)\times b\big),\qquad \omega_c=\frac{qB}{m}.$$

Two properties of $K$ carry all the physics of the trap: $K$ 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, $K$ is arbitrary — an arbitrary $K$ is exactly what "the axis of the potential is tilted relative to $b$, and the potential is elliptically distorted" means, so no separate tilt angle or ellipticity parameter appears anywhere.

Substituting the ansatz $r(t)=u\,e^{-i\omega t}$ with $u\in\mathbb{C}^3$ turns the equation of motion into the linear system $M(\omega)\,u=0$, where

$$M(\omega)\;=\;K-\omega^{2}I-i\,\omega\,\omega_c\,C(b), \qquad C(b)=\begin{pmatrix}0&-b_3&b_2\\ b_3&0&-b_1\\ -b_2&b_1&0\end{pmatrix}$$

is the matrix of $u\mapsto b\times u$. A frequency $\omega$ is a normal mode of the trap precisely when $\det M(\omega)=0$. The three eigenfrequencies of the trap, written $\bar\omega_c,\bar\omega_z,\bar\omega_m$ (angular versions of $\bar\nu_c,\bar\nu_z,\bar\nu_m$), are the non-negative solutions of that equation.

Target

The goal is the invariance theorem in the form: if the three numbers $\bar\omega_c,\bar\omega_z,\bar\omega_m$ are the eigenfrequencies of the trap, in the sense that

$$\det M(\omega)=-\big(\omega^{2}-\bar\omega_c^{2}\big)\big(\omega^{2}-\bar\omega_z^{2}\big)\big(\omega^{2}-\bar\omega_m^{2}\big)\quad\text{for all }\omega\in\mathbb{R},$$

then, for every symmetric traceless $K$ and every unit vector $b$,

$$\bar\omega_c^{2}+\bar\omega_z^{2}+\bar\omega_m^{2}\;=\;\omega_c^{2}.$$

The milestones are the three steps of the argument, in increasing order of dependence:

1. Mode equation. The exponential ansatz solves the equation of motion at every time if and only if its amplitude lies in the kernel of $M(\omega)$. This is what makes $M(\omega)$ the right object to take determinants of.
2. Characteristic polynomial. For symmetric $K$, $\det M(\omega)$ is real and depends on $\omega$ only through $\omega^2$: it equals $-q(\omega^2)$ with $q(\lambda)=\det(\lambda I-K)-\omega_c^{2}\lambda(\lambda\langle b,b\rangle-\langle b,Kb\rangle)$.
3. Ideal trap. For $K=\operatorname{diag}(-\omega_z^2/2,-\omega_z^2/2,\omega_z^2)$, $b=(0,0,1)$ and $\omega_c^2\ge 2\omega_z^2$, the determinant factors explicitly, with eigenfrequencies $(\omega_c\pm\sqrt{\omega_c^2-2\omega_z^2})/2$ and $\omega_z$.

Significance

The result. The invariance theorem is why the electron magnetic moment can be measured to $0.13$ 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 $\nu_c$ as a systematic error, and the frequency ratio $\nu_a/\nu_c$ that gives $g/2$ 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.

Difficulty

The obvious first idea — solve $\det M(\omega)=0$ 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 $\omega^4$ in the characteristic polynomial and therefore needs no root formula at all: it is Vieta plus the two structural facts $\operatorname{tr}K=0$ and $\langle b,b\rangle=1$. The work in Lean is consequently not analysis but bookkeeping: computing a $3\times3$ determinant with complex off-diagonal entries and extracting one coefficient of the resulting cubic in $\omega^2$. 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.

Formalization scope

Conventions fixed by the Lean statements, and not visible in the prose:

1. Vectors are functions on a three-element index set and matrices are $3\times3$; no abstract inner-product space is used.
2. $K$ is an arbitrary real matrix in the definitions; symmetry and tracelessness are hypotheses on the individual theorems, not part of the model.
3. "Unit vector" is the algebraic condition $\langle b,b\rangle=1$; no norm is used.
4. The magnetic term is $-i\,\omega\,\omega_c\,C(b)$ with $C(b)u=b\times u$, i.e. the sign convention is fixed by the ansatz $r(t)=u\,e^{-i\omega t}$ and the force $\omega_c\,(r'\times b)$.
5. "The eigenfrequencies are $\bar\omega_c,\bar\omega_z,\bar\omega_m$" is formalized as the functional identity $\det M(\omega)=-(\omega^2-\bar\omega_c^2)(\omega^2-\bar\omega_z^2)(\omega^2-\bar\omega_m^2)$ for all real $\omega$ — that is, as a factorization with multiplicity, not as a set of solutions of $\det M(\omega)=0$, which would not pin down multiplicities and would make the sum rule false in degenerate cases.
6. No sign conditions are imposed on $\bar\omega_c,\bar\omega_z,\bar\omega_m$; the conclusion involves only their squares.
7. Nothing in this mission formalizes any measured quantity: $g/2$, $\alpha$, and the frequencies of the actual apparatus appear only as motivation.

Only Mathlib is needed: matrices over $\mathbb{R}$ and $\mathbb{C}$, determinants of $3\times3$ 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.

Selected references

• X. Fan, T. G. Myers, B. A. D. Sukra, G. Gabrielse, Measurement of the Electron Magnetic Moment, Phys. Rev. Lett. 130, 071801 (2023), arXiv:2209.13084 — Eq. (4) is the statement formalized here.
• L. S. Brown, G. Gabrielse, Precision spectroscopy of a charged particle in an imperfect Penning trap, Phys. Rev. A 25, 2423 (1982), doi:10.1103/PhysRevA.25.2423 — the original invariance theorem.
• L. S. Brown, G. Gabrielse, Geonium theory: Physics of a single electron or ion in a Penning trap, Rev. Mod. Phys. 58, 233 (1986), doi:10.1103/RevModPhys.58.233 — the trap eigenfrequencies and the hierarchy $\bar\nu_c\gg\bar\nu_z\gg\bar\nu_m$.

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

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

A gas of $N$ interacting particles is described exactly by $6N$ coordinates, and by no useful equation. Kinetic theory replaces that description by a single scalar field, the one-particle distribution function $f(x,v,t)$, 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 $f$ towards the local Maxwellian at a fixed rate $1/\tau$. 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 $H$-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.

Setting

Velocities and positions range over $\mathbb R^3$. A distribution function is a map $f : \mathbb R^3 \to \mathbb R$ 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 $1$. Its moments are

$$\rho[f] = \int f\,\mathrm dv, \qquad u[f] = \frac 1{\rho[f]}\int v\,f\,\mathrm dv, \qquad \theta[f] = \frac 1{3\rho[f]}\int |v-u[f]|^2 f\,\mathrm dv,$$

the mass density, the bulk velocity and the temperature. The Maxwellian with parameters $(\rho,u,\theta)$ is

$$M_{\rho,u,\theta}(v) = \frac{\rho}{(2\pi\theta)^{3/2}} \exp\Big(-\frac{|v-u|^2}{2\theta}\Big),$$

and the local Maxwellian of $f$ is $f^{(0)} = M_{\rho[f],\,u[f],\,\theta[f]}$: the Maxwellian carrying the same three moments as $f$. The BGK collision operator with relaxation time $\tau>0$ is

$$C[f] = -\frac 1\tau\big(f - f^{(0)}\big),$$

and the Boltzmann equation with this operator is

$$\frac{\partial f}{\partial t} + v\cdot\nabla_x f = C[f].$$

In the slab geometry of parts (c)-(d) of the source, $x=(x,y,z)$, $u=(u,0,0)$, $v=(v,v_\perp)$ with $v_\perp=(v_y,v_z)$, and $f$ is independent of $y$ and $z$; the reduced fields are $g=\int f\,\mathrm dv_\perp$ and $h=\int |v_\perp|^2 f\,\mathrm dv_\perp$.

Formalization targets

Goal — the BGK $H$-theorem with its equality case

$$\int \mathrm dv\,(\log f)\,C[f] \le 0, \qquad\text{with equality iff } f = f^{(0)} \text{ almost everywhere.}$$

This is part (b) of the source question, including the answer to "under what conditions does equality hold". It is stated for every admissible $f$ and every $\tau>0$; it fixes no rate and no constant, so it is not invalidated by sharper quantitative versions.

Milestones

1. The Gaussian moments of $M_{\rho,u,\theta}$: mass $\rho$, momentum $\rho u$, and central second moment $3\rho\theta$; consequently $M_{\rho,u,\theta}$ is its own local Maxwellian.
2. Part (a): $\int C[f]\,\mathrm dv = 0$, $\int v\,C[f]\,\mathrm dv = 0$, $\int |v|^2 C[f]\,\mathrm dv = 0$ — the conservation of $\rho$, $u$ and $\theta$ by the collision operator.
3. The inequality of part (b) on its own.
4. Maxwellians, viewed as $x$- and $t$-independent distributions, solve the BGK equation.
5. Part (c): $\int M\,\mathrm dv_\perp = g^{(0)}$ and $\int |v_\perp|^2 M\,\mathrm dv_\perp = 2\theta\,g^{(0)}$, where $g^{(0)}(v)=\rho(2\pi\theta)^{-1/2}\exp(-(v-u)^2/2\theta)$, together with the expressions for $\rho$, $u$, $\theta$ in the reduced system.
6. Part (d): the quantities $T = -2\rho\theta + \int h\,\mathrm dv$ and $q = \tfrac12\int w^3 g\,\mathrm dv + \tfrac12\int w\,h\,\mathrm dv$ (with $w=v-u$) vanish when $g=g^{(0)}$ and $h=h^{(0)}$.

Significance

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 $H$-theorem: it forces the entropy $-\int f\log f\,\mathrm dv$ 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 $\mathbb R^3$ 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.

Difficulty

The obvious computation for the $H$-theorem — expand $\int (\log f)(f-f^{(0)})$ and integrate term by term — does not by itself give a sign: $\log f$ has no sign, and neither does $f - f^{(0)}$. The argument needs the conservation identities as an input, because they are what allows $\log f^{(0)}$, which is a quadratic polynomial in $v$, 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 $f = f^{(0)}$, and the strictness of $(\log a - \log b)(a-b) > 0$ for $a \ne b$ must be used pointwise.

Formalization scope

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 $\mathbb R^3 \to \mathbb R$ 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 $(2\pi\theta)^{3/2}$, so $\theta>0$ is required wherever it appears. The relaxation time satisfies $\tau>0$.

Two traps are worth naming. First, in Lean the integral of a non-integrable function is $0$ 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 $f$ 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 $\mathbb R\to\mathbb R$. The Gaussian moment lemmas produced here are reusable for any Maxwellian-based kinetic model; contributions that add Mathlib-level lemmas on Gaussian moments in $\mathbb R^n$, rather than ad-hoc computations, are especially welcome.

Selected references

• P. L. Bhatnagar, E. P. Gross, M. Krook, A model for collision processes in gases. I. Small amplitude processes in charged and neutral one-component systems, Physical Review 94 (1954) 511-525. https://doi.org/10.1103/PhysRev.94.511
• C. Cercignani, The Boltzmann Equation and Its Applications, Applied Mathematical Sciences 67, Springer, 1988. https://doi.org/10.1007/978-1-4612-1039-9
• Oxford MMathPhys Kinetic Theory examination paper A15089W1, Hilary Term 2019, Question 1. https://web.archive.org/web/20250913150648/https://mmathphys.physics.ox.ac.uk/sites/default/files/mmathphys/documents/media/kt_2019.pdf