Mathematical Physics

Motivation

General relativity is summed up, in S. M. Carroll's A No-Nonsense Introduction to General Relativity (2001), by two statements: spacetime is a curved pseudo-Riemannian manifold with a metric of signature $(-+++)$, and the metric obeys Einstein's equation $R_{\mu\nu}-\frac12Rg_{\mu\nu}=8\pi GT_{\mu\nu}$. The first exact solution of that equation, and still the most important one, is the Schwarzschild metric: it describes the gravitational field of the Sun outside its surface, the classical tests of GR (perihelion precession, light bending), and non-rotating black holes. Carroll's notes state its key property in one sentence: for a spherically symmetric metric, the vacuum equation has a unique solution, (72) — Birkhoff's theorem. This mission is the first of a series formalizing the capstone results of those notes.

Setting

We work in a single coordinate chart of four-dimensional spacetime. A point is $x=(x^0,x^1,x^2,x^3)\in\mathbb R^4$; a metric is a field $x\mapsto g_{\mu\nu}(x)$ of real symmetric $4\times4$ matrices of signature $(-+++)$, i.e. congruent to $\eta=\mathrm{diag}(-1,1,1,1)$. From $g$ and its inverse $g^{\mu\nu}$ one builds, exactly as in Carroll's equations:

• the Christoffel symbols $\Gamma^\sigma_{\mu\nu}=\frac12g^{\sigma\rho}(\partial_\mu g_{\nu\rho}+\partial_\nu g_{\rho\mu}-\partial_\rho g_{\mu\nu})$ (36) and the covariant derivative (35);
• the Riemann tensor $R^\sigma{}_{\mu\alpha\beta}=\partial_\alpha\Gamma^\sigma_{\mu\beta}-\partial_\beta\Gamma^\sigma_{\mu\alpha}+\Gamma^\sigma_{\alpha\lambda}\Gamma^\lambda_{\mu\beta}-\Gamma^\sigma_{\beta\lambda}\Gamma^\lambda_{\mu\alpha}$ (44);
• the Ricci tensor $R_{\alpha\beta}=R^\lambda{}_{\alpha\lambda\beta}$ (45), Ricci scalar $R=g^{\mu\nu}R_{\mu\nu}$ (46) and Einstein tensor $G_{\mu\nu}=R_{\mu\nu}-\frac12Rg_{\mu\nu}$ (50).

In spherical coordinates $(t,r,\theta,\phi)=(x^0,x^1,x^2,x^3)$ the general spherically symmetric metric is (71)

$$ds^2=-A(r,t)\,dt^2+B(r,t)\,dr^2+r^2(d\theta^2+\sin^2\theta\,d\phi^2),$$

and the Schwarzschild metric (72) is the case $A=1-2Gm/r$, $B=(1-2Gm/r)^{-1}$.

Target

The goal is the uniqueness statement of §6 of the notes, in the form: for $A,B$ smooth and positive on a rectangle $(r_1,r_2)\times(t_1,t_2)$ with $r_1\ge0$,

$$R_{\mu\nu}\big[-A\,dt^2+B\,dr^2+r^2d\Omega^2\big]=0\iff\exists\,m,\ f>0:\ A=f(t)\Big(1-\frac{2Gm}{r}\Big),\ B=\Big(1-\frac{2Gm}{r}\Big)^{-1}.$$

The milestones follow the notes in order:

1. eqs. (18)–(20): Minkowski space in spherical coordinates;
2. eq. (25): $g^{\mu\nu}g_{\mu\nu}=4$;
3. after eq. (36): $\Gamma^\sigma_{\mu\nu}=\Gamma^\sigma_{\nu\mu}$;
4. eq. (37): metric compatibility $\nabla_\sigma g_{\mu\nu}=0=\nabla_\sigma g^{\mu\nu}$;
5. eq. (47): the algebraic symmetries of $R_{\mu\nu\rho\sigma}$;
6. eq. (48): $R_{\mu\nu}=R_{\nu\mu}$;
7. eq. (49): the Bianchi identity $\nabla_{[\lambda}R_{\mu\nu]\rho\sigma}=0$;
8. eq. (51): the contracted Bianchi identity $\nabla_\mu G^{\mu\nu}=0$;
9. eq. (67): $-R=8\pi GT$;
10. eq. (68): the trace-reversed Einstein equation;
11. eq. (69): in vacuum, Einstein's equation is $R_{\mu\nu}=0$;
12. eq. (72): the Schwarzschild metric is Ricci-flat for $r>0$, $r\ne2Gm$;
13. Birkhoff's theorem (the "only if" direction of the goal);
14. eqs. (73)–(75): Kruskal coordinates, showing $r=2Gm$ is a coordinate singularity.

Significance

The result. Birkhoff's theorem says the exterior field of any spherically symmetric body — static, pulsating or collapsing — is the Schwarzschild field, determined by a single constant $m$. It is why the Schwarzschild solution governs the solar system and spherical collapse, and why spherically symmetric gravitational radiation does not exist. The identities (37), (47)–(51) and (67)–(69) are the working toolkit of every GR computation; (51) is what makes Einstein's equation consistent with local energy–momentum conservation.

Formalizing it. All results here are classical and proved in the textbooks. The value of the mission is a machine-checked, coordinate-level development of the curvature identities in Carroll's exact conventions, and a checked proof of Birkhoff's theorem, which requires solving the vacuum equations as a system of PDEs rather than verifying a given solution. The platform already contains a separate Einstein-field-equations development (built from a Wikipedia-based definition file with a slightly different index placement) in which Ricci-flatness of the Schwarzschild metric is proved; this mission uses its own Carroll-faithful definitions, and that earlier work may help with milestone 12.

Difficulty

Verifying that a given metric is Ricci-flat (milestone 12) is a long but mechanical computation of derivatives of explicit functions. The goal is different in kind: in the "only if" direction one must extract from $R_{\mu\nu}=0$ that $\partial_tB=0$ (from $R_{tr}=0$), integrate an ODE in $r$ to get $B=(1-C/r)^{-1}$ with $C$ independent of $t$, and then show $A/(1-C/r)$ depends on $t$ only — all with the coordinate derivatives of the formal definitions, inside a region where $A,B$ are only known to be smooth and positive. The general identities (47)–(51) need symmetry of second and third derivatives and the derivative of the matrix inverse.

Formalization scope

• Everything lives in one chart: Coord = Fin 4 → ℝ, a metric is a function Coord → Matrix (Fin 4) (Fin 4) ℝ, partial derivatives are Fréchet derivatives in coordinate directions. All functions are total: non-differentiable points give derivative $0$, singular matrices have inverse $0$, and $a/0=0$. For that reason every statement names the open region (smoothness, signature $(-+++)$, $r>0$, $r\ne2Gm$, $0<\theta<\pi$) on which it is claimed.
• "Spacetime metric on $U$" means: $U$ open, components $C^\infty$ on $U$, and $g(y)$ congruent to $\eta$ for every $y\in U$ (Carroll's standing assumption that the metric has signature $(-+++)$).
• The goal is stated on a coordinate rectangle $(r_1,r_2)\times(t_1,t_2)$ with the angular coordinates ranging over $0<\theta<\pi$, $\phi\in\mathbb R$. The uniqueness is up to rescaling $t$ (the factor $f(t)$); omitting $f$ would make the statement false.
• Kruskal "takes the form" is encoded as the change-of-variables identity $J^{\mathsf T}KJ=g_{\text{Schw}}$, with the implicit relation (75) as a separate conclusion.
• Reusable beyond this mission: the definition file CarrollGR_Defs (Christoffel symbols, covariant derivatives, curvature, Einstein tensor in coordinates) is shared by the whole series. Contributions welcome: general lemmas about partialD of products, quotients and matrix inverses, and a tensoriality lemma for the Ricci tensor under changes of coordinates.

Selected references

• S. M. Carroll, A No-Nonsense Introduction to General Relativity, lecture notes, 2001 (the source; equation numbers above refer to it).
• S. M. Carroll, Lecture Notes on General Relativity, 1997, arXiv:gr-qc/9712019 (the full notes of which the source is an abridgment).
• R. M. Wald, General Relativity, University of Chicago Press, 1984.

Motivation

The bosonic string can be quantized consistently only in $D=26$ spacetime dimensions. In lightcone quantization this appears in two ways in David Tong's Cambridge Part III lecture notes. First (Sections 2.2.2–2.3), the normal-ordering constant $a$ in the mass formula $M^2=\frac{4}{\alpha'}(N-a)$ is identified with a regularized Casimir energy $a=\frac{D-2}{24}$, using $\sum_{n\ge1}n$ "$=$" $-\frac1{12}$; Lorentz invariance then forces the first excited states to be massless, which happens only for $D=26$. Second (Section 2.4), the commutator $[M^{i-},M^{j-}]$ of lightcone Lorentz generators, which must vanish for the quantum theory to be Lorentz invariant, is proportional to a coefficient that vanishes for all oscillator levels $n$ exactly when $D=26$ and $a=1$ (Goddard–Goldstone–Rebbi–Thorn 1973).

Setting

Let $D\ge2$ be the number of spacetime dimensions, so there are $D-2$ transverse oscillator directions, and let $\alpha'>0$ be the Regge slope. In lightcone gauge the mass of a closed-string state at level $N=\tilde N$ is (2.25)

$$M^2=\frac{4}{\alpha'}(N-a),$$

with an undetermined normal-ordering constant $a$. The heuristic evaluation of $a$ replaces the divergent zero-point sum $\frac{D-2}2\sum_{n\ge1}n$ by its cut-off regularization $\sum_{n\ge1}ne^{-\epsilon n}$, or by the Riemann zeta function value $\zeta(-1)$, giving $a=\frac{D-2}{24}$ (2.26). The first excited states $\tilde\alpha^i_{-1}\alpha^j_{-1}|0;p\rangle$ (2.28) are $(D-2)^2$ in number and have $M^2=\frac4{\alpha'}\bigl(1-\frac{D-2}{24}\bigr)$. In one sector the level-2 states are $\alpha^i_{-1}\alpha^j_{-1}|0\rangle$ (unordered pairs $\{i,j\}$, since the oscillators commute) and $\alpha^i_{-2}|0\rangle$. Finally, Section 2.4 states that

$$[M^{i-},M^{j-}]=\frac{2}{(p^+)^2}\sum_{n>0}\left(\Big[\frac{D-2}{24}-1\Big]n+\frac1n\Big[a-\frac{D-2}{24}\Big]\right)\bigl(\alpha^i_{-n}\alpha^j_n-\alpha^j_{-n}\alpha^i_n\bigr)+(\alpha\leftrightarrow\tilde\alpha).$$

Formalization targets

Goal: the anomaly coefficient vanishes iff $D=26$, $a=1$

For $D\in\mathbb N$ and $a\in\mathbb R$,

$$\Big(\forall n\ge1:\ \Big[\frac{D-2}{24}-1\Big]n+\frac1n\Big[a-\frac{D-2}{24}\Big]=0\Big)\iff\bigl(D=26\ \text{and}\ a=1\bigr).$$

Milestones (in the order of the notes)

1. Cut-off regularization: $\sum_{n\ge1}ne^{-\epsilon n}=\frac1{\epsilon^2}-\frac1{12}+O(\epsilon)$ as $\epsilon\to0^+$.
2. Zeta-function regularization: $\zeta(-1)=-\frac1{12}$.
3. First excited states are massless iff $D=26$.
4. Level-2 counting: $\frac12(D-2)(D-1)+(D-2)=\frac12D(D-1)-1$, the dimension of the traceless symmetric tensor representation of $SO(D-1)$.

Significance

The result. The critical dimension is the single most-quoted prediction of the bosonic string, and the pair $(D,a)=(26,1)$ fixes the entire lightcone spectrum: the tachyon $M^2=-4/\alpha'$, the massless graviton, $B$-field and dilaton, and the massive tower $M^2=4(N-1)/\alpha'$.

Formalizing it. This mission formalizes the mathematical steps of Tong's lightcone derivation: the two regularizations of $\sum n$, the mass-shell and state-counting arithmetic, and the final algebraic step of the Lorentz-algebra argument. It does not formalize the operator computation of $[M^{i-},M^{j-}]$ in the lightcone Fock space, which Tong quotes ("After a tedious computation, one finds ...") without derivation; that computation is a natural follow-up mission. The value $\zeta(-1)=-1/12$ is already available in Mathlib through the Bernoulli-number formula for $\zeta$ at negative integers.

Difficulty

The individual statements are elementary once formalized; the difficulty is faithfulness rather than proof. The regularized sum is an asymptotic statement whose leading term diverges, so it has to be stated as an $O(\epsilon)$ remainder along $\epsilon\to0^+$ rather than as an equation; and the goal is a statement for all levels $n\ge1$, where a single level ($n=1$) only forces $a=1$ and two levels are needed to force $D=26$.

Formalization scope

The dimension $D$ is a natural number and the normal-ordering constant $a$ a real number. The regularized sum is Mathlib's tsum of $n e^{-\epsilon n}$ over $n\in\mathbb N$ (the $n=0$ term vanishes), and the asymptotic claim uses Mathlib's big-O along the right neighbourhood filter of $0$. Level-2 states of one sector are counted as unordered pairs with repetition of transverse indices (Mathlib's Sym2 (Fin (D-2))) plus the $D-2$ states $\alpha^i_{-2}|0\rangle$; natural-number subtraction and division are safe because $D\ge2$ is assumed and $D(D-1)$ is even. The zeta function is Mathlib's riemannZeta, i.e. the analytic continuation.

Selected references

• D. Tong, String Theory, Cambridge Part III lecture notes, 2009, Sections 2.2.2–2.4. http://www.damtp.cam.ac.uk/user/tong/string.html (arXiv:0908.0333)
• P. Goddard, J. Goldstone, C. Rebbi, C. B. Thorn, Quantum dynamics of a massless relativistic string, Nucl. Phys. B 56 (1973) 109. https://doi.org/10.1016/0550-3213(73)90223-X
• J. Polchinski, String Theory, Vol. 1, Cambridge University Press, 1998, Section 1.3.
• B. Zwiebach, A First Course in String Theory, 2nd ed., Cambridge University Press, 2009, Chapter 12.

Motivation

In 1973 Bardeen, Carter and Hawking showed that stationary black holes in general relativity obey four laws with the same structure as the laws of thermodynamics, with the surface gravity $\kappa$ of the horizon playing the role of temperature and the horizon area $A$ the role of entropy (Bardeen–Carter–Hawking 1973). Two years later Hawking showed that quantum fields near a black hole produce thermal radiation at temperature $T_{BH}=\kappa/2\pi$ (Hawking 1975), which turned the analogy into an identification, with entropy $S_{BH}=A/4$.

The M.Sc. dissertation Termodinâmica de Buracos Negros (F. H. de C. Menezes, UFMG, 2021) presents this construction for the Kerr black hole, the rotating stationary solution of Einstein's vacuum equations. The first law, eq. (3.79), is its central quantitative statement:

$$\delta M = \frac{\kappa}{8\pi}\,\delta A + \Omega_H\,\delta J,$$

relating first-order changes of mass $M$, horizon area $A$ and angular momentum $J$ between neighbouring Kerr black holes, where $\Omega_H$ is the angular velocity of the horizon.

Timeline: Kerr found the rotating solution (1963); Smarr derived the mass formula $M = \kappa A/4\pi + 2\Omega_H J$ (1973); Bardeen, Carter and Hawking stated the four laws (1973); Hawking derived the thermal emission (1974–75).

Setting

Units are geometrized, $G=c=1$ (and $\hbar=k_B=1$ for quantum quantities). A Kerr black hole has mass $M>0$ and rotation parameter $a$ with $a^2\le M^2$; its angular momentum is $J=Ma$. In Boyer–Lindquist coordinates $(t,r,\theta,\varphi)$ the metric involves

$$\Delta = r^2-2Mr+a^2,\qquad \Sigma = r^2+a^2\cos^2\theta,$$

with angular components $g_{\theta\theta}=\Sigma$ and $g_{\varphi\varphi} = \dfrac{(r^2+a^2)^2-\Delta a^2\sin^2\theta}{\Sigma}\sin^2\theta$. The zeros of $\Delta$ are $r_\pm = M\pm\sqrt{M^2-a^2}$; the event horizon is $r=r_+$.

• The horizon area $A$ is the area of the cross-section $t=\text{const}$, $r=r_+$, computed from the induced metric: $A=\int_0^\pi\int_0^{2\pi}\sqrt{g_{\theta\theta}g_{\varphi\varphi}}\,d\varphi\,d\theta$ at $r=r_+$.
• The surface gravity is $\kappa = \dfrac{\sqrt{M^2-a^2}}{2M(M+\sqrt{M^2-a^2})}$ (eq. (3.3)).
• The angular velocity of the horizon is $\Omega_H = \dfrac{a}{2M(M+\sqrt{M^2-a^2})}$ (eq. (2.42)).

A Kerr black hole is non-extremal when $a^2<M^2$, equivalently $|J|<M^2$.

Formalization targets

Goal — the first law (eq. (3.79))

Regard $A,\kappa,\Omega_H$ as functions of $(M,J)$ with $a=J/M$. For $M>0$ and $J^2<M^4$, the area is differentiable at $(M,J)$ and, as linear forms in $(\delta M,\delta J)$,

$$\delta M = \frac{\kappa}{8\pi}\,\delta A + \Omega_H\,\delta J .$$

Milestones, in the dissertation's order

1. Eq. (2.42): $\Omega_H = a/(r_+^2+a^2)$.
2. Eq. (3.4): $\kappa = (r_+-r_-)/(2(r_+^2+a^2))$.
3. Eq. (3.44): $A = 8\pi M\left(M+\sqrt{M^2-a^2}\right)$.
4. Eq. (3.43), Smarr formula: $M = \kappa A/4\pi + 2\Omega_H J$.
5. Eq. (3.78), variation of $\kappa$: $\delta M = -\frac{A}{4\pi}\delta\kappa - 2J\,\delta\Omega_H$.
6. Eq. (3.81) and the following remark: $\kappa=0 \iff |J|=M^2$.
7. Eq. (4.137): $M(t) = (M_0^3-t/256\pi)^{1/3}$ solves $\dot M = -(768\pi)^{-1}M^{-2}$, $M(0)=M_0$.

In the dissertation the first law is the sum of the variation (3.45) of the Smarr formula and the relation (3.78).

Significance

The first law is the identity behind the identification $T_{BH}=\kappa/2\pi$, $S_{BH}=A/4$: with these values it becomes $\delta M = T_{BH}\,\delta S_{BH} + \Omega_H\,\delta J$, the ordinary first law of thermodynamics for a rotating body. The Smarr formula is its integrated (Euler-relation) form, and the vanishing of $\kappa$ at extremality underlies the dissertation's formulation of the third law.

All results are classical and proved in the literature. The contribution of the mission is a machine-checked version of the explicit Kerr relations, with the horizon area computed from the metric rather than taken as given, and a check of the dissertation's formulas. One such check is already recorded: the coefficient $-2\pi J$ printed in eq. (3.78) conflicts with the dissertation's own eqs. (3.70) and (3.77), which give $-2J$, the value required for (3.79); the milestone uses $-2J$.

Difficulty

The dissertation derives the first law geometrically, from Komar integrals and a perturbation of the horizon Killing field. That route needs Lorentzian geometry, Killing horizons and Stokes' theorem on manifolds, which the Lean library does not provide. The explicit route through the Kerr formulas avoids this, but has its own obstacles: the horizon area is a double integral of a square root of a rational trigonometric expression that simplifies only on the horizon, where $\Delta(r_+)=0$; and the differentials involve $\sqrt{M^2-J^2/M^2}$, which is not differentiable at extremality, so the non-extremal hypothesis must be used when differentiating.

Formalization scope

All quantities are real-valued functions of real arguments, defined in one definition file in the namespace KerrBlackHoleThermo. Every theorem restricts to the physical range explicitly ($M>0$ and $a^2\le M^2$, or $M>0$ and $J^2<M^4$ for statements involving derivatives), so Lean's conventions for $\sqrt{\cdot}$ of negative numbers and division by zero do not enter the physical content. First-order variations "between two neighbouring Kerr configurations" are formalized as Fréchet derivatives (HasFDerivAt) of the explicit family in the coordinates $(M,J)$; the first law is an identity of linear forms on $\mathbb R^2$. The horizon area is defined as a metric integral, not as the closed form (3.44), so the goal cannot be reduced to a pure algebraic identity by definition.

Out of scope: the general-spacetime versions of the zeroth, second (area theorem) and third laws, which need a theory of Lorentzian manifolds, event horizons and energy conditions, and the quantum field theory derivation of Hawking radiation in Chapter 4. Contributions building that infrastructure are welcome as separate missions.

Selected references

• F. H. de C. Menezes, Termodinâmica de Buracos Negros, M.Sc. dissertation, Universidade Federal de Minas Gerais, 2021 (the source of this mission).
• J. M. Bardeen, B. Carter, S. W. Hawking, The four laws of black hole mechanics, Commun. Math. Phys. 31 (1973) 161–170. https://doi.org/10.1007/BF01645742
• S. W. Hawking, Particle creation by black holes, Commun. Math. Phys. 43 (1975) 199–220. https://doi.org/10.1007/BF02345020
• L. Smarr, Mass formula for Kerr black holes, Phys. Rev. Lett. 30 (1973) 71–73. https://doi.org/10.1103/PhysRevLett.30.71
• R. P. Kerr, Gravitational field of a spinning mass as an example of algebraically special metrics, Phys. Rev. Lett. 11 (1963) 237–238. https://doi.org/10.1103/PhysRevLett.11.237
• R. M. Wald, General Relativity, University of Chicago Press, 1984.

Motivation

Since 20 May 2019 the International System of Units (SI) is no longer defined through material artefacts or particular experiments. Instead, the 26th General Conference on Weights and Measures fixed the exact numerical values of seven defining constants and declared that the SI is the system of units in which these constants take these values. The reference text is the BIPM's SI Brochure, 9th edition (2019), bipm.org. Every calibration certificate, every value in the CODATA tables and every textbook formula expressed in SI units rests on this definition.

The mathematical content of the new definition is small but exact: from the seven fixed values, the Brochure derives, for each of the seven base units, an explicit formula expressing that unit as a rational multiple of a product of integer powers of the defining constants (Section 2.3.1), and it asserts that any SI unit can be written through products and quotients of the defining constants (Section 2.2). These are statements about a free abelian group of unit monomials together with exact rational coefficients, so they can be checked completely.

Timeline. 1960: the 11th CGPM establishes the SI with six base units (the mole is added in 1971). 1983: the metre is redefined by fixing the speed of light $c$. 2018–2019: the 26th CGPM (Resolution 1) redefines the kilogram, ampere, kelvin and mole by fixing $h$, $e$, $k$ and $N_A$; the new definitions enter into force on 20 May 2019 and are published in the 9th edition of the SI Brochure.

Setting

A quantity value is written as a number times a unit. In this mission a quantity value is a pair $(x, u)$, written $x\,u$, where $x\in\mathbb R$ is the numerical value and

$$u = \mathrm{s}^{a_1}\,\mathrm{m}^{a_2}\,\mathrm{kg}^{a_3}\,\mathrm{A}^{a_4}\,\mathrm{K}^{a_5}\,\mathrm{mol}^{a_6}\,\mathrm{cd}^{a_7},\qquad a_i\in\mathbb Z,$$

is a unit monomial in the seven base units second, metre, kilogram, ampere, kelvin, mole and candela (Table 2 of the Brochure). Products multiply numerical values and add exponents; quotients and integer powers are defined accordingly; a real number $r$ acts by $r\cdot(x\,u) = (rx)\,u$. Two quantity values are equal exactly when they have the same numerical value and the same seven exponents.

The derived units needed in Section 2.2 are $\mathrm{Hz}=\mathrm s^{-1}$, $\mathrm J=\mathrm{kg\,m^2\,s^{-2}}$, $\mathrm C=\mathrm{A\,s}$, $\mathrm W=\mathrm{kg\,m^2\,s^{-3}}$, $\mathrm{sr}=\mathrm{m^2\,m^{-2}}$ and $\mathrm{lm}=\mathrm{cd\,sr}$. The seven defining constants (Section 2.2, Table 1) are

$$\Delta\nu_{\mathrm{Cs}} = 9\,192\,631\,770\ \mathrm{Hz},\quad c = 299\,792\,458\ \mathrm{m\,s^{-1}},\quad h = 6.626\,070\,15\times10^{-34}\ \mathrm{J\,s},$$ $$e = 1.602\,176\,634\times10^{-19}\ \mathrm C,\quad k = 1.380\,649\times10^{-23}\ \mathrm{J\,K^{-1}},\quad N_A = 6.022\,140\,76\times10^{23}\ \mathrm{mol^{-1}},\quad K_{\mathrm{cd}} = 683\ \mathrm{lm\,W^{-1}}.$$

Formalization targets

Goal (Section 2.2, p. 127)

"The seven constants are chosen in such a way that any unit of the SI can be written either through a defining constant itself or through products or quotients of defining constants." Formally: for every exponent vector $u\in\mathbb Z^7$ there are a real number $a$ and integers $n_1,\dots,n_7$ with

$$\mathrm{s}^{u_1}\cdots\mathrm{cd}^{u_7} \;=\; a\cdot \Delta\nu_{\mathrm{Cs}}^{\,n_1}\, c^{\,n_2}\, h^{\,n_3}\, e^{\,n_4}\, k^{\,n_5}\, N_A^{\,n_6}\, K_{\mathrm{cd}}^{\,n_7}.$$

Milestones (Section 2.3.1, pp. 130–135)

The seven exact expressions of the base units in terms of the defining constants, each in both forms displayed by the Brochure:

$$1\ \mathrm s = \frac{9\,192\,631\,770}{\Delta\nu_{\mathrm{Cs}}},\qquad 1\ \mathrm m = \frac{9\,192\,631\,770}{299\,792\,458}\,\frac{c}{\Delta\nu_{\mathrm{Cs}}},\qquad 1\ \mathrm{kg} = \frac{(299\,792\,458)^2}{(6.626\,070\,15\times10^{-34})(9\,192\,631\,770)}\,\frac{h\,\Delta\nu_{\mathrm{Cs}}}{c^2},$$ $$1\ \mathrm A = \frac{\Delta\nu_{\mathrm{Cs}}\,e}{(9\,192\,631\,770)(1.602\,176\,634\times10^{-19})},\quad 1\ \mathrm K = \frac{1.380\,649\times10^{-23}}{(6.626\,070\,15\times10^{-34})(9\,192\,631\,770)}\,\frac{\Delta\nu_{\mathrm{Cs}}\,h}{k},$$ $$1\ \mathrm{mol} = \frac{6.022\,140\,76\times10^{23}}{N_A},\qquad 1\ \mathrm{cd} = \frac{(\Delta\nu_{\mathrm{Cs}})^2\,h\,K_{\mathrm{cd}}}{(6.626\,070\,15\times10^{-34})(9\,192\,631\,770)^2\,683},$$

together with the rounded decimal values quoted for the five non-trivial numerical factors ($\approx 30.663\,319$, $1.475\,5214\times10^{40}$, $6.789\,687\times10^{8}$, $2.266\,6653$, $2.614\,830\times10^{10}$).

Significance

The result itself. The milestones are the operational content of the 2019 redefinition: they say how each base unit is recovered from the fixed constants, and together they show that the matrix of exponents of the seven defining constants with respect to the seven base units is invertible over $\mathbb Z$, which is exactly what the goal asserts. Every derived unit is a monomial in base units, so the goal also covers the derived units.

Formalizing it. The platform already has purely numerical checks of these formulas (rational identities of the form "coefficient $\times$ constant values $=1$"). This mission adds a model with units as first-class data: equalities are between quantity values, so a wrong exponent or a missing factor of $c^2$ is a type-level failure, not a silent numerical coincidence. The definition file is reusable for later missions in this series (derived units, Tables 4–8, prefixes).

Difficulty

The individual milestones are exact finite computations; the only care needed is bookkeeping of exponents and of large decimal constants. The goal requires choosing the integer exponents $n_i$ as functions of $u$ and showing that the unit monomials match componentwise — an argument that the exponent matrix is unimodular, not merely invertible over $\mathbb Q$. Solving the system over the rationals is not enough.

Formalization scope

• Numerical values are real numbers; exponents are integers; base units form a seven-element type. Equality of quantity values is equality of the numerical value and of all seven exponents.
• The steradian is modelled as $\mathrm m^2\,\mathrm m^{-2}$, i.e. the unit of dimension one, as in the Brochure (Table 4); consequently $\mathrm{lm} = \mathrm{cd}$ in this model.
• Real division and inversion follow Mathlib's conventions ($0^{-1}=0$); all constants used here are non-zero, so this convention never enters the milestones.
• The goal allows an arbitrary real coefficient $a$; since unit monomials have numerical value $1$, $a$ is forced to be non-zero, so the statement cannot be satisfied trivially.
• Out of scope: the physical realization of units (Section 2.3.2 onward), uncertainties, and the definitions of the non-coherent and non-SI units.

Selected references

• BIPM, The International System of Units (SI), 9th edition, 2019. ISBN 978-92-822-2272-0. https://www.bipm.org/en/publications/si-brochure
• CGPM, Resolution 1 of the 26th meeting (2018), On the revision of the International System of Units (SI). https://www.bipm.org/en/committees/cg/cgpm/26-2018/resolution-1

Motivation

Neutrino oscillations are an interference phenomenon, so they are sensitive to any mechanism that degrades quantum coherence during propagation. The open quantum system description models such effects without specifying their microscopic origin: the neutrino is treated as a subsystem whose reduced density matrix evolves under a Markovian master equation. The dissertation of G. F. S. Alves (Instituto de Física, Universidade de São Paulo, 2020) develops this framework for two and three neutrino generations and uses public IceCube atmospheric data to constrain the new parameters. Its two-generation chapter derives closed-form oscillation probabilities under several choices of the dissipative term; this mission formalizes that chapter's mathematical content.

Setting

A density matrix is a positive semidefinite complex matrix of unit trace. For a two-level system (two neutrino mass eigenstates) the reduced state $\rho(t)\in\mathbb C^{2\times2}$ obeys the Lindblad equation with constant coefficients,

$$\dot\rho=-i[H,\rho]+D[\rho],\qquad D[\rho]=\tfrac12\sum_{i,j=1}^3 a_{ij}\bigl(2\sigma_i\rho\sigma_j-\{\sigma_j\sigma_i,\rho\}\bigr),$$

where $\sigma_1,\sigma_2,\sigma_3$ are the Pauli matrices and the $3\times3$ Kossakowski matrix $a=(a_{ij})$ is Hermitian positive semidefinite (the condition for complete positivity). In the mass basis the vacuum Hamiltonian is $H=\operatorname{diag}(0,\Delta m^2/2E)$, and the mixing matrix with Majorana phase $\alpha$ is

$$U=\begin{pmatrix}\cos\theta&e^{i\alpha}\sin\theta\\-e^{-i\alpha}\sin\theta&\cos\theta\end{pmatrix}.$$

The muon neutrino is produced in the state $\rho_\mu(0)=U^\dagger|\nu_1\rangle\langle\nu_1|U$, and the survival probability after a baseline $L$ is $P_{\nu_\mu\to\nu_\mu}=\operatorname{Tr}\{\rho(L)\rho_\mu(0)\}$. The linear entropy $S_l(\rho)=1-\operatorname{Tr}\rho^2$ and the von Neumann entropy $S(\rho)=-\operatorname{Tr}\rho\ln\rho$ measure the loss of purity.

Formalization targets

Goal: decoherent survival probability, eq. (3.24)

For the pure-decoherence Kossakowski matrix $a=\operatorname{diag}(0,0,\gamma)$, $\gamma\ge0$, every solution with $\rho(0)=\rho_\mu(0)$ satisfies, for all $L\ge0$,

$$P_{\nu_\mu\to\nu_\mu}=\frac14\Bigl(3+\cos4\theta+2e^{-2\gamma L}\cos\Bigl(\frac{\Delta m^2}{2E}L\Bigr)\sin^22\theta\Bigr).$$

Milestones

1. Range of the linear entropy, eq. (2.45), and of the von Neumann entropy, eqs. (2.40)–(2.41).
2. Non-negativity of the relative entropy, eq. (2.43).
3. Entropy increase whenever the maximally mixed state is a fixed point of $D$ (Appendix B.1, two-level case).
4. Pauli-basis form of the Dissipator, eq. (3.5).
5. Average-energy conservation holds iff $a=\operatorname{diag}(0,0,\gamma)$, eqs. (3.19)–(3.22).
6. The evolved state in case (1), eq. (3.23), and the population in case (4), eq. (3.26).

Significance

The goal is the formula used in the dissertation to show how decoherence damps oscillations: it reduces to the standard vacuum formula at $\gamma=0$, it tends to $\tfrac14(3+\cos4\theta)$ at large $L$ instead of oscillating, and it does not depend on $\alpha$. The milestones connect the formula to the structure of the Lindblad generator (energy conservation singles out this Dissipator) and to entropy growth. A formal development yields a checked two-level Lindblad toolkit (Pauli expansion of dissipators, explicit solutions, entropy bounds) reusable in other open-system missions. The results are proved informally in the source; none is known to be machine-checked.

Difficulty

The ODE part requires a uniqueness argument for a linear matrix ODE on $[0,\infty)$ given only one-sided derivatives at $t=0$, plus exact trigonometric bookkeeping. The entropy milestones need spectral calculus for Hermitian matrices (Klein's inequality, concavity of $-x\ln x$) and, for Appendix B.1, the monotonicity of relative entropy under completely positive trace-preserving maps together with complete positivity of Lindblad semigroups, neither of which is expected to be available off the shelf.

Formalization scope

Matrices are Matrix (Fin 2) (Fin 2) ℂ; the Kossakowski matrix is Matrix (Fin 3) (Fin 3) ℂ with indices $0,1,2$ for the thesis' $1,2,3$. Solutions are curves $\mathbb R\to\mathbb C^{2\times2}$ satisfying the Lindblad equation entrywise for $t\ge0$ (derivatives within $[0,\infty)$); the exponential $e^{\mathcal Lt}$ is not used. Entropies use the continuous functional calculus. Two printed formulas are corrected in the drafts: the sign of the $\rho_0\,\mathrm{Im}(a_{ij})$ terms in eq. (3.5), and the overall sign of the off-diagonal entries in eq. (3.23); both corrections are explained in the corresponding items. The two-generation cases (4) and (5) survival probabilities, eqs. (3.25) and (3.27), and the three-generation and IceCube analyses are out of scope.

Selected references

• G. F. S. Alves, Decoherence in Neutrino Oscillations in the IceCube Experiment, MSc dissertation, Instituto de Física, Universidade de São Paulo, 2020.
• G. Lindblad, On the generators of quantum dynamical semigroups, Commun. Math. Phys. 48 (1976) 119–130, https://doi.org/10.1007/BF01608499
• V. Gorini, A. Kossakowski, E. C. G. Sudarshan, Completely positive dynamical semigroups of N-level systems, J. Math. Phys. 17 (1976) 821–825, https://doi.org/10.1063/1.522979

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) reaches the Fano plane — the seven-point, seven-line configuration behind the seven imaginary units of the octonions — by a combinatorial route (C1 Formal Proofs, §3). Points are arranged in Steiner triple systems, and each point of each line is given one of three roles. The model's claim is that the role postulates alone force the number of points to be exactly seven. This mission proves that claim.

What this mission does NOT prove.

• Not that the system is the Fano plane. It proves the point count is $7$. That every Steiner triple system on $7$ points is the Fano plane up to relabelling is a classical result, but it is not formalized here.
• Not the modelling premise. Why lines have three points, and why there are three roles, is an input of the model, not derived here.
• Not the later steps from the Fano plane to the octonions, and from there to the node size $n = 3$ and $\mathfrak{u}(3)$.

Two corrections to C1 §3 built into this mission.

• At least one point is required. The empty system — no points, no lines — satisfies every condition vacuously and has $0$ points, so C1 Theorem 3.6 as stated is false for it. The goal carries the hypothesis $0 < n$. This is proved (in Lean, locally): the empty system is a Steiner triple system with a role colouring, so the statement without $0 < n$ is false.
• C1 Theorem 3.3(a) is not used. Its condition "any two lines meet" does not force $7$ points: it also holds for a single triple ($3$ points) and a single point, where there is no pair of lines to fail. This mission uses the role postulates instead.

Setting

Fix a natural number $n$ and take the points $\{0, \dots, n-1\}$. A Steiner triple system is a family of subsets, called lines, such that

1. every line has exactly $3$ points, and
2. every pair of distinct points lies on exactly one line.

A role colouring assigns to each point $x$ and line $\ell$ a role $\rho(x, \ell) \in \{0, 1, 2\}$ such that

1. the three points of a line get three different roles;
2. completeness: every point takes every role at least once, on some line through it;
3. minimality: every point takes every role at most once — two different lines through $x$ give $x$ different roles.

In Lean these are RolesForceSeven.STS n and RolesForceSeven.RoleColouring S role, with points Fin n and lines Finset (Fin n).

Formalization targets

Goal: the role postulates force exactly seven points

$$n \ge 1,\ \text{a Steiner triple system on } n \text{ points with a role colouring} \;\Longrightarrow\; n = 7 .$$

This is RolesForceSeven.roles_force_seven. It asserts the point count only.

Milestones

1. M1 (replication count). In any Steiner triple system, every point lies on exactly $r$ lines with $2r + 1 = n$.
2. M2 (three lines per point). Under a role colouring, every point lies on exactly $3$ lines.

Corollaries

• A — the Fano plane has a role colouring. The Fano plane on $\{0, \dots, 6\}$, with lines $\{i, i+1, i+3\}$ modulo $7$, admits a role colouring. Without this the goal could be vacuously true.
• B — AG(2, 3) is excluded (C1 Corollary 3.7): no Steiner triple system on $9$ points has a role colouring.

Significance

The result itself. It turns the model's role postulates into a precise count: whatever the Steiner triple system, if it carries a role colouring and has a point, it has exactly seven points. Corollary A shows the conditions are satisfiable, and Corollary B rules out the next Steiner triple system, AG(2, 3), explicitly.

Formalizing it. The C1 statement omits the non-emptiness hypothesis and is false for the empty system; the formal statement makes the hypothesis explicit and shows it is needed. The numerical check (Fano plane: $48$ role colourings; AG(2, 3): $0$; single triple: $0$) is replaced by a proof for every $n$.

Numerical cross-check

system	points	lines through each point	role colourings
Fano plane	7	3	48
AG(2, 3)	9	4	0
single triple	3	1	0
empty system	0	—	vacuous (all conditions hold)

Difficulty

Moderate. The central step is the replication count: the lines through a point $x$ must be shown to cover every other point exactly once, two at a time, which is a double-counting argument over the pairs through $x$. The role postulates then fix the replication number at three. The Fano plane corollary is a finite check.

Formalization scope

• Points are Fin n; lines are finite sets of points, with no ambient geometry assumed.
• The role function is total, Fin n → Finset (Fin n) → Fin 3; only its values on pairs $x \in \ell$ with $\ell$ a line matter.
• Completeness and minimality are both hypotheses; the goal uses both.
• $0 < n$ is necessary: without it the empty system is a counterexample (proved).
• The conclusion is the number $7$, not an isomorphism with the Fano plane.

Selected references

• Wikipedia, Steiner system (Steiner triple systems, replication number). https://en.wikipedia.org/wiki/Steiner_system
• Wikipedia, Fano plane. https://en.wikipedia.org/wiki/Fano_plane
• Wikipedia, Octonion (Fano plane mnemonic for the multiplication of imaginary units). https://en.wikipedia.org/wiki/Octonion

Motivation

Whether the quantization of the gravitational field is observable is a long-standing question at the interface of general relativity and quantum theory. In his 2013 talk Is a Graviton Detectable? (doi:10.1142/S0217751X1330041X), Freeman Dyson examined three families of hypothetical single-graviton detectors and estimated, for each, why it fails: LIGO-type interferometers (Sec. 3), atoms absorbing a graviton by the gravitoelectric effect (Secs. 4–5), and Gertsenshtein photon–graviton conversion in a magnetic field (Secs. 6–7).

Most of the paper consists of order-of-magnitude physical estimates. A part of it, however, consists of precise mathematical statements: exact algebraic consequences of the stated physical relations, and one genuine analytic inequality about the quadrupole factor $Q$ that controls the graviton absorption cross-section of a bound particle. This mission collects those statements.

Setting

Sections 3. Let $c, G, \hbar > 0$ be the speed of light, Newton's constant and the reduced Planck constant. The Planck length is $L_p = (G\hbar/c^3)^{1/2}$ (Eq. (5)). A gravitational wave of strain amplitude $f$ and angular frequency $\omega$ has energy density $E = \frac{c^2}{32\pi G}\omega^2 f^2$ (Eq. (2)); a single graviton of frequency $\omega$ has energy density at most $E_s = \hbar\omega^4/c^3$ (Eq. (3)).

Section 4. For an electron bound in a state with zero angular momentum about the $z$-axis, with real wave function $f(s,z)$ in cylindrical coordinates ($s>0$ the distance from the $z$-axis), let $f' = \partial f/\partial s$ and define

$$Q = \frac{\int_{\mathbb R}\int_0^\infty s^3 [f']^2\, ds\, dz}{2\int_{\mathbb R}\int_0^\infty s\, f^2\, ds\, dz} \qquad \text{(Eq. (16))}.$$

The s-state of Eq. (19) is $f = r^{-n} e^{-r/R}$ with $r = \sqrt{s^2+z^2}$.

Sections 6–7. For a transverse magnetic field $B$, the mixing length is $L = 2c^2/(G^{1/2}B)$ (Eq. (29)) and the photon-to-graviton conversion probability over a distance $D$ is $P = \sin^2(D/L)$ (Eq. (28)). Vacuum nonlinearity slows the photon by the fraction $g = k\alpha B^2/(360\pi^2 H_c^2)$ (Eq. (36)), where $\alpha$ is the fine-structure constant and $H_c$ the critical field, giving the coherence length $L_c = c/(g\omega)$ (Eq. (37)).

Formalization targets

Goal — Eq. (18)

For every nonzero, normalizable axially symmetric wave function with finite $\int s^3 [f']^2$,

$$Q > \tfrac12 .$$

Milestones

• Eq. (17): $\int\!\!\int s^3\,[f' + f/s]^2\, ds\,dz > 0$ (see the note on the sign below).
• Eq. (20): for the s-state (19), $Q = \frac45\left(1 - \frac n6\right)$.
• Eqs. (4), (6): equating (2) and (3) gives $f = (32\pi)^{1/2} L_p\omega/c$, and with $D = c/\omega$, $\delta = fD = (32\pi)^{1/2}L_p$.
• Eq. (8): free mirrors with $M\delta^2 \ge \hbar T$, $T \ge D/c$, $\delta = L_p$ satisfy $D \le GM/c^2$.
• Eq. (10): clamped mirrors with $\delta^2 \ge \hbar D/(Ms)$, $\delta = L_p$, $s < c$ satisfy $GM/c^2 \ge (c/s)D > D$.
• Eqs. (28)–(30): $P \le GB^2D^2/(4c^4)$, with asymptotic equality as $D \to 0^+$.
• Eq. (37): for $k = 4$, $L_c = 90\pi^2 c H_c^2/(\alpha B^2\omega)$.
• Eqs. (38)–(39): if $D \le L_c$ then $P \le 2025\pi^4 G H_c^4/(\alpha^2 c^2 B^2\omega^2)$ (the symbolic form of $P \le 10^{36}/(B^2\omega^2)$).

Significance

Eq. (18) is what allows Dyson to conclude that the averaged absorption cross-section $4\pi^2L_p^2 Q$ (Eq. (14)) is, for every bound particle, of the order of the Planck area; together with Eq. (20) it shows $Q$ is of order unity for tightly bound s-states. The Section 3 bounds are the precise algebraic content of the argument that measuring distances to Planck accuracy forces the apparatus inside its own Schwarzschild radius. The Section 7 bounds are the algebraic content of the argument that vacuum birefringence limits Gertsenshtein conversion.

None of these statements has, to our knowledge, a machine-checked proof. Eq. (18) is a weighted Hardy-type inequality on the half line with sharp constant, applied slice by slice; formalizing it produces reusable one-dimensional weighted Hardy inequalities. Eq. (20) requires explicit Gamma-function integrals in cylindrical coordinates.

Difficulty

For Eq. (18) the difficulty is analytic: the inequality must hold for all admissible $f$, including functions that are not compactly supported and may be singular on the $z$-axis, and it is strict although its sharp constant is not attained. Boundary terms of the integration by parts behind Eq. (17) must be controlled using only the integrability assumptions. The printed Eq. (17) has the sign $f' - f/s$; with that sign the integral is trivially positive and does not imply Eq. (18). The mission uses $f' + f/s$, the sign under which (17) implies (18). The algebraic milestones are elementary.

Formalization scope

All quantities are real. $f : \mathbb R \to \mathbb R \to \mathbb R$ is a function of $(s,z)$; $f'$ is deriv in the first variable; integrals are Lebesgue integrals over the half plane $\{s > 0\}\times\mathbb R$. The admissible class for Eqs. (17)–(18) is: $f(\cdot,z)$ differentiable at every $s>0$, $s f^2$ and $s^3[f']^2$ integrable on the half plane, and $f$ not almost-everywhere zero there. These hypotheses rule out the degenerate reading $Q = 0/0$ (Lean's division returns $0$). Eq. (20) requires $R > 0$ and $n < 3/2$, the range in which the integrals in Eq. (16) converge. Physical constants are arbitrary positive reals; numerical cgs values (e.g. Eqs. (5), (21), (31)) are not formalized. The heuristic parts of the paper (Bohr–Rosenfeld argument, the sum rule (14), astrophysical source estimates, neutrino backgrounds) are out of scope.

Selected references

• F. Dyson, Is a Graviton Detectable?, Int. J. Mod. Phys. A 28 (2013) 1330041. https://doi.org/10.1142/S0217751X1330041X
• T. Rothman and S. Boughn, Can gravitons be detected?, Found. Phys. 36 (2006) 1801. https://doi.org/10.1007/s10701-006-9081-9
• M. E. Gertsenshtein, Wave resonance of light and gravitational waves, Sov. Phys. JETP 14 (1962) 84.

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) aims to obtain all three factors of the Standard Model gauge structure — $U(1)$, $SU(2)$ and $SU(3)$ — from a single linear-algebra statement applied at three node sizes. A node carrying $n$ oscillator pairs has a $2n$-dimensional real state space with a complex structure $J$. Within the model, the couplings that do no net work (passive couplings) are the symmetric matrices, and those that respect $J$ are the ones commuting with it. The claim is that the couplings satisfying both conditions form a real vector space of dimension exactly $n^2$, which is the dimension of the unitary Lie algebra $\mathfrak{u}(n)$ (Unitary group):

node size $n$	admissible dimension	Lie algebra
1	1	$\mathfrak{u}(1)$
2	4	$\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$
3	9	$\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$

The dimension count has so far been checked numerically for $n = 1, \dots, 5$ only, giving $1, 4, 9, 16, 25$. A machine-checked proof covers every $n$, and it is the claim a physicist examining the model would check first.

What this mission does NOT prove. This mission proves the linear algebra: symmetric matrices commuting with $J$ form a space of dimension $n^2$. It does not prove the physics step that passivity forces a coupling to be symmetric. That step is a separate premise of the model, and a completed mission must not be read as establishing it.

Setting

Fix a natural number $n$. Consider real $2n \times 2n$ matrices, with rows and columns indexed by two copies of $\{0, \dots, n-1\}$, so that each matrix is written in $2 \times 2$ block form with $n \times n$ blocks:

$$W = \begin{pmatrix} A & B \\ C & D \end{pmatrix}.$$

Let $I$ be the $n \times n$ identity matrix and define the standard complex structure

$$J = \begin{pmatrix} 0 & -I \\ I & 0 \end{pmatrix},$$

which satisfies $J^2 = -1$. In the Lean development this matrix is PassivityUn.stdJ n, and the index type is PassivityUn.Blk n, the disjoint union of two copies of Fin n.

Two real linear subspaces of the $4n^2$-dimensional space of such matrices are defined:

1. symm n: the symmetric matrices, $W^{\mathsf T} = W$;
2. commJ n: the matrices commuting with $J$, $WJ = JW$.

The admissible coupling class admissible n is their intersection:

$$\mathcal{A}_n = \{\, W \in \mathbb{R}^{2n \times 2n} : W^{\mathsf T} = W \ \text{and}\ WJ = JW \,\}.$$

Formalization targets

Goal: the admissible class has dimension $n^2$

$$\dim_{\mathbb{R}} \mathcal{A}_n = n^2 \qquad \text{for every } n \in \mathbb{N}.$$

This is PassivityUn.admissible_finrank. It asserts the exact dimension for all $n$ at once, not for a particular node size.

Milestones

1. M1. $J \cdot J = -1$, so $J$ is a complex structure.
2. M2. A block matrix $\begin{pmatrix} A & B \\ C & D \end{pmatrix}$ commutes with $J$ exactly when $D = A$ and $B = -C$.
3. M3. A block matrix $\begin{pmatrix} A & -B \\ B & A \end{pmatrix}$ is symmetric exactly when $A^{\mathsf T} = A$ and $B^{\mathsf T} = -B$.
4. M4. The dimension counts of symmetric and antisymmetric $n \times n$ matrices add to $n^2$: $\tfrac{n(n+1)}{2} + \tfrac{n(n-1)}{2} = n^2$.

Significance

The result itself. The goal identifies the admissible coupling class with the real form of the $n \times n$ Hermitian matrices, the space whose dimension is that of $\mathfrak{u}(n)$ (Hermitian matrix). Applied at $n = 1, 2, 3$ it gives the dimensions $1$, $4$ and $9$, which the Shape Zero model matches with $\mathfrak{u}(1)$, $\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$ and $\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$. Without a proof for general $n$, the model rests on a finite numerical check.

Formalizing it. The underlying fact is standard linear algebra, a special case of the correspondence between real matrices commuting with a complex structure and complex-linear maps (Linear complex structure). No machine-checked statement of this exact dimension count was found in the platform library. The mission produces a verified, general-$n$ statement whose hypotheses are fully explicit, and it separates the verified linear algebra from the unverified physical premise.

Difficulty

Every step is standard linear algebra, so the difficulty is in the formal bookkeeping rather than the mathematics. The dimension of a subspace defined by equations is not computed by any Mathlib tactic. It has to be obtained by exhibiting an explicit linear equivalence with spaces of known dimension, and that requires moving between the $2n \times 2n$ matrix indexed by a disjoint union and its four $n \times n$ blocks. Checking small cases numerically, as has already been done, does not extend to a statement about every $n$.

Formalization scope

• Matrices are real (ℝ), not complex. The complex structure enters only through the fixed real matrix $J$.
• Matrices are indexed by Fin n ⊕ Fin n (PassivityUn.Blk n) rather than Fin (2n), so that block decomposition via Mathlib's Matrix.fromBlocks is direct. The first copy of Fin n indexes the upper/left blocks.
• Each condition is defined as the kernel of a linear map: symmetry as the kernel of $W \mapsto W^{\mathsf T} - W$, and commuting with $J$ as the kernel of $W \mapsto WJ - JW$. Both are therefore subspaces by construction, with no hand-written closure proofs.
• Dimension is Module.finrank ℝ. The ambient space is finite-dimensional, so the convention that finrank of an infinite-dimensional space is $0$ never applies.
• The case $n = 0$ is included, and there the statement reads $0 = 0$. This is not a trivialization: the claim is quantified over all $n$, and every $n \ge 1$ is a nontrivial instance.
• M4 is stated with natural-number division and truncated subtraction. Both are exact here, because $n(n \pm 1)$ is always even and $n \cdot (n - 1) = 0$ when $n = 0$.

The development needs only Mathlib's block matrices, transpose, linear maps and finrank. The block-characterization lemmas (M2, M3) are reusable for any statement relating real matrices commuting with $J$ to complex matrices. Contributions are welcome on the milestones and on the assembling isomorphism.

Selected references

• B. C. Hall, Lie Groups, Lie Algebras, and Representations: An Elementary Introduction, 2nd ed., Graduate Texts in Mathematics 222, Springer, 2015. https://doi.org/10.1007/978-3-319-13467-3
• Wikipedia, Unitary group. https://en.wikipedia.org/wiki/Unitary_group
• Wikipedia, Linear complex structure. https://en.wikipedia.org/wiki/Linear_complex_structure
• Wikipedia, Hermitian matrix. https://en.wikipedia.org/wiki/Hermitian_matrix
• Mathlib, Mathlib.Data.Matrix.Block (block matrices, Matrix.fromBlocks). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Block.html

Motivation

The g-factor of a particle, nucleus or atom is the dimensionless number that measures its magnetic moment in units of the moment a classical particle with the same charge and angular momentum would have. Because it is both measured and computed to very high precision, small discrepancies between measured and predicted g-factors are used as tests of the Standard Model; the electron g-factor is known to about two parts in $10^{13}$, and the muon g-factor has for two decades shown a several-standard-deviation tension between experiment and theory.

This mission formalizes the mathematical content of the Wikipedia article g-factor (physics): the definitions it gives, the elementary identities it states between them, and the numerical claims it makes about the experimental data.

Setting

All vectors live in $\mathbb R^3$, written as functions $\{0,1,2\}\to\mathbb R$, with component $2$ playing the role of the $z$ component.

• Dirac particle. For charge $e$, mass $m$, spin angular momentum $\mathbf S$ and g-factor $g$, the spin magnetic moment is $\boldsymbol\mu = g\,\frac{e}{2m}\,\mathbf S$ (diracMagneticMoment).
• Nuclear magneton convention. With $\mu_N = \frac{e\hbar}{2m_p}$ (nuclearMagneton), the moment of a nucleon or nucleus with spin $\mathbf I$ is $\boldsymbol\mu = g\,\frac{\mu_N}{\hbar}\,\mathbf I$ (nuclearMagneticMoment).
• Bohr magneton $\mu_B = \frac{e\hbar}{2m_e}$ (bohrMagneton) and electron orbital moment $\boldsymbol\mu_L = -g_L\frac{\mu_B}{\hbar}\mathbf L$ (electronOrbitalMagneticMoment).
• Classical point charges. For finitely many point particles with charges $q_i$, masses $m_i$, positions $\mathbf r_i$ and velocities $\mathbf v_i$, the magnetic moment is $\boldsymbol\mu = \sum_i \frac{q_i}{2}\,\mathbf r_i\times\mathbf v_i$ (classicalMagneticMoment) and the angular momentum is $\mathbf L = \sum_i m_i\,\mathbf r_i\times\mathbf v_i$ (classicalAngularMomentum).

Formalization targets

Goal: the classical baseline has $g = 1$

The article defines the g-factor as the ratio of a particle's magnetic moment to the one "expected of a classical particle of the same charge and angular momentum", and says $g_L = 1$ "by a quantum-mechanical argument analogous to the derivation of the classical magnetogyric ratio". The goal makes that classical baseline precise: for a system whose charge-to-mass ratio is the same for every particle ($q_i = \kappa m_i$, $m_i>0$), with total charge $Q=\sum_i q_i$ and total mass $M=\sum_i m_i$,

$$\boldsymbol\mu \;=\; 1\cdot\frac{Q}{2M}\,\mathbf L .$$

Milestones

1. The two forms of the nuclear-magneton formula agree: $g\frac{\mu_N}{\hbar}\mathbf I = g\frac{e}{2m_p}\mathbf I$.
2. For a particle of proton mass, the Dirac-particle and nuclear-magneton definitions assign the same g-factor.
3. The $z$ component of the electron orbital moment is $-g_L\mu_B m_\ell$, which equals $-\mu_B m_\ell$ when $g_L=1$.
4. The E821 muon result differs from the quoted theoretical prediction by between $3.4$ and $3.5$ combined standard deviations.
5. The relative standard uncertainties in the article's CODATA table round to the values printed there.

Significance

The goal is the statement that fixes the normalization of every g-factor in the article: it says that a classical body with uniform charge-to-mass ratio has gyromagnetic ratio exactly $Q/(2M)$, i.e. $g=1$, so any deviation from $1$ (such as $g_e\approx-2$) is a genuinely non-classical effect. The milestones pin down the conventions (Dirac versus nuclear magneton, sign conventions for the electron orbital moment) and check the numerical claims the article makes from its data. None of these results is new; the contribution is a machine-checked, convention-explicit record of them.

Difficulty

The mathematics is elementary. The work is in the conventions: division by a mass or by $\hbar$ is total in Lean and returns $0$ at $0$, so positivity of masses and of $\hbar$ must be carried explicitly, and the numerical milestones must be stated with the exact decimal values of the source rather than rounded ones.

Formalization scope

• Vectors are Fin 3 → ℝ; the cross product is Mathlib's crossProduct. Component index 2 is the $z$ axis.
• Physical constants are free real parameters; no numerical value of $e$, $\hbar$ or any mass is fixed. Where the source's formula divides by a quantity, the statement assumes it nonzero or positive.
• Uncertainties written as $x(\text{dd})$ in the article are read as a standard uncertainty in the last two digits of $x$; the E821 milestone combines the experimental and theoretical uncertainties in quadrature, which is the standard convention but is not spelled out in the article.
• Not formalized: the finite-nuclear-mass formula $g_L = 1 - 1/M$ and the Landé factor $g_J$, which the article quotes from other sources without derivation.

Selected references

• Wikipedia, g-factor (physics). https://en.wikipedia.org/wiki/G-factor_(physics)
• G. W. Bennett et al. (Muon g−2 Collaboration), Final report of the E821 muon anomalous magnetic moment measurement at BNL, Phys. Rev. D 73, 072003 (2006). https://doi.org/10.1103/PhysRevD.73.072003
• NIST, CODATA Internationally recommended values of the fundamental physical constants. https://physics.nist.gov/cuu/Constants/