Mathematical Physics

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.

Motivation

A fusion reactor only makes sense if the plasma gives back more energy than it loses. In 1955 J. D. Lawson turned that sentence into an inequality: for a hot, thermalized fuel, the product of the particle density $n$ and the energy confinement time $\tau_E$ must exceed a temperature-dependent threshold before the fusion products alone can keep the plasma hot. The criterion was published in 1957 (Lawson, Some Criteria for a Power Producing Thermonuclear Reactor, Proc. Phys. Soc. B 70 (1957) 6–10) and has been the standard figure of merit for magnetic and inertial confinement ever since: machines are compared by their $n\tau_E$ and by the triple product $nT\tau_E$.

Timeline, as far as this mission's material traces it:

• 1955 — Lawson derives the criterion in a classified AERE report, balancing the volumetric fusion rate against bremsstrahlung radiation losses and ignoring conduction losses.
• 1957 — the report is declassified and published.
• 2004 — the textbook derivation in the form used here, together with the reactivity fit $\langle\sigma v\rangle \approx 1.1\cdot 10^{-24}\,T^2\ \mathrm{m^3/s}$ valid near $T = 14$ keV (J. Wesson, Tokamaks, 3rd ed., Oxford, 2004).
• 2022 — an inertial-confinement experiment at the National Ignition Facility is reported to exceed the Lawson criterion for ignition (Abu-Shawareb et al., Phys. Rev. Lett. 129, 075001).

Setting

Consider a steady-state, fully ionized plasma of deuterium and tritium. All quantities are real numbers and strictly positive, and the temperature $T$ is measured in energy units (electronvolts), so Boltzmann's constant does not appear: the article's $k_\mathrm{B}T$ is our $T$.

• $n$ — the particle (electron) density. Under the standing assumptions of the derivation — all species at the same temperature, no ions other than fuel ions (no impurities, no helium ash), and deuterium and tritium in the optimal 50-50 mixture — the ion density equals the electron density and $n_\mathrm{d} = n_\mathrm{t} = n/2$.
• $W = 3nT$ — the energy density of electrons and ions together, by the ideal gas law.
• $\langle\sigma v\rangle$ — the fusion cross section times relative velocity, averaged over the Maxwellian velocity distribution at temperature $T$.
• $f = n_\mathrm{d} n_\mathrm{t}\langle\sigma v\rangle$ — the volume rate of fusion reactions (reactions per volume per time), which for the 50-50 mixture equals $\tfrac14 n^2\langle\sigma v\rangle$.
• $E_\mathrm{ch}$ — the energy carried by the charged fusion products, the only part that can heat the plasma; $E_\mathrm{ch} = 3.5$ MeV for D-T, the neutron's 14.1 MeV being lost.
• $P_\mathrm{loss}$ — the power loss density, and $\tau_E = W/P_\mathrm{loss}$ — the energy confinement time.

The plasma is self-heating when fusion heating exceeds the losses:

$$f\,E_\mathrm{ch} \;\ge\; P_\mathrm{loss}.$$

Target

The goal theorem is the Lawson criterion itself — equation (1) of the source — obtained by substituting the model quantities into the self-heating condition:

$$n\,\tau_E \;\ge\; L \;\equiv\; \frac{12\,T}{E_\mathrm{ch}\,\langle\sigma v\rangle}.$$

The milestones are the surrounding statements of the same derivation, in the order a reader meets them:

$$f = \tfrac14 n^2\langle\sigma v\rangle,\qquad P_\mathrm{loss} = \frac{3nT}{\tau_E},\qquad \tfrac14 n^2\langle\sigma v\rangle E_\mathrm{ch} \ge \frac{3nT}{\tau_E},$$

the triple-product form and its numerical D-T value,

$$nT\tau_E \;\ge\; \frac{12}{E_\mathrm{ch}}\frac{T^2}{\langle\sigma v\rangle},\qquad nT\tau_E \;\ge\; 3\cdot 10^{21}\ \mathrm{keV\,s\,m^{-3}}\quad (E_\mathrm{ch} = 3500\ \mathrm{keV},\ \langle\sigma v\rangle = 1.1\cdot10^{-24}T^2),$$

the inertial-confinement form obtained from $\tau_E \approx R\sqrt{m_i/T}$,

$$n R \;\ge\; \frac{12\,T^{3/2}}{E_\mathrm{ch}\langle\sigma v\rangle\sqrt{m_i}},$$

and the empirical tokamak scaling: if $\tau_E = c\,n^{1/3}/P^{2/3}$ and $P = a\,n^2T^2$, then $nT\tau_E = c\,a^{-2/3}T^{-1/3}$, independent of the density.

Significance

The result itself. The criterion is what makes different confinement concepts comparable at all: it converts "does this machine work?" into a single number that can be measured and plotted, and its triple-product form is the quantity reported by tokamaks and by inertial-confinement shots alike. The last milestone explains why the triple product, rather than $n\tau_E$, is the quantity of record for tokamaks: under the empirical energy-confinement scaling it does not depend on the density and depends on temperature only as $T^{-1/3}$.

Formalizing it. Nothing here is an open problem: every statement is a known consequence of the stated model, and the mathematical content is algebra and monotonicity over the positive reals. What the mission produces is a machine-checked, reusable encoding of the energy-balance model of a D-T plasma, with every degenerate case (zero density, zero confinement time, vanishing reactivity) explicitly excluded, and with the chain from the model assumptions to each published form of the criterion verified end to end. The value is in the faithfulness of the model layer, not in the difficulty of the deductions.

Difficulty

The deductive content is elementary; the difficulty is representational. Three places where a careless encoding silently changes the theorem:

• Division. $\tau_E = W/P_\mathrm{loss}$ and $12T/(E_\mathrm{ch}\langle\sigma v\rangle)$ are total functions in Lean and return $0$ on zero denominators. Without strict positivity of $n$, $T$, $\langle\sigma v\rangle$, $E_\mathrm{ch}$, $\tau_E$ and $P_\mathrm{loss}$, several of these statements become false or empty rather than merely degenerate.
• Direction of the inequality. The self-heating hypothesis and the conclusion point the same way only because one multiplies by the positive quantity $\tau_E/(n\,E_\mathrm{ch}\langle\sigma v\rangle)$; the factor $12 = 4\cdot 3$ comes from the $\tfrac14$ of the 50-50 mixture and the $3$ of $W = 3nT$, and either one dropped leaves a statement that still compiles.
• Fractional powers. The inertial-confinement and tokamak milestones involve $T^{3/2}$, $n^{1/3}$, $P^{2/3}$; these are Real.rpow, whose rules require positive bases, which is why the positivity hypotheses appear again there.

Formalization scope

The model is a Lean structure LawsonCriterion.DTPlasma bundling $n$, $T$, $\langle\sigma v\rangle$, $E_\mathrm{ch}$, $\tau_E$, $P_\mathrm{loss}$, all of type ℝ, with a strict-positivity field for each and one defining equation, tauE = energyDensity n T / Ploss where energyDensity n T = 3 * n * T. The 50-50 reaction rate is DTPlasma.rate, the heating rate is DTPlasma.fusionHeating = rate * Ech, and DTPlasma.SelfHeating is the proposition fusionHeating ≥ Ploss. Conventions this commits to:

• temperature in energy units, so T is $k_\mathrm{B}T$; the numerical milestone additionally fixes keV for T and Ech, m³/s for sigmav, and so keV·s·m⁻³ for the triple product;
• only the 50-50 D-T mixture and the charged-product energy enter; bremsstrahlung, conduction and impurities are not modelled separately — they are whatever Ploss is;
• Real.rpow for the fractional exponents, Real.sqrt for the thermal speed.

The statements are not vacuous: the definition file also publishes a witness, LawsonCriterion.unitDTPlasma, so the structure is inhabited and every hypothesis set here is satisfiable. Conversely, no statement is trivially true — each is an inequality between quantities that genuinely vary with the plasma parameters.

Contributions welcome beyond the listed milestones: a version that separates radiation from conduction losses, the D-D and D-³He variants, and the statement that $T \mapsto T/\langle\sigma v\rangle$ attains a minimum for a realistic reactivity model — the step where the source passes from the inequality to its "absolute lower limit", which this mission does not formalize.

Selected references

• J. D. Lawson, Some Criteria for a Power Producing Thermonuclear Reactor, Proceedings of the Physical Society, Section B 70 (1957) 6–10. doi:10.1088/0370-1301/70/1/303
• J. Wesson, Tokamaks, Oxford Engineering Science Series 48, 3rd ed., Clarendon Press, 2004.
• H. Abu-Shawareb et al., Lawson Criterion for Ignition Exceeded in an Inertial Fusion Experiment, Physical Review Letters 129, 075001 (2022). doi:10.1103/PhysRevLett.129.075001
• Lawson criterion, Wikipedia, revision 1367242125 — the source text this mission formalizes. link

Motivation

Hubble's law — officially the Hubble–Lemaître law — is the observation that galaxies recede from us at a speed proportional to their distance, $v = H_0 D$. It is the first observational basis for the expansion of the universe and one of the standard pieces of evidence cited for the Big Bang model. Georges Lemaître derived the proportionality from relativistic cosmology in 1927; Edwin Hubble published the observational relation in 1929, building on Vesto Slipher's redshifts and Henrietta Swan Leavitt's Cepheid distance scale. Alexander Friedmann had already shown in 1922 that the Einstein field equations admit expanding solutions, with an expansion rate governed by what is now called the scale factor.

Behind the astronomy sits a piece of elementary mathematics that is rarely written out in full: in a spatially homogeneous expansion, the linear velocity–distance relation is forced, it holds with the same constant for every observer, and the Hubble "constant" is in fact a function of time whose evolution is fixed by a single dimensionless parameter. This mission formalizes that kinematic core: the statements are about the scale factor and its derivatives, and involve no Einstein equations.

Setting

A scale factor is a function $a : \mathbb{R} \to \mathbb{R}$ of cosmic time $t$. A comoving point is labelled by a fixed coordinate $\mathbf{x} \in \mathbb{R}^3$ (with the Euclidean norm), and its proper position at time $t$ is

$$\mathbf{X}_{\mathbf{x}}(t) \;=\; a(t)\,\mathbf{x}.$$

The proper distance between the comoving points $\mathbf{x}$ and $\mathbf{y}$ is

$$D_{\mathbf{x},\mathbf{y}}(t) \;=\; \lVert a(t)\mathbf{x} - a(t)\mathbf{y}\rVert .$$

The Hubble parameter and the dimensionless deceleration parameter are

$$H(t) \;=\; \frac{\dot a(t)}{a(t)},\qquad q(t) \;=\; -\,\frac{\ddot a(t)\,a(t)}{\dot a(t)^{2}} .$$

$H_0$ denotes the present-day value of $H$; the name "Hubble constant" refers to the fact that $H$ is constant in space at a fixed time, not in time.

Target

The goal theorem is the idealized Hubble law, stated in the source as a theorem of Euclidean geometry: any two points moving away from the origin, each along a straight line and with speed proportional to its distance from the origin, move away from each other with a speed proportional to their distance apart. Formally, for $H \ge 0$, a time $t$ and curves $p, q : \mathbb{R} \to \mathbb{R}^3$ with

$$p'(t) = H\,p(t), \qquad q'(t) = H\,q(t),$$

the separation satisfies

$$\frac{d}{ds}\Big|_{s=t}\big(p(s) - q(s)\big) \;=\; H\,\big(p(t) - q(t)\big), \qquad \big\lVert H\,(p(t)-q(t))\big\rVert \;=\; H\,\lVert p(t)-q(t)\rVert .$$

The relative velocity is parallel to the separation vector and its magnitude is $H$ times the separation, with the same $H$ for every pair — so no comoving observer occupies a distinguished centre of the expansion.

The milestones supply the cosmological content that surrounds this geometric fact:

1. proper distances scale as $D(t) = \big(a(t)/a(t_0)\big) D(t_0)$;
2. a comoving point has velocity $H(t)$ times its proper position vector;
3. Hubble's law itself, $\dot D(t) = H(t)\,D(t)$;
4. the evolution law $\dot H = -(1+q)H^{2}$;
5. the zero-deceleration case: if $q \equiv 0$ then $H(t) = 1/t$, with $t$ the time since the Big Bang, so the Hubble time $1/H$ is exactly the age;
6. a constant Hubble parameter forces exponential growth $a(t) = a(t_0)e^{H_0(t-t_0)}$;
7. the small-redshift limit: with $1 + z = a(t_0)/a(t_\mathrm{e})$, the ratio $z/(t_0 - t_\mathrm{e})$ tends to $H(t_0)$ as $t_\mathrm{e} \to t_0$, which is the $z \approx H_0 D/c$ form of the law used observationally.

Significance

The result itself is elementary but load-bearing: it is what licenses reading a linear redshift–distance diagram as evidence for uniform expansion rather than for a privileged position in space, and items 4–6 are the statements through which cosmological observations (the sign of $q$, the approach of $q$ to $-1$ in $\Lambda$CDM) are turned into claims about the past and future behaviour of $H$ and $a$.

Formalizing it produces a small, reusable Lean layer for expansion kinematics: the scale factor, the Hubble and deceleration parameters, proper position and proper distance, with the differentiation lemmas that connect them. The platform already carries Friedmann-equation missions that fix the dynamics of $a$; this mission is the kinematic complement, and its Hubble parameter is the same function $\dot a/a$ that those developments use. Nothing here is an open research problem: every statement is a known textbook fact, and the work is the formalization.

Difficulty

The mathematical content is a few lines of calculus, so the difficulty is entirely in the encoding. Three places are easy to get wrong. First, proper distance is defined through a norm, so the identity $\lVert a(t)v\rVert = a(t)\lVert v\rVert$ needs positivity of $a$, and differentiating it needs positivity on a neighbourhood, not just at the point. Second, $q$ is defined by a quotient with $\dot a^{2}$ in the denominator: in Lean division by zero returns zero, so a statement about $q$ that forgets $\dot a(t) \ne 0$ silently changes meaning. Third, milestone 5 propagates a hypothesis stated on $(0,\infty)$ down to the endpoint $t=0$, where the Big Bang condition $a(0)=0$ lives; the continuity argument at the endpoint is the only step with any technical content.

Formalization scope

Time is $\mathbb{R}$ and space is EuclideanSpace ℝ (Fin 3); derivatives are Mathlib's deriv / HasDerivAt, so "velocity" is always a derivative at a point rather than a difference quotient. Smoothness is assumed exactly where it is used: differentiability at a single time for the first-order statements, ContDiff ℝ 2 for the statements involving $\ddot a$. Positivity of the scale factor is stated explicitly wherever it is needed, as is $\dot a(t) \ne 0$ in the statements mentioning $q$.

Degenerate readings are excluded: the goal's hypotheses are satisfiable (any pair of comoving points in an expanding universe satisfies them, as milestone 2 shows), and the milestones are non-vacuous for concrete scale factors such as $a(t) = t$ and $a(t) = e^{H_0 t}$. The goal theorem's second clause is a norm identity that is true for every $H \ge 0$; it carries the "speed proportional to distance" half of the source's statement, while the first clause carries the "moving away from each other along the separation" half.

The definition layer is a single self-contained file (scale factor derived quantities, proper position, proper distance); it is reusable by any mission about expansion kinematics. Contributions of the milestone proofs, and of variants such as the redshift relation $1+z = a(t_0)/a(t_\mathrm{e})$ derived from null geodesics rather than assumed, are welcome.

Selected references

• Wikipedia, "Hubble's law" (Hubble–Lemaître law), https://en.wikipedia.org/wiki/Hubble%27s_law — the source text for this mission, in particular the sections "Recessional velocity", "Time-dependence of Hubble parameter", "Idealized Hubble's law" and "Ultimate fate and age of the universe".
• E. Hubble, "A relation between distance and radial velocity among extra-galactic nebulae", PNAS 15 (1929) 168–173, https://doi.org/10.1073/pnas.15.3.168.
• G. Lemaître, "Un univers homogène de masse constante et de rayon croissant rendant compte de la vitesse radiale des nébuleuses extra-galactiques", Annales de la Société Scientifique de Bruxelles A47 (1927) 49–59.
• A. Friedmann, "Über die Krümmung des Raumes", Zeitschrift für Physik 10 (1922) 377–386, https://doi.org/10.1007/BF01332580.

Motivation

Perturbative quantum field theory computes correlation functions of a field by expanding around a Gaussian (free) theory. Every term of that expansion is a Feynman diagram, and the rule that turns a diagram into a number is Wick's theorem: the expectation of a product of Gaussian field modes is the sum, over all ways of pairing the modes up, of the product of the two-point functions of the pairs. The same identity is known in probability and statistics as the Isserlis theorem (L. Isserlis, 1918) and is the standard tool for computing moments of Gaussian vectors; in random-matrix theory the counting of pairings it produces is the origin of the Catalan-number asymptotics of Wigner's semicircle law.

The uploaded source is the Wikipedia article Feynman diagram, which states Wick's theorem for the free scalar field and then, in the section Higher Gaussian moments — completing Wick's theorem, verifies the one-variable case by direct Gaussian integration. This mission formalizes that content: the combinatorics of pairings, the one-dimensional Gaussian moment formulas, and the multivariate identity itself.

Setting

Fix $d, n \in \mathbb{N}$ and work on $\mathbb{R}^d$ with coordinates $x_1,\dots,x_d$. Let $\mu$ be a centered Gaussian measure on $\mathbb{R}^d$: a Gaussian probability measure all of whose coordinate means vanish, $\int x_i \, d\mu(x) = 0$ for every $i$. Its covariance (in the physics reading, the propagator) is

$$G_{ij} \;=\; \int x_i x_j \, d\mu(x).$$

A pairing of the labels $\{0,1,\dots,2n-1\}$ is a partition of these $2n$ labels into $n$ unordered pairs; equivalently, a permutation $\sigma$ of the labels with $\sigma\circ\sigma = \mathrm{id}$ and $\sigma(i)\neq i$ for all $i$ (a fixed-point-free involution). The set of pairings is written $P_n$. For a weight $W_{ab}$ indexed by labels, the Wick sum is

$$\mathrm{Wick}(W) \;=\; \sum_{\sigma \in P_n} \ \prod_{\substack{i \,:\, i < \sigma(i)}} W_{i\,\sigma(i)},$$

the inner product ranging over the $n$ pairs of $\sigma$, each counted once through its smaller element.

In the article's field-theory notation the labels are momenta $k_1,\dots,k_{2n}$, the coordinates are the field modes $\phi(k_j)$, and the two-point function carries the momentum-conserving delta function, $\langle \phi(k)\phi(k')\rangle = \delta(k-k')/k^2$. This mission works with the finite-dimensional Gaussian vector rather than the field, so the delta functions are absorbed into the covariance matrix $G$.

Formalization targets

Goal — Wick's theorem (Isserlis' theorem)

For a centered Gaussian measure $\mu$ on $\mathbb{R}^d$ and any labels $k_1,\dots,k_{2n} \in \{1,\dots,d\}$,

$$\int \prod_{j=1}^{2n} x_{k_j} \, d\mu(x) \;=\; \sum_{\sigma\in P_n} \ \prod_{i < \sigma(i)} \left( \int x_{k_i} x_{k_{\sigma(i)}} \, d\mu(x) \right).$$

No hypothesis is imposed on the covariance: it may be singular and the labels $k_j$ may repeat, which is exactly the situation the article's "completing Wick's theorem" section addresses.

Supporting targets (milestones)

1. $\int_{\mathbb{R}} e^{-a x^{2}/2}\,dx = \sqrt{2\pi/a}$ for $a>0$.
2. $\int_{\mathbb{R}} x^{2n} e^{-a x^{2}/2}\,dx = \dfrac{(2n-1)!!}{a^{n}}\sqrt{2\pi/a}$ for $a>0$.
3. $\int x^{2n}\,d\mathcal{N}(0,v) = (2n-1)!!\, v^{n}$ for a real Gaussian law of variance $v \ge 0$.
4. $\#P_n = (2n-1)!!$.
5. Correlation functions of odd order vanish: $\int \prod_{j=1}^{2n+1} x_{k_j}\,d\mu = 0$.
6. The four-point function: $\langle x_{k_1}x_{k_2}x_{k_3}x_{k_4}\rangle$ equals the sum of the three products $G_{k_1k_2}G_{k_3k_4} + G_{k_1k_3}G_{k_2k_4} + G_{k_1k_4}G_{k_2k_3}$.

Targets 1–3 are the article's displayed Gaussian integrals, target 4 is its pairing count, targets 5–6 are the two explicit consequences it records for the field correlators.

Significance

Wick's theorem is the computational content of every Feynman-diagram expansion: once it is available, a perturbative term is a finite sum over diagrams, and the symmetry factors of diagrams are bookkeeping on the pairing set $P_n$. On the probabilistic side it gives all moments of a Gaussian vector in closed form, which is the entry point to Gaussian chaos expansions, Wiener–Itô integrals, and moment methods for random matrices.

Mathlib (revision 0df444a) has real Gaussian measures gaussianReal, the general class IsGaussian of Gaussian measures on a topological vector space, the Gaussian integral $\int e^{-bx^2} = \sqrt{\pi/b}$, and the double factorial Nat.doubleFactorial, but no higher-moment formula for Gaussian measures and no Isserlis/Wick statement. The mission therefore produces new library-level content, not a re-derivation of existing formal results; the result itself has been classical since 1918 (Isserlis) and 1950 (Wick).

Difficulty

The obvious route — expand the characteristic function $\exp(-\tfrac12 t^{\mathsf T} G t)$ and differentiate $2n$ times at $t=0$ — requires differentiating under an integral sign $2n$ times and identifying the resulting combinatorial sum with a sum over pairings; both steps are where the formal work lies. Integrability is not automatic from the statement and has to be established (Gaussian measures have moments of all orders, but the product $\prod_j x_{k_j}$ must be shown integrable before any manipulation). The naive attempt to reduce to the independent case by diagonalizing $G$ meets a second difficulty: the change of variables must be tracked through the pairing sum, and $G$ may be singular, so no invertible whitening transform exists in general. The one-variable case (milestone 3) is not a special case to be waved through either: it is the statement the article singles out, because a naive "each mode pairs with a distinct partner" argument fails when all labels coincide.

Formalization scope

The ambient space is EuclideanSpace ℝ (Fin d); measures are Mathlib Measures and Gaussianity is the Mathlib class IsGaussian, which is defined by every continuous linear functional pushing forward to a real Gaussian law. Centering is stated as an explicit hypothesis on the coordinate means, so the measure is not assumed standard and the covariance is unconstrained (in particular degenerate covariances, and repeated labels $k_i = k_j$, are included). Integrals are Bochner integrals, which return $0$ for non-integrable functions; the statements are nonetheless non-vacuous because Gaussian measures integrate all polynomials.

Pairings are formalized as fixed-point-free involutions of Fin (2 * n) and the pair product ranges over $\{i : i < \sigma(i)\}$, so each pair contributes once. The case $n = 0$ is included: the empty product is $1$, the unique pairing of the empty label set is the identity, and both sides of the goal equal $1$. The double factorial is Mathlib's Nat.doubleFactorial, evaluated at 2 * n - 1 in truncated natural subtraction, so the $n = 0$ value is $0!! = 1$.

Contributions welcome: the Gaussian moment lemmas (milestones 1–3) as standalone Mathlib-style results, the pairing count (milestone 4) as pure combinatorics independent of the analysis, and any reduction of the goal to the independent-coordinate case.

Selected references

• L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12 (1918), 134–139. DOI: 10.1093/biomet/12.1-2.134
• G. C. Wick, The evaluation of the collision matrix, Physical Review 80 (1950), 268–272. DOI: 10.1103/PhysRev.80.268
• Feynman diagram, Wikipedia. https://en.wikipedia.org/wiki/Feynman_diagram

Motivation

Since the 2019 revision of the SI, seven constants of nature have fixed, exact numerical values: the caesium hyperfine frequency $\Delta\nu_{\mathrm{Cs}}$, the speed of light $c$, the Planck constant $h$, the elementary charge $e$, the Boltzmann constant $k$, the Avogadro constant $N_A$ and the luminous efficacy $K_{\mathrm{cd}}$. Every other constant is either measured, and then carries an uncertainty, or is a closed-form expression in the seven, and is then known exactly. The CODATA 2022 adjustment (Mohr, Newell, Taylor and Tiesinga, Rev. Mod. Phys. 97, 025002, 2025) is the authoritative statement of which constants fall on which side of that line, and of the statistical procedure that produces the recommended values of the measured ones.

The exactly known side of the line is pure mathematics: the tabulated value of the Stefan-Boltzmann constant, of the radiation constants, of the molar gas constant and of the Faraday constant are theorems about $\pi$, an integral, and rational arithmetic - not measurements. The measured side rests on one statistical object, the weighted linear least-squares fit of $N=133$ input data to $M=79$ adjusted constants, together with the diagnostics ($\chi^2$, the Birge ratio, normalized residuals, expansion factors) the task group uses to decide that the fit is acceptable. This mission formalizes both.

Setting

Write $h$, $c$, $k$, $e$, $N_A$ for the numerical values of the defining constants in coherent SI units, and $\hbar = h/2\pi$. The spectral radiance of a blackbody at thermodynamic temperature $T$, per unit frequency, is Planck's function

$$B_\nu(T,\nu) \;=\; \frac{2h\nu^3}{c^2}\,\frac{1}{e^{h\nu/kT}-1},$$

and per unit wavelength

$$B_\lambda(T,\lambda) \;=\; \frac{2hc^2}{\lambda^5}\,\frac{1}{e^{hc/(\lambda k T)}-1}.$$

The derived constants named in Tables XXXII and XXXIII of the paper are $\sigma = (\pi^2/60)k^4/\hbar^3c^2$ (Stefan-Boltzmann), $c_1 = 2\pi hc^2$ and $c_2 = hc/k$ (radiation constants), $R = N_Ak$ (molar gas), $F = N_Ae$ (Faraday), $K_J = 2e/h$ (Josephson) and $R_K = h/e^2$ (von Klitzing).

For the adjustment, let $A \in \mathbb{R}^{N\times M}$ be the design matrix of the linearized observational equations, $z \in \mathbb{R}^N$ the input data and $W \in \mathbb{R}^{N\times N}$ the weight matrix - the inverse of the covariance matrix of the data, symmetric and positive definite. The fit minimizes

$$\chi^2(x) \;=\; (z - Ax)^{\mathsf T} W (z - Ax), \qquad x \in \mathbb{R}^M,$$

with $\nu = N - M$ degrees of freedom, Birge ratio $R_B = (\chi^2/\nu)^{1/2}$ and normalized residuals $r_i = (X_i - \langle X_i\rangle)/u(X_i)$.

Formalization targets

Goal

$$\int_0^{\infty} \pi\,B_\nu(T,\nu)\,\mathrm{d}\nu \;=\; \sigma T^4 \qquad (T>0), \qquad \sigma = \frac{\pi^2}{60}\frac{k^4}{\hbar^3c^2}.$$

The goal fixes no digits: it asserts that the constant appearing in the tabulated closed form is exactly the one produced by integrating Planck's law over the spectrum and over a Lambertian hemisphere. The numerical enclosure of $\sigma$ is a separate, weaker milestone, so that the goal survives any change of tabulated digits.

Supporting targets

$$\int_0^\infty \frac{x^3}{e^x-1}\,\mathrm{d}x = \frac{\pi^4}{15}, \qquad \sigma = \frac{2\pi^5k^4}{15h^3c^2}, \qquad R = N_Ak, \qquad F = N_Ae,$$

together with the numerical enclosures of $\sigma$, of Wien's displacement constants $b = c_2/x_5$ and $b' = x_3k/h$ (where $x_5$, $x_3$ solve $x = 5(1-e^{-x})$ and $x = 3(1-e^{-x})$), and the identity $K_J^2R_K = 4/h$.

On the statistical side:

$$\chi^2(x) \;=\; \chi^2(\hat x) + (x-\hat x)^{\mathsf T}A^{\mathsf T}WA\,(x-\hat x) \quad\text{whenever}\quad A^{\mathsf T}WA\,\hat x = A^{\mathsf T}Wz,$$

the equivalence of minimality with the normal equations, the closed form $\hat x = (A^{\mathsf T}WA)^{-1}A^{\mathsf T}Wz$ when $A^{\mathsf T}WA$ is invertible, and the behaviour of $\chi^2$, $R_B$ and $r_i$ under an expansion factor $f$ applied to the uncertainties.

Significance

The exact-constant statements are what makes the tabulated values checkable rather than authoritative: a reader who accepts the SI definitions can, in principle, re-derive $R = 8.314\,462\,618\,153\,24\ \mathrm{J\,mol^{-1}K^{-1}}$ and $F = 96\,485.332\,123\,310\,0184\ \mathrm{C\,mol^{-1}}$ by arithmetic, and $\sigma = 5.670\,374\,419\ldots\times10^{-8}\ \mathrm{W\,m^{-2}K^{-4}}$ from Planck's law and $\zeta(4)$. Formalizing them turns "in principle" into a machine-checked derivation from the seven fixed numbers.

The least-squares statements make precise what the adjustment is, independently of the 133 data of this particular round: that the recommended values are the unique minimizer of a quadratic form, that the normal equations characterize it, and that multiplying a group of uncertainties by an expansion factor $f$ - the device used in 2022 with $f = 1.7$, $2.5$ and $3.9$ - rescales $\chi^2$ by $f^{-2}$, the Birge ratio by $f^{-1}$ and the residuals by $f^{-1}$, without moving the fitted values. None of these statements is new mathematics; none of them, as far as the catalog shows, is currently available as a machine-checked statement about the CODATA quantities.

Difficulty

Two hard points. First, $\int_0^\infty x^3/(e^x-1)\,\mathrm{d}x = \pi^4/15$: the obvious route expands $1/(e^x-1)$ as a geometric series and integrates term by term, which needs a dominated convergence or monotone convergence argument plus the value $\zeta(4)=\pi^4/90$; interchanging the sum and the integral is the step that must be justified, not assumed. The goal then needs this together with a change of variables $x = h\nu/kT$ on $(0,\infty)$ and an integrability argument for the original integrand.

Second, the numerical enclosures. $5.670\,374\,419\times10^{-8} < \sigma$ requires certified rational bounds on $\pi^5$; the Wien constants require certified bounds on a transcendental root, obtained from interval evaluation of $e^{-x}$ at rational points plus monotonicity of $x - n(1-e^{-x})$. Floating-point evaluation proves nothing here.

The least-squares milestones are routine linear algebra, with one subtlety: the decomposition identity needs symmetry of $W$, and the characterization of minimizers needs positive definiteness, so both hypotheses are carried explicitly.

Formalization scope

All physical quantities are plain real numbers: each constant is the numerical value of the quantity in the coherent SI unit named in its docstring, and the code carries no units. The defining constants are given by the exact decimal literals of Table XXXII, so they are exact rationals; $\hbar$ is defined as $h/2\pi$ and is therefore irrational.

Planck's function is a total function of two real arguments. Outside the physical regime it returns junk rather than failing - at $T = 0$ the exponent is $0$, the denominator $e^0 - 1 = 0$, and Lean's division returns $0$ - so every statement about it carries $0 < T$ and a positivity hypothesis on the spectral variable. The goal's integral is the Bochner integral over $(0,\infty)$ with respect to Lebesgue measure; it is not trivially true by non-integrability, since the integrand is integrable for $T>0$.

The adjustment is formalized over $\mathrm{Fin}\,N$ and $\mathrm{Fin}\,M$ with an arbitrary design matrix $A$ and an arbitrary weight matrix $W$, hypotheses on $W$ (Hermitian, positive definite) stated where they are used rather than baked into the definition; $\nu = N-M$ is an integer, not a truncated natural number.

Contributions welcome: the $\zeta(4)$ integral and the interval-arithmetic enclosures are reusable well beyond this mission, as are the least-squares statements.

Selected references

• P. J. Mohr, D. B. Newell, B. N. Taylor, E. Tiesinga, CODATA recommended values of the fundamental physical constants: 2022, Rev. Mod. Phys. 97, 025002 (2025). https://doi.org/10.1103/RevModPhys.97.025002
• Bureau International des Poids et Mesures, The International System of Units (SI), 9th edition (2019). https://www.bipm.org/en/publications/si-brochure

Motivation

In the Standard Model the scalar sector consists of a single complex $SU(2)_L$ doublet. The general Two-Higgs-Doublet Model (THDM) replaces it by two complex doublets $\varphi_1,\varphi_2$ of the same weak hypercharge $y=1/2$. This is the minimal extension of the scalar sector that is still renormalisable and gauge invariant, and it is forced on any supersymmetric completion: the Minimal Supersymmetric Standard Model has exactly two Higgs doublets. Before any phenomenology can be done with such a model, two questions have to be answered for the given parameter point: is the scalar potential stable, i.e. bounded from below, and does its global minimum break $SU(2)_L\times U(1)_Y$ down to the electromagnetic $U(1)_{\text{em}}$?

The general THDM potential has $14$ real parameters, and answering these questions directly in field space — eight real scalar degrees of freedom, of which three are gauge — is unwieldy. Maniatis, von Manteuffel, Nachtmann and Nagel (2006) proposed a reformulation in terms of gauge-invariant bilinears, in which the gauge orbits of the Higgs fields are parametrised by a Minkowski-type four-vector confined to the closed forward light cone, and the potential becomes a quadratic polynomial on that cone. In these variables the stability question reduces to a one-variable problem: the sign of an explicit rational function $f(u)$ on a finite set $I$ of at most ten real numbers. This mission formalizes that analysis: the gauge-orbit parametrisation (their Theorem 4), the classification of the stationary points of the potential (their Theorem 2), and the stability criterion itself (their Theorem 1).

Setting

Write the two doublets as rows of a $2\times 2$ complex matrix,

$$\phi=\begin{pmatrix}\varphi_1^+&\varphi_1^0\\ \varphi_2^+&\varphi_2^0\end{pmatrix},$$

and form the hermitian matrix of gauge-invariant scalar products $K^{ij}=\varphi_j^\dagger\varphi_i$, i.e. $K=\phi\,\phi^\dagger$. Decomposing $K$ in the Pauli basis gives four real functions

$$K_0=\operatorname{tr}K,\qquad K_a=\operatorname{tr}\!\left(K\sigma^a\right),\quad a=1,2,3 .$$

Positive semi-definiteness of $K$ is equivalent to $K_0\ge 0$ and $K_0^2-|K|^2\ge 0$: the four-vector $(K_0,K)$ lies on or inside the forward light cone. A gauge transformation acts as $\phi\mapsto \phi\,U^{\mathsf T}$ with $U\in U(2)$, and leaves $K$ invariant.

The most general gauge-invariant renormalisable potential is

$$V=\underbrace{\xi_0K_0+\xi^{\mathsf T}K}_{V_2}+\underbrace{\eta_{00}K_0^2+2K_0\,\eta^{\mathsf T}K+K^{\mathsf T}EK}_{V_4},$$

with real parameters $\xi_0,\eta_{00}\in\mathbb R$, $\xi,\eta\in\mathbb R^3$ and a real symmetric $3\times3$ matrix $E$. For $K_0>0$ one sets $k=K/K_0$, so that $|k|\le 1$, and

$$J_2(k)=\xi_0+\xi^{\mathsf T}k,\qquad J_4(k)=\eta_{00}+2\eta^{\mathsf T}k+k^{\mathsf T}Ek,\qquad V=K_0J_2(k)+K_0^2J_4(k).$$

Stationary points of $J_4$ on the ball $|k|\le1$ are governed by the functions

$$f(u)=u+\eta_{00}-\eta^{\mathsf T}(E-u)^{-1}\eta,\qquad f'(u)=1-\eta^{\mathsf T}(E-u)^{-2}\eta,\qquad g(u)=\xi_0-\xi^{\mathsf T}(E-u)^{-1}\eta,$$

where $u$ is a Lagrange multiplier for the constraint $|k|=1$. The finite set $I$ collects: every regular $u$ with $f'(u)=0$; the point $u=0$ when $f'(0)>0$; and every eigenvalue $\mu$ of $E$ at which $f$ stays finite and $f'(\mu)\ge0$. It has at most ten elements, and $\{f(u):u\in I\}$ is exactly the set of stationary values of $J_4$.

For the stationary points of the full potential one uses four-vector notation $\tilde K=(K_0,K)$, $\tilde\xi=(\xi_0,\xi)$, $\tilde E=\begin{pmatrix}\eta_{00}&\eta^{\mathsf T}\\ \eta&E\end{pmatrix}$ and the metric $\tilde g=\mathrm{diag}(1,-1,-1,-1)$, so that $V=\tilde K^{\mathsf T}\tilde\xi+\tilde K^{\mathsf T}\tilde E\tilde K$ on the domain $\tilde K^{\mathsf T}\tilde g\tilde K\ge0$, $K_0\ge0$, with $\tilde f(u)=-\tfrac14\tilde\xi^{\mathsf T}(\tilde E-u\tilde g)^{-1}\tilde\xi$.

Formalization targets

Goal — Theorem 1 (stability criterion)

For $V_4\equiv0$ the potential is stable for $\xi_0>|\xi|$, marginal for $\xi_0=|\xi|$ and unstable for $\xi_0<|\xi|$. For $V_4\not\equiv0$,

$$f(u_i)>0\ \ \forall u_i\in I\ \Longrightarrow\ J_4>0 \text{ on } |k|\le1 \quad\text{(stability in the strong sense)},$$ $$\exists u_i\in I:\ f(u_i)<0\ \Longrightarrow\ V \text{ unbounded below},$$

and if $f\ge0$ on $I$ with equality somewhere, the sign of $g(u_i)$ — replaced by $g(u_i)-|\xi_\perp(u_i)|\sqrt{f'(u_i)}$ when $u_i$ is an eigenvalue of $E$ — decides between stability in the weak sense and instability.

Milestones

Theorem 4 (gauge orbits); the four stability cases (a), (b.2), (b.3), (b.4) of Section 4 including the criterion $J_2^2\le CJ_4$ for the marginal case; equation (4.39) identifying the stationary values of $J_4$ with $\{f(u):u\in I\}$; equations (4.42)–(4.44) giving $J_2$ at those stationary points; and Theorem 2, the classification of the stationary points of $V$.

Significance

The criterion is a decision procedure: given the $14$ parameters of a THDM, stability is settled by evaluating one rational function at the roots of another, without any search in field space. The authors use it to re-derive the known stability conditions for the MSSM potential and to settle the stability and symmetry-breaking properties of the THDM potential of Gunion et al., for which $\lambda_1+\lambda_3>0$, $\lambda_2+\lambda_3>0$ and $\lambda_4,\kappa>-2\lambda_3-2\sqrt{(\lambda_1+\lambda_3)(\lambda_2+\lambda_3)}$ come out as the strong-stability conditions. Theorem 4 is what makes the whole approach legitimate: it says that nothing is lost in passing from fields to the invariants $(K_0,K)$, because the fibres of that map are exactly the gauge orbits.

The results are established in the published literature; what this mission adds is machine-checked proofs. The statements are not present in Mathlib in any form, and the note added in version 3 of the paper — a condition for the marginal case that was missing in the original version — is a concrete reminder that the case analysis here is easy to get subtly wrong.

Difficulty

The obvious route to stability is to minimise $V$ directly; it fails because the domain is a cone with a boundary, and the minimisation over the boundary $|k|=1$ introduces a Lagrange multiplier whose admissible values are the roots of $f'$, including the degenerate "exceptional" solutions where $E-u$ is singular. Those exceptional solutions are not a technicality: they are where the eigenvalue clauses of $I$, the $\xi_\perp$ correction in (4.43), and the junk-value behaviour of matrix inverses all live. The marginal case ($J_4$ and $J_2$ vanishing simultaneously somewhere) is not decided by the signs alone and needs the quantitative bound $J_2^2\le CJ_4$.

Formalization scope

Vectors in $\mathbb R^3$ are plain functions Fin 3 → ℝ with an explicitly defined dot product; $E$ is a Matrix (Fin 3) (Fin 3) ℝ and its symmetry is carried as a hypothesis. Four-vectors are indexed by Unit ⊕ Fin 3 so that $\tilde E$ and $\tilde g$ are block matrices, with the first component being $K_0$. Higgs configurations are $2\times2$ complex matrices and $K=\phi\phi^\dagger$; a gauge transformation is $\phi\mapsto\phi U^{\mathsf T}$ with $U^\dagger U=1$.

Stability is formalized as the honest statement that $V(K_0,k)$ is bounded from below on the physical domain $K_0\ge0$, $|k|\le1$ — not as any of the sign conditions that the theorem derives — so none of the implications is true by definition. Matrix inversion in Lean returns the zero matrix at a singular argument; every occurrence of $(E-u)^{-1}$ is therefore guarded by a regularity hypothesis, and the values of $f,f',g$ at an eigenvalue of $E$ are defined as limits, with the existence of those limits part of the membership condition for $I$. The projection $\xi_\perp(\mu)$ is characterised by its defining property (it lies in the eigenspace and $\xi-\xi_\perp$ is orthogonal to it) rather than by a choice of eigenbasis.

A complete development needs linear algebra over $\mathbb R$ (resolvents, symmetric matrices, eigenspaces), $U(2)$ and the spectral decomposition of positive semi-definite $2\times2$ complex matrices for Theorem 4, and elementary real analysis (compactness of the ball, limits of rational functions) for Section 4. The gauge-orbit statement and the light-cone parametrisation are reusable for any multi-doublet scalar sector; contributions of the $n$-doublet generalisation (Appendix B, Theorem 5) are welcome as follow-ups.

Selected references

• M. Maniatis, A. von Manteuffel, O. Nachtmann, F. Nagel, Stability and symmetry breaking in the general two-Higgs-doublet model, Eur. Phys. J. C 48 (2006) 805–823. https://arxiv.org/abs/hep-ph/0605184
• J. F. Gunion, H. E. Haber, G. L. Kane, S. Dawson, The Higgs Hunter's Guide, Addison-Wesley, 1990.

Motivation

Quantum field theory begins, mathematically, with a question that has a completely precise answer: what is the state space of a single relativistic particle? Non-relativistic quantum mechanics answers $L^2(\mathbb{R}^3)$ and moves on. Relativity does not allow that answer, because the state space must carry an action of the symmetry group of Minkowski spacetime — the Poincaré group — and the choice of Hilbert space is dictated by which such action one wants. The construction that results is the foundation on which Fock space, creation and annihilation operators, free fields and eventually interacting theories are built, and it is where the objects that reappear everywhere in the subject are introduced: the mass shell, the Lorentz-invariant measure on it, and the double cover $SL(2,\mathbb{C}) \to SO^{\uparrow}(1,3)$ that is responsible for spin.

This mission formalizes that construction as it is presented in S. Chatterjee's Lectures on Quantum Field Theory (Stanford, 2018–19), Lectures 9–11 and Lecture 25: the one-particle space of a massive scalar boson, the one-particle space of an electron, and the statement that both carry inner products invariant under the Poincaré action.

Setting

Minkowski spacetime is $\mathbb{R}^{1,3}$ with the bilinear form

$$(x, y) \;=\; x^0 y^0 - \big(x^1y^1 + x^2y^2 + x^3y^3\big), \qquad x^2 := (x,x).$$

A Lorentz transformation is a linear map $L$ with $(Lx, Ly) = (x,y)$; the restricted Lorentz group $SO^{\uparrow}(1,3)$ consists of those with $\det L = 1$ and $L^0{}_0 > 0$. The Poincaré group is $\mathcal{P} = \mathbb{R}^{1,3} \rtimes SO^{\uparrow}(1,3)$ with the group law $(a,A)(b,B) = (a + Ab,\, AB)$.

For a mass $m > 0$, the four-momentum of a particle satisfies $p^2 = m^2$ and $p^0 \ge 0$, so it lies on the mass shell

$$X_m \;=\; \{\, p \in \mathbb{R}^{1,3} : p^2 = m^2,\ p^0 \ge 0 \,\},$$

a three-dimensional manifold parametrised by the spatial momentum $q \in \mathbb{R}^3$ through $q \mapsto (\omega_q, q)$ with $\omega_q = \sqrt{m^2 + |q|^2}$. On $X_m$ there is, up to a multiplicative constant, exactly one measure invariant under $SO^{\uparrow}(1,3)$; with the normalisation used in the lectures it is the measure $\lambda_m$ determined by

$$\int_{X_m} f \, d\lambda_m \;=\; \int_{\mathbb{R}^3} \frac{d^3q}{(2\pi)^3\, 2\omega_q}\, f(\omega_q, q).$$

The state space of a massive scalar boson is $\mathcal{H} = L^2(X_m, d\lambda_m)$, acted on by $(U(a,L)\psi)(p) = e^{i(a,p)}\psi(L^{-1}p)$.

For an electron the wave function takes values in $\mathbb{C}^2$ and the group acts through the double cover. To each four-vector $x$ one attaches the Hermitian matrix

$$M(x) = \begin{pmatrix} x^0+x^3 & x^1 - ix^2\\ x^1+ix^2 & x^0-x^3\end{pmatrix}, \qquad \det M(x) = (x,x),$$

and for $A \in SL(2,\mathbb{C})$ the transformation $\kappa(A)$ of $\mathbb{R}^{1,3}$ is defined by $M(\kappa(A)x) = A M(x) A^{\dagger}$; the map $\kappa$ is a surjective two-to-one homomorphism onto $SO^{\uparrow}(1,3)$. Writing $p^* = (m,0,0,0)$, each $p \in X_m$ is reached from $p^*$ by a unique positive-definite $V_p \in SL(2,\mathbb{C})$, the pure boost, and the electron inner product is the $V_p^{-2}$-weighted one,

$$(\psi, \varphi) \;=\; \int_{X_m} d\lambda_m(p)\; \psi(p)^{\dagger} V_p^{-2} \varphi(p),$$

with the group acting by $(U(a,A)\psi)(p) = e^{i(a,p)} A\, \psi(\kappa(A)^{-1}p)$.

Formalization targets

Goal — both one-particle inner products are Poincaré invariant

For $m > 0$, $a \in \mathbb{R}^{1,3}$, $A \in SL(2,\mathbb{C})$ and $L = \kappa(A)$:

$$\int_{X_m} \overline{(U(a,L)\psi)}\,(U(a,L)\varphi)\, d\lambda_m \;=\; \int_{X_m} \overline{\psi}\,\varphi\, d\lambda_m \qquad (\psi,\varphi \in L^2(X_m, d\lambda_m)),$$ $$\int_{X_m} (U(a,A)\psi)^{\dagger}\,V_p^{-2}\,(U(a,A)\varphi)\, d\lambda_m \;=\; \int_{X_m} \psi^{\dagger}\,V_p^{-2}\,\varphi\, d\lambda_m$$

for $\psi, \varphi$ in the weighted $L^2$ space of $\mathbb{C}^2$-valued functions. The goal fixes no constants beyond the normalisation of $\lambda_m$, and it is the statement that the spaces defined in the mission really are the one-particle spaces of the theory: a Hilbert space together with a Poincaré action by isometries.

Supporting targets

The milestone list follows the lectures: the parametrisation of $X_m$; invariance of $X_m$ under $SO^{\uparrow}(1,3)$; the integration formula for $\lambda_m$ (eq. (10.1)); invariance of $\lambda_m$; uniqueness of the invariant measure up to a constant; the composition law and unitarity of the scalar representation; $\det M(x) = (x,x)$ and bijectivity of $M$ onto Hermitian matrices; $\kappa$ as a multiplicative map into $SO^{\uparrow}(1,3)$; surjectivity of $\kappa$ with fibres $\{\pm A\}$; existence and uniqueness of the pure boost $V_p$; Lemma 25.1; and the identification of the weighted electron space with the plain $\mathbb{C}^2$-valued $L^2$ space via $\psi \mapsto V_\cdot^{-1}\psi$.

Significance

The objects here are used unchanged for the rest of a QFT course: the bosonic and fermionic Fock spaces are built on these one-particle spaces, and the free scalar and Dirac fields are operator-valued distributions written as integrals against $d\lambda_m$ on $X_m$. Formalizing them fixes, once and for all, the conventions later work must match — the normalisation of $\lambda_m$, the sign convention of the metric, which of the two elements $\pm A$ of $SL(2,\mathbb{C})$ acts, and the weight in the electron inner product.

What this mission adds beyond the lectures is a machine-checked development of material usually treated as routine but rarely written out: the uniqueness of the invariant measure, the covering map and its fibres, and the existence-uniqueness of the pure boost are all stated in the source either without proof or as exercises. Mathlib has the general theory of $L^2$ spaces, push-forward measures, Hermitian and positive-definite matrices, and $SL_2$, but it has no mass shell, no invariant measure on it, and no covering map onto the restricted Lorentz group; all of that is constructed here and is reusable by any later mission on free fields or Fock spaces.

Difficulty

The obvious route to the invariant measure — "restrict Lebesgue measure to the submanifold $X_m$" — does not work: the induced Riemannian volume of the hyperboloid in the Euclidean metric is not Lorentz invariant. The lectures instead take a scaling limit of Lebesgue measure on the invariant annuli $\{m^2 < p^2 < (m+\varepsilon)^2\}$; the formalization takes the resulting formula (10.1) as the definition and must then prove invariance, which amounts to a change-of-variables computation whose Jacobian is exactly $\omega_{q}$-dependent. Uniqueness is harder: it is a statement about invariant measures on a homogeneous space of a non-compact group, with no finiteness available.

On the spinor side, the central difficulty is that the weight $V_p^{-2}$ is unbounded on $X_m$, so the electron space is not the naive $\mathbb{C}^2$-valued $L^2(X_m, d\lambda_m)$ — the two spaces consist of different functions, and are related only through the measurable field of isomorphisms $\psi \mapsto V_p^{-1}\psi$. A formalization that silently uses the unweighted space would prove a different, and false, unitarity statement.

Formalization scope

Four-vectors are functions $\mathbb{R}^{1,3} = (\text{four-element index}) \to \mathbb{R}$, with the metric signature $(+,-,-,-)$; Lorentz transformations are real $4\times4$ matrices, and membership in $SO^{\uparrow}(1,3)$ is the predicate ($\det = 1$, $L^0{}_0 > 0$, form preserved). $\lambda_m$ is a Borel measure on all of $\mathbb{R}^{1,3}$ carried by $X_m$, defined as the push-forward of $(2\pi)^{-3}(2\omega_q)^{-1}\,d^3q$; the boson space is the library $L^2$ space of that measure. The pure boost is given by the closed formula $V_p = (M(p)/m + I)/\sqrt{2 + 2p^0/m}$ — the positive-definite square root of $M(p)/m$ — rather than by a choice function, and a milestone certifies that it is the unique positive-definite element of $SL(2,\mathbb{C})$ carrying $p^*$ to $p$. The electron space is the set of $\mathbb{C}^2$-valued measurable functions of finite weighted norm, with the weighted pairing given explicitly; the milestone identifying it with the plain $L^2$ space via the inverse boost is what supplies its Hilbert-space structure.

The unitarity statements are formalized as equalities of integrals over pairs of wave functions rather than as statements about abstract operators, so that no trivializing reading is available: in particular the electron clause is stated for the weighted pairing, which is not the standard $L^2$ inner product, and the hypotheses ($m > 0$, $\det A = 1$, $\psi,\varphi$ in the respective spaces) are satisfiable, so no clause holds vacuously. Total-function conventions of the library (inverse of a singular matrix is $0$; integral of a non-integrable function is $0$) are visible in the statements and are recorded in each item's read-back.

Contributions of any of the milestones are welcome; the measure-theoretic milestones (invariance and uniqueness) and the $SL(2,\mathbb{C})$ covering milestones are independent of each other and can be attacked in parallel.

Selected references

• S. Chatterjee, Lectures on Quantum Field Theory, Stanford University, 2018–19 (scribed lecture notes). https://souravchatterjee.su.domains/qft-lectures-combined.pdf
• E. P. Wigner, On unitary representations of the inhomogeneous Lorentz group, Annals of Mathematics 40 (1939), 149–204. https://doi.org/10.2307/1968551