Mathematical Physics

1. Motivation

Carcassi, Landini and Aidala (arXiv:2411.00972) argue that classical mechanics is the high-entropy limit of quantum mechanics, in the same way that non-relativistic mechanics is the low-speed limit of relativistic mechanics. The usual mathematical recipe $\hbar \to 0$ is reinterpreted as sending the entropy of pure states to $-\infty$, i.e. as $S \gg 0$. The paper backs this with explicit formulas: Gaussian entropy–uncertainty curves, the black-body spectrum, the trace identity for the maximally mixed state, classical and quantum "stretching maps" on phase space, and a Lindblad master equation that implements the quantum stretch. This mission formalizes those mathematical claims.

2. Setting

We use one degree of freedom with phase space $\mathbb R^2 \ni (x,p)$.

• Gaussian entropies. For a Gaussian state with uncertainty $\Sigma = \sigma_x\sigma_p$ the classical (Gibbs) entropy is $S_C(\Sigma) = \ln(\Sigma/\hbar) + 1$ (Eq. 2). The quantum (von Neumann) entropy is $S_Q(\Sigma) = (\tfrac{\Sigma}{\hbar}+\tfrac12)\ln(\tfrac{\Sigma}{\hbar}+\tfrac12) - (\tfrac{\Sigma}{\hbar}-\tfrac12)\ln(\tfrac{\Sigma}{\hbar}-\tfrac12)$ (Eq. 3). The rescaled quantum entropy of Section 4.3 is $S^\lambda_Q(\Sigma) = S_Q(\lambda\Sigma) - \ln\lambda$. It is the quantum curve after shrinking the pure-state uncertainty from $\hbar$ to $\hbar/\lambda$ and moving the zero of entropy accordingly.
• Pure stretching map. $T(x,p) = (\sqrt\lambda x, \sqrt\lambda p)$ with $\lambda > 1$ (Eq. 16). It acts on densities by push-forward, $(T\rho)(z) = \lambda^{-1}\rho(z/\sqrt\lambda)$. The Gibbs entropy is $S(\rho) = -\int\rho\log\rho$ (Eq. 15). The same stretch acts on Husimi distributions on $\mathbb C$: $Q_\lambda(\alpha) = \lambda^{-1}Q_1(\alpha/\sqrt\lambda)$ (Eq. 24).
• Lindblad generator. In the Heisenberg picture, $\dot X = \tfrac{i}{\hbar}[H,X] + \sum_i\gamma_i(L_i^\dagger X L_i - \tfrac12\{L_i^\dagger L_i, X\})$ (Eq. 26). The quantum stretch uses $H = 0$ and a single jump operator $L = a^\dagger$, where the ladder operators satisfy $[a,a^\dagger] = 1$.

3. Target

The goal (Section 4.3, Fig. 3, p. 11): for all $\hbar > 0$ and $\Sigma > 0$,

$$\lim_{\lambda\to\infty}\big(S_Q(\lambda\Sigma) - \ln\lambda\big) = \ln(\Sigma/\hbar) + 1 = S_C(\Sigma).$$

This is the quantitative form of "taking $\lambda\to\infty$ is equivalent to $\hbar\to0$": the quantum Gaussian entropy curve converges to the classical one.

Milestones, in the order of the paper:

1. Zeros and signs of the entropy curves (Sec. 2.2): $S_Q(\hbar/2)=0$ and $S_Q>0$ above the Heisenberg bound; $S_C(\hbar/e) = 0$ and $S_C<0$ below it.
2. Fig. 2: $S_C(\Sigma) - S_Q(\Sigma) \to 0$ as $\Sigma\to\infty$.
3. Eq. (4): $\operatorname{tr}(AB\,I/n) = \operatorname{tr}(BA\,I/n)$.
4. Eq. (8): Planck's law divided by the Rayleigh–Jeans law tends to $1$ as $\beta\to0^+$.
5. Eq. (15): $S(T\rho) = S(\rho) + \log\lambda$.
6. Eq. (18): $\langle T(x^np^m)\rangle = \sqrt\lambda^{\,n+m}\langle x^np^m\rangle$.
7. Eq. (25): $\int\alpha^n\bar\alpha^m Q_\lambda = \sqrt\lambda^{\,n+m}\int\beta^n\bar\beta^mQ_1$.
8. Eq. (28): for $L = a^\dagger$, $H=0$, the generator maps $a^n(a^\dagger)^m$ to $\tfrac\gamma2(n+m)\,a^n(a^\dagger)^m$.
9. Eq. (38): $[\sqrt\lambda X, \sqrt\lambda P] = i\lambda\hbar$ when $[X,P] = i\hbar$.

4. Significance

The goal makes the slogan "classical = high-entropy quantum" precise for Gaussian states: the classical entropy–uncertainty law is exactly the limit of the quantum one under the entropy rescaling the paper constructs. The milestones are the computational facts the argument rests on. The paper derives them by hand and none has been machine-checked. Several are reusable well beyond this paper: entropy under scaling of densities, moment scaling under dilations, and the action of the Lindblad generator on anti-normally ordered monomials in the Weyl algebra.

5. Difficulty

The goal is an asymptotic expansion of $x\mapsto(x+\tfrac12)\ln(x+\tfrac12) - (x-\tfrac12)\ln(x-\tfrac12)$ at infinity. The naive term-by-term limit has the form $\infty-\infty$ and must be organised as a difference quotient or Taylor expansion of $x\ln x$. The measure-theoretic milestones need change of variables for the dilation $z\mapsto z/\sqrt\lambda$ on $\mathbb R^2$ and $\mathbb C$, plus careful integrability bookkeeping for $\rho\log\rho$. The Lindblad milestone needs the commutator identities $[a^n, a^\dagger] = n a^{n-1}$ and $[a, (a^\dagger)^m] = m (a^\dagger)^{m-1}$ in a noncommutative ring.

6. Formalization scope

• Entropies are real functions of $\hbar$ and $\Sigma$; we assume $\hbar>0$ and $\Sigma>0$. Lean's Real.log returns $0$ at $0$, which agrees with the convention $0\ln0=0$ at the Heisenberg point $\Sigma=\hbar/2$.
• Phase space is ℝ × ℝ with Lebesgue measure, and Husimi distributions live on ℂ. Densities are real functions. The entropy milestone assumes $\rho\ge0$, $\int\rho = 1$, and integrability of $\rho$ and $\rho\log\rho$, i.e. finite entropy, which the paper uses implicitly. The moment identities hold for every function, since an integral that does not converge is $0$ on both sides.
• Ladder operators are elements $a, a^\dagger$ of an abstract ℂ-algebra with $aa^\dagger - a^\dagger a = 1$, and the adjoint of each jump operator is passed explicitly. This avoids unbounded operators. The hypothesis is satisfiable, e.g. by differentiation and multiplication by $X$ on $\mathbb C[X]$. No bounded operators satisfy it, so do not specialise to a C*-algebra.
• $\lambda>1$ throughout, as in the paper ($\Delta S = \log\lambda > 0$).
• Out of scope: the CPTP property and entropy monotonicity of $T_Q$ (Eqs. 31–32), and the Wigner-function formulas (Eqs. 46–54). These need operator theory on $L^2$ that is not available in Mathlib.

Selected references

• G. Carcassi, M. Landini, C. A. Aidala, Classical mechanics as the high-entropy limit of quantum mechanics, arXiv:2411.00972v3 (2026). https://arxiv.org/abs/2411.00972
• M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press (2010).

Motivation

Quantum states are standardly modelled as rays in a complex Hilbert space, following von Neumann's 1932 axiomatisation. Carcassi, Aidala and Calderón (arXiv:2308.06669) examine which parts of this definition can be justified by physical requirements. They argue that the inner product space structure is physically required — it is exactly what is needed to describe statistical mixtures of states and their entropy — while completeness in infinite dimensions is not: it forces the state space to contain states with infinite expectation values, coordinate changes that turn finite expectations into infinite ones, and time evolutions that do so in finite time. The paper suggests Schwartz spaces as a possible alternative.

The physical conclusions of the paper (its Propositions 19 and 31) are arguments, not mathematical theorems. Behind them, however, sits a set of precise mathematical statements in Section VI and Appendix A. This mission formalizes those statements.

Setting

Let $H$ be a complex inner product space, not necessarily complete. For $\psi\in H$, $|\psi\rangle\langle\psi|$ is the operator $x\mapsto\langle\psi,x\rangle\psi$. A finite mixture of pure states is an operator $\sum_i a_i|\psi_i\rangle\langle\psi_i|$ with finitely many unit vectors $\psi_i$ and weights $a_i>0$ summing to $1$. The von Neumann entropy of such an operator is $S(\rho)=-\sum_k\lambda_k\log\lambda_k$ over its eigenvalues, and $I(\psi,\phi)$ denotes the entropy of the equal mixture $\frac12|\psi\rangle\langle\psi|+\frac12|\phi\rangle\langle\phi|$.

On the position side, $L^2(\mathbb R)$ is the Hilbert space of square-integrable complex wave functions. An orientation-preserving diffeomorphism $f:\mathbb R\to\mathbb R$ (smooth, strictly increasing, with smooth inverse) acts on wave functions by

$$(U_f\psi)(y)=\psi\bigl(f^{-1}(y)\bigr)\sqrt{|(f^{-1})'(y)|},$$

which is the transformation law of a wave function under the change of coordinate $y=f(x)$. The $n$-th absolute position moment of a state $\psi$ is $\int|x|^n|\psi(x)|^2\,dx\in[0,\infty]$; finite moments of all orders are the natural minimal requirement for the statistics of position to be well defined.

Formalization targets

Goal

$$\exists\,f,\ U=U_f,\ \psi\in L^2(\mathbb R),\ \|\psi\|=1:\quad \int|x|^n|\psi|^2<\infty\ \ \forall n,\qquad \int y^2\,|U\psi(y)|^2\,dy=\infty .$$

A unitary transformation of $L^2(\mathbb R)$ that is nothing but a change of the position coordinate can map a state with all moments finite to one with infinite expected squared position. The goal is stated existentially, leaving the particular change of coordinates free.

Milestones

1. Proposition 5 — rays alone do not determine the coefficients of a superposition.
2. Proposition 7 — equal strictly convex mixtures span the same subspace.
3. Proposition 8 — a finite-rank mixed state can be decomposed so as to include a given pure state from its range.
4. Proposition 9 — $\psi$ is a superposition of $\{\phi_j\}$ iff some mixture of the $\phi_j$ can also be written as a mixture including $\psi$.
5. Proposition 10 — $I(\psi,\phi)=f(|\langle\psi,\phi\rangle|)$ with an explicit $f$ injective on $[0,1]$.
6. Proposition 20 — the domain of an unbounded closed operator between Hilbert spaces is not complete.
7. Proposition 21 — a unitary can move a vector out of such a domain.
8. Proposition 24 — $U_f$ is unitary on $L^2(\mathbb R)$.
9. Equation (29) — $y(x)=\tan(\frac\pi2\operatorname{erf}x)$ is an orientation-preserving diffeomorphism transporting the Gaussian state $\sqrt{e^{-x^2}/\sqrt\pi}$ to $1/\sqrt{\pi(y^2+1)}$.
10. Equations (27)–(28) — the Gaussian state has all moments finite, the Lorentzian state has all moments of order $\ge2$ infinite.

Significance

The goal makes precise one of the paper's three claims about completeness: being an isomorphism of Hilbert spaces does not respect finiteness of expectation values, even for a transformation as innocuous as a smooth change of coordinates. Propositions 20 and 21 make precise the companion claim that completeness forces the inclusion of states outside the domain of every unbounded observable, and that unitaries do not preserve such domains. Propositions 7–10 make precise the paper's case for the inner product: equivalence of superposition with non-unique decomposition of mixtures, and the entropic meaning of the transition probability.

All statements are mathematically elementary relative to modern functional analysis, and none of them, to the knowledge of the proposer, has a machine-checked proof. Formalizing them pins down hypotheses the paper leaves implicit: two statements needed corrections to be true (see the notes on Propositions 8 and 20).

Difficulty

Most of the work is infrastructure rather than a single hard step. Proposition 24 requires the change-of-variables formula for Lebesgue integrals and a construction of the induced operator on $L^2$ equivalence classes, including surjectivity. Equation (29) requires developing the error function (limits $\pm1$ at $\pm\infty$, smoothness, positivity of its derivative) and differentiating $\tan\circ(\frac\pi2\operatorname{erf})$. Proposition 10 requires computing the spectrum of a rank-two operator through the eigenvalue API for self-adjoint operators on a finite-dimensional space. Proposition 20 rests on the closed graph theorem. The moment statements require Gaussian integrability and a comparison of $|y|^n/(1+y^2)$ with $1/|y|$ at infinity.

Formalization scope

All statements live in the namespace UnphysicalHilbert. State spaces are complex inner product spaces (InnerProductSpace ℂ H), completeness assumed only where the paper assumes a Hilbert space. Finite sets of states are finite indexed families; a finite-rank density operator is a finite strictly convex combination of pure states. The entropy of the equal mixture is computed on the span of the two vectors, on which the operator acts. $L^2(\mathbb R)$ is Lp ℂ 2 volume, unitaries are linear isometric equivalences, and finiteness of a moment means Lebesgue integrability of $|x|^n|\psi(x)|^2$.

Two departures from the text are deliberate and flagged in the item notes: Proposition 8 assumes $\psi\in\operatorname{range}\rho$ instead of $\langle\psi|\rho|\psi\rangle\neq0$ (the latter admits a counterexample in $\mathbb C^2$), and Propositions 20–21 assume the operator is closed (without some such hypothesis an everywhere-defined discontinuous functional is a counterexample). Proposition 5 assumes the coefficients are nonzero, which its proof uses. The time evolution of eq. (30) and the remarks on Schwartz spaces in Section VIII are not formalized, because the paper does not state them as propositions. The existential goal cannot be satisfied trivially: the operator is pinned to the change-of-variables formula, and $\psi$ must be a unit vector with all moments finite.

Contributions of reusable infrastructure are welcome, in particular: the error function, the unitary on $L^2(\mathbb R)$ induced by a diffeomorphism, and the spectrum of $\frac12(|\psi\rangle\langle\psi|+|\phi\rangle\langle\phi|)$.

Selected references

• G. Carcassi, C. A. Aidala, F. Calderón, The unphysicality of Hilbert spaces, arXiv:2308.06669v3, 2024. https://arxiv.org/abs/2308.06669
• J. von Neumann, Mathematische Grundlagen der Quantenmechanik, Springer, 1932.
• M. Reed, B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Academic Press, 1980.
• B. C. Hall, Quantum Theory for Mathematicians, Graduate Texts in Mathematics 267, Springer, 2013. https://doi.org/10.1007/978-1-4614-7116-5

Motivation

The rotation curves of spiral galaxies indicate that galaxies sit inside extended dark halos whose mass dominates the visible matter (Faber–Gallagher 1979). If the halo is a gas of elementary particles moving at galactic velocities ($v \sim 200$ km/s), those particles stream through every laboratory on Earth. In 1985 Goodman and Witten asked whether a detector then being proposed for neutrinos — the superconducting-grain detector of Drukier and Stodolsky, which registers nuclear recoils of tens of eV and up through elastic neutral-current scattering (Drukier–Stodolsky 1984) — could see halo particles by the same mechanism.

Their answer, worked out with a handful of explicit formulas, was yes for three broad classes of candidates: particles with coherent weak interactions, particles with spin-dependent interactions of weak strength (with the photino as the example), and strongly interacting particles. The paper is the starting point of direct dark-matter detection: the recoil-energy kinematics, the counting-rate formula and the split into spin-independent and spin-dependent couplings introduced here are still the standard framework of every nuclear-recoil experiment.

Setting

A halo particle of mass $m$ and speed $v$ scatters elastically from a target nucleus of mass number $A$, mass $M = A\,m_N$, at rest. In a non-relativistic elastic collision momentum and kinetic energy are conserved, and the recoil kinetic energy deposited in the nucleus is bounded by

$$\epsilon = \frac{(2mv)^2}{2M}.$$

A kilogram of detector contains $K = 6.0\times10^{26}/A$ target nuclei. Halo particles of mass density $\rho$ have number density $\rho/m$ and flux $F = \rho v/m$, so the counting rate with cross section $\sigma$ is $R = KF\sigma$, quoted in events per kilogram per day. The paper normalises with the reduced cross section $\bar\sigma = (\sigma/A)(1\ \mathrm{GeV}/m)$.

For a constant invariant amplitude $\mathcal M$ the elastic cross section is

$$\sigma = \frac{m^2M^2}{\pi(m+M)^2}\,|\mathcal M|^2 .$$

The three candidate classes differ only in $\mathcal M$ (or $\sigma$):

1. Coherent weak: $\mathcal M = G_F\bar Y\bar N/\sqrt2$, where $\bar Y$ is the weak hypercharge combination of the particle and $\bar N = N - (1-4\sin^2\theta)Z$ for a nucleus with $N$ neutrons and $Z$ protons.
2. Spin-dependent (photino): $\langle|\mathcal M|^2\rangle = (4q^4/M_{\tilde Q}^4)\,\lambda^2J(J+1)$, where $q$ is the charge of the light quark, $M_{\tilde Q}$ the mass of its scalar partner, $J$ the nuclear spin and $\lambda$ a nuclear-structure constant.
3. Strongly interacting: a hard-sphere cross section $\sigma = 4\pi R_{\mathrm{nuc}}^2$ with $R_{\mathrm{nuc}} = 1.25A^{1/3}\times10^{-13}$ cm, multiplied by a stopping factor $\epsilon \le 1$ for the earth or the atmosphere.

Standard halo values are $\rho = 10^{-24}$ g/cm$^3$ and $v = 200$ km/s, and the benchmark detector sensitivity is 1 event/kg/day.

Formalization targets

Goal: the three detectability claims

With $\rho = 10^{-24}$ g/cm$^3$ and $v = 200$ km/s:

1. for a lead target and $\bar Y = 1$, the coherent rate of Eq. (2) is at least 1 event/kg/day for all $1\ \mathrm{GeV}\le m\le10^7$ GeV (for any $0.2\le\sin^2\theta\le0.25$);
2. for photinos with mass equal to the nuclear mass and $\lambda^2J(J+1) = 1$, the rate is of order 1 event/kg/day, $1\le R<10$, for $(q, M_{\tilde Q}) = (\tfrac23e, 100\ \mathrm{GeV})$ and $(\tfrac13e, 50\ \mathrm{GeV})$;
3. for targets from aluminium to lead ($27\le A\le207$) and $\epsilon = 1$, strongly interacting particles give at least 1 event/kg/day exactly up to a mass

$$M^*\in[1.5\times10^{13},\,4.5\times10^{13}]\ \mathrm{GeV}.$$

Milestones

The milestones follow the paper's equations in order: the recoil bounds and the 1–2 GeV lower mass limit (p. 3059); the counting-rate formula, Eq. (1); the coherent reduced cross section, Eq. (2), and the resulting $10^4$/kg day rates; the photino rate, Eq. (3); the quark-model matrix elements, Eq. (4), and the factor-100 flavour asymmetry; and the hard-sphere cross section and rate, Eq. (6).

Significance

The result. The paper turned dark-matter direct detection from an abstract possibility into a quantitative experimental programme: it fixed the minimal detectable mass from kinematics, gave a single counting-rate formula into which any particle-physics model can be inserted, and showed that coherent (spin-independent) scattering on heavy nuclei is enhanced by $\bar N^2$ while spin-dependent scattering needs odd nuclei. These estimates set the scale of rates, from $10^4$ events/kg/day for coherent weak particles down to 1 event/kg/day for photinos, against which later experiments were designed.

Formalizing it. The statements are elementary but they are exactly the kind of order-of-magnitude chain where a unit conversion, a missing factor of 2 or $\pi$, or a convention for the nuclear mass silently changes a number. A machine-checked version records every convention explicitly, checks each printed coefficient against modern values of the constants, and separates genuine theorems (the kinematic bound) from numerical consequences of the formulas.

Difficulty

The only genuinely geometric statement is the recoil bound, which must hold for every direction of scattering in three dimensions, not just head-on collisions. All other milestones are exact identities between the definitions plus verified numerical bounds involving $\pi$, real powers $A^{1/3}$ and scientific-notation constants spanning more than fifty orders of magnitude. The obstacle is keeping these bounds tight enough: several of the paper's coefficients are reproduced only to a few percent, so loose estimates of $\pi$ or of $A^{1/3}$ over a range of $A$ will not close the inequalities, and the detectability statements require monotonicity arguments over whole mass intervals rather than evaluation at one point.

Formalization scope

All quantities are real numbers in a fixed unit system: masses and energies in GeV with $c = 1$, velocities as fractions of $c$ in kinematic statements and in cm/s in rate statements, densities in g/cm$^3$, cross sections in cm$^2$, squared amplitudes in GeV$^{-4}$ converted to cm$^2$ by $(\hbar c)^2$. The constants are $c$, $1\ \mathrm{GeV}/c^2$ in grams, $\hbar c$, $G_F$ and $\alpha$ at their modern values, the paper's $K = 6.0\times10^{26}/A$, and nuclear mass $M = A\,m_N$ with $m_N = 0.9383$ GeV (the paper writes $M\simeq A$ GeV; the nucleon mass reproduces its printed coefficients).

Approximate equalities "$\approx c_0$" in the paper are encoded as the existence of an exact coefficient $C$ with $|C/c_0-1|\le0.05$ for which the formula holds identically in all parameters, so a statement cannot be satisfied by a coefficient unrelated to the definitions. "Of order $10^k$" is encoded as $10^k\le R<10^{k+1}$. Eq. (2) is used without the nuclear form factor, as in the paper's sentence about lead; the reduced Table II rates with loss of coherence and Eqs. (5) and (7) are outside the scope of this mission.

The development needs only real analysis from Mathlib: inner-product geometry in $\mathbb R^3$ for the recoil bound, and bounds on $\pi$ and on real powers for the numerics. Contributions of reusable lemmas for certified numerical bounds on rpow expressions are welcome.

Selected references

• M. W. Goodman and E. Witten, Detectability of certain dark-matter candidates, Phys. Rev. D 31, 3059 (1985). https://doi.org/10.1103/PhysRevD.31.3059
• A. Drukier and L. Stodolsky, Principles and applications of a neutral-current detector for neutrino physics and astronomy, Phys. Rev. D 30, 2295 (1984). https://doi.org/10.1103/PhysRevD.30.2295
• S. M. Faber and J. S. Gallagher, Masses and mass-to-light ratios of galaxies, Annu. Rev. Astron. Astrophys. 17, 135 (1979). https://doi.org/10.1146/annurev.aa.17.090179.001031

Motivation

Single-field slow-roll inflation predicts primordial curvature fluctuations that are very close to Gaussian. The leading departure from Gaussianity is the three-point function (the bispectrum) of the curvature perturbation $\zeta$. Maldacena (2003) computed it from first principles: he derived the cubic action for scalar and tensor fluctuations, evaluated the tree-level correlators with the standard choice of vacuum, and gave closed formulas at leading order in slow roll, with exact numerical coefficients and full momentum dependence. For the three-scalar correlator, earlier estimates included only part of the effect.

The paper also points out a structural property. When one momentum is much smaller than the other two (the squeezed limit), the three-point function is fixed by the tilt of the two-point function. Today this is called Maldacena's consistency relation. It is the standard test of single-field inflation against cosmic microwave background and large-scale-structure data, and the starting point of a large literature on soft theorems in cosmology.

Setting

Units are $M_{pl}^{-2} = 8\pi G_N = 1$. The background is a spatially flat FRW metric $ds^2 = -dt^2 + e^{2\rho(t)}dx^i dx^i$ with a homogeneous scalar field $\phi(t)$ obeying

$$3\dot\rho^2 = \tfrac12\dot\phi^2 + V(\phi),\qquad \ddot\rho = -\tfrac12\dot\phi^2,\qquad \ddot\phi + 3\dot\rho\dot\phi + V'(\phi) = 0,$$

and $H = \dot\rho$. A starred quantity is evaluated at horizon crossing. Write $k_i = |\vec k_i|$ and $k_t = k_1+k_2+k_3$. Momentum conservation $\vec k_1 + \vec k_2 + \vec k_3 = 0$ means that $(k_1,k_2,k_3)$ are the side lengths of a (possibly degenerate) triangle. All correlators below are written without the overall factor $(2\pi)^3\delta^3(\sum_i \vec k_i)$.

1. Power spectra (eqs. 2.20, 2.29): $P_\zeta(k) = \frac{1}{2k^3}\dot\rho_*^2\frac{\dot\rho_*^2}{\dot\phi_*^2}$ and $P_\gamma(k) = \frac{1}{2k^3}\,2\dot\rho_*^2$.
2. Tilts (eqs. 2.22, 2.30): $n_s = -2\big(\frac{\ddot\phi_*}{\dot\rho_*\dot\phi_*} + \frac{\dot\phi_*^2}{\dot\rho_*^2}\big)$ and $n_t = -\frac{\dot\phi_*^2}{\dot\rho_*^2}$. Here $n_s$ is the exponent in $P_\zeta \propto k^{-3+n_s}$, so it is "$n_s - 1$" in the modern convention.
3. Three-scalar correlator (eqs. 4.5–4.6): $B_\zeta(k_1,k_2,k_3) = \frac{\dot\rho_*^4}{\dot\phi_*^4}H_*^4\frac{1}{\prod_i (2k_i^3)}\mathcal A$, where

$$\mathcal A = 2\frac{\ddot\phi_*}{\dot\phi_*\dot\rho_*}\sum_i k_i^3 + \frac{\dot\phi_*^2}{\dot\rho_*^2}\Big[\frac12\sum_i k_i^3 + \frac12\sum_{i\ne j}k_ik_j^2 + 4\frac{\sum_{i>j}k_i^2k_j^2}{k_t}\Big].$$

4. Graviton correlators (eqs. 4.10, 4.13, 4.15). These are built from the integral $I = -k_t + \frac{\sum_{i>j}k_ik_j}{k_t} + \frac{k_1k_2k_3}{k_t^2}$ of eq. (4.11), the transverse traceless polarization tensors $\epsilon^s_{ij}$, and the flat-space tensor $t_{ijl} = k_2^i\delta_{jl} + k_3^j\delta_{il} + k_1^l\delta_{ij}$.

Formalization targets

Goal: the squeezed-limit consistency relation (eqs. 4.5–4.7)

For fixed $k = k_1 > 0$, as $k_3 \to 0$ through momentum triangles (which forces $k_2 \to k_1$),

$$\frac{B_\zeta(k_1,k_2,k_3)}{P_\zeta(k_1)\,P_\zeta(k_3)} \longrightarrow -n_s .$$

This is the statement that "(4.5), with (4.6) goes over to (4.7) in the overlapping region of validity."

Milestones

1. The exact tilt formulas (2.22) and (2.30) for a background obeying the equations of motion.
2. The time integral (4.4) for the contribution of the cubic vertex in de Sitter space, and the time integral $I$ of (4.11), each with the $i\epsilon$ contour prescription.
3. The squeezed limit of the amplitude $\mathcal A$ (4.6 → 4.7).
4. The $k$-dependent $f_{NL}$ of (4.9): its expression through $n_s$, $n_t$ and a shape function $f(k)$; the range $0 \le f \le 5/6$; the values $f = 5/6$ (equilateral) and $f \to 0$ (squeezed).
5. The squeezed limits of the three graviton correlators: (4.10 → 4.12), (4.13 → 4.14), and (4.15 → 4.17).

Significance

The consistency relation ties a three-point observable to a two-point observable with no free parameters. If it is observed to fail, all single-field models in the Bunch–Davies vacuum are ruled out. The shape-function bound in (4.9) is what lets the paper conclude that the local-type $f_{NL}$ of single-field slow-roll models is of order the slow-roll parameters, too small to detect from the CMB alone.

All results here are established physics. As far as is known, none of the explicit formula manipulations, the contour integrals, or the consistency checks between the general and squeezed formulas has a machine-checked proof. This mission produces checked versions of each of them, so that later formal developments of cosmological perturbation theory can cite exact statements rather than prose.

Difficulty

The algebraic limits are elementary once the formulas are written down. The analytic content is in the two contour integrals. The integrand of (4.4) and (4.11) oscillates and does not decay on $(-\infty, 0]$, so the integrals exist only with the $i\epsilon$ prescription. The integrand of (4.11) also has a non-integrable $1/\eta^2$ singularity at $\eta = 0$, whose divergence is purely imaginary, so only the real part has a limit as the cutoff goes to zero. The shape bound $0 \le f \le 5/6$ is a degree-zero rational inequality on the triangle region; it is false outside the triangle region.

Formalization scope

• Every correlator is a real-valued Lean def with $M_{pl} = 1$, $H_* = \dot\rho_*$, and the factor $(2\pi)^3\delta^3(\sum_i\vec k_i)$ dropped. Background values at horizon crossing enter as real parameters ρd, φd, φdd $= \dot\rho_*, \dot\phi_*, \ddot\phi_*$. At leading order in slow roll, the different horizon-crossing times $*$ and $*'$ that appear in (4.7), (4.12), (4.14), and (4.17) coincide.
• The scalar correlators depend only on the magnitudes $k_i$, and momentum conservation is encoded by the triangle predicate IsMomentumTriangle. The graviton–scalar–scalar and three-graviton correlators use vectors in EuclideanSpace ℝ (Fin 3) and polarizations as real symmetric, traceless, transverse $3\times3$ matrices. A squeezed limit is taken along $\vec k_1 = t\hat n$, $t \to 0^+$.
• The $i\epsilon$ prescription ($\eta \to \eta + i\epsilon|\eta|$) is implemented by the damping factor $e^{\epsilon\eta}$, followed by $\epsilon \to 0^+$.
• The derivation of (4.5), (4.10), (4.13), and (4.15) from the cubic action of Section 3 (the in-in formalism, field redefinitions, gauge choices) is out of scope, because current Mathlib has no framework for interacting quantum fields on curved backgrounds. Contributions toward that infrastructure are welcome as separate missions.
• Eq. (2.22) as printed has the misprint $\dot\phi_*/\dot\rho_*$ in place of $\dot\phi_*^2/\dot\rho_*^2$. The corrected form, which equals $2(\eta - 3\epsilon)$ and is used in (4.7) and (4.9), is the one formalized.

Selected references

• J. Maldacena, Non-Gaussian features of primordial fluctuations in single field inflationary models, JHEP 05 (2003) 013. https://doi.org/10.1088/1126-6708/2003/05/013 (arXiv: https://arxiv.org/abs/astro-ph/0210603)

Motivation

Elko (from the German Eigenspinoren des Ladungskonjugationsoperators) is a class of spin-1/2 fields of mass dimension one, introduced by Ahluwalia and Grumiller (JCAP 07 (2005) 012) as a candidate for fermionic dark matter. Elko spinors are eigenstates of charge conjugation, so they are neutral. Because of their mass dimension they obey only a Klein–Gordon-type equation, and their allowed self-interactions are restricted to a quadratic and a quartic term.

Pereira and Guimarães (2017) propose that one homogeneous Elko field, coupled to gravity in the Einstein–Cartan framework (gravity with torsion) and subject to a symmetry-breaking potential, drives the whole expansion history: inflation, then a matter-dominated era, then late-time acceleration. The paper has two parts. The first is an analytic reduction of the field equations to a closed system of ordinary differential equations (Section 2 and Appendix A). The second is a numerical study of that system with a benchmark set of parameters (Section 3). This mission formalizes the analytic part and the closed-form estimates of Section 3.1.

Setting

Units are $c=1$ and $\kappa^2=8\pi G=8\pi/m_{\rm pl}^2$. The background is a spatially flat FRW metric with lapse $N(t)$ and scale factor $a(t)>0$. The Hubble rate is $H=\dot a/a$. The Elko field is $\lambda=\Phi(t)\,\xi$, where $\xi$ is a constant spinor normalized so that $\bar\xi\xi=1$. Only the real function $\Phi(t)$ carries dynamics. Homogeneity and isotropy leave two torsion functions $h(t)$ and $f(t)$. The minisuperspace Lagrangian (A.13) is

$$\mathcal L=-\frac1N\Big(\frac{3a\dot a^2}{\kappa^2}-\frac{3a^3h^2}{\kappa^2}-\frac12a^3\dot\Phi^2-\frac38a(\dot a+ah)^2\Phi^2\Big)-N\Big(\frac{3a^3f^2}{\kappa^2}+\frac38a^3f^2\Phi^2+a^3V(\Phi)\Big).$$

Its Euler–Lagrange equations in $N,a,\Phi,h,f$ (gauge $N=1$) are (A.14)–(A.17). They force $f=0$ and the torsion relation

$$h=-\frac18\,\frac{\kappa^2\Phi^2}{1+\kappa^2\Phi^2/8}\,H.\qquad(2.5)$$

Substituting $f=0$ gives the Friedmann equations with torsion (2.2)–(2.3) and the motion equation (2.4). Throughout, the factor $1+\kappa^2\Phi^2/8$ appears, and it is always positive. The potential of Section 3 is

$$V(\Phi)=v_0+\Lambda^4\Big(1-\frac{\Phi^2}{\sigma^2}\Big)^2 .\qquad(3.1)$$

Formalization targets

Goal: the reduced Elko system (2.6)–(2.10)

Assume (2.5), (2.2) and (2.3) on an open time set $I$, with $H,\Phi,\dot\Phi$ differentiable there. Then on $I$

$$H^2=\frac{\kappa^2}{3}\Big(1+\frac{\kappa^2\Phi^2}{8}\Big)\Big[\frac{\dot\Phi^2}{2}+V\Big],\qquad \dot H=-\frac{\kappa^2}{2}\Big(1+\frac{\kappa^2\Phi^2}{8}\Big)\Big[\dot\Phi^2-\frac{H\Phi\dot\Phi}{2(1+\kappa^2\Phi^2/8)^2}\Big],$$

$H^2=\kappa^2\rho/3$ and $\dot H=-\kappa^2(\rho+p)/2$ with $\rho,p$ given by (2.9)–(2.10). Wherever $\dot\Phi\neq0$, the motion equation (2.8) also holds:

$$\ddot\Phi+3H\dot\Phi+V'(\Phi)-\frac34\,\frac{H^2\Phi}{(1+\kappa^2\Phi^2/8)^2}=0 .$$

Milestones

1. Eqs. (A.14)–(A.17): the Euler–Lagrange equations of (A.13).
2. Appendix A: (A.14)–(A.16) with $f=0$ give (2.2)–(2.4).
3. Eq. (2.4) follows from differentiating (2.2) and using (2.3).
4. Eqs. (2.6), (2.7), (2.8): the torsion is eliminated from each equation.
5. Eqs. (2.9)–(2.10): (2.6)–(2.7) are the FRW equations for $\rho$ and $p$.
6. Eq. (3.1): polynomial form of the potential, global minimum $V(\sigma)=v_0$, and mass $V''(\sigma)=m^2$ with $m=\sqrt2\mu$.
7. Eq. (3.6) and Sec. 3.1: the benchmark values of $H^2(t_i)$, $t_i$, $V(\Phi_i)$, $\epsilon$, $\eta$, $m$ and $\alpha$.

Significance

The result itself. The reduced system (2.6)–(2.10) is the object the paper integrates numerically for every cosmological era. In the limit $H\ll m_{\rm pl}$ it differs from the standard single-scalar-field equations (1.1)–(1.3) only by the factor $1+\kappa^2\Phi^2/8$ and by the torsion term in (2.8). That term acts like the friction term $\Gamma\dot\phi$ that is added by hand in reheating models. The identification of $\rho$ and $p$ in (2.9)–(2.10) is what defines the equation-of-state parameter $\omega=p/\rho$, which the paper uses to argue for dust-like behaviour after inflation.

Formalizing it. The paper says the reduction is reached "after some algebraic manipulations" and does not show them. A formal proof checks every coefficient of (2.2)–(2.10) and of (A.14)–(A.17) against the Lagrangian (A.13). It also makes explicit the condition $\dot\Phi\neq0$ that is needed to recover the motion equation from the Friedmann equations. The numerical claims of Section 3.1 are closed-form evaluations and can be checked exactly.

Difficulty

The identities are elementary, but they are not purely pointwise. Equation (2.3) contains $\dot H$ on both sides, through $\frac{d}{dt}[(H+h)\Phi^2]$, and $h$ itself depends on $H$ and $\Phi$. Solving for $\dot H$ therefore requires differentiating (2.5) along the trajectory. This is valid only because (2.5) holds on an open set of times, not just at one instant. Similarly, deriving (2.4) means differentiating the constraint (2.2) in time and cancelling a factor $\dot\Phi$. The Euler–Lagrange milestone needs partial derivatives of $\mathcal L$ in each of its slots, composed with time derivatives along the trajectory. A careless treatment of which arguments are frozen gives wrong coefficients.

Formalization scope

All objects are real-valued functions of time $t\in\mathbb R$. Time derivatives are Mathlib deriv, and hypotheses are imposed on an open set $I$. Partial derivatives of the Lagrangian are deriv in one argument with the others fixed at their trajectory values. The constant $\kappa$ is an arbitrary real number; $\kappa\neq0$ is assumed only where $1/\kappa^2$ appears. The spinor structure of Elko is not modelled: as in the paper, only the scalar amplitude $\Phi(t)$ enters. The symbol "$\simeq$" in Section 3.1 is encoded as agreement within $5\%$ relative error.

Out of scope: the derivation of the Lagrangian (A.13) from the Einstein–Cartan action (A.1)–(A.12); the slow-roll approximations (3.2)–(3.5), which the paper states only as approximations in the regime $H\ll m_{\rm pl}$; and every output of the numerical integration of Section 3 and Appendix B, such as $N\approx93$ e-folds, the $t^{2/3}$ late-time behaviour, the oscillation of $\omega$ around $0$, and the present-day density.

A trivializing formalization is ruled out: the torsion function $h$ is constrained by (2.5) on all of $I$, and $\rho,p$ are fixed by (2.9)–(2.10), not left free.

Infrastructure needed: only basic one-variable calculus in Mathlib (deriv, DifferentiableAt, product and quotient rules), together with field arithmetic using the positivity of $1+\kappa^2\Phi^2/8$. The same reduction pattern (eliminate an algebraically determined auxiliary field, then differentiate a constraint) occurs in other torsion and scalar–tensor cosmologies.

Selected references

• S. H. Pereira, T. M. Guimarães, From inflation to recent cosmic acceleration: the fermionic Elko field driving the evolution of the universe, JCAP 09 (2017) 038. https://doi.org/10.1088/1475-7516/2017/09/038 (arXiv:1702.07385)
• D. V. Ahluwalia, D. Grumiller, Spin-half fermions with mass dimension one: theory, phenomenology, and dark matter, JCAP 07 (2005) 012. https://doi.org/10.1088/1475-7516/2005/07/012 (arXiv:hep-th/0412080)
• A. D. Linde, Chaotic inflation, Phys. Lett. B 129 (1983) 177. https://doi.org/10.1016/0370-2693(83)90837-7

Motivation

The Hubble constant $H_0$ is the present expansion rate of the universe. It is the slope of Hubble's law $v = H_0\, d$, which relates a galaxy's recession velocity $v$ (km s$^{-1}$) to its distance $d$ (Mpc). Two families of measurements currently disagree. Local, distance-ladder measurements calibrated with Cepheid variables give $H_0 \approx 73$ km s$^{-1}$ Mpc$^{-1}$ (SH0ES: $73.04 \pm 1.04$, Riess et al. 2022). The value inferred from the cosmic microwave background under $\Lambda$CDM is $67.4 \pm 0.5$ (Planck 2018). Calibrations with the tip of the red giant branch (TRGB) fall in between: $69.8 \pm 0.6\,(\text{stat}) \pm 1.6\,(\text{sys})$ (Freedman 2021). This disagreement is the Hubble tension. If it is real, it points to physics beyond $\Lambda$CDM.

The review Freedman & Madore 2023 surveys this landscape and makes a series of quantitative claims about it. Some are agreement or disagreement claims ("agrees at better than $0.2\sigma$", "differs at the $2\sigma$ level"). Others convert magnitudes to distances ("a 1.5% measurement", "corresponds to a 6% shift in $H_0$"). The central one, in §10, is a sensitivity argument: the claimed $5\sigma$ tension falls below $3\sigma$ if the local uncertainty has been underestimated by a factor of about $1.5$. This mission takes these claims literally and checks them against their stated numbers.

Setting

A measurement is reported as $x \pm \sigma$. Two independent uncertainties are combined in quadrature, $\operatorname{quadSum}(s,t) = \sqrt{s^2+t^2}$. This is the field's standard convention, used here for a quoted $x \pm s\,(\text{stat}) \pm t\,(\text{sys})$. The tension between independent measurements $a \pm \sigma_a$ and $b \pm \sigma_b$, in units of standard deviations, is

$$\operatorname{tension}(a,\sigma_a,b,\sigma_b) = \frac{|a-b|}{\sqrt{\sigma_a^2+\sigma_b^2}}.$$

The distance modulus of an object at distance $d$ parsecs is $\mu = 5\log_{10}(d/10)$, and conversely $d = 10^{\mu/5+1}$ pc ($\operatorname{distanceFromModulus}$). A modulus difference $\Delta\mu$ therefore multiplies distances by $10^{\Delta\mu/5}$. Through Hubble's law, $\operatorname{hubbleConstant}(v,d) = v/(d/10^6)$ (with $d$ in pc), the same difference divides the inferred $H_0$ by $10^{\Delta\mu/5}$.

Formalization targets

Goal (§10, p. 25)

$$4.5 \le \operatorname{tension}(73.04, 1.04, 67.4, 0.5) < 5.5,\qquad \operatorname{tension}(72.0, 1.5, 67.4, 0.5) < 3,\qquad 1.5 \le \operatorname{tension}(72.0, 2.0, 67.4, 0.5) < 2.5.$$

These are the "$5\sigma$" SH0ES–Planck tension, the "less than $3\sigma$" for $H_0 = 72.0 \pm 1.5$, and the "$2\sigma$" for $H_0 = 72.0 \pm 2.0$. Every rounded value ("$5\sigma$", "$2\sigma$") is read as the half-open interval of reals that round to it.

Milestones

• Distance modulus and distance are inverse to each other on $d > 0$.
• Hubble's law under a modulus shift: $H_0$ rescales by $10^{-\Delta/5}$. As consequences, the JWST "$+0.45$ mag farther" correction lowers $H_0$ (Summary, p. 26), and the R16→R22 offset of $-0.123$ mag is a $6\%$ shift (Summary, p. 27).
• NGC 4258 (§5.3): modulus $29.397$ is $7.6$ Mpc, and $\pm 0.033$ mag is a $1.5\%$ measurement. The TRGB modulus agrees with the maser modulus at $<0.2\sigma$ and $<1\%$. The Milky-Way-anchored Cepheid modulus differs by $7\%$ at the $2\sigma$ level.
• LMC (§5.1): $18.477 \pm 0.004 \pm 0.026$ is a $1.2\%$ distance uncertainty, $\sim 1\%$ from the Key Project value $18.5$.
• TRGB vs Cepheid (§4.1): $69.8 \pm 0.6 \pm 1.6$ agrees with $73.04 \pm 1.04$ at better than $2\sigma$.

Significance

The statements make the review's arithmetic exact and auditable. Each verbal claim of the form "$k\sigma$" or "$p\%$" becomes an explicit inequality under an explicit convention (quadrature, half-open rounding intervals). A reader can then see which claims follow from the quoted numbers and which do not. For example, under the quadrature convention the §4.1 statement that the TRGB value "differs only at the $1.2\sigma$ level" from Planck evaluates to about $1.35\sigma$. That claim is therefore not included as a milestone. The definitions (quadrature, tension, distance modulus, Hubble's law) are reusable for any distance-ladder mission. None of these statements has a machine-checked proof yet.

Difficulty

The mathematics is elementary. The difficulty is certified real-number bounds involving square roots and real powers $10^{x}$ with non-integer $x$, where a careless rounding direction flips a conclusion. Bounds on $10^{p/q}$ reduce to comparing $c^q$ with $10^p$ for large $q$. This requires care with exponent sizes, or an analytic bound on $\exp$ / $\log$.

Formalization scope

All quantities are real numbers (ℝ). Distances are in parsecs inside distanceFromModulus, and hubbleConstant converts to Mpc. Velocities are in km s$^{-1}$. Uncertainties are taken at face value as independent Gaussian standard deviations. Statistical and systematic errors are combined in quadrature, and no asymmetric errors are used. A rounded figure is encoded as the half-open interval of values rounding to it. "Better than $x$" is a strict inequality. "At the $2\sigma$ level" is $2 \le t < 3$. Real.logb 10 and Real.sqrt are total functions; every statement uses them only on positive arguments. Solutions should go through the given definitions rather than replacing them with decimal approximations.

Selected references

• W. L. Freedman and B. F. Madore, Progress in Direct Measurements of the Hubble Constant, JCAP (2023). https://arxiv.org/abs/2309.05618
• A. G. Riess et al., A Comprehensive Measurement of the Local Value of the Hubble Constant with 1 km/s/Mpc Uncertainty from HST and the SH0ES Team, ApJL 934 (2022) L7. https://arxiv.org/abs/2112.04510
• Planck Collaboration, Planck 2018 results. VI. Cosmological parameters, A&A 641 (2020) A6. https://arxiv.org/abs/1807.06209
• W. L. Freedman, Measurements of the Hubble Constant: Tensions in Perspective, ApJ 919 (2021) 16. https://arxiv.org/abs/2106.15656
• M. J. Reid, D. W. Pesce and A. G. Riess, An Improved Distance to NGC 4258 and Its Implications for the Hubble Constant, ApJL 886 (2019) L27. https://arxiv.org/abs/1908.05625

Motivation

Mass dimension one (MDO) fermionic fields — spin-1/2 fields built from eigenspinors of charge conjugation (historically called Elko) — have canonical mass dimension one instead of 3/2 and admit only very few couplings to Standard Model particles. This makes them natural dark-matter candidates. In an Einstein–Cartan framework with torsion, the homogeneous part of such a field obeys equations that closely resemble scalar-field cosmology but carry an extra spin–gravity coupling factor $1+\kappa^2\phi^2/8$.

S. H. Pereira, M. E. S. Alves and T. M. Guimarães (Eur. Phys. J. C 79 (2019) 543) propose that a single MDO field drives the whole cosmic history: inflation, reheating, dark matter and dark energy. The analytic backbone of that claim is Section 3 of the paper: once the field has rolled to the bottom $\phi_c$ of a symmetry-breaking potential, its gravitational coupling to baryons behaves exactly like cold dark matter and its residual potential energy behaves exactly like a cosmological constant.

Setting

Work in units $c=\hbar=1$ with $\kappa^2=8\pi G$, on a flat FLRW background with scale factor $a(t)>0$ and Hubble function $H=\dot a/a$. The MDO field is $\Lambda=\phi(t)\lambda$ with $\lambda$ a normalised Minkowski spinor; only the real function $\phi(t)$ enters. Other matter has energy density $\rho_m$ and pressure $p_m$. Writing $F(\phi)=1+\kappa^2\phi^2/8$, the model is governed by

$$H^2=\frac{\kappa^2}{3}F(\phi)\Big[\frac{\dot\phi^2}{2}+V(\phi)+\rho_m\Big],\quad \dot H=-\frac{\kappa^2}{2}F(\phi)\Big[\dot\phi^2-\frac{H\phi\dot\phi}{2F(\phi)^2}+\rho_m+p_m\Big],$$ $$\ddot\phi+3H\dot\phi+V'(\phi)-\frac34\frac{H^2\phi}{F(\phi)^2}=0,\qquad \dot\rho_m+3H(\rho_m+p_m)=0,$$

(Eqs. (5)–(7), (9)), with MDO energy density $\rho_\phi$ and pressure $p_\phi$ given by Eqs. (10)–(11). The potential is $V=V_1+V_2$ with $V_1(\phi)=A^4(1-\phi^2/\phi_c^2)^2$ and $V_2(\phi)=\frac12m^2\phi^2+\frac\alpha4\phi^4$, $A,\phi_c>0$.

Formalization targets

Goal: late-time $\Lambda$CDM form (Eq. (25))

If on a late-time interval $t>T$ the field is frozen at $\phi\equiv\phi_c$, the only other matter is pressureless baryonic matter $\rho_b$, and the Friedmann equation (5) holds, then with $a(t_0)=1$, $H_0=H(t_0)\ne0$,

$$\frac{H(t)^2}{H_0^2}=\frac{\Omega_b}{a^3}+\frac{\Omega_{DM,\phi}}{a^3}+\Omega_{\Lambda,\phi},\qquad \Omega_{DM,\phi}=\frac{\kappa^2\phi_c^2}{8}\Omega_b,\quad \Omega_{\Lambda,\phi}=\frac{\Lambda_{\mathrm{eff}}}{\kappa^2\rho_{\mathrm{crit},0}},$$

where $\rho_{\mathrm{crit},0}=3H_0^2/\kappa^2$, $\Omega_b=\rho_b(t_0)/\rho_{\mathrm{crit},0}$ and $\Lambda_{\mathrm{eff}}=\kappa^2F(\phi_c)V_2(\phi_c)$ (Eq. (24)).

Milestones

1. Eqs. (12)–(13): $\rho_\phi$ and $p_\phi$ rewritten through $\rho_m$, $p_m$.
2. Eqs. (15)–(16): equivalence of the Friedmann equations with their two-fluid forms.
3. Eq. (14): the MDO conservation equation is equivalent to the field equation (7) when $\dot\phi\ne0$.
4. Eqs. (20)–(21): expanded form of the potential and location of its minimum.
5. Eq. (9) with $p_m=0$: $\rho_b a^3$ is constant.
6. Eqs. (22)–(23): late-time density and pressure of the frozen field.
7. Eqs. (26)–(27) and the Sect. 3 estimate: $\phi_c=m_{pl}\sqrt{\Omega_{DM,\phi}/\pi\Omega_b}\simeq1.3\,m_{pl}$ and $V_2(\phi_c)$ in terms of $\Omega_{\Lambda,\phi}$.
8. Eq. (31): $q=-1-\dot H/H^2$.

Significance

The goal is the statement that makes the MDO field a unified dark sector at late times: the background expansion is indistinguishable from $\Lambda$CDM, the dark-matter density is fixed by $\phi_c$ and the baryon density rather than by an incomplete decay of the inflaton, and the dark-energy density is fixed by $V_2(\phi_c)$. Equations (12)–(16) are the reusable structural fact that the torsionful MDO system is equivalent in form to a torsion-free two-fluid model. The milestones collect the algebraic and differential identities the paper uses without proof.

Formalizing these makes the derivations machine-checked and isolates exactly which hypotheses (frozen field, pressureless baryons, Friedmann equation) the $\Lambda$CDM form depends on. The paper's numerical results for inflation (about 71 e-folds, Figs. 1–3) and the reheating discussion (Sect. 5) are numerical or qualitative and are outside the scope of this mission.

Difficulty

The algebra is elementary but error-prone: $\rho_\phi$ and $p_\phi$ themselves contain $H^2$ and $\dot H$, so the equivalences (15)–(16) are fixed-point identities rather than substitutions. Eq. (14) requires differentiating $\rho_\phi$, which involves $\dot\phi$, $V\circ\phi$ and $H$, so differentiability bookkeeping is the main formal cost. The dilution law $\rho_b\propto a^{-3}$ requires a mean-value argument on an interval, not a pointwise computation.

Formalization scope

All quantities are real functions of cosmic time; time derivatives are Mathlib's deriv, and each theorem carries the differentiability hypotheses it needs. Late-time statements are posed on an open half-line $(T,\infty)$, since a matter-filled expanding universe cannot have $a>0$ for all real $t$. The frozen-field regime is encoded exactly as $\phi\equiv\phi_c$ on that half-line, and the field equation (7) is not assumed there (the paper itself only uses Eqs. (12)/(15) in this regime, and (7) with $\dot\phi\equiv0$ and $H$ varying would be overdetermined). Lean's Real.sqrt returns $0$ on negative inputs; in Eq. (21) this gives $\phi_{\min}=0$ when $m_{\mathrm{eff}}^2\ge0$, which is the correct minimiser in that regime. Definitions live in a single shared file under the namespace MDOUnifiedCosmology.

Selected references

• S. H. Pereira, M. E. S. Alves, T. M. Guimarães, An unified cosmological evolution driven by a mass dimension one fermionic field, Eur. Phys. J. C 79 (2019) 543. https://doi.org/10.1140/epjc/s10052-019-7036-5
• S. H. Pereira, T. M. Guimarães, From inflation to recent cosmic acceleration: the fermionic Elko field driving the evolution of the universe, JCAP 09 (2017) 038. https://doi.org/10.1088/1475-7516/2017/09/038
• Planck Collaboration, Planck 2018 results. VI. Cosmological parameters, Astron. Astrophys. 641 (2020) A6. https://arxiv.org/abs/1807.06209