Mathematical Physics

Motivation

The particle in a ring is the simplest quantum system in which a boundary condition of purely topological origin — single-valuedness of the wave function on a circle — forces the energy spectrum to be discrete. A free particle of mass $m$ confined to a circle of radius $R$ has no potential well and no classical turning points; nothing about the differential equation alone selects a discrete set of energies. Quantization arises solely from the requirement that the solution close up after one revolution. For that reason the model is the standard first illustration of angular-momentum quantization in quantum mechanics courses, and the azimuthal factor of the hydrogen-atom eigenfunctions is exactly the eigenfunction family derived here.

The model is also used quantitatively. In organic chemistry the free-electron model treats the $\pi$ electrons of an aromatic ring, such as benzene, as particles on a circular waveguide; filling all levels up to index $n$ takes $2\times(2n+1) = 4n+2$ electrons once electron spin is counted, which is the counting behind Hückel's rule for aromatic stability. In rotational spectroscopy the same spectrum approximates the rotational levels of a rigid rotor.

This mission formalizes the model as presented in the Wikipedia article Particle in a ring (revision 1318339663): the eigenfunctions, the eigenenergies, the normalization and orthogonality relations, the two-fold degeneracy of every level with $n \neq 0$, the count of $2n+1$ states up to level $n$, and — as the goal — the statement that the admissible energies are exactly the quantized values.

Setting

Write $\theta$ for the angular coordinate on the ring of radius $R$. A state is a function $\psi : \mathbb{R} \to \mathbb{C}$ of $\theta$ alone. Since the Laplacian on the ring is $\nabla^2 = R^{-2}\,\partial^2/\partial\theta^2$, the time-independent Schrödinger equation $-\frac{\hbar^2}{2m}\nabla^2\psi = E\psi$ becomes

$$-\frac{\hbar^{2}}{2mR^{2}}\,\psi''(\theta) \;=\; E\,\psi(\theta), \qquad \theta \in \mathbb{R},$$

and single-valuedness on the circle is imposed as the periodic boundary condition

$$\psi(\theta + 2\pi) = \psi(\theta), \qquad \theta \in \mathbb{R}.$$

A stationary state of energy $E$ is a function $\psi$ that is twice continuously differentiable on $\mathbb{R}$, satisfies the periodic boundary condition, and solves the displayed equation. Normalization is over one period,

$$\int_0^{2\pi} |\psi(\theta)|^{2}\, d\theta = 1 .$$

For each integer $n$ put

$$\psi_n(\theta) \;=\; \frac{1}{\sqrt{2\pi}}\, e^{i n \theta}, \qquad E_n \;=\; \frac{n^{2}\hbar^{2}}{2mR^{2}} .$$

Here $\hbar, m, R$ are real parameters, taken positive where positivity matters.

Formalization targets

Goal — the spectrum is exactly the quantized set

For $\hbar, m, R > 0$ and $E \in \mathbb{R}$:

$$\Bigl(\exists\, \psi \not\equiv 0 \ \text{of class } C^{2},\ 2\pi\text{-periodic},\ -\tfrac{\hbar^{2}}{2mR^{2}}\psi'' = E\psi \Bigr) \iff \exists\, n \in \mathbb{Z},\ E = \frac{n^{2}\hbar^{2}}{2mR^{2}} .$$

The right-to-left direction is the construction of $\psi_n$; the left-to-right direction is the quantization statement proper, and it must rule out every $E$ that is not of this form, including all $E < 0$ and every positive $E$ whose associated wave number is not an integer.

Supporting targets

The milestones cover, in order: the periodicity of $\psi_n$; its normalization; the identity $\psi_n'' = -n^{2}\psi_n$; the resulting fact that $\psi_n$ is a stationary state of energy $E_n$; the orthonormality relation $\int_0^{2\pi}\overline{\psi_j}\,\psi_n\,d\theta = \delta_{jn}$; the two-fold degeneracy $E_{-n} = E_n$ with $\psi_n, \psi_{-n}$ linearly independent for $n \neq 0$; and the level count, that exactly $2N+1$ integers $n$ satisfy $E_n \le E_N$.

Significance

The result itself fixes the spectrum of the free Hamiltonian on the circle, with the degeneracy pattern $1, 2, 2, 2, \dots$ and the $2N+1$ level count that underlies the $4N+2$ electron count of Hückel's rule. The orthonormality relation is the statement that the eigenfunctions form the classical Fourier system on $[0, 2\pi]$; the assertion that every ring wave function is a superposition of the $\psi_n$ is precisely the Fourier expansion theorem for periodic functions.

Formalizing it produces a small, reusable Lean development: a periodic-boundary-condition predicate, a second-order eigenvalue problem stated through iteratedDeriv, and a complete spectral determination for that problem. Mathlib supplies the Fourier exponentials on AddCircle and their orthonormality in $L^2$, but the pointwise, $C^2$, real-eigenvalue formulation used here is not present as such, and no formalization of this spectral statement currently exists on the platform. The supporting milestones are routine analysis; the goal theorem is where the content sits.

The physics is standard textbook material and is not in question; what this mission adds is the machine-checked proof.

Difficulty

The naive argument — "write the general solution as $A e^{ik\theta} + B e^{-ik\theta}$ with $k = R\sqrt{2mE}/\hbar$, then impose periodicity" — assumes the classification of solutions of $\psi'' = -k^{2}\psi$, which must itself be established over $\mathbb{C}$ for a $C^{2}$, not a priori analytic, function. Three regimes must be treated separately and none may be skipped: $E > 0$, where periodicity forces $k \in \mathbb{Z}$ and hence $E = E_k$; $E = 0$, where the solutions are affine in $\theta$ and periodicity kills the linear term, leaving $n = 0$; and $E < 0$, where the solutions are real exponentials and periodicity forces $\psi \equiv 0$, contradicting nontriviality. The third case is where a careless proof quietly assumes what it should prove.

Formalization scope

Wave functions are total functions $\mathbb{R} \to \mathbb{C}$ of the angular variable, not functions on a quotient or on AddCircle; periodicity is an explicit hypothesis. Smoothness is ContDiff ℝ 2, and the second derivative is iteratedDeriv 2, so the Schrödinger equation is a pointwise identity in $\mathbb{C}$, holding at every real $\theta$. The energy $E$ ranges over $\mathbb{R}$, not $\mathbb{C}$: the mission does not address non-self-adjoint or complex-eigenvalue variants. The parameters $\hbar, m, R$ are explicit real arguments rather than fixed constants, and positivity is assumed exactly where it is needed; note that under Lean's convention for division by zero, degenerate parameter values make both sides of the equation vanish, which is why the goal theorem carries $\hbar, m, R > 0$. Integrals are interval integrals over $[0, 2\pi]$ with respect to Lebesgue measure.

The goal cannot be satisfied vacuously: the right-hand side of the equivalence is satisfiable (take $n = 0$), and the left-hand side explicitly requires a $\psi$ with $\psi(\theta) \neq 0$ at some point, so the trivial solution is excluded. Contributions that build reusable infrastructure — a classification of $C^{2}$ solutions of $\psi'' = c\,\psi$ over $\mathbb{C}$, or a bridge between this pointwise formulation and Mathlib's AddCircle Fourier basis — are welcome, and would serve any later mission on one-dimensional periodic Schrödinger operators.

Selected references

• Wikipedia, Particle in a ring, revision 1318339663, https://en.wikipedia.org/wiki/Particle_in_a_ring — the source text for this mission's statements.
• H. Cox, Problems and Solutions to accompany Physical Chemistry: a Molecular Approach, University Science Books, p. 141, ISBN 978-0935702439 — the reference cited by the source for the angular reduction of the Laplacian.
• Wikipedia, Hückel's rule, https://en.wikipedia.org/wiki/H%C3%BCckel%27s_rule — the $4n+2$ electron count obtained from the level count formalized here.

Motivation

The Standard Model of particle physics assigns to each elementary fermion a vector in a representation of the compact Lie group $G_{\mathrm{SM}} = \mathrm{U}(1)\times \mathrm{SU}(2)\times \mathrm{SU}(3)$. The pattern of hypercharges this forces on quarks and leptons looks arbitrary. Three grand unified theories from the mid 1970s explain the pattern by enlarging the symmetry group: Georgi and Glashow's $\mathrm{SU}(5)$ theory, Georgi's $\mathrm{Spin}(10)$ theory, and the Pati-Salam model based on $\mathrm{SU}(2)\times \mathrm{SU}(2)\times \mathrm{SU}(4)$.

Baez and Huerta, The Algebra of Grand Unified Theories (2011), isolates the part of this story that is pure algebra: homomorphisms out of $G_{\mathrm{SM}}$, their kernels and images, and the way the three unified groups sit inside one another. This mission formalizes that group theoretic core. It deliberately leaves out the representation theoretic half of the paper (the exterior algebra $\Lambda\mathbb{C}^5$, the binary codes, the Dirac spinor representations), which is a natural follow-up mission.

Setting

Write $\mathrm{U}(1)$ for the group of complex numbers of modulus one, and $\mathrm{SU}(n)$ for the $n\times n$ complex matrices $A$ with $A^{*}A = I$ and $\det A = 1$. The Standard Model gauge group is the product

$$G_{\mathrm{SM}} \;=\; \mathrm{U}(1)\times \mathrm{SU}(2)\times \mathrm{SU}(3).$$

Fix the splitting $\mathbb{C}^5 \cong \mathbb{C}^2\oplus\mathbb{C}^3$ and write matrices in $\mathrm{SU}(5)$ in the corresponding $2+3$ block form. The Georgi-Glashow homomorphism is

$$\varphi(\alpha, g, h) \;=\; \begin{pmatrix}\alpha^{3} g & 0\\ 0 & \alpha^{-2} h\end{pmatrix}, \qquad (\alpha, g, h)\in G_{\mathrm{SM}},$$

where $\alpha^{3}g$ means the scalar $\alpha^3$ times the $2\times2$ matrix $g$. Fixing instead the splitting $\mathbb{C}^4\cong\mathbb{C}^3\oplus\mathbb{C}$ (colour plus lepton number), the Pati-Salam homomorphism is

$$\beta(\alpha, g, h) \;=\; \left(g,\; \begin{pmatrix}\alpha^{3} & 0\\ 0& \alpha^{-3}\end{pmatrix},\; \begin{pmatrix}\alpha h & 0\\ 0 & \alpha^{-3}\end{pmatrix}\right) \in \mathrm{SU}(2)\times \mathrm{SU}(2)\times \mathrm{SU}(4).$$

Finally, forgetting the complex structure of $\mathbb{C}^5$ gives a real inner product space $\mathbb{R}^{10}$, and every complex-linear map becomes a real-linear one. Writing each complex coordinate as a pair of real coordinates turns a complex $5\times5$ matrix $A$ into a real $10\times 10$ matrix $\rho(A)$, built from the $2\times 2$ blocks $\begin{pmatrix}\operatorname{Re} A_{ij} & -\operatorname{Im} A_{ij}\\ \operatorname{Im} A_{ij} & \operatorname{Re} A_{ij}\end{pmatrix}$. Under $\rho$, the splitting $\mathbb{C}^2\oplus\mathbb{C}^3$ becomes $\mathbb{R}^4\oplus\mathbb{R}^6$.

Formalization targets

Goal — Theorem 8 (p. 68): the true gauge group as an intersection

$$G_{\mathrm{SM}}/\mathbb{Z}_6 \;=\; \mathrm{SU}(5)\,\cap\,\bigl(\mathrm{SO}(4)\times \mathrm{SO}(6)\bigr)\;\subseteq\;\mathrm{SO}(10).$$

Concretely: a real $10\times10$ matrix $M$ is simultaneously (i) the realification $\rho(A)$ of some $A\in \mathrm{SU}(5)$ and (ii) block diagonal with blocks in $\mathrm{SO}(4)$ and $\mathrm{SO}(6)$, if and only if $M = \rho(\varphi(x))$ for some $x\in G_{\mathrm{SM}}$. The image of $\varphi$ is a copy of $G_{\mathrm{SM}}/\mathbb{Z}_6$, which is why this is the statement of Theorem 8; the quotient itself never has to be formed.

Supporting targets

The milestones establish, in order: that $\varphi$ is a homomorphism into $\mathrm{SU}(5)$; that its kernel is exactly $\{(\alpha, \alpha^{-3}I,\alpha^{2}I): \alpha^6=1\}$, a group of order six; that its image is the subgroup $S(\mathrm{U}(2)\times \mathrm{U}(3))$ of $\mathrm{SU}(5)$ preserving the $2+3$ splitting; the same programme for the Pati-Salam homomorphism $\beta$, whose kernel turns out to have order three; that realification is an injective homomorphism carrying $\mathrm{SU}(5)$ into $\mathrm{SO}(10)$; and the diagram chase by which Theorem 9 (p. 69) upgrades Theorem 8 from $\mathrm{SO}(10)$ to $\mathrm{Spin}(10)$.

Significance

The kernel computation is what makes the $\mathrm{SU}(5)$ theory testable at the level of algebra: because $\ker\varphi \cong \mathbb{Z}_6$ is nontrivial, no representation coming from $\mathrm{SU}(5)$ can distinguish the six elements of that kernel, so the Standard Model representation must be trivial on them — a nontrivial relation between hypercharge, isospin and colour that the observed fermions do satisfy. The intersection theorem says the Standard Model group is not merely contained in both unified theories: inside $\mathrm{Spin}(10)$ it is precisely their intersection, so the two routes to unification determine it exactly.

Formalizing this produces reusable Lean infrastructure for classical matrix groups: block decompositions of $\mathrm{SU}(n)$, the subgroup $S(\mathrm{U}(p)\times \mathrm{U}(q))$, and the realification homomorphism $\mathrm{U}(n)\to \mathrm{SO}(2n)$ with its determinant and orthogonality properties, none of which is currently available off the shelf. The mathematics is classical and fully proved in the source; what is open here is only the formalization.

Difficulty

The obvious first move — "$\varphi$ is visibly a homomorphism, so quotient by its kernel and apply the first isomorphism theorem" — settles the $\mathrm{SU}(5)$ milestones but not the goal. The goal compares two subgroups of $\mathrm{SO}(10)$ that are defined by different structures: one by preserving a complex structure and a volume form, the other by preserving a $4+6$ splitting of the real space. Showing the intersection is no larger than the image of $\varphi$ requires knowing that a real matrix commuting with the complex structure and respecting the real splitting must respect the complex splitting, and that the determinant conditions then match up exactly; the surjectivity half needs a sixth root of the determinant of the $\mathrm{U}(2)$ block to exist inside $\mathrm{U}(1)$.

Theorem 9 is a second, independent difficulty: $\mathrm{Spin}(10)$ and its double cover of $\mathrm{SO}(10)$ are not available in the current Lean library, so the milestone states the diagram chase of the published proof with the covering data as hypotheses rather than constructing $\mathrm{Spin}(10)$.

Formalization scope

The Lean development commits to the following conventions.

1. $\mathbb{C}^5$ is indexed by the disjoint union $\{0,1\}\sqcup\{0,1,2\}$, so the $2+3$ splitting is built into the index type and $\mathrm{SU}(5)$ elements are written with fromBlocks. Likewise $\mathbb{C}^4$ is indexed by $\{0,1,2\}\sqcup\{0\}$.
2. $\mathbb{R}^{10}$ is indexed by $(\{0,1\}\times\{0,1\})\sqcup(\{0,1,2\}\times\{0,1\})$, the second factor being the real/imaginary coordinate; the $4+6$ splitting is likewise built in.
3. $\mathrm{SO}(n)$ means the real special orthogonal group, i.e. real matrices $M$ with $M^{\mathsf T}M = I$ and $\det M = 1$, and $\mathrm{SO}(4)\times\mathrm{SO}(6)$ means block diagonal matrices whose two diagonal blocks lie in $\mathrm{SO}(4)$ and $\mathrm{SO}(6)$ — the identity component of $S(\mathrm{O}(4)\times \mathrm{O}(6))$, as in the source.
4. $\varphi$ and $\beta$ are given as matrix-valued functions on $G_{\mathrm{SM}}$; that they land in the special unitary groups and are multiplicative are milestones, not definitional assumptions. Quotient groups are never formed: $G_{\mathrm{SM}}/\mathbb{Z}_6$ appears as the image of $\varphi$, and the order of the kernel is stated separately.

No statement is vacuous: every milestone is universally quantified over the whole group, the goal is an equivalence between two nonempty subsets of $\mathrm{SO}(10)$ (both contain the identity), and the hypotheses of the Theorem 9 milestone are satisfied by the real $\mathrm{Spin}$ data of the source.

Contributions welcome beyond the milestones: constructing $\mathrm{Spin}(10)$ and its covering map so Theorem 9 can be stated unconditionally, and the representation theoretic half of the paper (Theorems 1-7), which needs $\Lambda\mathbb{C}^5$ and the Dirac spinor representations.

Selected references

• John Baez and John Huerta, The Algebra of Grand Unified Theories, Bulletin of the American Mathematical Society 47 (2010), 483-552. https://math.ucr.edu/home/baez/guts.pdf
• Howard Georgi and Sheldon Glashow, Unity of All Elementary-Particle Forces, Physical Review Letters 32 (1974), 438-441. https://doi.org/10.1103/PhysRevLett.32.438
• Jogesh Pati and Abdus Salam, Lepton number as the fourth "color", Physical Review D 10 (1974), 275-289. https://doi.org/10.1103/PhysRevD.10.275

Motivation

A gas of $N$ interacting particles is described exactly by $6N$ coordinates, and by no useful equation. Kinetic theory replaces that description by a single scalar field, the one-particle distribution function $f(x,v,t)$, whose evolution is governed by the Boltzmann equation. The price is the collision operator: the true Boltzmann collision integral is quadratic and five-dimensional, and almost every statement about it is hard. The BGK operator (Bhatnagar, Gross and Krook, 1954) replaces it by simple relaxation of $f$ towards the local Maxwellian at a fixed rate $1/\tau$. It is the standard first model for rarefied gas dynamics, the basis of lattice-Boltzmann numerics, and the model in which the structural features of kinetic theory — conserved moments, an $H$-theorem, hydrodynamic closure — can be exhibited in closed form.

This mission formalizes the BGK material as it is posed in Question 1 of the Oxford MMathPhys Kinetic Theory examination paper of Hilary Term 2019: the conservation of the hydrodynamic moments by the collision operator, the sign of the entropy production together with the characterisation of equality, the slab-geometry reduction to a closed two-field system, and the vanishing of the resulting stress and heat-flux corrections at equilibrium.

Setting

Velocities and positions range over $\mathbb R^3$. A distribution function is a map $f : \mathbb R^3 \to \mathbb R$ on velocity space (at a fixed position and time), assumed everywhere positive, integrable, and with finite second velocity moment. Particles have unit mass and the Boltzmann constant is set to $1$. Its moments are

$$\rho[f] = \int f\,\mathrm dv, \qquad u[f] = \frac 1{\rho[f]}\int v\,f\,\mathrm dv, \qquad \theta[f] = \frac 1{3\rho[f]}\int |v-u[f]|^2 f\,\mathrm dv,$$

the mass density, the bulk velocity and the temperature. The Maxwellian with parameters $(\rho,u,\theta)$ is

$$M_{\rho,u,\theta}(v) = \frac{\rho}{(2\pi\theta)^{3/2}} \exp\Big(-\frac{|v-u|^2}{2\theta}\Big),$$

and the local Maxwellian of $f$ is $f^{(0)} = M_{\rho[f],\,u[f],\,\theta[f]}$: the Maxwellian carrying the same three moments as $f$. The BGK collision operator with relaxation time $\tau>0$ is

$$C[f] = -\frac 1\tau\big(f - f^{(0)}\big),$$

and the Boltzmann equation with this operator is

$$\frac{\partial f}{\partial t} + v\cdot\nabla_x f = C[f].$$

In the slab geometry of parts (c)-(d) of the source, $x=(x,y,z)$, $u=(u,0,0)$, $v=(v,v_\perp)$ with $v_\perp=(v_y,v_z)$, and $f$ is independent of $y$ and $z$; the reduced fields are $g=\int f\,\mathrm dv_\perp$ and $h=\int |v_\perp|^2 f\,\mathrm dv_\perp$.

Formalization targets

Goal — the BGK $H$-theorem with its equality case

$$\int \mathrm dv\,(\log f)\,C[f] \le 0, \qquad\text{with equality iff } f = f^{(0)} \text{ almost everywhere.}$$

This is part (b) of the source question, including the answer to "under what conditions does equality hold". It is stated for every admissible $f$ and every $\tau>0$; it fixes no rate and no constant, so it is not invalidated by sharper quantitative versions.

Milestones

1. The Gaussian moments of $M_{\rho,u,\theta}$: mass $\rho$, momentum $\rho u$, and central second moment $3\rho\theta$; consequently $M_{\rho,u,\theta}$ is its own local Maxwellian.
2. Part (a): $\int C[f]\,\mathrm dv = 0$, $\int v\,C[f]\,\mathrm dv = 0$, $\int |v|^2 C[f]\,\mathrm dv = 0$ — the conservation of $\rho$, $u$ and $\theta$ by the collision operator.
3. The inequality of part (b) on its own.
4. Maxwellians, viewed as $x$- and $t$-independent distributions, solve the BGK equation.
5. Part (c): $\int M\,\mathrm dv_\perp = g^{(0)}$ and $\int |v_\perp|^2 M\,\mathrm dv_\perp = 2\theta\,g^{(0)}$, where $g^{(0)}(v)=\rho(2\pi\theta)^{-1/2}\exp(-(v-u)^2/2\theta)$, together with the expressions for $\rho$, $u$, $\theta$ in the reduced system.
6. Part (d): the quantities $T = -2\rho\theta + \int h\,\mathrm dv$ and $q = \tfrac12\int w^3 g\,\mathrm dv + \tfrac12\int w\,h\,\mathrm dv$ (with $w=v-u$) vanish when $g=g^{(0)}$ and $h=h^{(0)}$.

Significance

The three conservation identities say that the BGK operator, however crude as a model of binary collisions, respects the exact conservation laws of the gas: they are what makes the moment hierarchy of the BGK equation reduce to the Euler equations at leading order. The entropy inequality is the model's $H$-theorem: it forces the entropy $-\int f\log f\,\mathrm dv$ to be non-decreasing under collisions and singles out the Maxwellians as the only collisional equilibria, which is the statement that fixes the direction of time in the model. The slab reduction of part (c) is the standard device by which a three-dimensional kinetic problem is reduced to a pair of one-dimensional kinetic equations, used throughout computational rarefied gas dynamics; part (d) identifies exactly which moments of the reduced fields carry the non-equilibrium stress and heat flux.

Formalizing this material requires building the moment calculus of Gaussians on $\mathbb R^3$ against Lebesgue measure — normalisation, first and central second moments, and the partial integration over two of the three velocity components — none of which exists in Mathlib in a form adapted to kinetic theory. The mathematics is classical and the proofs are known; the work is in the analysis bookkeeping: integrability of moments, dominated convergence, and the a.e. equality case of a strict pointwise inequality.

Difficulty

The obvious computation for the $H$-theorem — expand $\int (\log f)(f-f^{(0)})$ and integrate term by term — does not by itself give a sign: $\log f$ has no sign, and neither does $f - f^{(0)}$. The argument needs the conservation identities as an input, because they are what allows $\log f^{(0)}$, which is a quadratic polynomial in $v$, to be subtracted for free. Only then is the integrand pointwise of one sign. Formally, the obstacle is that none of the pieces of the integrand is separately integrable in general: the statements are formulated with the integrability of the entropy-production integrand as an explicit hypothesis, and any splitting of it must be justified.

The equality case adds a second difficulty. Vanishing of the integral of a non-negative integrable function gives vanishing only almost everywhere, so the conclusion is an a.e. identity $f = f^{(0)}$, and the strictness of $(\log a - \log b)(a-b) > 0$ for $a \ne b$ must be used pointwise.

Formalization scope

Velocity space is EuclideanSpace ℝ (Fin 3) with its Lebesgue (volume) measure, and integrals are Bochner integrals; vector-valued moments are integrals of EuclideanSpace-valued functions. Distribution functions are total functions $\mathbb R^3 \to \mathbb R$ with no measurability packaged into the type, so every statement carries its own integrability hypotheses; admissibility (positivity everywhere, integrability, finite second moment) is bundled in a predicate. The Maxwellian prefactor is written with a real power $(2\pi\theta)^{3/2}$, so $\theta>0$ is required wherever it appears. The relaxation time satisfies $\tau>0$.

Two traps are worth naming. First, in Lean the integral of a non-integrable function is $0$ by convention, so an entropy inequality stated without an integrability hypothesis would be satisfiable for trivial reasons; the goal therefore assumes the entropy-production integrand is integrable, and states the equality case as an iff, which is not satisfiable by a degenerate reading. Second, the local Maxwellian is defined from the moments of $f$ itself, not from externally supplied parameters, so none of the conservation statements can be discharged by choosing convenient parameters.

The slab-geometry part of the mission is developed in its own definition file, with the perpendicular velocity in EuclideanSpace ℝ (Fin 2) and the reduced fields as functions $\mathbb R\to\mathbb R$. The Gaussian moment lemmas produced here are reusable for any Maxwellian-based kinetic model; contributions that add Mathlib-level lemmas on Gaussian moments in $\mathbb R^n$, rather than ad-hoc computations, are especially welcome.

Selected references

• P. L. Bhatnagar, E. P. Gross, M. Krook, A model for collision processes in gases. I. Small amplitude processes in charged and neutral one-component systems, Physical Review 94 (1954) 511-525. https://doi.org/10.1103/PhysRev.94.511
• C. Cercignani, The Boltzmann Equation and Its Applications, Applied Mathematical Sciences 67, Springer, 1988. https://doi.org/10.1007/978-1-4612-1039-9
• Oxford MMathPhys Kinetic Theory examination paper A15089W1, Hilary Term 2019, Question 1. https://web.archive.org/web/20250913150648/https://mmathphys.physics.ox.ac.uk/sites/default/files/mmathphys/documents/media/kt_2019.pdf

Why the tides need their own equations

The rise and fall of the ocean surface under the gravitational pull of the moon and the sun is the oldest quantitative problem in physical oceanography, and it is still a working one: satellite altimetry can only see ocean circulation after the tidal signal has been removed, and the removal is done with a numerical solution of Laplace's tidal equations (LTE) constrained by tide-gauge and altimeter data (Le Provost et al., J. Geophys. Res. 99 (1994) 24777). The same equations carry the global tidal energy budget: an estimate of where the roughly 3.5 TW of tidal energy is dissipated — shallow-sea bottom drag versus conversion into internal tides over deep-ocean topography — is obtained by integrating the energy identity of these equations against observed elevation data (Egbert and Ray, Nature 405 (2000) 775).

The material formalized here is M. Hendershott, Lecture 3: Solutions to Laplace's Tidal Equations (Woods Hole Oceanographic Institution, Geophysical Fluid Dynamics Program lecture notes, pp. 34–44), notes taken by V. Birman and E. Williams Frajka. The lecture states the separable normal-mode solutions of the stratified problem, the solid Earth tide and the Love number decomposition, models of dissipation, coastal boundary conditions, and finally the energy equation of the tides, both ignoring and including the yielding of the solid Earth.

Setting

Write $u(x,y,t)$ and $v(x,y,t)$ for the two components of the depth-independent horizontal velocity, $\zeta(x,y,t)$ for the free-surface elevation, $\delta(x,y,t)$ for the solid Earth tide (the elastic displacement of the crust under the tidal load), and $\zeta_0 = \zeta - \delta$ for the observed, geocentric tide. The ocean has resting depth $D(x,y) > 0$, constant density $\rho > 0$, gravity $g$, and constant Coriolis parameter $f$. The astronomical forcing enters through the tide generating potential $\Gamma(x,y,t)$ and the dissipation through a force per unit area $(F^x, F^y)$.

Laplace's tidal equations are the two momentum equations

$$u_t - f v = -g\left(\zeta - \tfrac{\Gamma}{g}\right)_x + \frac{F^x}{\rho D}, \qquad v_t + f u = -g\left(\zeta - \tfrac{\Gamma}{g}\right)_y + \frac{F^y}{\rho D},$$

together with the continuity equation, which in the presence of the solid Earth tide reads

$$(\zeta - \delta)_t + (uD)_x + (vD)_y = 0 .$$

For a stratified ocean the same system arises mode by mode after separation of variables, with $D$ replaced by the equivalent depth $D_n$ of the $n$-th mode and the vertical structure $F_w(z)$ solving $F_{wzz} + (N^2/(gD_n))F_w = 0$, where $N(z)$ is the buoyancy frequency.

Formalization targets

Goal — the energy equation including the solid Earth tide (eqs. (35)–(39))

$$\mathrm{KE}_t + \mathrm{PE}_t + \nabla\cdot \vec{P} \;=\; W_t + \vec{u}\cdot \vec{F},$$

with

$$\mathrm{KE} = \tfrac12\rho D (u^2+v^2), \quad \mathrm{PE} = \tfrac12\rho g\,(\zeta_0^2 + 2\zeta_0\delta + 2\delta D), \quad \vec{P} = \rho g D \vec{u}(\zeta_0+\delta),$$ $$W_t = \rho\,\zeta_{0t}\Gamma + \rho\,\nabla\cdot(\vec{u}D\Gamma) + \rho g(\zeta_0 + D)\delta_t .$$

This is a pointwise identity, valid at every $(x,y,t)$ for every solution of the equations above, with variable depth $D(x,y)$ and no assumption on the form of the dissipation.

Supporting targets

The milestone list covers the corresponding identity with the solid Earth tide ignored (eqs. (29)–(30)), the two normal-mode facts of §2 — the vertical structure equation with the equivalent depth $D_n$ (eq. (4)) and the nonrotating barotropic plane wave with its dispersion relation $\sigma = \pm k\sqrt{gD_*}$ (§2.1) — and the two averaging statements of §6: that the period mean of the time derivative of a periodic energy density vanishes (eq. (31)) and the resulting period-averaged balance $\nabla\cdot\langle P\rangle = \langle W_t\rangle + \langle \vec{u}\cdot\vec{F}\rangle$ (eq. (32)).

Significance

The energy identity is what converts elevation observations into a dissipation estimate: averaged over a tidal period and integrated over a basin with no flux through its boundary, the flux divergence drops out and the work done by the tide generating potential equals the dissipation, so $\int \langle \vec{u}\cdot\vec{F}\rangle$ is computable from $\zeta_0$ alone. Every term in that chain — which terms are exact, which vanish only on average, which require the Love numbers to be real — is a hypothesis that a formal statement has to carry explicitly, and the lecture is explicit that the identity holds "provided that the Love numbers are real", i.e. provided the solid Earth tide is dissipation-free.

Formalizing this material produces a reusable model of a rotating shallow-water system with forcing, dissipation and an elastic bottom boundary, together with the calculus lemmas needed to differentiate products of fields of several variables. Nothing here is an open problem: the results are classical, and the contribution is a machine-checked derivation from a precisely stated model, including the bookkeeping that textbook derivations compress.

Difficulty

The obstacle is not depth of argument but faithfulness of the model. The derivation multiplies the two momentum equations by $\rho u D$ and $\rho v D$, the continuity equation by $\rho g \zeta$, and adds; every step needs a product rule for a field of three variables, and the Coriolis terms must cancel exactly rather than approximately. Two places in the source require care before they can be formalized: equation (29) prints the surface term with coefficient $\tfrac1g \rho g$, and the printed $PE_t$ in §6.1 has signs that do not follow from the printed $PE$; the identities are true with $\tfrac12\rho g(\zeta^2)_t$ and $PE_t = \rho g(\zeta\zeta_t - \delta\delta_t + D\delta_t)$ respectively. The potential energy (37) also differs from $\int_{-D+\delta}^{\zeta}\rho g z\,dz$ by a term independent of time, which is invisible in $PE_t$ and therefore harmless. A naive formalization that copies the printed formulas without checking these will state something false.

Formalization scope

Fields are real-valued functions of $x$, $y$ and $t$; partial derivatives are Lean's one-dimensional deriv applied slot-wise, and differentiability is imposed as an explicit hypothesis in each variable separately, rather than through Fréchet derivatives. Depth is a function $D(x,y)$ that does not depend on time, and positivity of $\rho$ and $D$ is assumed where the momentum equations are divided by $\rho D$. The equations themselves are packaged as a structure with three fields, one per equation, so that a solution is an explicit witness rather than an assumption schema; this rules out a vacuous reading, since constant fields with zero forcing satisfy the structure. The barotropic plane wave of §2.1 is stated with complex-valued $Z$ and $U$ and the physical normalization $a \neq 0$, $\sigma \neq 0$, and is an equivalence: the wave solves the system exactly when $\sigma = \pm k\sqrt{gD_*}$. The vertical mode statement uses the rigid-lid conditions $F_w(-D_*) = F_w(0) = 0$; the lecture's free-surface condition $F_w - D_n F_{wz} = 0$ at $z = 0$ is satisfied by the sine modes only in the limit of small equivalent depth, and is not claimed. Period averaging is formalized as $\frac1T\int_0^T$ of an interval integral at a fixed horizontal position, with periodicity and continuity of the relevant time derivative as hypotheses.

Contributions extending this mission are welcome in three directions: the derivation of the equations from the linearized Euler equations of Lecture 2, the solid Earth tide of §3 with the Love number decomposition (17)–(20), and the basin-integrated form of the energy budget (33), which needs a divergence theorem for the flux term.

Selected references

• M. Hendershott, Lecture 3: Solutions to Laplace's Tidal Equations, WHOI GFD Program lecture notes, pp. 34–44. PDF
• C. Le Provost, M. L. Genco, F. Lyard, P. Vincent, P. Canceil, "Spectroscopy of the world ocean tides from a finite element hydrodynamic model", J. Geophys. Res. 99 (1994) 24777. DOI
• G. D. Egbert, R. D. Ray, "Significant dissipation of tidal energy in the deep ocean inferred from satellite altimeter data", Nature 405 (2000) 775. DOI
• W. E. Farrell, "Deformation of the Earth by surface loads", Rev. Geophys. 10 (1972) 761. DOI

Motivation

Graphene is a single sheet of carbon atoms arranged on a honeycomb lattice. Its electrons are described, to a first approximation that is quantitatively good near the Fermi level, by a nearest-neighbour tight-binding model: a hopping amplitude $t$ between adjacent carbon sites and nothing else. What makes the model worth studying is that this two-parameter lattice problem produces a band structure with two bands that touch at isolated points of the Brillouin zone and disperse linearly around them, so that low-energy electrons obey a two-dimensional massless Dirac equation rather than a Schrödinger equation with an effective mass. That observation organises the standard review literature on graphene (Castro Neto, Guinea, Peres, Novoselov, Geim, The electronic properties of graphene, Rev. Mod. Phys. 81 (2009) 109), and goes back to Wallace's 1947 band theory of graphite.

This mission formalises a self-contained set of lecture notes that carries the computation out in full: F. Utermohlen, Tight-Binding Model for Graphene (2018). It is the two-dimensional, two-sublattice counterpart of the tight-binding chain: the chain gives a single band $\varepsilon(k)=-2t\cos(ka)$ with no band touching, while the honeycomb lattice, whose unit cell contains two inequivalent sites, produces a $2\times2$ Bloch matrix and the conical band touchings targeted here.

Setting

Fix a carbon–carbon distance $a>0$ and a hopping amplitude $t>0$. The honeycomb lattice is two interpenetrating triangular lattices, the $A$ and $B$ sublattices, with lattice unit vectors $a_1=\tfrac{a}{2}(3,\sqrt3)$, $a_2=\tfrac{a}{2}(3,-\sqrt3)$ and nearest-neighbour vectors

$$\delta_1=\tfrac{a}{2}\bigl(1,\sqrt3\bigr),\qquad \delta_2=\tfrac{a}{2}\bigl(1,-\sqrt3\bigr),\qquad \delta_3=-a\bigl(1,0\bigr),$$

each joining an $A$ site to one of its three $B$ neighbours. The corners of the first Brillouin zone — the Dirac points — are

$$K=\frac{2\pi}{3\sqrt3\,a}\bigl(\sqrt3,1\bigr),\qquad K'=\frac{2\pi}{3\sqrt3\,a}\bigl(\sqrt3,-1\bigr).$$

Fourier transforming the second-quantised hopping Hamiltonian $\hat H=-t\sum_{\langle ij\rangle}(\hat a^\dagger_i\hat b_j+\mathrm{h.c.})$ gives $\hat H=\sum_k\Psi^\dagger h(k)\Psi$ with $\Psi=(\hat a_k,\hat b_k)^{T}$ and the Bloch Hamiltonian

$$h(k)=-t\begin{pmatrix}0&\Delta_k\\ \overline{\Delta_k}&0\end{pmatrix}, \qquad \Delta_k=\sum_{j=1}^{3}e^{i\,k\cdot\delta_j},$$

where $\Delta_k$ is called the structure factor. The mission takes this $2\times2$ matrix as its starting point: the second-quantised derivation (Eqs. 2–8 of the notes) is not formalised, and $h(k)$ together with $\Delta_k$ is defined by the displayed formulas. The band energies are the eigenvalues $E_\pm(k)$ of $h(k)$, and $E_+(k)=t|\Delta_k|$ is the quantity the statements are written in terms of. The Fermi velocity is $v_F=\tfrac{3at}{2}$ (units with $\hbar=1$).

Formalization targets

Goal — the Dirac cone

$$\chi_{h(k)}(X)=X^2-E_+(k)^2\ \text{ for all }k,\qquad E_+(K)=0,\qquad E_+(K+q)=v_F\,|q|+o(|q|)\ \ (q\to0),$$

with $E_+(k)=t|\Delta_k|$, $|q|=\sqrt{q_x^2+q_y^2}$ and $v_F=\tfrac{3at}{2}$. The three clauses say, in order, that $\pm E_+$ really are the eigenvalues of the Bloch Hamiltonian, that the two bands touch at the Brillouin-zone corner $K$, and that they disperse linearly and isotropically around it. The goal deliberately asserts the shape of the low-energy dispersion — a first-order expansion, with no quantitative remainder — so it is not invalidated by sharper error estimates.

Milestones

The milestone list follows the notes equation by equation: the closed form of $\Delta_k$ (Eq. 11), the characteristic polynomial of $h(k)$ (Eq. 9), the two explicit forms of the dispersion (Eqs. 12 and 13–14), the Pauli-matrix form of $h(k)$ (Eq. 18), the vanishing of $\Delta$ at $K$ and $K'$, the first-order expansions at both Dirac points (Eqs. 22–23 and 30), the spectrum of the linearised Hamiltonians (Eq. 32), and the gap opened by a $\sigma_z$ mass term (Eqs. 33–34).

Significance

The three clauses of the goal are what turn a lattice hopping problem into the massless-Dirac-fermion picture used throughout graphene physics: they are the precise sense in which "graphene has Dirac cones at $K$ and $K'$ with Fermi velocity $3at/2$". Downstream, the same objects carry the valley structure — the two expansions are complex conjugates of one another — and the mass milestone shows how a sublattice-asymmetric on-site potential (boron nitride rather than graphene) opens a gap $2v_F|M|$, the standard model of a gapped Dirac material.

The mathematics is classical and the physics literature regards it as settled; what this mission adds is a machine-checked development in which the honeycomb geometry, the Bloch matrix, its spectrum and the Dirac-point expansions are reusable definitions and lemmas rather than a computation redone by hand. No part of the development is claimed to be new mathematics.

Difficulty

The obstacles are in the analysis, not the algebra. The first two clauses of the goal are a trigonometric identity and a $2\times2$ determinant. The third is a genuine differentiability statement, and the naive route — expand $\Delta_{K+q}$, cancel the zeroth-order terms, read off the linear term — has to be carried out uniformly in the direction of $q$; moreover the quantity being expanded is $|\Delta_{K+q}|$, a modulus, which is not differentiable at a zero of $\Delta$. The linear behaviour of $E_+$ survives only because the modulus of a function with a nonzero complex-linear differential at a zero is asymptotically the modulus of that differential, and the elementary estimate $\bigl||z+w|-|z|\bigr|\le|w|$ is what lets the $o(|q|)$ error be transported through the modulus. Note also that $E_+$ itself is not differentiable at $K$ — the cone has a vertex there — so no Taylor theorem applies to $E_+$ directly.

Formalization scope

Wave vectors and lattice vectors are pairs of reals, $\mathbb{R}\times\mathbb{R}$. Because that product type carries the sup norm, the Euclidean length $|q|=\sqrt{q_x^2+q_y^2}$ is introduced as a separate definition and is the one used in every statement; the little-o statements are taken with respect to the neighbourhood filter of the origin, for which the two norms agree up to constants. $\Delta_k$ is a finite sum over a three-element index set, $h(k)$ is a concrete $2\times2$ complex matrix, and "eigenvalues" are always expressed through the characteristic polynomial rather than through an eigenvector predicate. Lattice constant and hopping amplitude are real parameters; the standing hypotheses of the goal are exactly $a>0$ and $t>0$, and several milestones need less. Units are $\hbar=1$, so $v_F=\tfrac{3at}{2}$.

Two things the formalization deliberately does not do: it does not derive the Bloch Hamiltonian from the second-quantised hopping Hamiltonian (Eqs. 2–8), which would require a Fock-space development, and it does not claim that $K$ and $K'$ are the only zeros of $\Delta$. No statement is vacuous: every hypothesis is satisfiable (take $a=t=1$), and the goal's third clause is a nontrivial asymptotic rather than an identity.

Contributions welcome beyond the milestone list: the second-quantised derivation, the identification of the full zero set of $\Delta_k$ modulo the reciprocal lattice, eigenvector-level (pseudospin) statements, the density of states, and the extension to next-nearest-neighbour hopping.

Selected references

• F. Utermohlen, Tight-Binding Model for Graphene, lecture notes, Ohio State University, 2018.
• A. H. Castro Neto, F. Guinea, N. M. R. Peres, K. S. Novoselov, A. K. Geim, The electronic properties of graphene, Rev. Mod. Phys. 81 (2009) 109. https://doi.org/10.1103/RevModPhys.81.109
• P. R. Wallace, The Band Theory of Graphite, Phys. Rev. 71 (1947) 622. https://doi.org/10.1103/PhysRev.71.622

Motivation

A micron-sized bead suspended in water and held by an optical tweezer is one of the standard measuring instruments of soft-matter physics: the bead's fluctuating position reports on the viscosity of the medium, on the stiffness of the trap, and on the forces exerted by whatever is attached to the bead. The quantity that experiments record is the mean-squared displacement (MSD) $\langle r^2 \rangle (t)$ of the bead. Interpreting such data rests on a single classical calculation, due to Paul Langevin (1908): write Newton's second law for the bead including the drag of the fluid, the trap force and the fluctuating force of the molecular environment, multiply the equation by the position, and average over realizations. What comes out is a closed, deterministic, second-order ordinary differential equation for $\langle r^2 \rangle$ — no stochastic calculus required. This mission formalizes exactly that derivation, and the solution of the resulting equation, for a particle in a harmonic trap.

Setting

A particle of mass $m > 0$ moves in $d$ Cartesian dimensions. Its position at time $t \in \mathbb{R}$ is the vector $r(t)$ with components $x_i(t)$, $i = 1,\dots,d$; its velocity components are $v_i(t) = \dot{x}_i(t)$ and its acceleration components $a_i(t) = \dot{v}_i(t)$. The particle feels three forces: a hydrodynamic drag $-\zeta \dot{r}$ with drag coefficient $\zeta$; a harmonic trap force $-k r$ with spring constant $k$; and a random force $f(t)$ exerted by the surrounding medium, which is held at temperature $T$. Newton's second law then reads

$$m \ddot{r}(t) = -\zeta \dot{r}(t) - k\, r(t) + f(t).$$

A single solution of this equation, for one realization of the random force, is called a path. An ensemble is a probability space $(\Omega,\mu)$ of such paths, and the ensemble average of a quantity $A$ is $\langle A \rangle = \int_\Omega A \, d\mu$. Two physical inputs single out a thermal environment: the random force is uncorrelated with the instantaneous position, $\langle r \cdot f \rangle = 0$, and the velocity obeys equipartition, $m \langle \dot{r}^2 \rangle = d\, k_B T$ with $k_B$ Boltzmann's constant. The mean-squared displacement is $M(t) = \langle r(t)^2 \rangle$.

Formalization targets

Goal — the MSD equation

$$m \ddot{M}(t) + \zeta \dot{M}(t) + 2 k\, M(t) = 2 d\, k_B T , \qquad M(t) = \langle r(t)^2 \rangle .$$

This is the weakest stable form of the result: it fixes no initial condition, no sign convention on the roots, and no regime (inertial or overdamped), and every later statement about the MSD of a trapped Brownian particle is a consequence of it.

Milestone level — the pathwise identity

For each realization, with $S = r^2$,

$$\tfrac{m}{2} \ddot{S} + \tfrac{\zeta}{2} \dot{S} + k\, S = m\, \dot{r}^2 + r \cdot f ,$$

which is Newton's equation contracted with $r$ and rewritten using $r \cdot \dot r = \tfrac12 \dot S$ and $r \cdot \ddot r = \tfrac12 \ddot S - \dot r^2$.

Milestone level — the explicit solution

With $\lambda_\pm$ the two distinct roots of $m\lambda^2 + \zeta\lambda + 2k = 0$,

$$M(t) = \frac{d\,k_B T}{k} \left[ 1 + \frac{\lambda_- e^{\lambda_+ t} - \lambda_+ e^{\lambda_- t}} {\lambda_+ - \lambda_-} \right]$$

solves the goal equation with $M(0) = \dot M(0) = 0$, and in the inertialess (overdamped) case the solution reduces to $M(t) = \frac{d k_B T}{k}\left(1 - e^{-2kt/\zeta}\right)$, which grows as $2 d (k_B T/\zeta) t$ at short times and saturates at the equipartition plateau $d k_B T / k$.

Significance

The MSD equation is what converts a measured displacement trace into physical numbers: its plateau $d k_B T/k$ calibrates trap stiffness, its short-time slope gives the diffusion coefficient $D = k_B T/\zeta$, and the crossover between the two identifies the relaxation time $\zeta/(2k)$. The derivation is also the historical template for treating noisy dynamics without a theory of stochastic integrals: Langevin's move of averaging the equation multiplied by $r$ is what makes the noise term drop out.

Formalizing it produces a machine-checked statement of the classical calculation together with the assumptions it actually needs, each of which is carried explicitly as a hypothesis rather than left implicit in the prose: interchange of ensemble averaging with time differentiation, integrability of the averaged quantities, decorrelation of the random force from the position, and equipartition. The pathwise identity and the solution-verification statements are elementary calculus; the substance of the mission is that the physical derivation is faithful once those hypotheses are written down.

Difficulty

The obvious route — solve the stochastic equation for $r(t)$ and then square and average — requires a theory of stochastic integration against the random force, whose statistics the problem never specifies beyond the two averaged facts above. Langevin's derivation avoids this entirely, but the step "average the equation" hides two real assumptions: that $\langle \cdot \rangle$ commutes with $d/dt$ (so that $\langle \ddot{S}\rangle$ is the second derivative of $M$), and that $\langle r \cdot f \rangle$ vanishes at every time. Neither follows from the equation of motion; both must be hypotheses, and stating them precisely without weakening the theorem into vacuity is the formalization problem.

Formalization scope

Paths are represented in components: position, velocity, acceleration and force are families $x, v, a, f : \mathrm{Fin}\ d \to \mathbb{R} \to \mathbb{R}$, and the model predicate records that $v$ is the derivative of $x$, that $a$ is the derivative of $v$, and that Newton's law holds at every time, so no differentiability is smuggled in. Euclidean contractions are the single helper $\mathrm{dotSum}\ d\ u\ w\ t = \sum_i u_i(t) w_i(t)$, so that $r^2$, $r\cdot\dot r$, $\dot r^2$ and $r \cdot f$ are all instances of one definition. Ensembles are an arbitrary probability space with the integral as average, and paths are indexed by the sample point; the averaging assumptions appear as hypotheses relating $M$ and its derivatives to integrals of the pathwise quantities. Dimension $d$ is arbitrary, the source's $d = 3$ being a special case.

No hypothesis of the goal is vacuous: a deterministic ensemble (one path, a Dirac measure) with $f \equiv 0$ and a particle at rest satisfies all of them when $k_B T = 0$, and nondegenerate instances exist for every choice of parameters, so the statement is not satisfied only in an empty context. All statements target real-valued time and real coefficients; no positivity of $m$, $\zeta$, $k$ is assumed except where a milestone needs it for an asymptotic claim.

Selected references

• P. Langevin, Sur la théorie du mouvement brownien, C. R. Acad. Sci. Paris 146 (1908), 530–533. English translation: D. S. Lemons and A. Gythiel, Paul Langevin's 1908 paper "On the Theory of Brownian Motion", American Journal of Physics 65 (1997), 1079–1081. https://doi.org/10.1119/1.18725
• Nonequilibrium Statistical Physics, Honour School of Mathematical and Theoretical Physics Part C, Trinity Term 2018 examination paper A15282W1, Question 1.

Motivation

A black body is an idealized object that absorbs all radiation falling on it and, when held at a fixed absolute temperature $T$, re-emits radiation whose spectrum depends on $T$ alone — not on the material, shape, or history of the body. Measuring that spectrum, and explaining it, was the central problem of late nineteenth-century thermal physics: the classical prediction of Rayleigh and Jeans grows without bound at short wavelengths, which is not what cavity radiation does.

Max Planck's 1900 formula fits the measured spectrum at every temperature and every wavelength, and it does so by quantizing the energy exchanged between matter and the radiation field. Two features of that formula are used constantly outside physics proper — in astronomy, remote sensing, radiometry, and illumination engineering. The first is the shape of the curve. The second is where its maximum sits: the peak wavelength is inversely proportional to the temperature, which is Wien's displacement law, discovered by Wilhelm Wien several years before Planck's formula and recovered from it as a corollary. This is why a heated piece of metal runs red, then orange, then white; why the Sun's per-wavelength emission peaks near $500\ \mathrm{nm}$; and why infrared cameras aimed at mammals at $300\ \mathrm{K}$ are built for about $10\ \mu\mathrm{m}$.

This mission formalizes Planck's law as a definition and derives Wien's displacement law from it, in both the wavelength and the frequency parameterization, including the transcendental maximization equation and the numerical value of its root.

Setting

Fix three positive real parameters: the Planck constant $h$, the speed of light $c$, and the Boltzmann constant $k_B$. They are left as variables rather than numerical constants, so that every statement is a theorem about the functional form, valid in any unit system.

For an absolute temperature $T > 0$, Planck's law is given in two parameterizations. Per unit frequency $\nu > 0$, the spectral radiance is

$$B_\nu(\nu, T) \;=\; \frac{2h\nu^3/c^2}{\exp\!\left(\dfrac{h\nu}{k_B T}\right) - 1},$$

and per unit wavelength $\lambda > 0$ it is

$$B_\lambda(\lambda, T) \;=\; \frac{2hc^2/\lambda^5}{\exp\!\left(\dfrac{hc}{\lambda k_B T}\right) - 1}.$$

These are different functions, not the same function in different letters: radiance is defined per increment of the independent variable, so passing between them carries the Jacobian factor $|d\nu/d\lambda| = c/\lambda^2$. Consequently the two curves peak at different physical locations, and the mission keeps both.

The third object is the dimensionless shape function

$$g_n(x) \;=\; \frac{x^n}{e^x - 1}, \qquad x > 0,$$

with $n = 5$ for the wavelength form and $n = 3$ for the frequency form.

Target

The goal is Wien's displacement law in the wavelength parameterization. Writing $x_5$ for the positive solution of the maximization equation $x = 5\,(1 - e^{-x})$, the goal asserts the existence of a constant

$$b \;=\; \frac{hc}{x_5 k_B} \;>\; 0$$

such that for every temperature $T > 0$ the function $\lambda \mapsto B_\lambda(\lambda, T)$ on $(0, \infty)$ has a strict global maximum, attained at

$$\lambda_{\mathrm{peak}} \;=\; \frac{b}{T},$$

and nowhere else. With SI values of $h$, $c$, $k_B$ this is $b = 2.897\,771\,955\ldots \times 10^{-3}\ \mathrm{m\cdot K}$.

The milestones build to this: the Jacobian relation between the two parameterizations; the strong (temperature-independent shape) form of the law; existence and uniqueness of the root of the maximization equation; the strict maximum of $g_n$ at that root; the frequency-parameterized displacement law, with $\nu_{\mathrm{peak}} = x_3 k_B T / h$ and $x_3 = 2.821\,439\,372\ldots$; and a rigorous numerical enclosure of $x_5$.

Significance

The result itself. Wien's displacement law is the quantitative content of "hotter means bluer". It converts an observed color into a temperature, which is how stellar surface temperatures, incandescent filament temperatures, and remote-sensed surface temperatures are read off in practice. Its strong form — that the spectrum has one fixed shape, rescaled by $T$ — is what licenses tabulating the Planck spectrum once and reusing it at all temperatures, including the percentile table of the radiation distribution.

Formalizing it. Both results are classical and completely settled mathematically; the work here is machine-checked derivation, not discovery. Mathlib has the exponential function, derivatives, and the tools for strict-monotonicity and interval arguments, but carries no formalization of the Planck spectrum. This mission contributes a definition bundle for the Planck spectral radiance that later work (Stefan–Boltzmann, the Rayleigh–Jeans and Wien-approximation limits, the percentile table) can import directly, plus reusable analytic lemmas about $x \mapsto x^n/(e^x - 1)$ and about the equation $x = n(1 - e^{-x})$ that are independent of the physics.

Difficulty

The obvious argument — differentiate, set the derivative to zero, solve — fails at the last step: $x = 5(1 - e^{-x})$ has no closed-form solution in elementary functions, and the informal source resolves it with the Lambert $W$ function. A formal proof therefore cannot produce the maximizer explicitly; it must establish existence and uniqueness of the critical point and separately prove the critical point is a strict global maximum, which needs the behavior of $x^n/(e^x - 1)$ at both ends of $(0, \infty)$ rather than a local second-derivative test. The numerical milestone adds a different difficulty: certified bounds on a transcendental root require explicit rigorous estimates on $\exp$ at a specific rational point, not floating-point evaluation.

A second trap is the parameterization. Substituting $\nu = c/\lambda$ into $B_\nu$ does not give $B_\lambda$, and the two peaks genuinely differ (for $T = 6000\ \mathrm{K}$, $482.96\ \mathrm{nm}$ against $849.91\ \mathrm{nm}$). The Jacobian milestone is stated precisely so that this cannot be blurred.

Formalization scope

Everything is over the real numbers. $h$, $c$, $k_B$, $T$, $\lambda$, $\nu$ are real variables carrying explicit positivity hypotheses wherever the statement needs them; no numerical values of the physical constants are hard-coded, and the physical dimensions are not modeled. The spectral radiance is defined by a total function, so it returns a junk value outside the intended domain (in particular where the denominator vanishes, at $x = 0$); every theorem restricts to the physical range by hypothesis, so no claim rests on junk values.

The peak statements are formulated as strict inequalities against all other admissible arguments — for the goal, every $\lambda > 0$ with $\lambda \neq b/T$ — rather than as a local maximum or a vanishing-derivative condition. This rules out the trivializing formalizations: a first-order condition alone would not exclude a minimum or an inflection, and a local statement would not exclude a second, higher peak elsewhere.

The maximization constants are pinned down, not merely asserted to exist: the goal requires the constant $b$ to equal $hc/(x k_B)$ for a positive $x$ satisfying $x = 5(1 - e^{-x})$, and a separate milestone gives the enclosure $4.9651142317 < x < 4.9651142318$. Uniqueness of that root is itself a milestone, so the pair determines $b$ completely.

A complete development needs Mathlib's Real.exp API, differentiability and the mean value theorem or a strict-monotonicity argument, and interval arithmetic or explicit Taylor bounds for the numerical enclosure. The lemmas about the shape function and about $x = n(1 - e^{-x})$ are stated for a general exponent $n$ and are reusable beyond this mission. Contributions of the Stefan–Boltzmann integral, the Rayleigh–Jeans and Wien approximation limits, and the logarithmic ("per proportional bandwidth") parameterization would be natural follow-ups but are out of scope here.

Selected references

• M. Planck, Über das Gesetz der Energieverteilung im Normalspectrum, Annalen der Physik 4 (1901), 553–563. DOI: https://doi.org/10.1002/andp.19013090310
• W. Wien, Über die Energievertheilung im Emissionsspectrum eines schwarzen Körpers, Annalen der Physik 294 (1896), 662–669. DOI: https://doi.org/10.1002/andp.18962940803
• Planck's law, Wikipedia. https://en.wikipedia.org/wiki/Planck%27s_law
• Wien's displacement law, Wikipedia. https://en.wikipedia.org/wiki/Wien%27s_displacement_law

Motivation

Roughly half of the stars in our galaxy belong to binary star systems: pairs of stars close enough to each other that their mutual gravitational attraction dominates every other influence, and far enough from every other star that the rest of the galaxy can be ignored. Such a pair is the cleanest physical realization of the Newtonian two-body problem, and it is the reason the two-body problem is not merely a textbook exercise: the masses of stars other than the Sun are known almost entirely because binaries can be observed, and the observation is converted into a mass by exactly the chain of reasoning formalized in this mission.

This mission formalizes Section 4.16, "Binary star systems", of Richard Fitzpatrick's Celestial Mechanics lecture notes (University of Texas at Austin), Eqs. (4.108)–(4.119). It is the first mission of a planned series on the same source; the whole series shares the Lean namespace CelestialMechanics.

Setting

Two point masses $m_1, m_2 > 0$ move in $\mathbb{R}^3$ under Newtonian gravity, with position vectors $\mathbf{r}_1(t)$ and $\mathbf{r}_2(t)$ defined for all times $t \in \mathbb{R}$. Write $\mathbf{r} = \mathbf{r}_2 - \mathbf{r}_1$ for the relative separation and $r = \lVert \mathbf{r} \rVert$ for the distance between the stars. The gravitational force the first star exerts on the second is Eq. (4.108),

$$\mathbf{f} = -\frac{G\,m_1 m_2}{r^{3}}\,\mathbf{r},$$

and Newton's second law for each star reads

$$m_1\,\ddot{\mathbf{r}}_1 = \frac{G\,m_1m_2}{r^{3}}\,\mathbf{r}, \qquad m_2\,\ddot{\mathbf{r}}_2 = -\frac{G\,m_1m_2}{r^{3}}\,\mathbf{r}.$$

A pair of twice continuously differentiable, never-colliding trajectories satisfying these two equations is what this mission calls a Newtonian gravitational two-body system.

Three derived objects organize the material. The center of mass is $\mathbf{R} = (m_1\mathbf{r}_1 + m_2\mathbf{r}_2)/(m_1+m_2)$. The relative Kepler problem with gravitational parameter $GM$, $M = m_1+m_2$, is the equation

$$\ddot{\mathbf{r}} = -\frac{G M}{r^{3}}\,\mathbf{r} \tag{4.110}$$

for a nowhere-vanishing curve $\mathbf{r}$. A Keplerian conic orbit with major radius $a$, eccentricity $e$ and angular momentum per unit reduced mass $h$ is a planar curve given in polar coordinates $(\rho, \theta)$ by

$$\mathbf{r} = (\rho\cos\theta,\ \rho\sin\theta,\ 0), \qquad \rho = \frac{a\,(1-e^{2})}{1+e\cos\theta}, \qquad \dot\theta = \frac{h}{\rho^{2}},$$

which are Eqs. (4.112)–(4.114); the elements are tied together by Eq. (4.115), $a = h^{2}/\bigl((1-e^{2})GM\bigr)$.

Target

The goal theorem is an existence-and-description statement: for every $G>0$, every pair of masses $m_1,m_2>0$ and every choice of orbital elements $a>0$, $0 \le e < 1$, there exist trajectories $\mathbf{r}_1, \mathbf{r}_2$, polar functions $\rho, \theta$ and a time $T>0$ such that

$$\text{(i) } \mathbf{r}_1, \mathbf{r}_2 \text{ solve the two-body equations above}; \qquad \text{(ii) } m_1\mathbf{r}_1 + m_2\mathbf{r}_2 = \mathbf{0};$$ $$\text{(iii) } \mathbf{r}_2 - \mathbf{r}_1 \text{ is the Keplerian conic with elements } (a, e, h), \quad h = \sqrt{(1-e^{2})\,G\,(m_1+m_2)\,a};$$ $$\text{(iv) } \mathbf{r}_1 = -\frac{m_2}{m_1+m_2}\,\mathbf{r}, \quad \mathbf{r}_2 = \frac{m_1}{m_1+m_2}\,\mathbf{r}; \qquad \text{(v) } T = \sqrt{\frac{4\pi^{2}a^{3}}{G(m_1+m_2)}} \text{ and both orbits are } T\text{-periodic}.$$

The milestones are the individual steps of Section 4.16, ordered as in the source: the reduction of the two-body system to the one-body problem (4.110)–(4.111); the uniform motion of the center of mass, which makes the center-of-mass frame inertial; the positions of the two stars in that frame (4.118)–(4.119); the verification that the conic (4.112)–(4.115) solves (4.110); the period of revolution (4.116)–(4.117); and the inversion of these relations that yields the two stellar masses from observation.

Significance

The result itself. The theorem is the complete qualitative and quantitative picture of a binary orbit: each star traverses an ellipse about the common center of mass, the two stars are diametrically opposite one another at every instant, the distances from the center of mass are in the fixed ratio $m_2 : m_1$, and the period depends only on the major radius and the total mass. The last two facts are what astronomers use: the measured pair $(a, T)$ gives the mass sum $m_1 + m_2 = 4\pi^{2}a^{3}/(GT^{2})$, the observed ratio of the two apparent orbits gives $m_1/m_2$, and sum plus ratio give the individual masses. The same reduction also supplies the finite-mass correction to one-body solar-system orbit theory, in which $G M_{\odot}$ is replaced by $G(M_{\odot} + m)$.

Formalizing it. The mathematics has been settled since Newton, so the contribution here is a machine-checked development rather than a new result. Mathlib currently has extensive analysis infrastructure — iterated derivatives, ContDiff, Euclidean spaces — but no development of the Kepler problem: neither the conic solution of the inverse-square equation of motion nor Kepler's laws. The reusable output of this mission is therefore a small, self-contained Kepler library: the two-body reduction, the conic solution, and the period law, stated for curves in $\mathbb{R}^3$ in a form that later missions in the series (perturbations, orbital elements, the restricted three-body problem) can import unchanged.

Difficulty

Two milestones carry essentially all of the analytic work.

The first is showing that the conic really solves (4.110). The obvious route — differentiate $\rho(t)$ twice and simplify — runs into the fact that $\rho$ is given as a function of $\theta(t)$ and $\theta$ is given only implicitly, through the angular-momentum law $\dot\theta = h/\rho^{2}$. Even the regularity in the conclusion has to be earned: the hypotheses supply only differentiability of $\theta$, and twice-continuous differentiability of the curve must be bootstrapped from the two polar equations. Getting the Cartesian second derivative into the form $-(GM/\rho^{3})\mathbf{r}$ requires the relation $h^{2} = (1-e^{2})GMa$ at exactly the right place, and this is where a sign or a factor typically goes wrong.

The second is the goal theorem, which is an existence statement and therefore needs the angular equation $\dot\theta = h/\rho(\theta)^{2}$ to be solved globally in time, on all of $\mathbb{R}$ and not merely on a small interval. The right-hand side is smooth and, for $0 \le e < 1$, bounded above and below by positive constants, so the solution exists for all time and advances by $2\pi$ in a fixed time $T$; but "exists for all time" is a real obligation in Lean, and a naive appeal to a local existence theorem does not discharge it.

Formalization scope

Space is EuclideanSpace ℝ (Fin 3), so the norm is the Euclidean one and the three Cartesian components are indexed $0, 1, 2$; the orbital plane is fixed to be the $x$-$y$ plane, exactly as in Eq. (4.112). Trajectories are total functions $\mathbb{R} \to \mathbb{R}^3$: all statements are global in time, and no restriction to an interval or to positive times is made. Derivatives are iteratedDeriv, and smoothness is ContDiff ℝ 2. Masses and $G$ are positive reals wherever the physics needs it, and this is stated explicitly rather than left implicit. Eccentricity is restricted to $0 \le e < 1$ throughout, so only bound (elliptical and circular) orbits are in scope; the parabolic and hyperbolic cases of Sections 4.13–4.15 are left to later missions.

Two trivializing formalizations are ruled out by construction. The definitions never allow the separation to vanish, so no statement is satisfied by a collision; and in the goal theorem the angular momentum $h$ and the period $T$ are not existentially quantified but pinned to their Keplerian values in terms of $(G, m_1+m_2, a, e)$, so the orbit cannot be rescaled to make the conditions easy to meet.

Contributions of independent interest are welcome: conservation of angular momentum and of energy for (4.110), the equal-areas law, the eccentricity (Laplace–Runge–Lenz) vector, and the Kepler equation relating mean and eccentric anomaly all sit naturally on top of this development.

Selected references

• Richard Fitzpatrick, Celestial Mechanics, University of Texas at Austin lecture notes, Chapter 4 "Keplerian orbits", Section 4.16 "Binary star systems", https://farside.ph.utexas.edu/teaching/celestial/Celestial/node38.html. The source of this mission; Eqs. (4.108)–(4.119).
• Isaac Newton, Philosophiæ Naturalis Principia Mathematica, 1687. Book I contains the original solution of the inverse-square two-body problem.