Mathematical Physics

Motivation

Planar flows are tame: the Poincaré–Bendixson theorem says that a bounded forward orbit in the plane tends to a fixed point or a periodic orbit. From dimension three on this fails, and the long-time behavior of a flow has to be described through sets rather than single orbits. Chapter 8 of Gerald Teschl's graduate text Ordinary Differential Equations and Dynamical Systems (AMS GSM 140, 2012; author's preliminary version at mat.univie.ac.at) develops two tools for this. The first is the attracting set produced by a trapping region, the device used to show that the Lorenz equation (Lorenz 1963) has an attractor. The second is volume: Liouville's formula for volumes measures how a flow expands or contracts phase space, which shows that the Lorenz attractor has Lebesgue measure zero, and in the special case of a Hamiltonian system gives Liouville's theorem, that the flow preserves volume. Liouville's theorem, with Poincaré's recurrence theorem as its companion, underlies Hamiltonian mechanics and equilibrium statistical mechanics.

This mission states those results for the local flow of a $C^1$ vector field on an open subset of $\mathbb{R}^n$, as in the book.

Setting

Let $M \subseteq \mathbb{R}^n$ be open and $f : M \to \mathbb{R}^n$ of class $C^1$. An integral curve of $\dot x = f(x)$ is a differentiable $\varphi$ on an open interval with $\dot\varphi(t) = f(\varphi(t))$. For each $x \in M$ there is a unique maximal one through $x$ at time $0$, defined on the open interval $I_x \ni 0$. Its value at time $t$ is $\Phi(t, x)$, the flow. The flow is local: $I_x$ may be bounded.

For $X \subseteq M$, the $\omega_+$-limit set $\omega_+(X)$ is the set of $y \in M$ for which there are $t_k \to \infty$ and $x_k \in X$ with $\Phi(t_k, x_k) \to y$. The stable and unstable sets of $\Lambda$ are $W^\pm(\Lambda) = \{x \in M : d(\Phi(t, x), \Lambda) \to 0 \text{ as } t \to \pm\infty\}$, where $d$ is the distance to a set. A set is invariant if it contains the full orbit of each of its points. An invariant $\Lambda$ is attracting if $W^+(\Lambda)$ is a neighborhood of $\Lambda$. A trapping region is an open connected $E$ with compact closure $\overline E \subseteq M$ such that $\Phi(t, \overline E) \subset E$ for all $t > 0$.

The divergence of $f$ is $\operatorname{div} f = \sum_i \partial f_i / \partial x_i = \operatorname{tr}(df)$. On phase space $\mathbb{R}^n \times \mathbb{R}^n \ni (p, q)$, a Hamilton function $H \in C^2$ defines Hamilton's equations $\dot q = \partial H / \partial p$, $\dot p = -\partial H / \partial q$, whose right-hand side is the Hamiltonian vector field $X_H$. The Lorenz equation is $\dot x = -\sigma(x - y)$, $\dot y = rx - y - xz$, $\dot z = xy - bz$ with $\sigma, r, b > 0$. Volume $|\cdot|$ is Lebesgue measure.

Formalization targets

Goal: Liouville's theorem (Theorem 8.10)

For $H \in C^2(\Omega)$ on an open $\Omega \subseteq \mathbb{R}^n \times \mathbb{R}^n$, with $\Phi$ the flow of $X_H$ on $\Omega$, every measurable $U \subseteq \Omega$ and every time $t$ at which all points of $U$ are alive satisfy

$$|\Phi(t, U)| = |U| .$$

Milestones

• Lemma 8.8 (Liouville's formula for volumes). Take $f \in C^1(\mathbb{R}^n)$, $U$ bounded and open, and $t_0$ with every point of $\overline U$ alive at $t_0$. Write $V(t) = |\Phi(t, U)|$. Then $V(t_0) < \infty$ and

$$\dot V(t_0) = \int_{\Phi(t_0, U)} \operatorname{div} f(x)\,dx .$$

• Theorem 8.11 (Poincaré). Let $\Phi$ be a volume preserving bijection of a bounded region $D$. Then every neighborhood $U \subseteq D$ contains an $x$ with $\Phi^k(x) \in U$ for some $k \ge 1$.
• Lemma 8.5. For a trapping region $E$, $\Lambda = \omega_+(E) = \bigcap_{t \ge 0} \Phi(t, E)$ is nonempty, invariant, compact, connected and attracting.
• Lemma 8.6. For a trapping region $E$, $W^-(x) \subseteq \omega_+(E)$ for every $x \in \omega_+(E)$.
• Lemma 8.7. For the Lorenz equation with $r \le 1$, the origin is the only fixed point, and every solution exists for all $t \ge 0$ and tends to the origin.

Significance

The result itself. Liouville's theorem is the basic structural fact of Hamiltonian dynamics. It rules out asymptotically stable equilibria and attractors of positive measure for Hamiltonian systems. It makes Lebesgue measure invariant, which is the starting point of ergodic theory for mechanical systems. Combined with Theorem 8.11, it gives recurrence for any Hamiltonian motion confined to a bounded energy region. Lemma 8.8 is the quantitative version for arbitrary flows: for the Lorenz equation it gives $V(t) = V e^{-(1+\sigma+b)t}$, so the attractor from Lemma 8.5 has measure zero. Lemmas 8.5 and 8.6 produce attractors and show that they contain the unstable manifolds of their points.

Formalizing it. All of these results are classical and proved in the book. Mathlib has the change-of-variables formula, Poincaré recurrence for conservative measure-preserving maps (MeasureTheory.Conservative), and an $\omega$-limit set for global flows (omegaLimit). It has no flow of a nonlinear ODE with its differentiable dependence on initial conditions, no volume formula along such a flow, and no Hamiltonian formalism. The mission asks for those pieces in the book's local-flow setting, with its hypotheses made explicit.

Difficulty

Lemma 8.8 and Theorem 8.10 need the flow map $x \mapsto \Phi(t, x)$ to be a $C^1$ diffeomorphism of the set of points alive at time $t$ onto its image. They also need its Jacobian to satisfy the first variational equation $\dot\Pi = df(\Phi_t(x))\,\Pi$, whose determinant obeys Liouville's formula for linear systems. None of this is available for a general $C^1$ vector field in Mathlib, which provides local existence and uniqueness of integral curves but not differentiability of the flow in the initial condition. Differentiating $V(t)$ under the integral also needs uniform control on a compact set of initial points. That is why Lemma 8.8 asks the closure of $U$, not just $U$, to be alive at $t_0$. Without that, $\Phi(t_0, U)$ can have infinite volume ($\dot x = x^2$, $U = (0, 1)$, $t_0 = 1$).

Lemmas 8.5 and 8.6 are point-set topology. The obstacle there is the local flow: every statement about $\Phi(t, \cdot)$ must first establish that the points involved are alive at time $t$. The book avoids this by assuming completeness at the start of the chapter. For Lemma 8.7, the Liapunov function $L = rx^2 + \sigma y^2 + \sigma z^2$ from the text has $\dot L \le 0$, not $\dot L < 0$, so convergence to the origin requires the Krasovskii–LaSalle argument, not a plain Liapunov one.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) and phase space is EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) with points $(p, q)$, momenta first. volume on it is Lebesgue measure on $\mathbb{R}^{2n}$. The flow is a pair $(I, \Phi)$ satisfying IsMaximalFlow, which makes $t \mapsto \Phi(t, x)$ the unique maximal integral curve on $I_x$. Nothing assumes $I_x = \mathbb{R}$. The chapter's standing completeness assumption is replaced by explicit aliveness hypotheses, and these are implied by completeness. The explicit readings are:

• Theorem 8.10: "Hamiltonian flow" means $H \in C^2$ on an open $\Omega$. "Volume" means Lebesgue measure of any measurable $U \subseteq \Omega$ that is alive at time $t$.
• Lemma 8.8: $f \in C^1$ on $\mathbb{R}^n$. $\overline U$ is alive at $t_0$. The conclusion also states $V(t_0) < \infty$ and integrability of $\operatorname{div} f$ on $\Phi(t_0, U)$, and $V$ is the real-valued volume.
• Theorem 8.11: "region" means a measurable bounded set. "Volume preserving" means that images of measurable subsets of $D$ are measurable and have the same measure. "Any neighborhood $U$" means a neighborhood of some point, hence nonempty. $n \in \mathbb{N}$ means $k \ge 1$.
• Lemma 8.5: a trapping region has $\overline E \subseteq M$ and $\overline E$ forward complete, and "connected" includes nonempty. "Invariant" is two-sided.
• Lemma 8.7: "all solutions converge" includes existence for all $t \ge 0$. The flow is quantified universally.

A trivializing formalization is excluded. The goal is not stated for a complete or globally Lipschitz flow, not for sets of measure zero or bounded open sets only, and not with $\operatorname{div} X_H = 0$ assumed. It must be proved for the flow of $X_H$ built from $H$ itself.

A complete development needs differentiability of the flow in the initial condition and the first variational equation. It also needs Liouville's formula $\det \Pi(t) = \exp \int_0^t \operatorname{tr} A$ for linear systems, and change of variables for the flow map. Each is reusable beyond this mission; contributions of any of them as separate lemmas are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012 (cited: author's preliminary version, Chapter 8, pp. 229–241). https://doi.org/10.1090/gsm/140 · https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf
• E. N. Lorenz, Deterministic nonperiodic flow, Journal of the Atmospheric Sciences 20 (1963), 130–141. https://doi.org/10.1175/1520-0469(1963)020%3C0130:DNF%3E2.0.CO;2
• V. I. Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., Graduate Texts in Mathematics 60, Springer, 1989. https://doi.org/10.1007/978-1-4757-2063-1
• The Mathlib Community, Mathlib, Mathlib/Dynamics/Ergodic/Conservative.lean. https://github.com/leanprover-community/mathlib4

Motivation

Newton's law of universal gravitation states that any two point masses attract each other with a force proportional to the product of their masses and inversely proportional to the square of their distance. It is the first quantitative law of gravity (Newton, Principia, 1687) and it remains the working model of gravity in celestial mechanics, geophysics and engineering whenever relativistic effects are negligible.

The law is stated for point masses, while planets, moons and apples are extended bodies. Newton delayed publication for about twenty years because he could not prove that the Earth attracts external bodies as if all its mass were concentrated at its centre. The result that closes this gap is the shell theorem: a spherically symmetric distribution of mass exerts, on every external point, the same gravitational attraction as a point mass at its centre carrying the total mass; and mass located at radii larger than that of the test point exerts no net force at all.

Timeline (as described in the source):

• c. 1666: Newton applies the inverse-square law to the orbit of the Moon, assuming — without proof — that the Earth acts as a point mass.
• 1687: Principia published, including the proof of the shell theorem (Book I, Proposition 75, Theorem 35).
• 1798: Cavendish experiment, the first laboratory test of gravitation between masses.

Setting

Space is $\mathbb{E}^3 = \mathbb{R}^3$ with the Euclidean norm. The gravitational constant is $G = 6.67430\times10^{-11}$.

• Point force. A body of mass $m_1$ at $r_1$ exerts on a body of mass $m_2$ at $r_2$ the force

$$F_{21} = -\frac{G m_1 m_2}{\|r_{21}\|^2}\,\hat r_{21},\qquad r_{21}=r_2-r_1,\quad \hat r_{21} = \frac{r_{21}}{\|r_{21}\|}.$$

• Point field and potential. A point mass $M$ at $c$ produces the field $g(x) = -\frac{GM}{\|x-c\|^3}(x-c)$ and the potential $V(x) = -\frac{GM}{\|x-c\|}$.
• Mass distributions. An extended body is a (finite, Borel) measure $\mu$ on $\mathbb{E}^3$; $\mu(A)$ is the mass contained in the region $A$. Its gravitational field is the superposition of the point fields of its elements,

$$g_\mu(x) = \int_{\mathbb{E}^3} -\frac{G}{\|x-y\|^3}\,(x-y)\,d\mu(y).$$

• Spherical symmetry. $\mu$ is spherically symmetric (about the origin) if $\mu$ is invariant under every linear isometry of $\mathbb{E}^3$ (every rotation and reflection fixing $0$).
• Model bodies. The uniform shell $\sigma_{M,a}$ of mass $M$ and radius $a$ (normalised surface measure on the sphere $\|y\| = a$) and the uniform solid ball $\beta_{M,R}$ of mass $M$ and radius $R$ (normalised Lebesgue measure on $\|y\|<R$).

Formalization targets

Goal: shell theorem, exterior part

If $\mu$ is a finite, spherically symmetric mass distribution carried by the closed ball $\|y\|\le R$, then for every $x$ with $\|x\|>R$,

$$g_\mu(x) = -\frac{G\,\mu(\mathbb{E}^3)}{\|x\|^3}\,x .$$

Milestones

1. Vector form: $F_{12} = -F_{21}$, and $\|F_{21}\| = G m_1 m_2/\|r_2-r_1\|^2$.
2. Field form: $F_{21} = m_2\, g(r_2)$ where $g$ is the field of $m_1$ at $r_1$; the field is conservative, $g = -\nabla V$.
3. Shell theorem, interior part: mass at radii larger than $\|x\|$ exerts no net field at $x$; more precisely, the field at $x$ equals that of the mass enclosed in the ball of radius $\|x\|$, concentrated at the centre.
4. Hollow sphere: $g = 0$ inside, $g =$ point field of $M$ outside.
5. Uniform solid sphere: $g(x) = -\frac{GM}{R^3}x$ inside, point field of $M$ for $\|x\|\ge R$.

Significance

The shell theorem is what licenses treating the Sun, planets and moons as point masses in the $n$-body problem and in Kepler orbit computations, and it gives the linear growth of the gravitational field inside a uniform planet. The interior statement ("no net force inside a hollow shell") has an exact analogue in electrostatics (Coulomb's law is also inverse-square).

The results are classical and fully proved on paper. This mission asks for machine-checked proofs, together with the reusable infrastructure they require: vector-valued integrals against rotation-invariant measures, the surface measure of the sphere, and the Newtonian kernel $x/\|x\|^3$.

Difficulty

Newton's argument (or the modern one via Gauss's law) is geometric: slice the shell into rings, or apply the divergence theorem to a sphere. Neither is directly available: Mathlib has no divergence theorem on spheres in the required form, and the ring-slicing computation requires explicit spherical coordinates for a surface measure that is defined abstractly. Using symmetry alone shows the field is radial, but its magnitude requires an actual computation of a singular integral (for the interior of a solid ball the integrand is unbounded).

Formalization scope

• Space is EuclideanSpace ℝ (Fin 3). Mass distributions are Measures; the field is a Bochner integral. Because a non-integrable Bochner integral is defined to be $0$, statements where integrability is not automatic either carry an explicit integrability hypothesis or are placed where the integrand is bounded (test point strictly outside the support).
• Spherical symmetry is invariance under all linear isometries (Space ≃ₗᵢ[ℝ] Space), centred at the origin.
• Masses of model bodies are nonnegative reals (NNReal); radii are assumed strictly positive.
• The uniform shell uses Mathlib's Measure.toSphere (surface measure on the unit sphere) pushed forward by scaling.
• Units are not modelled; $G$ is the real number $6.67430\times10^{-11}$.

Contributions welcome: a general "radial field" lemma from spherical symmetry, the computation of the field of a uniform shell, and the disintegration of a spherically symmetric measure into shells.

Selected references

• Wikipedia, Newton's law of universal gravitation, revision 1370960529. https://en.wikipedia.org/w/index.php?title=Newton%27s_law_of_universal_gravitation&oldid=1370960529
• I. Newton, The Principia: Mathematical Principles of Natural Philosophy, transl. I. B. Cohen and A. Whitman, University of California Press, 1999 — Book I, Proposition 75, Theorem 35.

Motivation

In Witten's cubic open string field theory (Witten 1986) the interaction glues half-strings together, and in the usual center-of-mass variables the action contains infinitely many time derivatives. Such a theory has no evident initial value formulation, which obstructs a Hamiltonian treatment and a direct discussion of causality.

Erler and Gross (2004) show that after a unitary change of basis in which the string field depends on the lightcone component of the string midpoint $x^+(\pi/2)$ (and on transverse center-of-mass coordinates), the cubic vertex contains no derivatives with respect to lightcone time. This reduces to five linear relations among the Neumann coefficients of the three-string vertex, the midpoint identities (A.6)–(A.10) of the paper. One of them, (A.8), is a closed numerical identity: a specific infinite series built from Neumann coefficients equals $-\ln\frac{27}{16}$, where $\ln\frac{27}{16}=V_{00}$ is the zero-mode Neumann coefficient. This mission formalizes that identity and the chain of intermediate results the paper uses to prove it (Appendix B), together with a divergence statement from Section 2 explaining why other midpoint bases fail.

Setting

Define real constants $A_k$ ($k\ge0$) by the expansion

$$\left(\frac{1+iz}{1-iz}\right)^{1/3}=\exp\!\left(\tfrac{2i}{3}\tan^{-1}z\right)=1+\sum_{n\ge1}A_{2n}z^{2n}+i\sum_{n\ge1}A_{2n-1}z^{2n-1}.$$

For real $z$ the left side is $\cos(\tfrac23\arctan z)+i\sin(\tfrac23\arctan z)$, so $A_{2n}$ is the $2n$-th Taylor coefficient of $\cos(\tfrac23\arctan z)$ at $0$ (e.g. $A_2=-\tfrac29$). The even Neumann vector and the vector $\beta$ are

$$m_{2n}=-\frac23\,\frac{A_{2n}}{\sqrt{2n}},\qquad \beta_k=\frac{\cos(k\pi/2)}{\sqrt k},\quad\text{so }\beta_{2n}=\frac{(-1)^n}{\sqrt{2n}}.$$

In Lean these are ErlerGross.neumannA, ErlerGross.neumannMEven (with neumannMEven n $=m_{2n}$) and ErlerGross.betaVec. Two auxiliary objects appear in the proof: the (B.3) terms

$$b_n=\frac{2}{2n-1}-\frac{1}{2n-\frac23}-\frac{1}{2n-\frac43}\qquad(n\ge1),$$

(ErlerGross.b3Term) and the $\kappa$-basis integrand

$$g(\kappa)=\frac{1-\cosh\frac{\pi\kappa}{2}}{1+2\cosh\frac{\pi\kappa}{2}}\cdot\frac{1}{2\kappa\sinh\frac{\pi\kappa}{2}}$$

(ErlerGross.kappaIntegrand), which arises from the continuous spectrum $\kappa\in\mathbb R$ of the Neumann matrices (Rastelli–Sen–Zwiebach 2001).

Formalization targets

Goal — midpoint identity (A.8)

$$\ln\frac{27}{16}+\sum_{n\ge1}3\,m_{2n}\beta_{2n}=0,$$

formalized as: the series $\sum_{n\ge1}3m_{2n}\beta_{2n}$ converges absolutely (Lean HasSum) to $-\ln\frac{27}{16}$.

Milestones (Appendix B and Section 2)

• $\kappa$-basis representation: $g$ is integrable and $\sum_{n\ge1}3m_{2n}\beta_{2n}=2\int_{\mathbb R}g$.
• Residue evaluation: $\int_{\mathbb R}g=\sum_{n\ge1}b_n$.
• Eq. (B.3): $\sum_{n\ge1}3m_{2n}\beta_{2n}=2\sum_{n\ge1}b_n$.
• Auxiliary series: $\sum_{n\ge1}\frac{1}{n(2n+1)}=2-2\ln2$ and $\sum_{n\ge1}\frac{1}{n(9n^2-1)}=\frac32(\ln3-1)$.
• Closed form: $\sum_{n\ge1}b_n=-\frac12\ln\frac{27}{16}$.
• Integral formula: $\int_0^\infty\frac{\cosh ax}{\cosh bx}\,dx=\frac{\pi}{2b}\frac{1}{\cos\frac{\pi a}{2b}}$ for complex $a,b$ with $|\Re a|<\Re b$.
• Section 2: for any real regulator with $\omega_{2n}\to0$, $\sum_{n\ge1}\frac{((-1)^n-\omega_{2n})^2}{2n}=+\infty$.

Significance

In the paper, (A.8) is one of the relations which, together with (A.6), (A.7), (A.9), (A.10), removes lightcone-time derivatives from the cubic vertex. This is what gives the theory an initial value formulation in lightcone time and makes the Hamiltonian BRST quantization of Section 4 possible. Unlike the other four identities, which are relations between distributions and are verified in the paper's spectral basis, (A.8) is an equality of real numbers. It can therefore be checked completely in Lean.

A complete formalization would produce a machine-checked proof of a Neumann-coefficient identity. It would also add reusable material: Taylor coefficients of $\exp(\tfrac{2i}{3}\arctan z)$, the $\cosh/\cosh$ integral, and digamma-type evaluations of rational series.

Difficulty

The goal defines $m_{2n}$ through Taylor coefficients, which have no closed form. The paper does not sum the series in the mode basis. It moves to the continuous $\kappa$ basis of the Neumann spectrum and closes a contour. That step rests on eigenvector expansions $v_{2n}(\kappa)$ and the principal-value distribution $\beta(\kappa)$, neither of which is in Mathlib. A direct route has to connect the coefficients $A_{2n}$ to the integral $\int g$, or to the series $\sum b_n$, some other way. The terms of $\sum b_n$ decay like $n^{-2}$. The terms $(-1)^nA_{2n}/n$ of the goal series decay only like $n^{-5/3}$, so the goal series converges slowly.

Formalization scope

• All quantities are real. $A_k$ is given as $f^{(k)}(0)/k!$ for $f=\cos(\tfrac23\arctan\cdot)$ (even $k$) or $\sin(\tfrac23\arctan\cdot)$ (odd $k$), using Mathlib's iteratedDeriv.
• Series are indexed from $n=1$ by shifting the Lean index $n\mapsto n+1$. HasSum is unconditional (equivalently absolute) convergence. Every statement asserts convergence, so no statement can hold only because Lean assigns $0$ to a divergent tsum.
• $g(0)=0$ by Lean's convention $x/0=0$. This single point does not affect the integral.
• Source misprints corrected: the paper's first auxiliary formula prints $\sum\frac{1}{n(2n+1)}=2-\ln2$. The true value is $2-2\ln2\approx0.6137$, and that value is formalized. The formula for $m_{2n}$ is printed with left side $m_{2m}$.
• In the Section 2 statement the dimension factor $D>0$ is omitted, and only divergence to $+\infty$ is asserted, not the logarithmic rate.
• Not formalized: the identities (A.6), (A.7), (A.9), (A.10), eq. (B.2), and the eigenvectors $v_n(\kappa)$. Contributions that build this spectral machinery are welcome.

Selected references

• T. G. Erler, D. J. Gross, Locality, Causality, and an Initial Value Formulation for Open String Field Theory, 2004. https://arxiv.org/abs/hep-th/0406199
• E. Witten, Noncommutative Geometry and String Field Theory, Nucl. Phys. B 268 (1986) 253. https://doi.org/10.1016/0550-3213(86)90155-0
• L. Rastelli, A. Sen, B. Zwiebach, Star Algebra Spectroscopy, JHEP 2002. https://arxiv.org/abs/hep-th/0111281

Motivation

Flatly Foliated Relativity (FFR) is a theory of gravity introduced by Bray, Hamm, Hirsch, Wheeler and Zhang (arXiv:1911.00967, 2019) that sits between special and general relativity. It keeps the Einstein–Hilbert action of general relativity (GR) but restricts it to spacetimes that are foliated by flat Euclidean spaces (Assumption 1 of the paper): "matter curves spacetime, but not space". The authors motivate this by the observed spatial flatness of the local universe. Since gravitational waves are excluded, FFR is proposed as an approximation of GR whose metric equations are much more tractable. It still contains the big bang (FLRW spacetimes with $k = 0$), accelerated expansion and the exterior Schwarzschild spacetime.

One headline feature of the theory is how a positive cosmological constant $\Lambda > 0$ (Assumption 2) shapes it. For $\Lambda>0$ the paper shows that the FFR metric equations are elliptic on every slice, that the mean curvature of the foliation gives a geometric arrow of time, and that there is exactly one vacuum solution among solutions that are spherically symmetric at infinity. For $\Lambda=0$ uniqueness fails, and for $\Lambda<0$ existence fails. This mission formalizes Sections 3.2–5 of the paper, which contain these statements.

Setting

All FFR equations live on a single flat slice $\mathbb R^3_t$, with no time derivatives, so the formalization works on $\mathbb R^3$ with coordinates $x_1,x_2,x_3$. The spacetime metric is

$$g = (-\eta^2+|\omega|^2)\,dt^2-(\omega\otimes dt+dt\otimes\omega)+\delta_{\mathbb R^3},$$

where $\eta>0$ is the lapse and $\omega$ is a one-form on $\mathbb R^3$, identified with a vector field through the flat metric. Matter enters through the energy density $\mu$ and the momentum density $J$. Writing $\omega_{i,j}=\partial_j\omega_i$, $\nabla\cdot\omega=\omega_{i,i}$ and $\Delta$ for the flat Laplacian (summation over repeated indices), the FFR equations (34)–(35) are

$$2\Lambda+16\pi\mu=\frac1{\eta^2}\Big[(\nabla\cdot\omega)^2-\tfrac14\|\omega_{i,j}+\omega_{j,i}\|^2\Big],$$ $$16\pi J_i=\frac1\eta\big(\Delta\omega_i-\partial_i(\nabla\cdot\omega)\big)+\frac2{\eta^2}(\nabla\cdot\omega)\eta_i-\frac1{\eta^2}(\omega_{i,j}+\omega_{j,i})\eta_j .$$

Substituting $\omega=df+\zeta$ with $\nabla\cdot\zeta=0$ gives the elliptic form (39)–(41), with unknowns $(f,\zeta,\eta)$. Here $Q_{ij}=f_{ij}+\tfrac12(\zeta_{i,j}+\zeta_{j,i})$:

$$(\Delta f)^2-\|Q\|^2=(16\pi\mu+2\Lambda)\eta^2,$$ $$\Delta\zeta_i=16\pi J_i\eta-\tfrac2\eta(\Delta f\,\delta_{ij}-Q_{ij})\eta_j,$$ $$(\Delta f\,\delta_{ij}-Q_{ij})\eta_{ij}=8\pi\nabla\cdot(J\eta^2),$$

together with the requirement $\nabla\cdot\zeta\to0$ at infinity. Vacuum means $\mu=0$ and $J=0$. When $\Lambda>0$, the paper fixes the time orientation by the arrow-of-time convention $K=(\nabla\cdot\omega)/\eta=\Delta f/\eta>0$ (Convention 1). A pair $(\omega,\eta)$ is spherically symmetric at infinity if it is spherically symmetric on $\{r\ge r_0\}$ for some $r_0>0$. Two vacuum solutions count as the same if they differ by an overall positive constant factor, which corresponds to rescaling $t$.

Formalization targets

Goal: Corollary 2

For $\Lambda>0$, the pair $\omega=\sqrt{\Lambda/3}\,r\,\partial_r$, $\eta=1$ is a smooth vacuum solution that is spherically symmetric at infinity. Every smooth vacuum solution with $\eta>0$ and $(\nabla\cdot\omega)/\eta>0$ that is spherically symmetric at infinity has the form

$$\eta\equiv c,\qquad \omega=c\sqrt{\Lambda/3}\;x\qquad(c>0).$$

Milestones

Theorem 2 (equivalence with the elliptic form), Theorem 3 (arrow of time), Theorem 4 (ellipticity inequality), Lemma 1 (symmetrization), identity (82)–(83), Theorem 5 (uniqueness for the elliptic form under approximate spherical symmetry), Lemma 2 ($\Lambda=0$: many vacua) and Lemma 3 ($\Lambda<0$: no vacuum).

Significance

Corollary 2 is the fourth claim of the paper's main result (Theorem 1). It is the precise sense in which FFR with $\Lambda>0$ is rigid, in contrast to GR, which has many vacuum solutions that are spherically symmetric at infinity (gravitational waves). Together with Lemmas 2 and 3, it singles out the sign of $\Lambda$ as the parameter that controls existence and uniqueness. The intermediate results are of independent use. Theorem 2 lets the elliptic system replace the original one, Theorem 4 is the ellipticity statement behind the existence question posed in the paper (Question 1), and Lemma 1 is a symmetrization inequality for the $2$-Hessian operator $\sigma_2(\nabla^2 f)$.

These are paper proofs. No machine-checked version of any of them is known to the proposer. The mission asks for a complete formal proof of the goal and the milestones in Lean 4 with Mathlib.

Difficulty

The algebra is elementary. The difficulty is analytic. The uniqueness arguments rest on maximum principles for the elliptic equations (41) and (45) on all of $\mathbb R^3$ under conditions at infinity, on Liouville-type arguments for harmonic functions, and on a Newtonian-potential representation (convolution with the Green's function of $\Delta$) used to show $\zeta\to0$. Lemma 1 needs averaging over rotations (spherical symmetrization), Jensen's inequality and a characterization of its equality case. Theorem 5 then needs a divergence-theorem argument on large balls that is controlled only by the approximate symmetry hypothesis. Mathlib provides the divergence theorem on boxes and some harmonic-function theory, but no ready-made maximum principle for second-order elliptic operators with variable coefficients on $\mathbb R^n$.

Formalization scope

• Space is EuclideanSpace ℝ (Fin 3). One-forms $\omega,\zeta,J$ are vector fields $\mathbb R^3\to\mathbb R^3$, and the paper's $\omega$ is written w in Lean. Partial derivatives are fderiv applied to the standard basis vectors. Because fderiv returns $0$ at non-differentiable points, every statement assumes smoothness (ContDiff ℝ ∞) of all fields, as the paper does.
• "Spherically symmetric" means invariance (for scalars) or equivariance (for one-forms) under all linear isometries of $\mathbb R^3$. Because $SO(3)$ acts transitively on spheres, this is equivalent to rotational symmetry.
• The spherical symmetrization $\bar f(x)$ is the average of $f$ over the sphere of radius $|x|$, taken with respect to the surface measure volume.toSphere. "Approximately spherically symmetric at $\infty$" is read as: $f-\bar f$ is bounded and $r^2\,\|\nabla^2(f-\bar f)\|\,\|\nabla(f-\bar f)\|\to0$ uniformly as $r\to\infty$, using operator norms.
• The arrow-of-time convention $\Delta f/\eta>0$ (respectively $(\nabla\cdot\omega)/\eta>0$) is an explicit hypothesis wherever the paper invokes it. Without it, $f\mapsto-f$ (time reversal) produces a second solution.
• Existence parts are stated with explicit witnesses. A formalization that drops smoothness, $\eta>0$ or the convention would be trivial or false, and is not acceptable.
• Contributions such as maximum principles, Liouville theorems and spherical averaging in $\mathbb R^n$ are reusable well beyond this mission and are welcome as separate lemmas.

Selected references

• H. L. Bray, B. Hamm, S. Hirsch, J. Wheeler, Y. Zhang, Flatly Foliated Relativity, arXiv:1911.00967v2, 2019. https://arxiv.org/abs/1911.00967
• L. Caffarelli, L. Nirenberg, J. Spruck, The Dirichlet problem for nonlinear second order elliptic equations, III: Functions of the eigenvalues of the Hessian, Acta Mathematica 155 (1985), 261–301 (cited in the paper for the existence theory of the $J=0$ case).
• J. Corvino, R. M. Schoen, On the asymptotics for the vacuum Einstein constraint equations, Journal of Differential Geometry 73(2) (2006), 185–217 (cited in the paper for the comparison with GR).

Motivation

Mass–energy equivalence is the relationship between mass and energy in a system's rest frame: the two differ only by the constant factor $c^2$, the square of the speed of light,

$$E = mc^2 .$$

It was proposed as a general principle by Albert Einstein in 1905 ("Does the inertia of a body depend upon its energy-content?") as a consequence of special relativity, and it underlies nuclear and particle physics: the mass defect of a nucleus measures its binding energy, and the energy released in fission or annihilation is accounted for by the change in rest mass.

Timeline. Electromagnetic-mass relations of the form $m \propto E_{em}/c^2$ were considered in the late 1800s and by Poincaré (1900) and Hasenöhrl (1904). Einstein (1905) derived the relativistic kinetic energy $E_k = mc^2(\gamma-1)$ and stated that a body emitting energy $L$ as radiation loses mass $L/c^2$. Planck, Stark, Lewis–Tolman and Lorentz (1907–1914) rewrote the relation in its modern forms, and von Laue (1911) gave a proof from the stress–energy tensor. This mission follows the Wikipedia article Mass–energy equivalence.

Setting

Velocities and momenta are vectors in $\mathbb R^3$ with Euclidean norm $|\cdot|$. Fix a speed of light $c>0$. A body of rest mass $m\ge0$ moving with velocity $\mathbf v$, $|\mathbf v|<c$, has

• Lorentz factor $\gamma = 1/\sqrt{1-|\mathbf v|^2/c^2}$,
• relativistic energy $E_{\mathrm{rel}} = \gamma mc^2$ and relativistic momentum $\mathbf p = \gamma m\mathbf v$,
• rest energy $E_0 = mc^2$, kinetic energy $E_k = E_{\mathrm{rel}} - mc^2$, and relativistic mass $m_{\mathrm{rel}} = E_{\mathrm{rel}}/c^2$.

For a finite system of free particles $i\in s$ the invariant mass is $M = c^{-2}\sqrt{(\sum_i E_i)^2 - c^2|\sum_i\mathbf p_i|^2}$, the total energy over $c^2$ in the centre-of-momentum frame (zero total momentum). A Lorentz boost with speed $|u|<c$ along the first axis sends $(E,\mathbf p)$ to $E' = \gamma_u(E-up_1)$, $\mathbf p' = (\gamma_u(p_1 - uE/c^2), p_2, p_3)$.

Formalization targets

Goal: energy–momentum relation

$$E_{\mathrm{rel}}^2 - |\mathbf p|^2c^2 = m_0^2c^4 \qquad (c>0,\ m_0\ge 0,\ |\mathbf v|<c).$$

It contains $E=mc^2$ as the case $\mathbf p = 0$.

Milestones

1. $E = mc^2$ in the rest frame ($\mathbf v = 0 \Rightarrow \mathbf p = 0,\ E = mc^2$).
2. $E_{\mathrm{rel}} = \sqrt{(m_0c^2)^2 + (pc)^2}$.
3. Massless particles: $E^2-(pc)^2 = 0$, $E,p\ge0 \Rightarrow E = pc$.
4. Relativistic mass: $m_0 \le m_{\mathrm{rel}} = m_0 + E_k/c^2$, with equality iff $\mathbf v = 0$ (for $m_0>0$).
5. Power series $E = m_0c^2\sum_n \binom{2n}{n}4^{-n}(v/c)^{2n} = m_0c^2[1+\tfrac12(v/c)^2+\tfrac38(v/c)^4+\tfrac5{16}(v/c)^6+\cdots]$.
6. Correspondence principle: $E_k = \tfrac12 m_0v^2 + O(v^4)$ as $\mathbf v\to0$.
7. Third-order approximation: $E = m_0c^2 + \tfrac12 m_0v^2(1+\tfrac{3v^2}{4c^2}) + O(v^6)$.
8. Parker Solar Probe: $\tfrac{3v^2}{4c^2}\approx 3.9\times10^{-8}$ for $v = 68\,600$ m/s.
9. $c^2 = 89\,875\,517\,873\,681\,764$ J/kg.
10. Boost invariance of $E^2 - c^2|\mathbf p|^2$: rest mass is the same in all inertial frames.
11. Zero total momentum $\Rightarrow M = \sum_i E_i/c^2$.
12. Non-additivity: $\sum_i m_i \le M$, with equality iff all constituents share one velocity.

Significance

The energy–momentum relation is the kinematic identity behind relativistic energy bookkeeping: rest energy, kinetic energy, invariant-mass reconstruction and the frame independence of rest mass all follow from it. The low-speed expansion makes precise in what sense Newtonian mechanics is the $v\ll c$ limit of relativity. The composite-system statements formalize why, in relativity, mass is neither additive nor separately conserved while energy and momentum are conserved.

All results are classical and established in the physics literature. The mission produces machine-checked versions of these kinematic facts in a reusable $\mathbb R^3$-vector setting with an explicit speed of light.

Difficulty

Most single-particle statements are algebraic once the square roots are controlled; the work lies in handling the square-root and division conventions of a total formal language. The power-series milestone requires the binomial series of $(1-x)^{-1/2}$, and the asymptotic milestones require Taylor-type bounds near $\mathbf v = 0$. The non-additivity milestone is a reverse triangle inequality for future-pointing timelike four-vectors, including its equality case, which does not reduce to a one-line computation.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin 3) for $\mathbb R^3$, with explicit $c$ (no natural units). All definitions are total functions: $\sqrt{x}=0$ for $x<0$ and $x/0 = 0$, so every theorem assumes $c>0$ and $|\mathbf v|<c$; rest masses are assumed non-negative. Massless particles cannot be described by velocity-based quantities ($\gamma$ is undefined at $|\mathbf v| = c$), so milestone 3 is phrased directly in terms of an energy–momentum pair. Only boosts along the first axis are formalized. Systems are finite and free (no interaction potential). Historical derivations (Einstein 1905, Rohrlich 1990) and the nuclear-physics applications are not formalized.

Selected references

• A. Einstein, Ist die Trägheit eines Körpers von seinem Energieinhalt abhängig?, Annalen der Physik 18 (1905) 639–641. https://doi.org/10.1002/andp.19053231314
• A. Einstein, Zur Elektrodynamik bewegter Körper, Annalen der Physik 17 (1905) 891–921. https://doi.org/10.1002/andp.19053221004
• Wikipedia, Mass–energy equivalence. https://en.wikipedia.org/wiki/Mass%E2%80%93energy_equivalence

Motivation

The Yukawa potential (or screened Coulomb potential)

$$V_{\mathrm{Yukawa}}(r) = -g^2\,\frac{e^{-\alpha m r}}{r}$$

was introduced by Hideki Yukawa in 1935 to model the short-range nuclear force as the exchange of a massive particle, later identified with the pion. The same profile reappears as the Debye–Hückel screened interaction in plasmas and electrolytes, as the static Green's function of the massive Klein–Gordon (screened Poisson) operator, and as the Newtonian correction in massive-graviton models. The mathematical facts behind these uses are classical, short, and stated in every textbook treatment — which makes them a natural, self-contained target for formalization: each one is an explicit identity of real analysis in three dimensions.

Timeline. Heisenberg (1932–33) proposed a short-range exchange interaction between nucleons; Fermi (1934) introduced exchange of light particles in beta decay; Yukawa (1935, Proc. Phys.-Math. Soc. Japan 17, 48) combined the two ideas, derived the potential above, and predicted a mediating particle of mass about 200 electron masses; the pion was observed in 1947.

Setting

Throughout, $g\in\mathbb R$ is the coupling (amplitude) constant, $\alpha>0$ a scaling constant, $m\ge 0$ the mass of the exchanged particle and $r>0$ the radial distance; $1/(\alpha m)$ is the range. The potential is the function

$$V(r) = -g^2\,\frac{e^{-\alpha m r}}{r}.$$

Points of space are $x\in\mathbb R^3$ with Euclidean norm $|x|$, and the potential of a point source at the origin is $x\mapsto V(|x|)$. The Laplacian $\Delta$ is the usual sum of unmixed second partial derivatives on $\mathbb R^3$. For a uniform, infinitesimally thin spherical shell of radius $R$ with total scaling constant $G$, the potential felt by a point of scaling constant $g$ located at $x$ is

$$V_{\mathrm{shell}}(x) = G\,g\;\frac{1}{4\pi}\int_{S^2}\frac{e^{-\alpha m |x-Ru|}}{|x-Ru|}\,d\sigma(u),$$

the average over the unit sphere $S^2$ (uniform surface measure $\sigma$) of the pair interaction.

Formalization targets

Goal — Fourier transform of the Yukawa potential

For $\alpha m>0$ and every $k\in\mathbb R^3$,

$$\int_{\mathbb R^3} e^{-i k\cdot x}\,V(|x|)\,d^3x \;=\; -g^2\,\frac{4\pi}{|k|^2+(\alpha m)^2}.$$

This is the identity the article's sections Fourier transform and Feynman amplitude rest on: the momentum-space Yukawa potential is the massive propagator $4\pi/(k^2+(\alpha m)^2)$ times $-g^2$.

Milestones (in the order of the article)

1. Negativity and monotonicity — for $g\neq0$, $V<0$ on $(0,\infty)$ and $V$ is strictly increasing there.
2. Massless limit — for $m=0$, $V(r) = -g^2\cdot\frac1r$ (the Coulomb potential).
3. Screened Poisson equation — $\Delta\,V(|x|) = (\alpha m)^2\,V(|x|)$ for $x\neq0$.
4. Inverse Fourier representation — for $x\ne0$, $V(|x|) = \lim_{\Lambda\to\infty} \frac{-g^2}{(2\pi)^3}\int_{|k|<\Lambda} e^{ik\cdot x}\frac{4\pi}{|k|^2+(\alpha m)^2}\,d^3k$.
5. Born amplitude — $\frac{-2\mu}{\hbar^2 q}\int_0^\infty r\,V(r)\sin(qr)\,dr = \frac{2\mu g^2}{\hbar^2[(\alpha m)^2+q^2]}$ for $q>0$.
6. Momentum transfer — $|\vec p-\vec p'| = 2p\sin(\theta/2)$ when $|\vec p|=|\vec p'|=p$ and $\theta$ is the angle between them.
7. Total cross section — $\frac{4\mu^2g^4}{\hbar^4}\int_0^\pi\frac{2\pi\sin\theta\,d\theta}{[(\alpha m)^2+4p^2\sin^2(\theta/2)]^2} = \frac{4\mu^2g^4}{\hbar^4}\,\frac{4\pi}{(\alpha m)^2[(\alpha m)^2+4p^2]}$.
8. Shell, exterior — for $|x|>R$, $V_{\mathrm{shell}}(x) = G g\,\frac{e^{-\alpha m|x|}}{|x|}\,\frac{\sinh(\alpha m R)}{\alpha m R}$.
9. Shell, interior — for $0<|x|<R$, $V_{\mathrm{shell}}(x) = G g\,\frac{e^{-\alpha m R}}{R}\,\frac{\sinh(\alpha m |x|)}{\alpha m |x|}$.

Significance

The results. The Fourier identity is what makes the Yukawa potential the non-relativistic limit of single-meson exchange; milestone 3 identifies it as the Green's function of the screened Poisson operator $-\Delta + (\alpha m)^2$; milestones 5–7 give the Born-approximation scattering amplitude and the closed-form total cross section quoted in quantum mechanics textbooks (e.g. Griffiths); milestones 8–9 are the Yukawa analogue of Newton's shell theorem, whose failure to reduce to a point source of the same strength is the reason massive-graviton models violate the weak equivalence principle.

Formalizing them. All statements are classical and proved on paper. The mission produces machine-checked versions together with reusable infrastructure: three-dimensional Fourier integrals of radial functions, Laplacians of radial functions, spherical averages with respect to the surface measure, and conditionally convergent oscillatory integrals.

Difficulty

The individual computations are short on paper but each crosses a gap in the library. The goal requires reducing a three-dimensional Lebesgue integral of a radial function to a one-dimensional integral (polar coordinates in $\mathbb R^3$), then evaluating $\int_0^\infty e^{-ar}\sin(kr)\,dr$. The inverse transform is not absolutely convergent — $1/(|k|^2+a^2)$ is not integrable on $\mathbb R^3$ — so the naive Lebesgue statement is false (it would assign the value $0$); only the ball-truncated limit is meaningful, and its evaluation needs the improper integral $\int_0^\infty \frac{k\sin(kr)}{k^2+a^2}dk = \frac{\pi}{2}e^{-ar}$. The shell theorem needs the surface measure on $S^2$ and the Archimedes-type change of variables $u\mapsto |x-Ru|$.

Formalization scope

All quantities are real numbers; space is EuclideanSpace ℝ (Fin 3) with Lebesgue measure. The potential is a single definition YukawaPotential.yukawaPotential g α m r; at $r=0$ Lean's division convention gives the junk value $0$, so every statement either restricts to $r>0$ / $x\neq0$ or integrates (where a single point is null). The physical conventions $\alpha>0$, $m\ge0$ (and $m>0$ where the article divides by $\alpha m$) are explicit hypotheses. The Fourier transform uses the convention $\hat V(k)=\int e^{-ik\cdot x}V$, $V=(2\pi)^{-3}\int e^{ik\cdot x}\hat V$; the inverse is stated as a limit over balls. The shell potential averages over the unit sphere with Mathlib's Measure.toSphere (uniform surface measure); since it is an average, its normalisation is irrelevant. The Laplacian is Mathlib's Laplacian.laplacian on inner-product spaces. Physical constants $\mu,\hbar$ in milestones 5 and 7 are arbitrary reals: the identities hold without sign assumptions on them.

Out of scope: the historical mass estimate of the pion, the heuristic wave-equation derivation of the photon/pion dispersion relations, the perturbative asymptotic expansions of Schrödinger eigenvalues and Regge trajectories (stated in the source only up to unspecified $\mathcal O(K^{-7})$ and "$\cdots$" terms), and the $m\to0$ limits of the shell formulas.

Contributions welcome: polar-coordinate integration for radial functions on $\mathbb R^3$, spherical-average lemmas, and the improper integrals above as standalone lemmas.

Selected references

• H. Yukawa, On the interaction of elementary particles, Proc. Phys.-Math. Soc. Japan 17, 48 (1935). https://doi.org/10.11429/ppmsj1919.17.0_48
• D. J. Griffiths, Introduction to Quantum Mechanics, Cambridge University Press (2017), p. 415.
• R. P. Feynman, R. B. Leighton, M. Sands, The Feynman Lectures on Physics, Vol. II, Ch. 28 (1964). https://www.feynmanlectures.caltech.edu/II_28.html
• K. McDonald, A Naïve Estimate of the Coupling Constant in Yukawa Theory (1984/2021). http://kirkmcd.princeton.edu/examples/yukawa.pdf
• Wikipedia, Yukawa potential, revision 1371658231. https://en.wikipedia.org/w/index.php?title=Yukawa_potential&oldid=1371658231

Motivation

In the usual textbook presentation, quantum theory starts from postulates that have no obvious operational meaning: states are density operators on a complex Hilbert space, measurements are positive operators, and probabilities are given by the trace formula $p=\mathrm{tr}(\hat A\hat\rho)$. In Quantum Theory From Five Reasonable Axioms (Hardy 2001), Lucien Hardy asks whether this structure can instead be derived from simple statements about preparations, transformations and measurements, in the same way that classical probability theory can be set up by pure thought. He proposes five axioms (probabilities, simplicity, subspaces, composite systems, continuity) and argues that they single out finite- and countably-infinite-dimensional quantum theory. Dropping a single word, "continuous" in Axiom 5, leaves classical probability theory instead.

The paper is one of the starting points of the operational or generalized probabilistic theory (GPT) approach to the foundations of quantum mechanics. It was followed by reconstructions that replace the simplicity axiom, e.g. Dakić–Brukner 2009, Masanes–Müller 2011 and Chiribella–D'Ariano–Perinotti 2011.

Setting

A system is described by two integers. The dimension $N$ is the maximum number of states that can be distinguished in a single-shot measurement. The number of degrees of freedom $K$ is the minimum number of probability measurements needed to determine the state. The state is the vector $p=(p^1,\dots,p^K)\in\mathbb R^K$ of the probabilities of $K$ fiducial measurements. States are not assumed normalized: the null state $p=0$ (no system present) is allowed. The set $S$ of allowed states is convex, and its pure states are its extremal points other than $0$.

The five axioms are:

1. Probabilities. Relative frequencies converge to the same limit for every ensemble prepared by a given preparation.
2. Simplicity. $K=K(N)$ is a function of $N=1,2,\dots$, and for each $N$ it takes the minimum value consistent with the axioms.
3. Subspaces. A system whose state is constrained to an $M$-dimensional subspace behaves like a system of dimension $M$.
4. Composite systems. A composite of systems $A$ and $B$ has $N=N_AN_B$ and $K=K_AK_B$.
5. Continuity. Between any two pure states there is a continuous reversible transformation.

A probability theory can be summarized by its signature $x=(x_1,x_2,\dots)$, defined through

$$K=Nx_1+\tfrac1{2!}N(N-1)x_2+\tfrac1{3!}N(N-1)(N-2)x_3+\cdots=\sum_{k\ge1}\binom Nk x_k .$$

Classical probability theory has $x=(1,0,0,\dots)$ and $K=N$. Complex quantum theory has $x=(1,2,0,\dots)$ and $K=N^2$. Real and quaternionic quantum theory have $x=(1,1,0,\dots)$ and $x=(1,4,0,\dots)$.

Formalization targets

Goal: $K(N)=N^r$

Section 8.1 shows that Axiom 3 forces $K(N+1)\ge K(N)+1$, and Axiom 4 forces $K(N_AN_B)=K(N_A)K(N_B)$. The goal theorem is the purely arithmetic consequence (Eq. (57)):

$$K(N+1)\ge K(N)+1\ \text{ and }\ K(N_AN_B)=K(N_A)K(N_B)\ \ (N,N_A,N_B\ge1)\quad\Longrightarrow\quad \exists r\in\{1,2,3,\dots\}:\ K(N)=N^r\ \ \forall N\ge1 .$$

Milestones

The milestones follow the paper's own steps, in the paper's numbering:

• Appendix 2: a strictly increasing, completely multiplicative $K$ on the positive integers satisfies $K(n)=n^\alpha$. Section 8.1: if every $n^\alpha$ is an integer, then $\alpha$ is a positive integer.
• Section 6.6 / Appendix 1: measured probabilities are linear in the state, $p_{\rm meas}=r\cdot p$. Section 6.7: transformations act as matrices, $p\mapsto Zp$. Section 7: reversible transformations send pure states to pure states.
• Section 4 / 8.5: in classical probability theory the pure states are exactly the $N$ basis states, and no continuous path of pure states joins two distinct ones. The equations $\sum_k(p^k)^2=1$, $0\le p^k\le1$, $\sum_kp^k=1$ force a basis vector.
• Sections 5 and 8.1: the signatures of the classical, quantum, real, quaternionic and $K=N^3$ theories, and the failure of $K=K_AK_B$ for real (too many) and quaternionic (too few) composites.
• Section 5: the $N^2$ projectors $|n\rangle\langle n|$, $|mn\rangle_x\langle mn|$, $|mn\rangle_y\langle mn|$ are linearly independent over $\mathbb R$ and span the Hermitian operators.
• Sections 5 and 8.6 ($N=2$): the overlap formula (35) for $c$; $\det D>0 \iff c_-<c<c_+$; the decomposition $r^TDr'=\vec v^{\,T}A\vec v'+\mu\mu'/2$; $A$ positive definite $\iff c_-<c<c_+$; the Bloch matrix (87).
• Section 8.7 ($N=3$): the $9\times9$ matrix $D_{ij}=\mathrm{tr}(\hat P_i\hat P_j)$ with $h=1/2$, $q=1/4$.

Significance

The goal is the step at which the two structural axioms (subspaces and composites) cut the space of possible theories down to a single integer parameter $r$. Combined with Section 8.5, which rules out $r=1$ by continuity, and with the simplicity axiom, it gives $K=N^2$. Everything after that in the paper (the Bloch sphere, general $N$, the trace formula, complete positivity) is carried out inside the $K=N^2$ case. The milestones on signatures make precise in which sense real and quaternionic quantum theory are excluded: their degree-of-freedom counts are not multiplicative under composition.

The paper's argument is informal physics. This mission isolates the mathematically precise statements that the argument relies on, so that they can be proved independently of the physical interpretation. It does not formalize the axioms themselves as a single Lean structure.

Difficulty

The arithmetic goal is an instance of a classical question about monotone completely multiplicative functions. Complete multiplicativity alone fixes $K$ only through its values at the primes, which are a priori unrelated to one another, and monotonicity is the only link between different primes. The step from a real exponent $\alpha$ to an integer exponent is a separate integrality argument that the paper does not spell out. The linearity milestones need care because the hypotheses hold only on a convex set containing $0$, not on all of $\mathbb R^K$. The $N=2$ milestones are explicit but delicate algebra with square roots and boundary cases $a,b\in\{0,1\}$.

Formalization scope

• All theorems live in the namespace HardyFiveAxioms. State vectors are functions Fin K → ℝ. Indices are $0$-based, so the paper's fiducial vector $k$ is index $k-1$.
• $K(N)$ is a function ℕ → ℕ (goal) or ℕ → ℝ (Appendix 2), constrained only at arguments $\ge1$. The value at $0$ is irrelevant.
• The signature is a finite list [x₁, …, x_L], and $\frac1{k!}N(N-1)\cdots(N-k+1)$ is written as the binomial coefficient $\binom Nk$.
• Pure states are Set.extremePoints ℝ S \ {0}. The classical state space is $\{p\ge0,\ \sum_np_n\le1\}$.
• The quantum projectors are explicit matrices vecMulVec v (star v) over ℂ, and the qubit matrices $D$, $C$, $A$ and the roots $c_\pm$ are explicit definitions.
• Axiom 5's "continuous reversible transformation" enters only through the classical milestone, as a continuous path unitInterval → ℝᴺ that stays inside the pure states.
• The goal does not assume the conclusion in disguise. Its hypotheses are the two consequences of Axioms 3 and 4 derived in Section 8.1. It is not vacuous: $K(N)=N^r$ satisfies both hypotheses for every $r\ge1$.

Contributions are welcome on any milestone. The linearity, extreme-point and positive-definiteness lemmas are reusable beyond this mission.

Selected references

• L. Hardy, Quantum Theory From Five Reasonable Axioms, arXiv:quant-ph/0101012v4, 2001. https://arxiv.org/abs/quant-ph/0101012
• B. Dakić, Č. Brukner, Quantum Theory and Beyond: Is Entanglement Special?, 2009. https://arxiv.org/abs/0911.0695
• Ll. Masanes, M. P. Müller, A derivation of quantum theory from physical requirements, New J. Phys. 13, 063001, 2011. https://arxiv.org/abs/1004.1483
• G. Chiribella, G. M. D'Ariano, P. Perinotti, Informational derivation of quantum theory, Phys. Rev. A 84, 012311, 2011. https://arxiv.org/abs/1011.6451