Mathematical Physics

Motivation

Neutrinos are produced and detected in charged-current weak interactions as flavour eigenstates $\nu_e,\nu_\mu,\nu_\tau$, but they propagate as superpositions of mass eigenstates $\nu_1,\nu_2,\nu_3$. When the masses differ, the mass components acquire different quantum-mechanical phases and the flavour content of the beam changes periodically along its path: neutrino flavour oscillations, first proposed by Pontecorvo. Oscillations of atmospheric and solar neutrinos are the experimental evidence that neutrinos are massive and that leptons mix, and the vacuum oscillation formula is what experiments fit to extract mass-squared differences, mixing angles and the CP-violating phase.

The formulas are elementary quantum mechanics, but the standard three-flavour form requires careful bookkeeping of phases, of unitarity relations, and of the sign conventions for the CP-odd term. The source for this mission, Section 4 of P. Lipari's lecture notes Introduction to Neutrino Physics, derives the whole chain in a few pages (Eqs. (44)–(73)). The mission turns that chain into machine-checkable statements.

Setting

Fix $n$ flavours and $n$ mass eigenstates. The mixing matrix $U$ is a complex $n\times n$ matrix, rows indexed by flavour $\alpha$ and columns by mass eigenstate $j$, with $|\nu_\alpha\rangle=\sum_j U^*_{\alpha j}|\nu_j\rangle$; physically $U$ is unitary. Let $m_j^2$ be the squared masses, $L$ the distance travelled and $E$ the neutrino energy. In the relativistic approximation ($L\simeq t$, $E_j\simeq E+m_j^2/2E$) the transition amplitude and transition probability are

$$A(\nu_\alpha\to\nu_\beta)=\sum_j U_{\beta j}U^*_{\alpha j}\,e^{-i m_j^2 L/(2E)},\qquad P(\nu_\alpha\to\nu_\beta)=|A(\nu_\alpha\to\nu_\beta)|^2 .$$

The antineutrino probability $P(\bar\nu_\alpha\to\bar\nu_\beta)$ is the same expression with $U$ replaced by its entrywise complex conjugate $U^*$. Write $\Delta m^2_{jk}=m_k^2-m_j^2$ and define the CP-even amplitudes and the CP/T-odd coefficients

$$A^{jk}_{\alpha\beta}=-4\,\mathrm{Re}\bigl[U_{\alpha j}U^*_{\beta j}U^*_{\alpha k}U_{\beta k}\bigr],\qquad J^{\alpha\beta}_{jk}=-\mathrm{Im}\bigl[U_{\alpha j}U^*_{\alpha k}U^*_{\beta j}U_{\beta k}\bigr].$$

For two flavours the mixing matrix is the rotation $\begin{pmatrix}\cos\theta&\sin\theta\\-\sin\theta&\cos\theta\end{pmatrix}$; for three flavours the standard parametrization is $U=R_{23}\,U_{13}(\delta)\,R_{12}$ with mixing angles $\theta_{12},\theta_{13},\theta_{23}$ and CP phase $\delta$ (Eq. (57)).

Formalization targets

Goal: three-flavour transition probability (Eq. (71))

For unitary $3\times3$ $U$ and flavours $\alpha\ne\beta$,

$$P(\nu_\alpha\to\nu_\beta)=\sum_{(j,k)\in\{(1,2),(2,3),(1,3)\}}A^{jk}_{\alpha\beta}\sin^2\frac{\Delta m^2_{jk}L}{4E}\;-\;8\,J^{\alpha\beta}_{12}\,\sin\frac{\Delta m^2_{12}L}{4E}\sin\frac{\Delta m^2_{23}L}{4E}\sin\frac{\Delta m^2_{13}L}{4E}.$$

The source writes the last term as $\pm8J$; the formal goal fixes the sign by writing it in terms of $J^{\alpha\beta}_{12}$.

Milestones

1. Eq. (52): two-flavour probability $P(\nu_e\to\nu_\mu)=\sin^22\theta\,\sin^2(\Delta m^2L/4E)$.
2. Eq. (61): expansion of the three-flavour probability into a constant term, three cosine terms and three sine terms (any $3\times3$ matrix).
3. Eqs. (65)–(66): $J^{\alpha\beta}_{jk}=-J^{\alpha\beta}_{kj}=-J^{\beta\alpha}_{jk}$, $J^{\alpha\beta}_{jj}=J^{\alpha\alpha}_{jk}=0$.
4. Eq. (67): $J^{\alpha\beta}_{12}=J^{\alpha\beta}_{23}=J^{\alpha\beta}_{31}$ for unitary $3\times3$ $U$.
5. Eq. (68): $J^{e\mu}_{jk}=J^{\mu\tau}_{jk}=J^{\tau e}_{jk}$ for unitary $3\times3$ $U$.
6. Eqs. (69)–(70): the Jarlskog parameter of the standard parametrization.
7. Eq. (72): $\sin a+\sin b-\sin(a+b)=4\sin\frac a2\sin\frac b2\sin\frac{a+b}2$.
8. Eq. (60): CPT invariance $P(\nu_\alpha\to\nu_\beta)=P(\bar\nu_\beta\to\bar\nu_\alpha)$.
9. p. 135: no CP violation in survival probabilities, $P(\bar\nu_\alpha\to\bar\nu_\alpha)=P(\nu_\alpha\to\nu_\alpha)$.

Significance

The goal is the formula used to interpret long-baseline accelerator and reactor oscillation data: the three amplitudes $A^{jk}_{\alpha\beta}$ govern the CP-conserving oscillation pattern, and the single product term isolates all CP- and T-violating effects in vacuum. Together with milestones 3–6 it shows that one real number, the Jarlskog parameter, controls CP violation, and that such violation requires a nontrivial phase, three nonzero mixing angles and three active oscillation frequencies.

These results are textbook material and their proofs are known; what this mission adds is a machine-checked derivation with every convention explicit. Two points in the printed source are resolved by the formal statements: the constant term of Eq. (61) is printed with exponent $4$ where squaring the amplitude gives exponent $2$, and with the source's own Eqs. (57) and (69), the value of $J^{e\mu}_{12}$ has the opposite overall sign from the one printed in Eq. (70). Milestone 6 is stated with the sign that follows from (57) and (69).

Difficulty

No step is conceptually deep. The work is in the algebra: expanding a squared modulus of a sum of three complex exponentials, and then using unitarity to remove the constant term and to identify the sine coefficients with one another. The unitarity relations among the products $U_{\alpha j}U^*_{\beta j}$ (footnote 8 of the source) have to be combined in the right order, and it is easy to lose a sign or a conjugate. Eq. (70) needs an explicit expansion of a product of three $3\times3$ complex matrices.

Formalization scope

• The mixing matrix is Matrix (Fin n) (Fin n) ℂ; flavours $e,\mu,\tau$ and mass labels $1,2,3$ are the indices 0, 1, 2. Unitarity is membership in Matrix.unitaryGroup (Fin 3) ℂ, assumed only where the source uses it (Eqs. (67), (68), (71)).
• Squared masses are an arbitrary function m2 : Fin n → ℝ; $L$ and $E$ are arbitrary reals. No positivity of $E$ is imposed: all statements remain true at $E=0$, where Lean's convention $x/0=0$ makes every phase vanish.
• Probabilities are Complex.normSq of the amplitude. Antineutrino probabilities use the entrywise conjugate U.map star, not the conjugate transpose.
• The approximate formulas of §4.4 (one-mass-scale dominance, averaged oscillations) and the unit conversions of Eqs. (53)–(54) are out of scope.
• Definitions live in two files: the oscillation objects (amplitude, probability, antineutrino probability, $A^{jk}_{\alpha\beta}$, $J^{\alpha\beta}_{jk}$) and the mixing matrices (two-flavour rotation, standard PMNS parametrization). They are reusable for later missions on matter effects (Section 6 of the source).

Selected references

• P. Lipari, Introduction to Neutrino Physics, lecture notes; Section 4 "Neutrino oscillations in vacuum", pp. 130–137 of the proceedings pagination (source of every statement in this mission).
• B. Pontecorvo, original proposal of neutrino oscillations (reference [1] of the source).

Motivation

When a charged particle scatters, it can radiate photons of arbitrarily low energy. In perturbative quantum electrodynamics this shows up as infrared divergences: loop integrals over very soft virtual photons diverge logarithmically, and so do the rates for emitting soft real photons. The standard resolution, due to Bloch and Nordsieck and systematized by Yennie, Frautschi and Suura, is that the divergences cancel in any rate that sums over undetectable soft emissions below an energy resolution $E$.

S. Weinberg's paper Infrared Photons and Gravitons (Phys. Rev. 140, B516 (1965)) shows that the same mechanism works for gravitons, derives explicit formulas for the exponents that control the soft factors, and proves that the extra "collinear" divergences produced by massless hard particles cancel for gravitons but not for photons. The soft-graviton factor (2.5)–(2.7) used there is the factor that appears in Weinberg's soft graviton theorem, and the spectrum formula is used in the paper to estimate the gravitational radiation from thermal collisions in the sun.

Timeline.

• 1937 — Bloch and Nordsieck: soft-photon divergences cancel between virtual and real emission.
• 1961 — Yennie, Frautschi and Suura: all-orders exponentiation of soft-photon factors in QED.
• 1965 — Weinberg: the analogous treatment for gravitons, closed forms (2.16) and (2.26) for the exponents $A$ and $B$, cancellation of collinear divergences for gravitons (Sec. III), and the Coulomb-phase result conjectured by Dalitz (Sec. V).

Setting

Work in units $\hbar=c=1$ with the paper's metric: for four-vectors $p=(\mathbf p,p^0)$ and $q=(\mathbf q,q^0)$, $p\cdot q=\mathbf p\cdot\mathbf q-p^0q^0$. A process $\alpha\to\beta$ has finitely many external lines $n$; line $n$ has mass $m_n$, three-momentum $\mathbf p_n\in\mathbb R^3$, on-shell energy $E_n=\sqrt{|\mathbf p_n|^2+m_n^2}$, charge $e_n$, and sign $\eta_n=+1$ (outgoing) or $-1$ (incoming). The relative velocity of lines $n,m$ is

$$\beta_{nm}=\Bigl[1-\frac{m_n^2m_m^2}{(p_n\cdot p_m)^2}\Bigr]^{1/2}.$$

For a unit vector $\hat q$ (the direction of a soft quantum) define the photon and graviton angular functions

$$A(\hat q)=\frac{1}{2(2\pi)^3}\sum_{n,m}\frac{e_ne_m\eta_n\eta_m(p_n\cdot p_m)}{[E_n-\mathbf p_n\cdot\hat q][E_m-\mathbf p_m\cdot\hat q]},\qquad B(\hat q)=\frac{8\pi G}{2(2\pi)^3}\sum_{n,m}\frac{\eta_n\eta_m\{(p_n\cdot p_m)^2-\frac12m_n^2m_m^2\}}{[E_n-\mathbf p_n\cdot\hat q][E_m-\mathbf p_m\cdot\hat q]},$$

and the infrared exponents $A=\int d^2\Omega\,A(\hat q)$ and $B=\int d^2\Omega\,B(\hat q)$, integrals over the unit sphere against surface measure. With infrared cutoff $\lambda$ and dividing point $\Lambda$, virtual soft quanta multiply a rate by $(\lambda/\Lambda)^A$ or $(\lambda/\Lambda)^B$, and summing over real soft emission of total energy at most $E$ gives the cutoff-free factors $(E/\Lambda)^Ab(A)$ and $(E/\Lambda)^Bb(B)$ of Eqs. (2.51)–(2.52).

Formalization targets

Goal — Eq. (2.26)

For masses $m_n>0$,

$$B=\frac{G}{2\pi}\sum_{n,m}\eta_n\eta_mm_nm_m\frac{1+\beta_{nm}^2}{\beta_{nm}(1-\beta_{nm}^2)^{1/2}}\ln\Bigl(\frac{1+\beta_{nm}}{1-\beta_{nm}}\Bigr)=\frac{G}{\pi}\sum_{n,m}\eta_nm_n\eta_mm_mf(\beta_{nm}),$$

with $f(0)=1$ for the diagonal terms. This is the formula for graviton bremsstrahlung in an arbitrary collision.

Milestones

1. Sec. II.2 — summed over the $N!$ orderings, the multiple pole factors of $N$ soft emissions from one line factorize into single-emission factors.
2. Eq. (2.13) — the real part of the virtual-photon exponent equals $-A\ln(\Lambda/\lambda)$.
3. Eq. (2.16) — $A=-\frac{1}{8\pi^2}\sum_{n,m}\eta_n\eta_me_ne_m\beta_{nm}^{-1}\ln\frac{1+\beta_{nm}}{1-\beta_{nm}}$.
4. Eq. (2.14) — $A\ge0$ under charge conservation.
5. Eq. (2.24) — $B\ge0$ under energy–momentum conservation.
6. Eqs. (3.4)–(3.5) — if one line becomes massless, $B$ stays finite (the $\ln m_1$ terms cancel by energy–momentum conservation).
7. Eq. (3.3) — for photons the corresponding limit is $A\to+\infty$ when the massless line is charged.
8. Eq. (4.9) — $f(\beta)=1+\frac{11}{6}\beta^2+\frac{63}{40}\beta^4+O(\beta^6)$.

Significance

The exponents $A$ and $B$ are the only process-dependent quantities in the soft factors: once they are known in closed form, the infrared behaviour of any rate, the shape $E^A$ or $E^B$ of the soft spectrum, and the soft power spectrum $E\,d\Gamma=B\,\Gamma^0\,dE$ (2.53) follow. The Sec. III cancellation is the statement that gravitation, unlike massless electrodynamics or Yang–Mills theory, is free of unremovable collinear divergences at this level; the paper uses the contrast to argue that charged massless particles are problematic. The expansion (4.9) feeds the nonrelativistic quadrupole formula (4.13) behind the solar estimate.

The paper's arguments are informal physics derivations. This mission makes the mathematical content of those derivations precise and machine-checkable: the angular integrals, the sign statements, the limiting behaviour as a mass goes to zero, and the combinatorial factorization.

Difficulty

The closed forms need the solid-angle integral of a product of two denominators $[E_n-\mathbf p_n\cdot\hat q]^{-1}[E_m-\mathbf p_m\cdot\hat q]^{-1}$ for two arbitrary, non-collinear momenta; the one-denominator case is a textbook integral in polar coordinates, but the two-denominator case does not reduce to it by an obvious choice of axis. The positivity statements are false without the conservation laws, so any proof must use them in an essential way. The massless-limit statements concern the interplay of a logarithmically divergent term with a coefficient that vanishes only at the limiting configuration, so a termwise limit fails.

Formalization scope

Three-momenta live in EuclideanSpace ℝ (Fin 3); energies are the on-shell values $\sqrt{|\mathbf p|^2+m^2}$ and are not free variables. Solid-angle integrals are Bochner integrals on the unit sphere against Mathlib's volume.toSphere (total mass $4\pi$). External lines are indexed by an arbitrary Fintype; the signs $\eta_n$ are real numbers constrained to $\pm1$ by hypothesis. Sums over $n,m$ run over all ordered pairs, including $n=m$, where $\beta_{nn}=0$; the kernels $\beta^{-1}\ln\frac{1+\beta}{1-\beta}$ and $f$ are extended by their limits $2$ and $1$ at $\beta=0$, so the formulas are not trivialized by Lean's convention $x/0=0$. The printed Eq. (4.6) has an exponent $1/2$ on the logarithm's argument that contradicts (2.26), (4.5) and (4.9); the definition of $f$ drops it. The $-i\eta\epsilon$ prescriptions are suppressed. The $\delta(q^2)$ integration in (2.13) is carried out, leaving an integral over the shell $\lambda\le|\mathbf q|\le\Lambda$. Positivity is stated as $\ge0$, because $A=B=0$ in degenerate configurations. Sec. IV beyond (4.9) (the velocity expansion (4.8), the quadrupole formula (4.13), the solar estimate) and the Coulomb phases of Sec. V are out of scope for this mission.

A complete development needs solid-angle integration on $S^2$ (a spherical-coordinates change of variables for volume.toSphere), integration in polar coordinates on $\mathbb R^3$, and elementary inequalities for Minkowski products of timelike and null vectors. These are reusable beyond this mission, and contributions of them as separate lemmas are welcome.

Selected references

• S. Weinberg, Infrared Photons and Gravitons, Phys. Rev. 140, B516 (1965). https://doi.org/10.1103/PhysRev.140.B516
• F. Bloch and A. Nordsieck, Note on the Radiation Field of the Electron, Phys. Rev. 52, 54 (1937). https://doi.org/10.1103/PhysRev.52.54
• D. R. Yennie, S. C. Frautschi and H. Suura, The infrared divergence phenomena and high-energy processes, Ann. Phys. 13, 379 (1961). https://doi.org/10.1016/0003-4916(61)90151-8

Motivation

Solitons (localized, finite-energy, non-dissipating solutions of classical field equations) are the simplest examples of the topological objects that dominate the non-perturbative physics of gauge theories: vortices, magnetic monopoles and instantons. G. 't Hooft's lecture notes Monopoles, Instantons and Confinement (arXiv:hep-th/0010225) open with the two textbook examples in one space and one time dimension, the φ⁴ kink and the sine-Gordon soliton, because every later construction in the notes (the Abrikosov–Nielsen–Olesen vortex, the 't Hooft–Polyakov monopole, the BPST instanton) repeats the same pattern: a degenerate vacuum, a static solution interpolating between two vacua, and an energy (or action) bounded below by a topological quantity — the Bogomol'nyi bound — which the soliton saturates.

This mission formalizes that pattern in its cleanest setting, Chapter 1 (Sections 1.1–1.2) together with Exercise (i) of the notes.

Setting

A static real scalar field is a function $\varphi : \mathbb R \to \mathbb R$. Its energy (eq. (1.5)) for a potential $V$ is

$$E_V[\varphi] = \int_{-\infty}^{\infty} \Big(\tfrac12 (\partial_x\varphi)^2 + V(\varphi)\Big)\,dx \in [0,\infty].$$

Two potentials are considered, with parameters $\lambda, A, F > 0$:

1. Case (a), the "Mexican hat" (eq. (1.2)): $V_a(\varphi) = \frac{\lambda}{4!}(\varphi^2 - F^2)^2$, with the two vacua $\varphi = \pm F$ and particle mass $m$ given by $m^2 = \lambda F^2/3$.
2. Case (b), sine-Gordon (eq. (1.3)): $V_b(\varphi) = A\big(1 - \cos(2\pi\varphi/F)\big)$, with vacua $\varphi = nF$, $n \in \mathbb Z$, particle mass $m = 2\pi\sqrt A/F$ and quartic coupling $\lambda = 16\pi^4 A/F^4$.

The static field equation is $\partial_x^2\varphi = V'(\varphi)$. The notes give the explicit solutions

$$\varphi_a(x) = F\tanh\big(\tfrac12 m(x-x_0)\big), \qquad \varphi_b(x) = \frac{2F}{\pi}\arctan\big(e^{m(x-x_0)}\big),$$

which interpolate between $-F$ and $F$ (case (a)) and between $0$ and $F$ (case (b)).

Formalization targets

Goal

For every $x_0$: in case (a) the kink has energy $2m^3/\lambda$ and no differentiable configuration with $\varphi(-\infty) = -F$, $\varphi(+\infty) = F$ has smaller energy; in case (b) the soliton has energy $8m^3/\lambda$ and no differentiable configuration with $\varphi(-\infty) = 0$, $\varphi(+\infty) = F$ has smaller energy:

$$E_{V_a}[\varphi_a] = \frac{2m^3}{\lambda} \le E_{V_a}[\varphi], \qquad E_{V_b}[\varphi_b] = \frac{8m^3}{\lambda} \le E_{V_b}[\varphi].$$

Milestones

1. First integral of the static equation, eq. (1.4).
2. The φ⁴ kink solves the static equation with the stated boundary values.
3. The sine-Gordon soliton solves the static equation with the stated boundary values.
4. The φ⁴ kink mass $2m^3/\lambda$ (p. 5).
5. The sine-Gordon soliton mass $8m^3/\lambda$ (p. 5).
6. Bogomol'nyi bound, case (a) (eq. (1.7), Exercise (i)).
7. Bogomol'nyi bound, case (b) (eq. (1.7), Exercise (i)).

Significance

The result identifies the soliton mass with a boundary term, $E = W(\varphi)\big|_{\varphi_{-\infty}}^{\varphi_{+\infty}}$ with $W' = \sqrt{2V}$, so the mass depends only on the pair of vacua joined, and shows the kink is a global energy minimizer in its topological sector — the classical stability statement behind treating the kink as a particle of mass $\propto m^3/\lambda$, heavy in the weak-coupling regime.

The physics is classical and fully known. What this mission adds is a machine-checked account: explicit verification of the closed-form solutions, exact evaluation of improper energy integrals, and a rigorous Bogomol'nyi argument for configurations that are merely differentiable, with limits at $\pm\infty$ rather than compact support. No existing platform theorem matching these statements was found by a library search at drafting time.

Difficulty

The pointwise inequality $\tfrac12\varphi'^2 + V(\varphi) \ge \varphi'\sqrt{2V(\varphi)}$ is elementary; the difficulty lies in turning it into a statement about improper integrals over $\mathbb R$ for arbitrary differentiable fields. One must handle configurations of infinite energy, pass from integrals over $[a,b]$ to $\mathbb R$ using only the boundary limits, and deal with $\sqrt{2V}$ being non-smooth at the vacua of $V_a$ and at every vacuum of $V_b$ (a configuration may overshoot a vacuum). The explicit energy computations require exact evaluation of $\int \mathrm{sech}^4$ and $\int \mathrm{sech}^2$ type integrals as Lebesgue integrals.

Formalization scope

• Fields are functions $\mathbb R \to \mathbb R$; derivatives are Mathlib's deriv. Every competitor in the bounds is assumed differentiable everywhere, and boundary values are expressed as limits at $-\infty$ and $+\infty$.
• The energy is a lower Lebesgue integral valued in $[0,\infty]$ of the (nonnegative) energy density, so configurations with infinite energy are allowed and satisfy the bounds trivially; no integrability hypothesis is imposed.
• The parameters are strictly positive: $\lambda > 0$, $A > 0$, $F > 0$. The masses $m$ and the sine-Gordon coupling are defined from $\lambda, A, F$ by the relations of Section 1.1, not left as free parameters.
• The statements do not assume the competitor solves the field equation, and do not assume finite energy — assuming either would weaken the bound.
• All declarations live in the namespace MonopolesInstantonsConfinement, intended to be shared by later missions drawn from the same notes.

Selected references

• G. 't Hooft, Monopoles, Instantons and Confinement, lecture notes (Saalburg 1999) written by F. Bruckmann, 2000. arXiv:hep-th/0010225
• E. B. Bogomol'nyi, The stability of classical solutions, Sov. J. Nucl. Phys. 24 (1976) 449.
• R. Rajaraman, Solitons and Instantons, North-Holland, 1982.

Motivation

Big-bang nucleosynthesis and the acoustic peaks of the cosmic microwave background fix the baryon density of the universe to about 5% of its total energy density, but in the low-redshift universe only some 10% of those baryons are seen in galaxies, with another 10% in the circumgalactic and intracluster medium. Simulations place the remainder — the missing baryons — in a diffuse warm-hot intergalactic medium (WHIM) at $10^5$–$10^7$ K, spread along the filaments of the cosmic web. Absorption-line studies and X-ray emission from individual filaments probe the cool and the hot ends of that range respectively, leaving the bulk poorly constrained.

de Graaff, Cai, Heymans & Peacock (2019) attack the problem statistically, by stacking the Planck Compton-$y$ map over $1\,020\,334$ pairs of CMASS galaxies and measuring the residual signal in the bridge between each pair. Interpreting that residual requires an analytic model of a filament, and that model — a cylinder with a Gaussian cross-section, convolved with the instrument beam — is what this mission formalizes. The same model, applied to the CMB lensing convergence map, converts the measured signals into a gas density and temperature, and hence into a baryon fraction.

Setting

A filament is modelled as an infinite cylinder seen side-on. In the plane perpendicular to the filament axis, write $\ell$ for the line-of-sight coordinate and $r_\perp$ for the transverse coordinate on the sky. The electron density is taken to be a two-dimensional Gaussian

$$n_e(\ell, r_\perp) = n_0 \exp\!\left(-\frac{\ell^2}{2\sigma^2}\right)\exp\!\left(-\frac{r_\perp^2}{2(\sigma^2+\sigma_B^2)}\right),$$

with central density $n_0$, intrinsic width $\sigma$ and beam width $\sigma_B$; the transverse direction, unlike the line of sight, is smoothed by the instrument beam, which is why $\sigma_B$ appears only there.

The Compton $y$ parameter of a line of sight is the optical-depth-weighted temperature of the scattering electrons,

$$y = \frac{k_B T_e \sigma_T}{m_e c^2}\int n_e \, d\ell,$$

with $k_B$ the Boltzmann constant, $\sigma_T$ the Thomson cross-section, $m_e c^2$ the electron rest energy and $T_e$ the electron temperature, assumed constant across the filament. The convergence $\kappa$ of CMB lensing is the analogous projection of the total matter density contrast $\delta = \rho/\bar\rho - 1$,

$$\kappa = \frac{3H_0^2\Omega_m}{2c^2}\int_0^{D_S} \frac{D_L(D_S-D_L)}{D_S}\,\frac{\delta}{a}\, dD_L,$$

with $H_0$ the Hubble constant, $\Omega_m$ the matter density parameter, $a$ the scale factor and $D_L, D_S$ the comoving distances of lens and source. For a structure thin compared with the lensing kernel, the geometric factor is constant across it and $\kappa$ reduces to a line-of-sight integral of $\delta$ against a fixed prefactor.

The significance of the measurement is assessed with a second, statistical layer. A stack of $N$ binned profiles $y^k_i$ ($k$ the map index, $i$ the bin index) has mean profile $\bar y_i = \frac1N\sum_k y^k_i$ and covariance estimator $C_{i,j} = \frac1N\sum_k (y^k_i-\bar y_i)(y^k_j-\bar y_j)$; the deviation of the mean profile from zero is measured by $\chi^2 = \sum_{i,j}\bar y_i (C^{-1})_{i,j}\bar y_j$. Because the stacked maps overlap on the sky, the paper replaces $C$ by a jackknife covariance built from $N_{\mathrm{sub}}$ sky sub-samples, $C^{JK}_{i,j} = \frac{N_{\mathrm{sub}}-1}{N_{\mathrm{sub}}}\sum_k (y^k_i-\bar y_i)(y^k_j-\bar y_j)$, and multiplies the inverse by the Hartlap factor $(N_{\mathrm{sub}}-n-2)/(N_{\mathrm{sub}}-1)$, with $n$ the number of bins.

Measurements enter through two numbers: the mean Compton parameter $\bar{y}$ and the mean convergence $\bar{\kappa}$ over the boxed filament region, together with the empirical observation that the peak of each profile is close to $1/0.9$ times its mean. Every statement in this mission imposes that calibration as a hypothesis on the model.

Formalization targets

Goal — total electron content, Eq. (A.4)

$$N_e \;=\; L \iint n_e\, d\ell\, dr_\perp \;=\; \frac{\bar y}{0.9}\,\frac{m_e c^2}{k_B T_e \sigma_T}\,\sqrt{2\pi}\, L\, \sqrt{\sigma^2+\sigma_B^2}.$$

This is the quantity the paper's baryon budget is computed from: given the measured $\bar y$, an assumed temperature $T_e$ and the beam width, it fixes the number of electrons in a filament of length $L$.

Milestone — projected profile, Eq. (A.2)

$$y(r_\perp) = \sqrt{2\pi}\, n_0\sigma\,\frac{k_B T_e \sigma_T}{m_e c^2}\exp\!\left(-\frac{r_\perp^2}{2(\sigma^2+\sigma_B^2)}\right).$$

Milestone — central density, Eq. (A.3)

$$n_0 = \frac{\bar y/0.9}{\sqrt{2\pi}\,\sigma}\cdot\frac{m_e c^2}{k_B T_e \sigma_T}.$$

Milestone — lensing counterpart, Eq. (A.5)

$$\delta_0 = \frac{\bar\kappa/0.9}{\sqrt{2\pi}\,\sigma}\cdot\frac{2ac^2}{3H_0^2\Omega_m}\cdot\frac{D_S}{D_L(D_S-D_L)}.$$

Milestone — beam dominance, the remark after Eq. (A.4)

$$\sigma_B \le \sqrt{\sigma^2+\sigma_B^2}\le \sigma_B\left(1+\frac{\sigma^2}{2\sigma_B^2}\right).$$

Milestone — the covariance estimators, Eqs. (3) and (5)-(6)

Both $C$ and $C^{JK}$ are symmetric and positive semidefinite, for every data set and every sample size.

Milestone — the significance statistic, Eq. (4)

$$C \text{ positive definite} \implies \chi^2 = \sum_{i,j}\bar y_i (C^{-1})_{i,j}\bar y_j \ge 0.$$

Milestone — the Hartlap correction, Eq. (7)

$$\sum_{i,j}\bar y_i\left[\frac{N_{\mathrm{sub}}-n-2}{N_{\mathrm{sub}}-1}C^{-1}\right]_{i,j}\bar y_j = \frac{N_{\mathrm{sub}}-n-2}{N_{\mathrm{sub}}-1}\sum_{i,j}\bar y_i (C^{-1})_{i,j}\bar y_j.$$

Significance

The four displayed identities are the entire inferential chain from two stacked maps to a baryon fraction. Eq. (A.2) says what the model predicts for the observable; Eq. (A.3) inverts it at the filament axis; Eq. (A.4) turns the inversion into a total electron count, from which the paper obtains gas at $(5.5\pm2.9)\,\bar\rho_b$ and $T=(2.7\pm1.7)\times10^6$ K, accounting for $11\pm7\%$ of the cosmic baryon budget; Eq. (A.5) supplies the independent lensing constraint that breaks the density–temperature degeneracy of the SZ measurement alone. The statistical milestones cover the other half of the analysis: the covariance estimators of Eqs. (3) and (5)-(6) that turn a stack into an error bar, the nonnegativity of the $\chi^2$ of Eq. (4) that is converted into the quoted $2.9\sigma$, and the Hartlap rescaling of Eq. (7). The beam-dominance milestone quantifies the paper's claim that the result barely depends on the one free shape parameter, the intrinsic width $\sigma$, which is taken from simulations rather than measured.

Formalizing them contributes a machine-checked derivation layer for a widely used observational technique: the projection of a Gaussian cylinder onto a Compton-$y$ or convergence map, and the inversion of that projection, recur throughout stacked-SZ and stacked-lensing analyses. What this mission adds over the paper is a statement of each identity with all its hypotheses exposed — which positivity conditions are needed, which parameters genuinely drop out — rather than a new physical result. The physics is not re-derived and the measurement is not re-analysed; the empirical inputs $\bar y$, $\bar\kappa$ and the peak-to-mean ratio $1/0.9$ enter as hypotheses, not as claims.

Difficulty

The identities are Gaussian integrals, so the mathematical depth is modest; the difficulty is bookkeeping and faithfulness. Three specific traps. First, the line-of-sight and transverse directions have different widths — $\sigma$ against $\sqrt{\sigma^2+\sigma_B^2}$ — and the asymmetry is what makes the final answer depend on the beam; a formalization that symmetrizes them is a different theorem. Second, the paper's $n_0$ is not free: it is pinned by the calibration $y_{\text{peak}} = \bar y/0.9$, so the goal must carry that equation as a hypothesis rather than substituting a closed form for $n_0$ silently. Third, the total electron count is an iterated integral over the plane, and the inner and outer variables must be kept in the paper's order.

Formalization scope

Everything is stated over $\mathbb{R}$ with no units, so every physical constant is an explicit real variable; integrals are Bochner integrals over the whole real line with Lebesgue measure, which return $0$ on a non-integrable integrand. The definition bundle fixes the model once — the SZ prefactor, the Gaussian cylinder profile, the Compton parameter, the thin-lens convergence prefactor, the convergence and the total electron content — and every statement is phrased against it. The convergence definition is the thin-lens specialization of Eq. (2): the geometric kernel is a constant prefactor, not an integral over lens distance, and the mission does not claim the reduction from the full Eq. (2) to that form.

Degenerate readings are ruled out as follows. The calibration hypotheses are satisfiable for every admissible choice of constants, so no statement is vacuous; conversely they genuinely constrain the central amplitude, so no statement holds for a trivial reason. The positivity hypotheses are the minimal ones that make the denominators nonzero, and the widths enter as $\sigma > 0$ with $\sigma_B$ unrestricted, so the beam-free case $\sigma_B = 0$ is included rather than excluded. The statistical layer is finite-dimensional: profiles are real arrays indexed by a finite bin type, covariances are real matrices, and matrix inversion is the nonsingular inverse, which returns the zero matrix on a singular argument — hence the positive-definiteness hypothesis in the $\chi^2$ milestone. Counts are natural numbers but all arithmetic in the prefactors is performed after casting to the reals, so $N_{\mathrm{sub}} - n - 2$ is a genuine real subtraction and may be negative. The statistical statements assert the structural properties of the estimators as written; they do not assert unbiasedness, nor the reduction $C \to C/N$ for the covariance of a mean, nor any property of the resampling scheme. Only Mathlib's Gaussian-integral, measure-theory and positive-semidefinite-matrix API is needed; no new infrastructure is required, and the resulting projection lemmas are reusable for any other stacked-profile analysis.

Selected references

• A. de Graaff, Y.-C. Cai, C. Heymans, J. A. Peacock, Probing the missing baryons with the Sunyaev-Zel'dovich effect from filaments, Astronomy & Astrophysics 624, A48 (2019). doi:10.1051/0004-6361/201935159
• R. A. Sunyaev, Y. B. Zeldovich, The Observations of Relic Radiation as a Test of the Nature of X-Ray Radiation from the Clusters of Galaxies, Comments on Astrophysics and Space Physics 4, 173 (1972).
• Planck Collaboration XXII, Planck 2015 results. XXII. A map of the thermal Sunyaev-Zeldovich effect, A&A 594, A22 (2016). doi:10.1051/0004-6361/201525826
• Planck Collaboration XV, Planck 2015 results. XV. Gravitational lensing, A&A 594, A15 (2016). doi:10.1051/0004-6361/201525941
• J. Hartlap, P. Simon, P. Schneider, Why your model parameter confidences might be too optimistic: unbiased estimation of the inverse covariance matrix, A&A 464, 399 (2007). doi:10.1051/0004-6361:20066170
• H. Tanimura et al., A search for warm/hot gas filaments between pairs of SDSS Luminous Red Galaxies, MNRAS 483, 223 (2019). doi:10.1093/mnras/sty3118

Motivation

The Rydberg constant $R_\infty$ is the constant of spectroscopy that sets the scale of the hydrogen spectrum. It first appeared as an empirical fitting parameter in J. Rydberg's formula for the hydrogen spectral series; N. Bohr later showed that its value can be computed from more fundamental constants within his model of the atom. Before the 2019 revision of the SI it was, together with the electron spin $g$-factor, among the most accurately measured physical constants (relative standard uncertainty about $1.1\times 10^{-12}$, CODATA 2022). This mission formalizes the algebraic content of the standard account of $R_\infty$ as presented in the Wikipedia article Rydberg constant: its closed form, its reduced-mass correction, its alternative expressions through the fine-structure constant, and the Bohr-model derivation of the Rydberg formula.

Setting

Fix five strictly positive real numbers: the electron rest mass $m_e$, the elementary charge $e$, the vacuum permittivity $\varepsilon_0$, the Planck constant $h$ and the speed of light $c$. From them define

$$R_\infty=\frac{m_e e^4}{8\varepsilon_0^2h^3c},\qquad \hbar=\frac{h}{2\pi},\qquad \alpha=\frac{1}{4\pi\varepsilon_0}\frac{e^2}{\hbar c},$$

the Compton wavelength $\lambda_e=h/(m_ec)$, Compton frequency $f_C=m_ec^2/h$, Compton angular frequency $\omega_C=2\pi f_C$, Bohr radius $a_0=4\pi\varepsilon_0\hbar^2/(e^2m_e)$, classical electron radius $r_e=\frac{1}{4\pi\varepsilon_0}\frac{e^2}{m_ec^2}$, and the Rydberg unit of energy $\mathrm{Ry}=hcR_\infty$.

For a nucleus of mass $M>0$ the reduced mass is $\mu=1/(1/m_e+1/M)$ and the corrected Rydberg constant is $R_M=(\mu/m_e)R_\infty$; for hydrogen $M=m_p$ and $R_M=R_{\mathrm H}$.

A Bohr orbit with principal quantum number $n$ of a particle of mass $m$ and charge $-e$ about a fixed charge $+e$ is a circular orbit of radius $r>0$ and speed $v>0$ such that the Coulomb force supplies the centripetal force and the angular momentum is quantized:

$$\frac{mv^2}{r}=\frac{e^2}{4\pi\varepsilon_0r^2},\qquad mvr=n\hbar .$$

Its energy is $E=\tfrac12mv^2-\dfrac{e^2}{4\pi\varepsilon_0 r}$. The infinite-nuclear-mass model uses $m=m_e$; the reduced-mass model uses $m=\mu$.

Formalization targets

Goal: the Rydberg formula with reduced mass

For distinct positive integers $n_1,n_2$ and Bohr orbits of mass $\mu$ with quantum numbers $n_1,n_2$, the wavenumber $1/\lambda=(E_{n_2}-E_{n_1})/(hc)$ of the photon emitted in the transition satisfies

$$\frac1\lambda=R_M\left(\frac1{n_1^2}-\frac1{n_2^2}\right).$$

Milestones

1. Equivalent forms of the reduced-mass correction: $R_M=\frac{\mu}{m_e}R_\infty=\frac{R_\infty}{1+m_e/M}=\frac{M}{m_e+M}R_\infty$.
2. Isotopic shift: $R_M$ is strictly increasing in $M$ and stays below $R_\infty$.
3. Rydberg unit of energy: $hcR_\infty=\alpha^2m_ec^2/2$.
4. Alternative expressions: $R_\infty=\frac{\alpha^2m_ec}{2h}=\frac{\alpha^2}{2\lambda_e}=\frac{\alpha}{4\pi a_0}$, and $1/R_\infty=(4\pi/\alpha)a_0$.
5. Energy-unit expressions: $\mathrm{Ry}=\tfrac12m_ec^2\alpha^2=\tfrac12\frac{e^4m_e}{(4\pi\varepsilon_0)^2\hbar^2}=\tfrac12\frac{m_ec^2r_e}{a_0}=\tfrac12\frac{hc\alpha^2}{\lambda_e}=\tfrac12hf_C\alpha^2=\tfrac12\hbar\omega_C\alpha^2$.
6. Bohr energy levels (infinite nuclear mass): $E_n=-hcR_\infty/n^2$.
7. Rydberg formula (infinite nuclear mass): $\frac1\lambda=\mathrm{Ry}\cdot\frac1{hc}\left(\frac1{n_1^2}-\frac1{n_2^2}\right)=\frac{m_ee^4}{8\varepsilon_0^2h^3c}\left(\frac1{n_1^2}-\frac1{n_2^2}\right)$.
8. Bohr energy levels with reduced mass: $E_n=-hcR_M/n^2$.

Significance

These identities are the standard bridge between the empirical Rydberg formula and the constants $m_e,e,\varepsilon_0,h,c$: they explain why a single constant governs all hydrogen series, why isotopes such as deuterium show shifted lines (the shift led to the discovery of deuterium), and how $R_\infty$ relates to $\alpha$, $a_0$ and the Compton scales. The results are classical and not open; the mission's contribution is a machine-checked, reusable layer of definitions (Bohr orbits, reduced mass, the named atomic length and energy scales) on which later atomic-physics formalizations can build.

Difficulty

The content is elementary algebra with positivity side conditions. The main point to handle carefully is that the Bohr-orbit conditions determine $v$ and $r$ only implicitly; the energy must be computed from the two defining equations rather than from explicit formulas, and every division must be justified by positivity of the constants.

Formalization scope

All constants are real numbers bundled in a structure with strict positivity fields; no SI numerical values (CODATA figures, $1.09678\times10^7\,\mathrm m^{-1}$, etc.) are formalized, and the precision-measurement and QED discussion of the source is out of scope. The Bohr model is formalized for a single particle of mass $m$ orbiting a fixed charge $+e$ (hydrogen-like, $Z=1$); the reduced-mass correction is modelled, as in the source, by substituting $\mu$ for $m_e$. The photon wavenumber is taken to be the orbital energy difference divided by $hc$. The Bohr-orbit hypotheses are satisfiable for every $n\ge1$ and every $m>0$, so the Bohr-model statements are not vacuous. Contributions of alternative proofs and of generalizations (nuclear charge $Z$, explicit orbit radii and speeds) are welcome.

Selected references

• Wikipedia contributors, Rydberg constant, revision 1341645811. https://en.wikipedia.org/w/index.php?title=Rydberg_constant&oldid=1341645811
• CODATA 2022 value of the Rydberg constant, NIST Reference on Constants, Units, and Uncertainty. https://physics.nist.gov/cgi-bin/cuu/Value?ryd
• B. H. Bransden, C. J. Joachain, Quantum Mechanics, 2nd ed., Prentice Hall, 2000.

Motivation

Since the 2019 revision of the International System of Units (SI), the elementary charge $e$ is no longer a measured quantity: it is one of the seven defining constants of the SI and is fixed by definition at

$$e = 1.602\,176\,634 \times 10^{-19}\ \mathrm{C}.$$

Before that revision, $e$ had to be extracted from experiment, and the metrology literature accumulated several independent routes to it: Faraday's laws of electrolysis combined with the Avogadro constant, Millikan and Fletcher's oil-drop experiment (1909), shot-noise analysis, and — since the 1980s — the combination of the Josephson effect and the quantum Hall effect. Each route is a short algebraic recipe that turns other measured constants into $e$. The 2019 redefinition did not delete those recipes; it inverted their role. With $e$, the Planck constant $h$, the Avogadro constant $N_\mathrm{A}$ and the speed of light $c$ all fixed exactly, the recipes become exact arithmetic identities between defining constants, and the residual measurement uncertainty migrates to the constants that are no longer fixed (the vacuum magnetic permeability $\mu_0$, equivalently the fine-structure constant $\alpha$).

This mission formalizes exactly those identities, as they are stated in the source article, together with the two quantization statements the same article records: Dirac's 1931 argument that a magnetic monopole forces charge quantization, and the closure property behind the observation that although quarks carry charges in multiples of $e/3$, isolatable particles carry integer multiples of $e$.

Setting

All quantities are real numbers carrying SI units implicitly; the Lean development works in ℝ and fixes the numerical values as exact rationals, never as floating-point approximations.

The defining constants used here are $e = 1.602\,176\,634\times10^{-19}$ (coulomb), $N_\mathrm{A} = 6.022\,140\,76\times10^{23}$ (per mole), $h = 6.626\,070\,15\times10^{-34}$ (joule second) and $c = 299\,792\,458$ (metre per second).

From these the article builds four derived constants, each of which is a definition in this mission rather than an axiom:

• the Faraday constant $F = N_\mathrm{A} e$, the charge of one mole of electrons;
• the Josephson constant $K_\mathrm{J} = 2e/h$, measurable through the Josephson effect;
• the von Klitzing constant $R_\mathrm{K} = h/e^{2}$, measurable through the quantum Hall effect;
• the fine-structure constant in the form used by CODATA, $\alpha = \mu_0 c e^{2}/(2h)$, with $\mu_0$ the vacuum magnetic permeability.

A fifth definition captures the natural unit of charge $q_0 = \sqrt{4\pi\varepsilon_0\hbar c}$ of those natural unit systems in which $e = q_0\sqrt{\alpha}$, with $\varepsilon_0$ the electric constant and $\hbar$ the reduced Planck constant.

Target

The goal theorem asserts that the three determination routes recorded in the source return one and the same number, the fixed SI value of $e$, and that the electrolysis route's intermediate constant has its exact SI value:

$$F = N_\mathrm{A} e = 96\,485.332\,123\,310\,018\,4,\qquad \frac{F}{N_\mathrm{A}} = e,$$ $$\frac{2}{K_\mathrm{J} R_\mathrm{K}} = e, \qquad \sqrt{\frac{2h\alpha}{\mu_0 c}} = e \quad\text{whenever}\quad \alpha = \frac{\mu_0 c e^{2}}{2h}.$$

The milestones are the individual identities, each stated for arbitrary positive values of the constants rather than only at the SI values, plus the two quantization statements:

1. $F/N_\mathrm{A} = e$ for any $N_\mathrm{A} \neq 0$;
2. the exact value of $F$ at the SI values of $N_\mathrm{A}$ and $e$;
3. $2/(K_\mathrm{J}R_\mathrm{K}) = e$ for $e \neq 0$, $h \neq 0$;
4. the CODATA relation $e = \sqrt{2h\alpha/(\mu_0 c)}$;
5. $e = q_0\sqrt{\alpha}$ for $q_0 = \sqrt{4\pi\varepsilon_0\hbar c}$ and $\alpha = e^{2}/(4\pi\varepsilon_0\hbar c)$;
6. Dirac quantization: if a monopole charge $g \neq 0$ satisfies $qg \in \tfrac{\hbar}{2}\mathbb{Z}$ for every charge $q$ in a collection, then every such $q$ is an integer multiple of the fixed quantum $\hbar/(2g)$;
7. if every charge in a collection $S$ is an integer multiple of a quantum $q_0$, then so is every charge in the additive subgroup of $\mathbb{R}$ generated by $S$.

Significance

The result itself. The content is the coherence of the SI's electrical sector: the same $e$ comes out of an electrochemical measurement chain, a quantum-electrical one and the CODATA relation, and the arithmetic that links them is exact. Milestones 6 and 7 record the two quantization statements in the source: the Dirac argument is a genuine implication (a monopole forces the charge spectrum into a discrete subgroup), while milestone 7 isolates the algebraic half of "stable groupings of quarks carry integer charge" — closure of a quantized spectrum under composition.

Formalizing it. What this mission produces is a small, faithful, reusable encoding of the 2019 SI defining constants and of the standard derived constants, with the exact rational values rather than floating-point ones, and with the degenerate cases made explicit. Nothing here is an open problem, and the mission should not be read as one: the value is a checked reference layer for physics-flavoured formalization, not a research advance.

Difficulty

Low, and stated as such deliberately. Milestones 1–3 are field arithmetic; 4 and 5 are field arithmetic plus Real.sqrt of a square, which needs the positivity hypotheses that are carried explicitly; 6 and 7 are elementary manipulations of ℤ-multiples and of AddSubgroup.closure. The only places a solver can go wrong are the degenerate ones: division by a constant that has not been assumed nonzero, and Real.sqrt of a quantity not known to be nonnegative — which is why every statement carries positivity or nonvanishing hypotheses rather than leaving Lean's junk values to decide the outcome.

Formalization scope

Conventions this mission commits to:

• Units are implicit; every constant is a bare real number in the SI unit named in its docstring.
• The fixed values are exact rationals (for example eSI = 1602176634 / 10 ^ 28), so the numeric milestone is an exact identity, provable by norm_num, not a floating-point comparison.
• The derived constants are functions of their arguments, so that each identity can be stated for general positive values and then instantiated at the SI values. This rules out a trivializing reading in which a "relation" holds only because both sides are the same closed numeral.
• Every division carries a nonvanishing hypothesis and every Real.sqrt a nonnegativity or positivity hypothesis, so no statement is discharged by a Lean junk value.
• Dirac's condition is stated as membership of $qg$ in $\tfrac{\hbar}{2}\mathbb{Z}$ for each charge in a given set, and its conclusion as membership of $q$ in $\tfrac{\hbar}{2g}\mathbb{Z}$; the physical derivation of the condition is not part of the mission.
• No physics is assumed as an axiom: everything is a definition plus arithmetic over ℝ, using only Mathlib.

Contributions welcome beyond the current list: the shot-noise and oil-drop routes, which the source describes qualitatively rather than by a formula, would need a probabilistic or mechanical model before they can be stated, and that model would be a worthwhile addition.

Selected references

• "Elementary charge", Wikipedia, the revision supplied as the mission source: https://en.wikipedia.org/wiki/Elementary_charge
• D. B. Newell and E. Tiesinga, The International System of Units (SI), NIST Special Publication 330 (2019). DOI: 10.6028/NIST.SP.330-2019
• Bureau International des Poids et Mesures, The International System of Units (SI Brochure), 9th ed. https://www.bipm.org/documents/20126/41483022/SI-Brochure-9-EN.pdf
• R. A. Millikan, "The isolation of an ion, a precision measurement of its charge, and the correction of Stokes's law", Science 32 (822), 436–448 (1910). DOI: 10.1126/science.32.822.436
• J. Preskill, "Magnetic Monopoles", Annual Review of Nuclear and Particle Science 34, 461–530 (1984). DOI: 10.1146/annurev.ns.34.120184.002333
• CODATA 2022 value of the elementary charge, NIST: https://physics.nist.gov/cgi-bin/cuu/Value?e

Motivation

The Boltzmann constant $k_B$ is the proportionality factor relating the average thermal energy of the particles of a system to its thermodynamic temperature. It appears wherever a microscopic energy has to be compared with a macroscopic temperature: in the ideal gas law written per molecule, in the equipartition theorem, in the Boltzmann factor $e^{-E/k_BT}$ that governs equilibrium occupation probabilities, in Boltzmann's entropy formula $S = k\log W$, in the thermal voltage of a $p$–$n$ junction, and in the Johnson noise of a resistor.

The constant also has an unusual documentary history. Boltzmann linked entropy and probability in 1877 but never introduced a constant; Max Planck first wrote $k$, and gave the first numerical value ($1.346\times10^{-23}$ J/K, about 2.5% below the modern figure), in his 1900–1901 derivation of the black-body law — the terse $S = k\log W$ on Boltzmann's tombstone is Planck's formulation. For most of the twentieth century $k_B$ was a measured quantity; the 2017 acoustic gas thermometry campaign reached a relative uncertainty of 0.2 ppm, and as part of the 2019 revision of the SI the constant was defined to the exact value $1.380649\times10^{-23}$ J·K⁻¹, which is now what fixes the kelvin.

This mission formalizes the elementary quantitative content of that picture: the identities that make $k_B$ a conversion factor, and the exact arithmetic that the 2019 SI definitions make possible.

Setting

Work throughout with real numbers; units are carried in the prose, not in the types. Fix the exact post-2019 SI values

$$k_B = 1.380649\times10^{-23}\ \mathrm{J\,K^{-1}}, \qquad N_A = 6.02214076\times10^{23}\ \mathrm{mol^{-1}}, \qquad q = 1.602176634\times10^{-19}\ \mathrm{C},$$

and define the molar gas constant as the product $R = k_B N_A$.

A gas sample is described by its pressure $p$, volume $V$, absolute temperature $T$, amount of substance $n$, molecule count $N = nN_A$, particle mass $m$, and mean square particle speed $\langle v^2\rangle$. A system with a finite set $s$ of microstates is described by an energy function $E : s \to \mathbb{R}$; its partition function is $Z = \sum_{i\in s} e^{-E_i/(k_BT)}$ and its Boltzmann probabilities are $P_i = e^{-E_i/(k_BT)}/Z$. For a distribution $p$ on $s$, the Gibbs entropy is $S = -k_B\sum_i p_i\log p_i$, the Shannon entropy (in nats) is $-\sum_i p_i\log p_i$, and for $W$ equiprobable microstates Boltzmann's entropy is $k_B \log W$. The thermal voltage is $V_T(T) = k_BT/q$. All logarithms are natural.

Target

The goal theorem is the statement that fixes the physical meaning of $k_B$: kinetic theory plus the per-molecule gas law determine the mean translational kinetic energy. From

$$pV = \tfrac{1}{3}Nm\langle v^2\rangle \qquad\text{and}\qquad pV = Nk_BT$$

conclude

$$\tfrac{1}{2}m\langle v^2\rangle = \tfrac{3}{2}k_BT, \qquad v_{\mathrm{rms}} = \sqrt{3k_BT/m}.$$

The milestones are the surrounding identities, in the order of the source: the equivalence $pV = nRT \iff pV = Nk_BT$; equipartition, $\tfrac{1}{2}m\langle v_x^2\rangle = \tfrac{1}{2}k_BT$ per degree of freedom; the ratio law $v_{\mathrm{rms}}(m_1)/v_{\mathrm{rms}}(m_2) = \sqrt{m_2/m_1}$; normalisation of the Boltzmann factors, $\sum_i P_i = 1$; the reduction of the Gibbs entropy on the uniform distribution to $S = k_B\log W$; the identification $S/k_B =$ Shannon entropy; the energy $k_BT$ of one nat of rescaled entropy; and three numerical facts — $V_T(300\ \mathrm{K}) \approx 25.85$ mV, $k_B \approx 8.617333262\times10^{-5}$ eV/K, and the exact value $R = 8.31446261815324$ J·K⁻¹·mol⁻¹.

Significance

The results. Individually these are the standard first facts of kinetic theory and statistical mechanics; together they pin down what the constant does. The equipartition chain converts a temperature into a velocity distribution scale and explains the measured room-temperature rms speeds from helium (about 1370 m/s) to xenon (about 240 m/s). The entropy statements make precise the claim that thermodynamic entropy is Shannon entropy in energy units, with $k_B$ as the exchange rate — the statement behind the natural-unit convention $k_B = 1$. The numerical milestones exercise the consequence of the 2019 SI revision that unit conversions involving $k_B$ are now exact rational arithmetic rather than propagated measurement uncertainty.

Formalizing them. All of these are settled physics; nothing here is open. What the mission produces is a small, reusable Lean development of the SI defining constants and of the elementary statistical-mechanical vocabulary (Boltzmann weights, partition function, Gibbs/Shannon/Boltzmann entropies), with each textbook identity stated against that shared model rather than re-derived ad hoc. It is a suitable entry-level mission and a foundation other physics missions can import.

Difficulty

The mathematics is elementary; the difficulty is entirely one of faithful modelling, and solvers should expect the friction to be there rather than in the proofs. Three specific points. First, Lean's division and logarithm are total: $e^{-E/(k_BT)}$ is defined at $T = 0$ and evaluates to $1$, and $\log x = 0$ for $x \le 0$, so statements must carry the positivity hypotheses that keep them physically meaningful rather than relying on the definitions to exclude bad inputs. Second, the entropy definitions are stated for an arbitrary real-valued weight function, not for a distribution; normalisation is a hypothesis where it is needed, never an assumption baked into the type. Third, the numerical milestones are claims about specific decimal numerals, and the tolerance in each is part of the statement: two of them are genuine approximations and one, the value of $R$, is an exact identity, which is only true because both factors are exact SI numerals.

Formalization scope

Quantities are real numbers (ℝ); no dimensional-analysis layer is used, and unit correctness is a convention of the prose. Finite state spaces are Finsets over an arbitrary index type, with nonemptiness stated as a hypothesis where the partition function must be nonzero. Entropies use the natural logarithm, so they are measured in nats, and the Shannon entropy is the Gibbs entropy divided by $k_B$ by construction. Temperatures, masses, volumes and particle counts are positive reals where the physics requires it. The mean square speed is a free real variable constrained only by the stated equations; it is not built from a velocity distribution, and extending the development to an actual Maxwell–Boltzmann distribution is out of scope here and a natural follow-up mission.

The statements are deliberately non-vacuous: every hypothesis set in the mission is satisfiable (positive temperature, positive mass, nonempty state space), and the numerical items admit no trivializing reading since they are closed claims about fixed numerals. Only Mathlib is required — Real.exp, Real.log, Real.sqrt, and Finset.sum. The definition file is intended to be reusable: any later mission about thermodynamics, black-body radiation, or the Shockley diode equation can import the SI constants and entropy vocabulary unchanged.

Selected references

• Wikipedia, Boltzmann constant — the source text this mission formalizes: https://en.wikipedia.org/wiki/Boltzmann_constant
• D. B. Newell and E. Tiesinga (eds.), The International System of Units (SI), NIST Special Publication 330 (2019). DOI: https://doi.org/10.6028/NIST.SP.330-2019 — the exact defining values of $k_B$, $N_A$ and $q$.
• M. Planck, "Ueber das Gesetz der Energieverteilung im Normalspectrum", Annalen der Physik 309(3):553–563 (1901). DOI: https://doi.org/10.1002/andp.19013090310 — the first introduction of $k$ and of $S = k\log W$.
• R. P. Feynman, R. B. Leighton and M. Sands, The Feynman Lectures on Physics, Vol. I, ch. 39 (kinetic theory of gases): https://www.feynmanlectures.caltech.edu/I_39.html

Motivation

Introductory physics is normally taught as a sequence of unrelated chapters — kinematics, dynamics, energy, optics, gravitation — each with its own rules. A recurring proposal in physics education is to teach instead from a single organising statement: among all conceivable histories of a system, the one realised in nature is the one that makes a certain integral, the action, stationary. Edwin Taylor's editorial A Call to Action (American Journal of Physics, 2003) argued for building the first-year curriculum on it; Lachlan McGinness and Craig Savage reported classroom results for such a course at the Australian National University (Action physics, American Journal of Physics, 2016); Massimiliano Malgieri tested a sum-over-paths treatment in an Italian secondary school (2017).

The source monograph for this mission, Julliana Rodrigues Martins, A Ação Estacionária como Eixo Unificador do Ensino de Física no Ensino Médio (Trabalho de Conclusão de Curso, Universidade Federal do Ceará, 2025), develops this programme for secondary education. Its Chapters 2 and 3 are quantitative: they follow the historical line from antiquity to the nineteenth century and carry out every calculation in full. This mission formalises that quantitative core, and nothing of the pedagogical Chapter 4.

The historical line the monograph reconstructs, and which the milestone list follows:

• Heron of Alexandria (c. 60 AD), Catoptrics: the law of reflection derived from the shortest reflected path (§2.2).
• Galileo (1638), Two New Sciences: uniformly accelerated descent on an inclined plane, and the law of chords — descent from rest along any chord of a vertical circle takes the same time (§2.3).
• Fermat (1657–1662): the method of maxima and minima, and the law of refraction obtained by minimising travel time, with the velocities entering inversely to Descartes' version (§2.4, §2.4.1).
• Maupertuis (1744, 1746): the quantity of action $mvl$, the refraction law, and the equilibrium of a lever obtained by minimising action (§2.6).
• Euler (1744), Methodus inveniendi, including Additamentum II: the discretise–vary–pass-to-the-limit method, the resulting differential equation, and Keplerian orbits from Maupertuis' principle under conservation of total energy (§2.7).
• Lagrange (1760, 1788) and Hamilton (1834–1835): the general variational derivation and the principle of stationary action $\delta\int (T-U)\,dt = 0$ (Chapter 3, §3.1).

Setting

Fix real endpoints $x_1 < x_2$ and an integrand $f(y, y', x)$, a real-valued function of three real arguments. A path is a function $y : \mathbb{R} \to \mathbb{R}$, and its action over $[x_1,x_2]$ is

$$S[y] \;=\; \int_{x_1}^{x_2} f\bigl(y(x),\, y'(x),\, x\bigr)\, dx .$$

Neighbouring paths are produced by an admissible variation: a twice continuously differentiable $\eta$ with $\eta(x_1) = \eta(x_2) = 0$, giving the family $y(x,\alpha) = y(x) + \alpha\,\eta(x)$. The path $y$ is stationary when

$$\left.\frac{d}{d\alpha}\, S[\,y + \alpha\eta\,]\right|_{\alpha = 0} = 0 \qquad \text{for every admissible } \eta .$$

Writing $\partial f/\partial y$ and $\partial f/\partial y'$ for the partial derivatives of $f$ in its first and second slots, the Euler–Lagrange expression along $y$ is

$$E_f[y](x) \;=\; \frac{\partial f}{\partial y}\bigl(y(x), y'(x), x\bigr) \;-\; \frac{d}{dx}\left[\frac{\partial f}{\partial y'}\bigl(y(x), y'(x), x\bigr)\right].$$

In mechanics one takes $x = t$, $y = q$ and $f = L = T - U$, so that stationarity of $\int (T-U)\,dt$ is Hamilton's principle and $E_L[q] = 0$ is the Lagrange equation of motion.

Formalization targets

Goal — the Euler–Lagrange equation from stationary action

For $x_1 < x_2$, $f$ twice continuously differentiable in all three arguments and $y$ twice continuously differentiable, if $y$ is stationary for $S$ then

$$\frac{\partial f}{\partial y} - \frac{d}{dx}\,\frac{\partial f}{\partial y'} \;=\; 0 \qquad \text{at every } x \in [x_1, x_2].$$

This is equation (3.9) of the monograph, and — through the substitution $x \mapsto t$, $y \mapsto q_i$, $f \mapsto L$ — equation (3.17). It is stated as the weakest stable form: stationarity, not minimality, and an arbitrary admissible integrand rather than a particular Lagrangian.

Milestones

The supporting statements are the analytic ingredients of that derivation (the fundamental lemma, the first variation formula, the first integral for a cyclic coordinate), its two mechanical applications worked out in the monograph (harmonic oscillator, plane pendulum), its geometric application (shortest path), and the historical minimisation problems of Chapter 2 (Heron, Galileo, Fermat, Maupertuis).

Significance

The Euler–Lagrange equation is the bridge the whole unification argument rests on: once it is available, Newton's second law, the pendulum equation, Snell's law, geodesics and conservation laws all become consequences of one statement about an integral, which is exactly the claim the monograph makes to justify teaching physics this way. The Chapter 2 statements are the historically prior special cases, each obtained by a one-variable minimisation rather than by the general machinery, and together they exhibit how far elementary optimisation alone reaches before the calculus of variations is needed.

What this mission adds beyond the source is a machine-checked version of an argument that, in every textbook presentation including this one, is carried out at the level of rigour of formal manipulation: the interchange of differentiation and integration is performed without justification, the passage from a vanishing integral to a vanishing integrand is asserted, and the regularity needed for $\frac{d}{dx}\,\partial f/\partial y'$ to exist is left implicit. All of it is true under the stated hypotheses; none of it is proved in the source. Mathlib has the analytic infrastructure (interval integrals, differentiation under the integral sign, smooth bump functions) but, at the environment pinned for this mission, no Euler–Lagrange equation and no calculus-of-variations layer built on it. The definitions published here — action, admissible variation, stationary path, Euler–Lagrange expression — are reusable by any later variational mission.

Difficulty

The obvious argument is three lines: differentiate under the integral sign, integrate by parts, and conclude that the integrand vanishes because $\eta$ is arbitrary. Each line is where the work is.

Differentiating under the integral sign needs a dominating bound valid uniformly for $\alpha$ near $0$; it is available here because the data are $C^2$ and the interval is compact, but it has to be produced. The integration by parts needs $x \mapsto \partial f/\partial y'(y(x), y'(x), x)$ to be differentiable, which is where the second derivative of $y$ and the second derivatives of $f$ are consumed — a $C^1$ path is not enough for this formulation. The final step needs test functions: a $C^2$ bump supported in a small interval around a point where the continuous coefficient is nonzero, which is why the fundamental lemma is a separate milestone rather than a step.

A standing trap in the Lean formulation is that deriv returns $0$ at points where a function is not differentiable, so a statement about $\frac{d}{dx}\,\partial f/\partial y'$ can be accidentally true for the wrong reason unless the regularity hypotheses are genuinely strong enough. Every statement here carries the hypotheses that make each derivative a real derivative.

Formalization scope

The development is one-dimensional and real: paths are $\mathbb{R} \to \mathbb{R}$, the integrand is a curried $f : \mathbb{R} \to \mathbb{R} \to \mathbb{R} \to \mathbb{R}$ with argument order $(y, y', x)$ matching the source's $f(y(x), y'(x), x)$, and all integrals are interval integrals over $[x_1, x_2]$. Partial derivatives are one-dimensional derivatives in the frozen remaining arguments; smoothness of $f$ is stated for its uncurried form on $\mathbb{R} \times \mathbb{R} \times \mathbb{R}$. Regularity is $C^2$ throughout — for the integrand, for the path, and for the variations — matching the monograph's requirement that $\eta$ have continuous first and second derivatives.

Stationarity is a hypothesis quantified over all admissible variations, so the goal cannot be satisfied by exhibiting one convenient $\eta$; and the conclusion is an equation at every point of the closed interval, not almost everywhere, so it cannot be weakened to a null-set statement. The mechanical milestones are stated as equivalences between the Euler–Lagrange equation for the explicit Lagrangian and the classical equation of motion, which rules out a one-directional reading that would be vacuous for a path that never satisfies either.

Physical constants ($m$, $k$, $g$, $\ell$, the speeds $v_1, v_2$) are free real parameters, with positivity or non-vanishing assumed only where the source's conclusion requires it — the pendulum equivalence divides by $m\ell^2$, so $m \neq 0$ and $\ell \neq 0$ appear, while the oscillator equivalence needs no such assumption. Angles never appear as primitive objects in the optics milestones: the sines of the incidence and refraction angles are written as the ratios $x/\sqrt{a^2+x^2}$ that the figures define them by, so no convention about angle ranges is smuggled in.

Contributions welcome: proofs of any milestone, and reusable infrastructure for differentiation under the interval integral sign and for $C^k$ bump functions with prescribed support, both of which are of use well beyond this mission.

Selected references

• Julliana Rodrigues Martins, A Ação Estacionária como Eixo Unificador do Ensino de Física no Ensino Médio, Trabalho de Conclusão de Curso (Licenciatura em Física), Universidade Federal do Ceará, Fortaleza, 2025, 60 pp. (the source of every statement in this mission; Chapters 2–3).
• Alberto Rojo and Anthony Bloch, The Principle of Least Action: History and Physics, Cambridge University Press, 2018 (the historical reconstruction the monograph follows for Chapter 2).
• Edwin F. Taylor, A call to action, American Journal of Physics 71 (2003), guest editorial.
• Lachlan P. McGinness and Craig M. Savage, Action physics, American Journal of Physics 84 (2016).
• Massimiliano Malgieri, Test on the effectiveness of the sum over paths approach in favoring the construction of an integrated knowledge of quantum physics in high school, 2017.
• Leonhard Euler, Methodus inveniendi lineas curvas maximi minimive proprietate gaudentes, Lausanne, 1744, in particular Additamentum II.