Partial Differential Equations

Motivation

Quantum electrodynamics (QED) is the relativistic quantum field theory of electrodynamics: it describes how light and charged matter interact, and it is the most precisely tested theory in physics, reproducing quantities such as the anomalous magnetic moment of the electron and the Lamb shift of hydrogen to many digits. Its modern covariant formulation was developed by Tomonaga, Schwinger and Feynman, with Dyson showing the equivalence of the operator and diagrammatic approaches.

Every one of those computations starts from a single classical object: the QED action, a functional of a Dirac spinor field and an electromagnetic four-potential on Minkowski space. Perturbation theory, Feynman rules, renormalization and the S-matrix are all built on top of the classical Lagrangian and the structural facts about it — the Clifford algebra of the Dirac matrices, the $U(1)$ gauge symmetry, the conserved Noether current, and the Euler–Lagrange field equations. This mission formalizes exactly that classical layer, in the notation of the "Mathematical formulation" section of the Wikipedia article on quantum electrodynamics.

Nothing quantized is attempted here: no Fock space, no Dyson series, no renormalization. Those require a separate infrastructure and, in the interacting case, are not covered by any complete rigorous construction in four spacetime dimensions. What is formalizable today, and what this mission asks for, is the classical field theory that the quantum theory quantizes.

Setting

Spacetime is $\mathbb{R}^4$ with coordinates $x = (x^0, x^1, x^2, x^3)$ and the Minkowski metric $\eta$ of signature $(+,-,-,-)$: $\eta_{00} = 1$, $\eta_{11} = \eta_{22} = \eta_{33} = -1$, and $\eta_{\mu\nu} = 0$ for $\mu \ne \nu$. Since $\eta$ is its own inverse, the same array serves as the contravariant metric $\eta^{\mu\nu}$ used to raise indices. The symbol $\partial_\mu$ denotes the partial derivative in the $\mu$-th coordinate direction, and $\Box = \eta^{\mu\nu}\partial_\mu\partial_\nu$ is the wave operator.

The Dirac matrices are four complex $4\times4$ matrices $\gamma^0,\dots,\gamma^3$ subject to the Clifford relation

$$\gamma^\mu\gamma^\nu + \gamma^\nu\gamma^\mu = 2\eta^{\mu\nu} I_4$$

together with the hermiticity relation $(\gamma^\mu)^\dagger = \gamma^0\gamma^\mu\gamma^0$, which makes $\gamma^0$ hermitian and $\gamma^1,\gamma^2,\gamma^3$ anti-hermitian. The standard Dirac basis is one concrete solution of these relations.

A spinor field is a map $\psi : \mathbb{R}^4 \to \mathbb{C}^4$; its Dirac adjoint is $\bar\psi = \psi^\dagger\gamma^0$, and for a $4\times4$ matrix $M$ the pairing $\bar\psi M \chi$ is the complex number $\sum_{i,j}\overline{\psi_i}\,(\gamma^0 M)_{ij}\,\chi_j$. A gauge field is a map $A : \mathbb{R}^4 \to \mathbb{R}^4$ whose value $A_\mu(x)$ is the covariant component of the electromagnetic four-potential. From it one forms the field tensor (the curvature of the gauge connection)

$$F_{\mu\nu} = \partial_\mu A_\nu - \partial_\nu A_\mu, \qquad F^{\mu\nu} = \eta^{\mu\alpha}\eta^{\nu\beta}F_{\alpha\beta},$$

and, for a coupling constant $e$, the gauge covariant derivative $D_\mu\psi = \partial_\mu\psi + ieA_\mu\psi$. The Dirac current is $J^\mu = \bar\psi\gamma^\mu\psi$.

With $m$ the mass of the spinor field, the QED Lagrangian density is

$$\mathcal{L} = \bar\psi\,(i\gamma^\mu D_\mu - m)\,\psi - \tfrac{1}{4}F_{\mu\nu}F^{\mu\nu}.$$

Its Euler–Lagrange equations are the Dirac equation $(i\gamma^\mu D_\mu - m)\psi = 0$ and the Maxwell equation $\partial_\mu F^{\mu\nu} = e J^\nu$. The Lorenz gauge condition is $\eta^{\mu\nu}\partial_\mu A_\nu = 0$.

Formalization targets

Goal

For a coupled solution $(\psi, A)$ of the QED field equations in the Lorenz gauge, the four-potential obeys an inhomogeneous wave equation whose source is a conserved current:

$$\Box A^\nu = e\,J^\nu \qquad\text{and}\qquad \partial_\nu J^\nu = 0 .$$

This is the "QED version of the classical Maxwell equations in the Lorenz gauge" of the source, together with the conservation law that makes the source of that wave equation consistent. It fixes no gauge beyond Lorenz, no representation of the Dirac matrices, and no sign or normalization beyond those of the stated Lagrangian.

Supporting targets

$$\gamma^\mu\gamma^\nu+\gamma^\nu\gamma^\mu = 2\eta^{\mu\nu}I_4,\qquad (\gamma^\mu)^\dagger = \gamma^0\gamma^\mu\gamma^0 \quad\text{for the Dirac basis;}$$ $$\partial_\lambda F_{\mu\nu} + \partial_\mu F_{\nu\lambda} + \partial_\nu F_{\lambda\mu} = 0;$$ $$F_{\mu\nu}[A + d\chi] = F_{\mu\nu}[A],\qquad D_\mu\big(e^{-ie\chi}\psi\big)\big[A + d\chi\big] = e^{-ie\chi} D_\mu\psi[A],\qquad \mathcal{L}\big[e^{-ie\chi}\psi, A + d\chi\big] = \mathcal{L}[\psi, A];$$ $$\bar\psi\gamma^\mu\psi \in \mathbb{R},\qquad \partial_\mu(\bar\psi\gamma^\mu\psi) = 0 \ \text{ for solutions of the Dirac equation},\qquad \Box A^\nu = eJ^\nu \ \text{ in Lorenz gauge.}$$

Significance

The classical layer is what every later construction quantizes. The Clifford relation is what makes the Dirac operator a square root of the wave operator; the $U(1)$ invariance of $\mathcal{L}$ is what forces the coupling to be through $D_\mu$ and what makes the current conserved by Noether's theorem; conservation of $J^\mu$ is the consistency condition without which $\partial_\mu F^{\mu\nu} = eJ^\nu$ has no solutions at all, since the left side is annihilated by $\partial_\nu$ identically. The Lorenz-gauge wave equation is the form in which the photon propagator is read off.

Formalizing it adds a reusable, machine-checked Minkowski-space field-theory layer: a metric with index raising, coordinate partial derivatives on $\mathbb{R}^4$ with a wave operator, an abstract Dirac representation together with a concrete basis satisfying it, the field tensor, the covariant derivative, the Dirac current and the QED Lagrangian. Mathlib has Clifford algebras and Fréchet calculus, but not this concrete apparatus. None of the statements in this mission is currently known to have a machine-checked proof; all are standard textbook results with well-understood proofs, so the work is formalization rather than discovery.

Difficulty

The arguments are elementary on paper and awkward in Lean for three separate reasons.

First, all index manipulation is explicit: raising an index is a sum over $\mathrm{Fin}\ 4$, and every "obvious" rearrangement of $\sum_{\mu\alpha\beta}\eta^{\mu\alpha}\eta^{\nu\beta}\partial_\mu\partial_\alpha A_\beta$ has to be done by hand with Finset.sum lemmas.

Second, differentiation is Fréchet differentiation in disguise: $\partial_\mu f$ is the derivative of $f$ evaluated at a basis vector, so the product rule, the sum rule and the symmetry of second derivatives each require the corresponding differentiability side conditions. The naive move of treating $\partial_\mu$ as a formal symbol that commutes with everything fails: without a $C^2$ hypothesis, $\partial_\mu\partial_\nu \ne \partial_\nu\partial_\mu$, and without differentiability the derivative takes the junk value $0$, so an identity that "obviously" holds termwise may hold only under the stated smoothness assumption.

Third, the current conservation law is not a pure computation: it needs the Dirac equation, the hermiticity relation $(\gamma^\mu)^\dagger = \gamma^0\gamma^\mu\gamma^0$, and the reality of $m$, $e$ and $A_\mu$, in the precise combination that cancels the terms containing $A_\mu$ between $\partial_\mu\bar\psi$ and $\partial_\mu\psi$. Any attempt to prove it from smoothness alone, without the equation of motion, cannot work — the current of an arbitrary smooth spinor field is not conserved.

Formalization scope

Spacetime is Fin 4 → ℝ, a gauge field is Spacetime → Fin 4 → ℝ with lower index, a spinor field is Spacetime → Fin 4 → ℂ, and the Dirac matrices are Fin 4 → Matrix (Fin 4) (Fin 4) ℂ. Sums over indices are Finset.sum over Fin 4. Partial derivatives are fderiv ℝ f x (Pi.single μ 1), which is $0$ when $f$ is not differentiable at $x$; smoothness hypotheses are stated as ContDiff ℝ 1 or ContDiff ℝ 2 exactly where they are used. Complex conjugation is starRingEnd ℂ, matrix adjoint is Matrix.conjTranspose, and the coupling constant $e$, the mass $m$ and the gauge parameter $\chi$ are real, with no positivity or nonvanishing assumption on $e$ or $m$.

Conventions fixed once and shared by every statement: signature $(+,-,-,-)$; $D_\mu = \partial_\mu + ieA_\mu$; $F_{\mu\nu} = \partial_\mu A_\nu - \partial_\nu A_\mu$; $J^\mu = \bar\psi\gamma^\mu\psi$ taken as a real number via its real part, with the reality of the underlying complex pairing stated as a separate target; the Maxwell equation carries the coupling on the right-hand side as $\partial_\mu F^{\mu\nu} = eJ^\nu$; and the Dirac equation is $\sum_\mu i\gamma^\mu D_\mu\psi = m\psi$.

The statements are not vacuous: $\psi = 0$, $A = 0$ satisfies all field equations, plane-wave solutions of the free Dirac equation satisfy the Dirac hypothesis with $A = 0$, and the concrete Dirac basis witnesses the abstract representation hypothesis, so no hypothesis in the mission is unsatisfiable. The goal is not trivially true: it asserts a pointwise identity between second derivatives of $A$ and a quadratic expression in $\psi$, not an implication between definitionally equal objects.

A complete development needs Mathlib's fderiv calculus (product rule, symmetry of the second derivative via IsSymmSndFDerivAt), Finset.sum manipulation, Matrix arithmetic over ℂ, and Complex.exp. The Minkowski-space layer — metric, partial derivatives, wave operator, field tensor, Dirac representation — is reusable for any later mission on classical field theory or on the quantized theory. Contributions of further structural results in this notation (energy–momentum tensor, plane-wave solutions, the free-field propagator) are welcome as follow-up problems.

Selected references

• Wikipedia, Quantum electrodynamics, section "Mathematical formulation". https://en.wikipedia.org/wiki/Quantum_electrodynamics
• C. Itzykson and J.-B. Zuber, Quantum Field Theory, McGraw-Hill, 1980.
• M. E. Peskin and D. V. Schroeder, An Introduction to Quantum Field Theory, Addison-Wesley, 1995.
• R. P. Feynman, QED: The Strange Theory of Light and Matter, Princeton University Press, 1985.

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

The Cauchy–Riemann operator $\bar\partial=\partial_s+i\,\partial_t$ on $\mathbb{C}$ is the model elliptic operator of symplectic topology: pseudoholomorphic curves solve nonlinear perturbations of $\bar\partial u=0$, and their regularity, compactness and Fredholm theory all start from an $L^p$ a priori estimate for $\bar\partial$. In Hofer–Wysocki–Zehnder's asymptotic analysis of pseudoholomorphic curves in symplectisations, this estimate appears as formula (49): on a disc $B$ of radius $R$, every smooth map $\varphi$ supported in the interior of $B$ satisfies

$$\|\varphi\|_{W^{k,p}(B)}\le M(k,p,R)\,\|\bar\partial\varphi\|_{W^{k-1,p}(B)},\qquad k\ge1,\ p>1 .$$

Hofer–Wysocki–Zehnder cite it from E. M. Stein's Singular Integrals and Differentiability Properties of Functions and from Abbas–Hofer's Holomorphic Curves and Global Questions in Contact Geometry.

This mission formalizes estimate (49), together with the core of the real-variable theory of singular integrals on $\mathbb{R}^d$ from Stein, Chapters I–III, and the $L^2$ and $L^p$ estimates for ar\partial of Abbas–Hofer, § 4.2. None of these results is in Mathlib, which has no Hardy–Littlewood maximal function, no Calderón–Zygmund decomposition, no Marcinkiewicz interpolation theorem and no $L^p$ theory of singular integral operators.

Setting

• $\mathbb{R}^d$ carries Lebesgue measure $m$, and $\|\cdot\|_p$ is the $L^p(\mathbb{R}^d)$ norm for complex-valued functions.
• Maximal function. $Mf(x)=\sup_{r>0}m(B(x,r))^{-1}\int_{B(x,r)}|f|\in[0,\infty]$.
• Weak type. An operator $T$ is of weak type $(q,q)$, $q<\infty$, if $m\{|Tf|>\alpha\}\le(A\|f\|_q/\alpha)^q$ for all $\alpha>0$, and of strong type $(p,p)$ if $\|Tf\|_p\le A\|f\|_p$.
• Truncated singular integrals. For a kernel $K$ on $\mathbb{R}^d\setminus\{0\}$ and $\varepsilon>0$, $T_\varepsilon f(x)=\int_{|y|\ge\varepsilon}f(x-y)K(y)\,dy$.
• Cauchy–Riemann operator. For $\varphi:\mathbb{C}\to\mathbb{C}^n$ and $z=s+it$, $\bar\partial\varphi=\varphi_s+i\varphi_t$ (without the factor $\tfrac12$).
• Sobolev norms of smooth maps on a set $U\subset\mathbb{C}$: $\|\varphi\|_{W^{k,p}(U)}=\sum_{j\le k}\|D^j\varphi\|_{L^p(U)}$, where $D^j\varphi$ is the $j$-th derivative.

Formalization targets

Goal: the $W^{k,p}$ estimate for $\bar\partial$ on a disc

For an integer $k\ge1$, $p>1$ and $R>0$ there is $M=M(k,p,R)$ such that for every disc $B\subset\mathbb{C}$ of radius $R$ and every smooth $\varphi:\mathbb{C}\to\mathbb{C}^n$ supported in the interior of $B$, $\|\varphi\|_{W^{k,p}(B)}\le M\|\bar\partial\varphi\|_{W^{k-1,p}(B)}$ (Hofer–Wysocki–Zehnder I, estimate (49), p. 366).

Milestones

1. Maximal theorem. $Mf$ is finite a.e. for $f\in L^p$, $1\le p\le\infty$; $M$ is of weak type $(1,1)$ and of strong type $(p,p)$ for $1<p\le\infty$ (Stein I, § 1.3, Theorem 1).
2. Calderón–Zygmund decomposition. A non-negative integrable $f$ and a height $\alpha>0$ give $\mathbb{R}^d=F\cup\Omega$ with $f\le\alpha$ a.e. on $F$ and $\Omega$ a union of cubes with disjoint interiors on which the average of $f$ lies in $(\alpha,2^d\alpha]$ (Stein I, § 3.2, Theorem 4).
3. Marcinkiewicz interpolation theorem. A sub-additive operator of weak types $(1,1)$ and $(r,r)$, $1<r\le\infty$, is of strong type $(p,p)$ for $1<p<r$ (Stein I, § 4.2, Theorem 5).
4. Convolution kernels with bounded Fourier transform. If $K\in L^2$, $|\hat K|\le B$ and $|\nabla K(x)|\le B|x|^{-d-1}$, then $f\mapsto K*f$ is bounded on $L^p$, $1<p<\infty$, with a constant depending only on $p$, $B$, $d$ (Stein II, § 2.2, Theorem 1).
5. Truncated singular integrals. If $|K(x)|\le B|x|^{-d}$, $\int_{|x|\ge2|y|}|K(x-y)-K(x)|\,dx\le B$ and $K$ has integral zero over every annulus, then the truncations $T_\varepsilon$ are bounded on $L^p$ uniformly in $\varepsilon$ and converge in $L^p$ as $\varepsilon\to0$ (Stein II, § 3.2, Theorem 2).
6. Homogeneous kernels. The same conclusion for $K(y)=\Omega(y)/|y|^d$ with $\Omega$ homogeneous of degree $0$, of mean zero on the unit sphere and Dini-continuous there (Stein II, § 4.2, Theorem 3 (a), (b)).
7. The Cauchy–Riemann estimate on the plane. $\|\partial_1f\|_p+\|\partial_2f\|_p\le A_p\|\partial_1f+i\partial_2f\|_p$ for compactly supported $C^1$ functions $f:\mathbb{R}^2\to\mathbb{C}$, $1<p<\infty$ (Stein III, § 1.3, Proposition 4).
8. $L^2$ identity. $\|\bar\partial\varphi\|_{L^2}^2=\|\varphi_s\|_{L^2}^2+\|\varphi_t\|_{L^2}^2$ for smooth compactly supported $\varphi:\mathbb{C}\to\mathbb{C}^n$ (Abbas–Hofer, § 4.2, (4.4)).
9. $L^2$ estimate on a disc. $\|\varphi_s\|_{L^2}^2+\|\varphi_t\|_{L^2}^2+\|\varphi\|_{L^2}^2\le(4R^2+1)\|\bar\partial\varphi\|_{L^2}^2$ for $\varphi$ with compact support in $B_R(0)$ (Abbas–Hofer, Theorem 4.2.1).
10. $L^p$ estimate on a disc. $\|\varphi\|_{W^{1,p}}\le c(p,R)\|\bar\partial\varphi\|_{L^p}$ for $\varphi$ with compact support in $B_R(0)$, $1<p<\infty$ (Abbas–Hofer, Theorem 4.2.2).

Significance

The result. The $W^{k,p}$ estimate for $\bar\partial$ is the analytic input behind elliptic bootstrapping for pseudoholomorphic curves: interior regularity, $C^\infty$ bounds from gradient bounds, removal of singularities, and the Fredholm theory of linearized Cauchy–Riemann operators on Sobolev spaces. In Hofer–Wysocki–Zehnder's work it controls the derivatives of pseudoholomorphic half-cylinders near a nondegenerate periodic orbit.

Formalizing it. The milestones from Stein are the standard real-variable toolkit of harmonic analysis on $\mathbb{R}^d$: the maximal theorem, the Calderón–Zygmund decomposition, Marcinkiewicz interpolation and the $L^p$ theory of singular integrals with smooth or homogeneous kernels. None of them is in Mathlib, and each is reusable well beyond this mission, for instance for elliptic estimates of other operators, Sobolev embeddings in $L^p$, and other $L^p$ estimates.

Difficulty

The statements are quantitative and the order of quantifiers matters: the constants are chosen before the functions, and in milestones 3 and 4 also before the operator or the kernel, with the dependence stated by the source. Several objects take infinite values or are defined only almost everywhere: the maximal function is valued in $[0,\infty]$, the case $r=\infty$ of the interpolation theorem uses a strong-type bound in place of a weak-type one, and the singular integrals are limits in $L^p$ of absolutely convergent truncated integrals. The Dini condition on $\Omega$ is a condition on a supremum over pairs of points of the unit sphere. The Cauchy–Riemann statements involve vector-valued maps $\mathbb{C}\to\mathbb{C}^n$, real derivatives of all orders and Sobolev norms on discs.

Formalization scope

• Namespace DbarRegularity. The definition module DbarRegularity_Setting defines maximalFunction, closedCube, dbar and sobolevNorm. The mission is standalone and imports no definitions from other missions.
• Spaces. $\mathbb{R}^d$ is EuclideanSpace ℝ (Fin d) with volume, functions on it are complex-valued, $\mathbb{R}^2$ in milestone 7 is EuclideanSpace ℝ (Fin 2), and $\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n). Stein's dimension is written $d$ throughout, and $n$ is the dimension of the target $\mathbb{C}^n$.
• Norms and exponents. $L^p$ norms are eLpNorm in ℝ≥0∞. Exponents $1<p<\infty$ are real and enter as ENNReal.ofReal p; exponents allowed to be infinite are in ℝ≥0∞. Constants are in ℝ≥0 or ℝ, never in ℝ≥0∞.
• Derivatives. $\varphi_s$, $\varphi_t$ are fderiv ℝ φ z 1, fderiv ℝ φ z Complex.I; smoothness is ContDiff ℝ ∞ ($C^\infty$, not analytic); higher derivatives are iteratedFDeriv ℝ j. Supports are tsupport.
• Limits. Limits as $\varepsilon\to0$ are along 𝓝[>] 0, in the $L^p$ seminorm.

Contributions welcome: reusable general lemmas of real-variable harmonic analysis on $\mathbb{R}^d$, and calculus lemmas for smooth compactly supported maps on $\mathbb{C}$.

Selected references

• E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), Chapters I–III. ISBN 0-691-08079-8.
• C. Abbas, H. Hofer, Holomorphic Curves and Global Questions in Contact Geometry, Birkhäuser Advanced Texts Basler Lehrbücher, Birkhäuser (2019), § 4.2. https://doi.org/10.1007/978-3-030-11803-7
• H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations I: asymptotics, Ann. Inst. H. Poincaré Anal. Non Linéaire 13(3) (1996), 337–379. http://www.numdam.org/item/AIHPC_1996__13_3_337_0/
• A. P. Calderón, A. Zygmund, On the existence of certain singular integrals, Acta Math. 88 (1952), 85–139. https://doi.org/10.1007/BF02392130

Motivation

Gustafson, Meinert and Melcher construct axisymmetric saddle points of the micromagnetic energy of a spherical shell in two ways (a heat flow, and continuation from an explicit solution at $\kappa=4$). Their Remark 3.18 conjectures that a single uniqueness statement identifies the two; it is problem 241 of the AIM open problem list.

Timeline. 2016: Kravchuk et al. propose the model. 2025: Gustafson–Meinert–Melcher construct the saddle points and state the conjecture.

Setting

For anisotropy $\kappa>0$ the energy of $m:S^2\to S^2$ is $\mathcal E_\kappa(m)=\frac12\int_{S^2}|\nabla m|^2+\kappa\,(1-(m\cdot x)^2)$. An axisymmetric field $m=(\sin h\cos\varphi,\ \sin h\sin\varphi,\ \cos h)$ with profile $h(\theta)$ is critical exactly when

$$h''+\cot\theta\,h'-\frac{\sin 2h}{2\sin^2\theta}-\frac{\kappa}{2}\sin(2h-2\theta)=0\qquad(0<\theta<\pi).\tag{2.6}$$

The hemispheric class $H_{0,2}$ adds $h(0)=0$, $h(\pi)=2\pi$, $h(\pi-\theta)=2\pi-h(\theta)$.

Formalization target

For every $\kappa\ge4$ there is exactly one smooth profile in $H_{0,2}$ that solves (2.6) and induces a smooth map $S^2\to S^2$. The statement may be proved or disproved.

Significance

Uniqueness would identify the two constructions as one saddle branch; a counterexample would give further degree-zero critical points of $\mathcal E_\kappa$.

Difficulty

(2.6) is singular at both poles and $H_{0,2}$ is a two-point boundary condition, so standard ODE uniqueness does not apply, and the paper's comparison arguments only control solutions in the wedge $\theta\le h\le 2\theta$. Numerical evidence (shooting) finds at $\kappa=4$, besides $h=2\theta$, a second solution in the class with $h'(0)\approx3.899$ (similarly at $\kappa=5,8$), which leaves the wedge.

Formalization scope

Profiles are functions $h:\mathbb R\to\mathbb R$; all conditions, and the uniqueness, are imposed on $[0,\pi]$ only (values outside are unconstrained, so uniqueness on $\mathbb R$ would be trivially false). Smoothness is ContDiffOn ℝ ∞ on $[0,\pi]$. "Induces a smooth map" means the field extended to $\mathbb R^3\setminus\{0\}$ as a function of $x/|x|$ is $C^\infty$ there; this excludes profiles with a cone singularity at a pole. The paper's $H_{0,2}$ uses piecewise $C^1$ profiles; by its Corollary 2.7 it has the same solutions.

Selected references

• S. Gustafson, D. Meinert, C. Melcher, Saddle Point Configurations for Spherical Ferromagnets, preprint, 2025. arXiv:2509.05159
• V. P. Kravchuk et al., Topologically stable magnetization states on a spherical shell: Curvature-stabilized skyrmions, Phys. Rev. B 94, 144402, 2016. DOI
• AIM open problems list, problem 241. github.com/MColbrook/AIM