Differential Geometry

Motivation

Flatly Foliated Relativity (FFR) is a theory of gravity introduced by Bray, Hamm, Hirsch, Wheeler and Zhang (arXiv:1911.00967, 2019) that sits between special and general relativity. It keeps the Einstein–Hilbert action of general relativity (GR) but restricts it to spacetimes that are foliated by flat Euclidean spaces (Assumption 1 of the paper): "matter curves spacetime, but not space". The authors motivate this by the observed spatial flatness of the local universe. Since gravitational waves are excluded, FFR is proposed as an approximation of GR whose metric equations are much more tractable. It still contains the big bang (FLRW spacetimes with $k = 0$), accelerated expansion and the exterior Schwarzschild spacetime.

One headline feature of the theory is how a positive cosmological constant $\Lambda > 0$ (Assumption 2) shapes it. For $\Lambda>0$ the paper shows that the FFR metric equations are elliptic on every slice, that the mean curvature of the foliation gives a geometric arrow of time, and that there is exactly one vacuum solution among solutions that are spherically symmetric at infinity. For $\Lambda=0$ uniqueness fails, and for $\Lambda<0$ existence fails. This mission formalizes Sections 3.2–5 of the paper, which contain these statements.

Setting

All FFR equations live on a single flat slice $\mathbb R^3_t$, with no time derivatives, so the formalization works on $\mathbb R^3$ with coordinates $x_1,x_2,x_3$. The spacetime metric is

$$g = (-\eta^2+|\omega|^2)\,dt^2-(\omega\otimes dt+dt\otimes\omega)+\delta_{\mathbb R^3},$$

where $\eta>0$ is the lapse and $\omega$ is a one-form on $\mathbb R^3$, identified with a vector field through the flat metric. Matter enters through the energy density $\mu$ and the momentum density $J$. Writing $\omega_{i,j}=\partial_j\omega_i$, $\nabla\cdot\omega=\omega_{i,i}$ and $\Delta$ for the flat Laplacian (summation over repeated indices), the FFR equations (34)–(35) are

$$2\Lambda+16\pi\mu=\frac1{\eta^2}\Big[(\nabla\cdot\omega)^2-\tfrac14\|\omega_{i,j}+\omega_{j,i}\|^2\Big],$$ $$16\pi J_i=\frac1\eta\big(\Delta\omega_i-\partial_i(\nabla\cdot\omega)\big)+\frac2{\eta^2}(\nabla\cdot\omega)\eta_i-\frac1{\eta^2}(\omega_{i,j}+\omega_{j,i})\eta_j .$$

Substituting $\omega=df+\zeta$ with $\nabla\cdot\zeta=0$ gives the elliptic form (39)–(41), with unknowns $(f,\zeta,\eta)$. Here $Q_{ij}=f_{ij}+\tfrac12(\zeta_{i,j}+\zeta_{j,i})$:

$$(\Delta f)^2-\|Q\|^2=(16\pi\mu+2\Lambda)\eta^2,$$ $$\Delta\zeta_i=16\pi J_i\eta-\tfrac2\eta(\Delta f\,\delta_{ij}-Q_{ij})\eta_j,$$ $$(\Delta f\,\delta_{ij}-Q_{ij})\eta_{ij}=8\pi\nabla\cdot(J\eta^2),$$

together with the requirement $\nabla\cdot\zeta\to0$ at infinity. Vacuum means $\mu=0$ and $J=0$. When $\Lambda>0$, the paper fixes the time orientation by the arrow-of-time convention $K=(\nabla\cdot\omega)/\eta=\Delta f/\eta>0$ (Convention 1). A pair $(\omega,\eta)$ is spherically symmetric at infinity if it is spherically symmetric on $\{r\ge r_0\}$ for some $r_0>0$. Two vacuum solutions count as the same if they differ by an overall positive constant factor, which corresponds to rescaling $t$.

Formalization targets

Goal: Corollary 2

For $\Lambda>0$, the pair $\omega=\sqrt{\Lambda/3}\,r\,\partial_r$, $\eta=1$ is a smooth vacuum solution that is spherically symmetric at infinity. Every smooth vacuum solution with $\eta>0$ and $(\nabla\cdot\omega)/\eta>0$ that is spherically symmetric at infinity has the form

$$\eta\equiv c,\qquad \omega=c\sqrt{\Lambda/3}\;x\qquad(c>0).$$

Milestones

Theorem 2 (equivalence with the elliptic form), Theorem 3 (arrow of time), Theorem 4 (ellipticity inequality), Lemma 1 (symmetrization), identity (82)–(83), Theorem 5 (uniqueness for the elliptic form under approximate spherical symmetry), Lemma 2 ($\Lambda=0$: many vacua) and Lemma 3 ($\Lambda<0$: no vacuum).

Significance

Corollary 2 is the fourth claim of the paper's main result (Theorem 1). It is the precise sense in which FFR with $\Lambda>0$ is rigid, in contrast to GR, which has many vacuum solutions that are spherically symmetric at infinity (gravitational waves). Together with Lemmas 2 and 3, it singles out the sign of $\Lambda$ as the parameter that controls existence and uniqueness. The intermediate results are of independent use. Theorem 2 lets the elliptic system replace the original one, Theorem 4 is the ellipticity statement behind the existence question posed in the paper (Question 1), and Lemma 1 is a symmetrization inequality for the $2$-Hessian operator $\sigma_2(\nabla^2 f)$.

These are paper proofs. No machine-checked version of any of them is known to the proposer. The mission asks for a complete formal proof of the goal and the milestones in Lean 4 with Mathlib.

Difficulty

The algebra is elementary. The difficulty is analytic. The uniqueness arguments rest on maximum principles for the elliptic equations (41) and (45) on all of $\mathbb R^3$ under conditions at infinity, on Liouville-type arguments for harmonic functions, and on a Newtonian-potential representation (convolution with the Green's function of $\Delta$) used to show $\zeta\to0$. Lemma 1 needs averaging over rotations (spherical symmetrization), Jensen's inequality and a characterization of its equality case. Theorem 5 then needs a divergence-theorem argument on large balls that is controlled only by the approximate symmetry hypothesis. Mathlib provides the divergence theorem on boxes and some harmonic-function theory, but no ready-made maximum principle for second-order elliptic operators with variable coefficients on $\mathbb R^n$.

Formalization scope

• Space is EuclideanSpace ℝ (Fin 3). One-forms $\omega,\zeta,J$ are vector fields $\mathbb R^3\to\mathbb R^3$, and the paper's $\omega$ is written w in Lean. Partial derivatives are fderiv applied to the standard basis vectors. Because fderiv returns $0$ at non-differentiable points, every statement assumes smoothness (ContDiff ℝ ∞) of all fields, as the paper does.
• "Spherically symmetric" means invariance (for scalars) or equivariance (for one-forms) under all linear isometries of $\mathbb R^3$. Because $SO(3)$ acts transitively on spheres, this is equivalent to rotational symmetry.
• The spherical symmetrization $\bar f(x)$ is the average of $f$ over the sphere of radius $|x|$, taken with respect to the surface measure volume.toSphere. "Approximately spherically symmetric at $\infty$" is read as: $f-\bar f$ is bounded and $r^2\,\|\nabla^2(f-\bar f)\|\,\|\nabla(f-\bar f)\|\to0$ uniformly as $r\to\infty$, using operator norms.
• The arrow-of-time convention $\Delta f/\eta>0$ (respectively $(\nabla\cdot\omega)/\eta>0$) is an explicit hypothesis wherever the paper invokes it. Without it, $f\mapsto-f$ (time reversal) produces a second solution.
• Existence parts are stated with explicit witnesses. A formalization that drops smoothness, $\eta>0$ or the convention would be trivial or false, and is not acceptable.
• Contributions such as maximum principles, Liouville theorems and spherical averaging in $\mathbb R^n$ are reusable well beyond this mission and are welcome as separate lemmas.

Selected references

• H. L. Bray, B. Hamm, S. Hirsch, J. Wheeler, Y. Zhang, Flatly Foliated Relativity, arXiv:1911.00967v2, 2019. https://arxiv.org/abs/1911.00967
• L. Caffarelli, L. Nirenberg, J. Spruck, The Dirichlet problem for nonlinear second order elliptic equations, III: Functions of the eigenvalues of the Hessian, Acta Mathematica 155 (1985), 261–301 (cited in the paper for the existence theory of the $J=0$ case).
• J. Corvino, R. M. Schoen, On the asymptotics for the vacuum Einstein constraint equations, Journal of Differential Geometry 73(2) (2006), 185–217 (cited in the paper for the comparison with GR).

Motivation

Mirror symmetry began as an empirical observation in string theory: certain pairs $(X,Y)$ of Calabi–Yau threefolds, with no evident geometric relation, give rise to the same physical theory, and invariants that are hard to compute on $X$ (counts of holomorphic curves) turn into easy computations on $Y$ (variations of complex structure). The paper Mirror symmetry is T-duality by A. Strominger, S.-T. Yau and E. Zaslow, Nucl. Phys. B 479 (1996) 243–259, proposed the first structural explanation: $X$ should carry a fibration by special Lagrangian 3-tori, the mirror $Y$ should be obtained by replacing each fibre with its dual torus, and the mirror map should be fibrewise T-duality. This proposal is now called the SYZ conjecture, and it organises most later geometric work on mirror symmetry.

The string-theoretic argument of Sections 1–2 of the paper is heuristic and is not formalizable as stated. Section 3 is different: it is a self-contained piece of differential geometry about the moduli space of a special Lagrangian submanifold together with a flat $U(1)$ connection on it. This mission formalizes Section 3.

A short timeline of the mathematics the section rests on:

• Harvey and Lawson, Calibrated geometries (Acta Math. 148, 1982), introduced special Lagrangian submanifolds as a calibrated geometry in a Calabi–Yau manifold.
• R. McLean, Deformations of calibrated submanifolds (Duke preprint 96-01, 1996; Comm. Anal. Geom. 6 (1998) 705–747), proved that the space of deformations of a compact special Lagrangian submanifold $L$ is a smooth manifold of dimension $b_1(L)$, whose tangent space at $L$ is the space of harmonic $1$-forms on $L$. The paper cites this as its reference [7].
• SYZ (1996), Section 3, add the moduli of flat $U(1)$ connections, exhibit an $L^2$ metric $g_{ab}$ and a compatible almost complex structure $\mathcal J$ on the resulting $2b_1$-dimensional moduli space $\mathcal M$, derive the identity $\partial_a g_{bc} = \partial_b g_{ac}$ (their Eq. (3.4)), and conclude that $\mathcal M$ is Kähler. They also exhibit a natural $n$-form $\Theta$ on $\mathcal M$, holomorphic when the brane is a torus.
• N. Hitchin, The moduli space of special Lagrangian submanifolds (Ann. Scuola Norm. Sup. Pisa 25, 1997), gave a rigorous treatment in which the McLean metric is Hessian with respect to natural affine structures — the coordinate-free counterpart of Eq. (3.4).

Setting

Fix $n \ge 1$. The ambient Calabi–Yau manifold is modelled by $\mathbb C^n$, carrying

• the Riemannian metric $g(u,v) = \operatorname{Re}\langle u, v\rangle$,
• the complex structure $J u = i u$,
• the Kähler form $\omega(u,v) = \operatorname{Im}\langle u,v\rangle$, which equals $g(Ju, v)$,
• the holomorphic volume form $\Omega = dz^1 \wedge \cdots \wedge dz^n$, evaluated on $n$ vectors as the complex determinant of the matrix they span, and its imaginary part $\kappa = \operatorname{Im}\Omega$.

Here $\langle\cdot,\cdot\rangle$ is the standard Hermitian product of $\mathbb C^n$, conjugate-linear in its first argument.

The brane $L$ is an $n$-torus. It is presented by its universal cover: a map $f : \mathbb R^n \to \mathbb C^n$ that is periodic up to translation,

$$f(x + e_a) = f(x) + \lambda_a, \qquad a = 1,\dots,n,$$

for a fixed family of periods $\lambda_1,\dots,\lambda_n \in \mathbb C^n$. Such an $f$ is exactly a map of the torus $\mathbb R^n/\mathbb Z^n$ into the complex torus $\mathbb C^n/\Lambda$, and integration over $L$ is integration over the unit cube $[0,1]^n$.

Write $\partial_i f$ for the partial derivatives of $f$. The map $f$ is Lagrangian at $x$ if $\omega(\partial_i f, \partial_j f) = 0$ for all $i,j$, i.e. $f^{*}\omega = 0$; it is special Lagrangian if in addition $\kappa(\partial_1 f, \dots, \partial_n f) = 0$, i.e. $f^{*}\kappa = 0$. This is the supersymmetry condition of the paper (Section 2, conditions (ii) and (iii)). The induced metric is $g_{ij} = g(\partial_i f, \partial_j f)$, the volume density is $\sqrt{\det g}$, and the second fundamental form of a Lagrangian immersion is the totally symmetric tensor

$$h_{ijk} = \omega(\partial_i \partial_j f, \partial_k f).$$

Given a family $f_t$ of such maps, its deformation $1$-form is

$$\theta_i = \omega\!\left(\tfrac{\partial f}{\partial t}, \partial_i f\right),$$

the $1$-form obtained by contracting the velocity into the Kähler form. For an $m$-parameter family $F : \mathbb R^m \to (\mathbb R^n \to \mathbb C^n)$, $t \mapsto f_t$, one gets $m$ such forms $\theta^a$, $a = 1,\dots,m$, one per moduli direction.

The moduli data of Section 3 is a smooth $m$-parameter family $F$ of special Lagrangian tori, all with the same periods, subject to two normalizations taken from the paper: each $\theta^a(t)$ is harmonic for the induced metric $g(t)$ (closed and co-closed), and the cohomology class of each $\theta^a$ is constant along the family. The $L^2$ (McLean) metric on the moduli parameters is

$$g_{ab}(t) \;=\; \int_{L} g^{ij}\,\theta^a_i\,\theta^b_j \; \sqrt{\det g}\; d^n x .$$

The full moduli space $\mathcal M$ of the paper also records the flat $U(1)$ connection; its moduli form a torus of the same dimension, with coordinates $s^a$. On $\mathcal M$, modelled by $\mathbb R^m \times \mathbb R^m$ with coordinates $(t^a, s^a)$, the paper puts the block-diagonal metric $G = g_{ab}(dt^a dt^b + ds^a ds^b)$ and the constant almost complex structure $\mathcal J(\partial_{t^a}) = \partial_{s^a}$, $\mathcal J(\partial_{s^a}) = -\partial_{t^a}$, with fundamental $2$-form $\omega_{\mathcal M}(X,Y) = G(\mathcal J X, Y)$.

Target

The goal theorem is the conclusion of Section 3: for every such family, the fundamental $2$-form of the moduli space is closed,

$$d\,\omega_{\mathcal M} = 0,$$

and since $\mathcal J$ is constant in these coordinates it is integrable, so $(\mathcal M, G, \mathcal J)$ is Kähler.

The milestones are the numbered intermediate results of the paper, in the paper's own order:

$$\textbf{Prop. 1:}\quad \frac{d}{dt} f_t^{*}\omega = d\theta .$$ $$\textbf{Prop. 2:}\quad \frac{d}{dt} f_t^{*}\kappa = -\,d(\ast\theta), \quad\text{so}\quad \frac{d}{dt} f_t^{*}\kappa = 0 \iff d^{\dagger}\theta = 0 .$$ $$\textbf{Prop. 4:}\quad \frac{d}{dt} g_{ij} = 2\,h_{ijk}\,w^{k}\quad\text{for the flow } \dot f = J f_{*} w .$$ $$\textbf{Eq. (A.2):}\quad \partial_a \theta^b \text{ is exact.}$$ $$\textbf{Eq. (3.4):}\quad \partial_a g_{bc} = \partial_b g_{ac}.$$

$$\textbf{$\Theta$ closed:}\quad \partial_c \int_L \theta^{a_1}\wedge\cdots\wedge\theta^{a_n} = 0 .

$$$$

\textbf{Hessian} \Rightarrow \textbf{Kähler:}\quad \partial_a g_{bc} = \partial_b g_{ac} ;\Longrightarrow; d,\omega_{\mathcal M} = 0 .$$

Together, Propositions 1 and 2 are the statement that the tangent space to the moduli space consists of harmonic $1$-forms — McLean's theorem in the form the paper uses it. Eq. (3.4) is the technical heart, and the last milestone is the step from it to the goal.

Significance

The result. Section 3 supplies the only rigorous mathematics in the paper. It says that the object the physics predicts to be a Calabi–Yau manifold — the moduli space of a supersymmetric brane — does carry the first piece of that structure, a Kähler metric, and that it carries a natural $n$-form which, for toroidal branes, is a holomorphic $b_1$-form and hence a candidate for the Calabi–Yau form of the mirror. Eq. (3.4) says the McLean metric is locally the Hessian of a potential; this affine-Hessian structure of the SYZ base is the starting point of the later large-complex-structure-limit programme.

Formalizing it. The Section 3 results have rigorous published proofs (McLean for the tangent space, Hitchin for the Hessian property), but no machine-checked proof exists for any of them, and Mathlib currently has no special Lagrangian geometry, no Hodge theory, and no differential forms on manifolds. The mission therefore also produces reusable infrastructure: a workable coordinate model of calibrated submanifold geometry, the variation formulas for the induced metric and for the pullbacks of $\omega$ and $\kappa$, and the Hessian-metric criterion for a Kähler structure, which is independent of the rest and reusable wherever affine-Kähler geometry appears.

Difficulty

The obvious approach to the goal — "the metric is Hessian, so take the potential and write down the Kähler form" — is not available: the potential is not part of the data, and producing it requires the symmetry $\partial_a g_{bc} = \partial_b g_{ac}$ first. That symmetry is the hard step, and it is hard for a specific reason: differentiating $g_{bc}(t) = \int_L g^{ij}\theta^b_i\theta^c_j \sqrt{\det g}$ in the direction $t^a$ produces four terms — from $\theta^b$, from $\theta^c$, from the inverse metric $g^{ij}$, and from the volume density — and only their sum is symmetric in $(a,b)$. Two of them are killed by an integration by parts that needs both harmonicity of $\theta$ and compactness of $L$ (this is where the torus, and not a coordinate patch, is essential); one is killed because a special Lagrangian submanifold is minimal, so the mean curvature term in $\partial_a \sqrt{\det g}$ vanishes; what survives is $-2\int_L h_{ijk} w_a^i w_b^j w_c^k$, which is symmetric because $h$ is a symmetric $3$-tensor. Every one of those four cancellations has to be carried out.

Proposition 2 carries a separate difficulty: it is an identity between the variation of a determinant and a divergence, and it is false without the hypothesis that $f_t$ is special Lagrangian at the point in question — for a merely Lagrangian $f$ there is a further term proportional to the Lagrangian angle.

Formalization scope

The formalization commits to the following, all of which are visible in the definition item and none of which are silent:

• The ambient Calabi–Yau is flat. Sections 2 and 3 of the paper work with a general Calabi–Yau; here the ambient space is $\mathbb C^n$ (equivalently, after imposing periodicity, a flat complex torus $\mathbb C^n/\Lambda$). This is the semi-flat/large-complex-structure regime in which the paper's own Section 2 check is carried out, and it is the price of Mathlib having no differential forms on manifolds. Propositions 1, 2 and 4 are stated for arbitrary smooth maps $\mathbb R^n \to \mathbb C^n$ and are genuinely local, so for them the restriction only removes the ambient curvature terms that the paper also drops by working in normal coordinates. The moduli-level statements do use the flat ambient.
• The brane is a torus, presented by periodicity up to a fixed period lattice; $L^2$ pairings are integrals over $[0,1]^n$ against Lebesgue measure. Compactness is used, and cannot be dropped.
• Derivatives are Fréchet derivatives of maps on $\mathbb R^k$ contracted with a standard basis vector. Lean's fderiv returns $0$ at a point of non-differentiability, so a statement about derivatives of a non-smooth map is a statement about zeros; every item therefore carries an explicit smoothness hypothesis, and the moduli-level items carry it inside the family structure.
• Matrix inversion and square roots are total. The inverse of a singular matrix is $0$ and the square root of a negative real is $0$ in Lean. The items that use $g^{ij}$ or $\sqrt{\det g}$ therefore carry an explicit immersion hypothesis $\det g \ne 0$.
• Closedness of a $2$-form is the Palais formula on constant vector fields, $d\omega(X,Y,Z) = X\,\omega(Y,Z) + Y\,\omega(Z,X) + Z\,\omega(X,Y)$, which is the exterior derivative because the fields are constant. Closedness is asserted for all triples of tangent vectors at all points.
• Non-triviality. The hypotheses are satisfiable: for $\lambda_a$ the standard real basis vectors of $\mathbb C^n$, the family $F(t)(x) = x + i t$ of flat real subtori of $\mathbb C^n/\Lambda$ meets every condition of the family structure, with $\theta^a_i = -\delta^a_i$ and $g_{ab} = \delta_{ab}$. The goal is therefore not vacuous, and it is also not trivially true: $\mathcal{J}$ is constant but $g_{ab}$ is not, so $d\omega_{\mathcal M}=0$ is a genuine condition on the family.

A complete development needs, beyond the definition item: the chain and product rules for fderiv on $\mathbb R^k$, symmetry of second derivatives, differentiation under the integral sign on a compact box, integration by parts for periodic functions on $[0,1]^n$, and the derivative of $\det$ and of matrix inversion. The last two, and the Hessian-implies-Kähler milestone, are reusable outside this mission. Contributions that replace the flat ambient by a general Kähler ambient chart, or that lift the model to Mathlib manifolds once differential forms exist there, are welcome and would supersede parts of this development.

Selected references

• A. Strominger, S.-T. Yau, E. Zaslow, Mirror symmetry is T-duality, Nuclear Physics B 479 (1996) 243–259. doi:10.1016/0550-3213(96)00434-8, arXiv:hep-th/9606040
• R. Harvey, H. B. Lawson, Calibrated geometries, Acta Mathematica 148 (1982) 47–157. doi:10.1007/BF02392726
• R. C. McLean, Deformations of calibrated submanifolds, Communications in Analysis and Geometry 6 (1998) 705–747. doi:10.4310/CAG.1998.v6.n4.a4
• N. J. Hitchin, The moduli space of special Lagrangian submanifolds, Annali della Scuola Normale Superiore di Pisa 25 (1997) 503–515. arXiv:dg-ga/9711002

Motivation

The local theory of curves describes what happens near one point; the global theory asks what a curve must satisfy because it closes up. Two classical statements make the difference visible. The isoperimetric inequality says that among all simple closed plane curves of a given length, the circle encloses the largest area — a question already settled in intent by the Greeks, but given a satisfactory proof only in the nineteenth century, and the short proof reproduced by do Carmo is E. Schmidt's from 1939. The four-vertex theorem says that the curvature of a simple closed convex curve has at least four critical points, so no convex oval has the curvature profile of a curve that just rises and falls once.

The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §1-7, "Global Properties of Plane Curves" (pp. 31–46): the area formula, equation (1) on p. 33; the isoperimetric inequality, Theorem 1 on p. 34; the theorem of turning tangents on p. 37; the lemma, equation (5) on p. 38; and the four-vertex theorem, Theorem 2 on p. 37.

This is the third mission of a series formalizing do Carmo's book, and shares the namespace DoCarmoDG with the earlier ones.

Setting

A closed plane curve of length $l$ is a regular map $\alpha : [0,l] \to \mathbb{R}^2$ whose derivatives of all orders agree at the two endpoints; equivalently, and as used here, a smooth $l$-periodic map $\alpha : \mathbb{R} \to \mathbb{R}^2$. It is parametrized by arc length when $|\alpha'(s)| = 1$ for all $s$, in which case $l$ is its length. It is simple when it has no self-intersection: $\alpha(t_1) \neq \alpha(t_2)$ for distinct $t_1, t_2 \in [0,l)$.

Write $J$ for rotation by $+\pi/2$, $J(a,b) = (-b,a)$. For a curve parametrized by arc length the signed curvature is

$$k(s) = \bigl\langle \alpha''(s),\, J\alpha'(s) \bigr\rangle,$$

which is do Carmo's convention of §1-5, Remark 1: the normal is chosen so that $\{\alpha', J\alpha'\}$ has the orientation of the natural basis, and then $\alpha'' = k\,J\alpha'$. A vertex is a parameter $t$ with $k'(t) = 0$. The curve is convex when, for every parameter $t$, the whole trace lies in one of the two closed half-planes bounded by the tangent line at $t$.

An angle function for $\alpha$ is a smooth $\theta$ with $\alpha'(s) = (\cos\theta(s), \sin\theta(s))$; the rotation index is $(\theta(l) - \theta(0))/2\pi$. The area bounded by a positively oriented simple closed curve is given by do Carmo's equation (1),

$$A = \frac{1}{2}\int_0^l \bigl(x\,y' - y\,x'\bigr)\,dt, \qquad \alpha = (x,y).$$

Formalization targets

Goal — Four-vertex theorem (do Carmo, Theorem 2, p. 37)

$$\alpha \ \text{simple closed convex} \quad \Longrightarrow \quad \#\{\,t \in [0,l) : k'(t) = 0\,\} \ge 4 .$$

Supporting statements

The three equivalent forms of the area formula (1); the existence of a smooth angle function; the identity $k = \theta'$; the theorem of turning tangents (the rotation index of a simple closed curve is $\pm 1$); the isoperimetric inequality $l^2 \ge 4\pi A$ with equality exactly for circles; and do Carmo's lemma (5), $\int_0^l (Ax + By + C)\,k'(s)\,ds = 0$, which drives the proof of the goal.

Significance

The isoperimetric inequality is the ancestor of a large family of geometric inequalities, and its sharp case characterizes the circle — the first instance of the pattern "extremal configuration is the round one" that recurs throughout geometry. The four-vertex theorem is a genuinely global statement with no local counterpart: locally, the curvature of a convex arc may be strictly monotone, and it is only the requirement that the curve close up convexly that forces four critical points. Its converse, for strictly positive curvature, was proved by H. Gluck in 1971; do Carmo notes that the theorem also holds for simple closed curves that are not convex, by a harder argument.

Mathlib contains integration, the winding number of a loop in the complex plane and the Jordan curve theorem, but it does not contain the signed curvature of a plane curve, the theorem of turning tangents in this form, the isoperimetric inequality for curves with its equality case, or the four-vertex theorem. What this mission adds is that vocabulary and machine-checked proofs of the four classical statements.

Difficulty

Each target fails for a different reason under the naive approach.

For the area formula, the identification of $\frac12\oint(x\,dy - y\,dx)$ with the area of the interior is exactly the Jordan-curve input that do Carmo declares he is assuming; the formalization avoids that dependency by defining the bounded area through the integral, so a solver has to prove only the integration-by-parts identities among the three forms of (1).

For the theorem of turning tangents, the difficulty is that a smooth lift $\theta$ of the tangent indicatrix must be produced and then shown to increase by exactly $\pm 2\pi$ over one period — a degree-theoretic statement about a loop in the circle, where simplicity of the curve is what excludes the values $0, \pm 2, \pm 3, \dots$.

For the isoperimetric inequality, Schmidt's proof compares the curve with a circle tangent to two parallel supporting lines and uses the arithmetic–geometric mean inequality; the equality discussion, which is where the characterization of the circle lives, is the delicate part.

For the four-vertex theorem, the obvious argument — "curvature on a compact interval attains a maximum and a minimum, so there are two vertices" — gives only two, and the whole content is the step from two to four. The lemma (5) supplies the contradiction: if $k'$ changed sign only at the maximum and the minimum, a suitable line $Ax + By + C = 0$ through those two points would make the integrand of (5) of one sign and not identically zero.

Formalization scope

Curves are smooth maps ℝ → EuclideanSpace ℝ (Fin 2), closedness being $l$-periodicity with $l > 0$, which is do Carmo's condition that the curve and all its derivatives agree at the endpoints. Unit speed is imposed globally, so the parameter is arc length and $l$ is the length. Simplicity is injectivity on the half-open period $[0,l)$. Convexity is stated per parameter: for each $t$ the trace lies in one closed half-plane of the tangent line at $t$, the choice of side being allowed to depend on $t$, as in the book's phrasing.

The area is defined by do Carmo's integral (1) rather than as the measure of the interior of the curve, so no Jordan curve theorem is presupposed; consequently the isoperimetric statement is formulated with the absolute value $|A|$, which makes it independent of the curve's orientation and equal to the enclosed area for a positively oriented simple curve. The equality case asserts that the trace lies on a circle of positive radius.

"At least four vertices" is formalized as the existence of four pairwise distinct parameters in $[0,l)$ at which $k'$ vanishes, which rules out the degenerate reading in which one vertex is counted several times.

Selected references

• Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition, Dover, 2016, §1-7 (area formula, eq. (1), p. 33; isoperimetric inequality, Theorem 1, p. 34; theorem of turning tangents, p. 37; lemma, eq. (5), p. 38; four-vertex theorem, Theorem 2, p. 37).
• E. Schmidt, Über das isoperimetrische Problem im Raum von n Dimensionen, Mathematische Zeitschrift 44 (1939), 689–788.
• H. Gluck, The converse to the four-vertex theorem, L'Enseignement Mathématique 17 (1971), 295–309.

Motivation

Chapter 10 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) builds the calculus of differential forms in $\mathbb{R}^n$ and proves the theorem that unifies the integral theorems of vector analysis. The fundamental theorem of calculus, the Green, divergence and classical Stokes theorems all say the same thing — that integrating a derivative over a region is the same as integrating the original object over the boundary of that region — and Stokes' theorem (Theorem 10.33),

$$\int_\Psi d\omega = \int_{\partial \Psi} \omega ,$$

is that statement, once "region" is made precise as a chain of parametrized surfaces and "derivative" as the exterior derivative.

This mission is the tenth in a series formalizing Rudin Chapters 1–11; it uses the inverse function theorem and the several-variable calculus of Mission IX.

Setting

For an open $E \subseteq \mathbb{R}^n$, a $k$-surface in $E$ is a $C'$-mapping $\Phi$ from a parameter domain $D \subseteq \mathbb{R}^k$ — a $k$-cell or the standard simplex $Q^k = \{u : u_i \ge 0, \sum u_i \le 1\}$ — into $E$; surfaces are maps, not point sets. A $k$-form in $E$ is a formal sum

$$\omega = \sum a_{i_1\cdots i_k}(\mathbf{x})\,dx_{i_1}\wedge\cdots\wedge dx_{i_k}$$

with continuous coefficients, whose meaning is the rule assigning to each $k$-surface $\Phi$ the number

$$\int_\Phi \omega = \int_D \sum a_{i_1\cdots i_k}(\Phi(\mathbf{u}))\, \frac{\partial(\varphi_{i_1},\dots,\varphi_{i_k})}{\partial(u_1,\dots,u_k)}\,d\mathbf{u}.$$

The exterior derivative of $\omega$ is the $(k+1)$-form with coefficients $D_j a_I$; the pullback $\omega_T$ along a differentiable $T$ substitutes $T$ into the coefficients and the differentials. A $k$-chain is a formal integer combination of $k$-surfaces with parameter domain $Q^k$, its integral is the corresponding combination of integrals, and its boundary $\partial\Psi$ is obtained from the alternating sum $\sum_j (-1)^j$ of the faces of $Q^k$.

Formalization targets

Goal — Stokes' theorem (Theorem 10.33)

If $\Psi$ is a $k$-chain of class $C''$ in an open $V \subseteq \mathbb{R}^n$ and $\omega$ is a $(k-1)$-form of class $C'$ in $V$, then

$$\int_\Psi d\omega = \int_{\partial\Psi} \omega .$$

For $k = n = 1$ this is the fundamental theorem of calculus, for $k = n = 2$ Green's theorem, for $k = n = 3$ the divergence theorem, and for $k = 2$, $n = 3$ the theorem of Stokes.

Milestones

$$\text{the iterated integrals of a continuous function on a cell agree} \qquad (10.2)$$ $$\text{partitions of unity subordinate to an open cover of a compact set} \qquad (10.8)$$ $$\int f(\mathbf{y})\,d\mathbf{y} = \int f(T(\mathbf{x}))\,|J_T(\mathbf{x})|\,d\mathbf{x} \qquad (10.9)$$ $$d(d\omega) = 0 \qquad (10.20)$$ $$(d\omega)_T = d(\omega_T) \qquad (10.22\mathrm{c})$$ $$\int_{T\circ\Phi}\omega = \int_\Phi \omega_T \qquad (10.25)$$ $$\text{reordering the vertices of a simplex multiplies the integral by the sign} \qquad (10.27)$$ $$\text{Poincaré's lemma: on a convex open set, closed forms are exact} \qquad (10.39)$$

Significance

Stokes' theorem is the organizing theorem of multivariable analysis; its formal content is that $d$ and $\partial$ are adjoint, which is also the starting point of de Rham cohomology. Poincaré's lemma is its local converse: on a convex set the only obstruction to a closed form being exact disappears, so the failure of exactness measures the shape of the domain. The change of variables theorem (10.9) is what makes integrals independent of the parametrization and is used in the proof of Stokes itself, and partitions of unity (10.8) are the standard device for passing from local to global statements.

Mathlib has a general change-of-variables theorem for the Lebesgue integral, smooth partitions of unity, and the theory of alternating forms and de Rham differentials on manifolds; it does not have Rudin's concrete apparatus of parametrized surfaces, affine chains, and their boundaries, nor a version of Stokes' theorem for such chains. This mission builds that apparatus and states the chapter's theorems for it; the definitions are reusable for any development that wants a hands-on, coordinate-based treatment of forms.

Difficulty

This is the most demanding mission of the series, for two reasons. First, the objects have to be set up before anything can be said: forms as coefficient families, their integrals as Jacobian integrals, chains, and the boundary operator with its signs. Second, Stokes' theorem is proved by reducing to a single oriented simplex, transporting along the parametrization by Theorem 10.25, and then computing the integral over $Q^k$ by an iterated integral in which all but two terms of the boundary cancel; the cancellation is entirely a matter of getting the signs of the face maps right, and it is where a formalization will spend its time.

A further subtlety: with forms presented by coefficients indexed by all index tuples, the identity $d(d\omega) = 0$ is false coefficient-wise and true as an identity of forms. Since Rudin defines a form to be its integration functional, statements of the shape "this form vanishes" are formalized as "its integral over every surface vanishes", and that is how 10.20, 10.22(c) and 10.39 are stated here.

Formalization scope

Conventions fixed by this mission:

• Points of $\mathbb{R}^n$ are Fin n → ℝ. A $k$-form is Rudin.KForm k n, a coefficient function indexed by all tuples Fin k → Fin n, following Rudin's equation (34).
• Rudin.integralOverCell and Rudin.integralOverSimplex are Rudin's equation (35) for the two admissible parameter domains, with Rudin.jacobian the determinant of the matrix of partial derivatives. The integral over the parameter domain is the Lebesgue integral for the volume measure, which agrees with Rudin's Riemann integral for continuous integrands.
• Rudin.extDeriv and Rudin.pullback are the exterior derivative and the pullback; Rudin.Chain, Rudin.Chain.integral and Rudin.Chain.boundary are chains with integer multiplicities, their integrals, and the boundary built from the faces of the standard simplex with Rudin's signs $(-1)^j$.
• Regularity is ContDiff ℝ 1 and ContDiff ℝ 2 for Rudin's $C'$ and $C''$.
• Equalities between forms are stated as equalities of their integrals over surfaces, as explained above; the goal theorem is an equality of two real numbers, so it is not vacuous.

Contributions of the supporting differential-form identities (10.20, 10.22, 10.25) are especially welcome, since they are exactly the lemmas the goal theorem consumes.

Selected references

• Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 10 (pp. 245–299).
• Michael Spivak, Calculus on Manifolds, W. A. Benjamin, 1965.

Motivation

The Yang–Mills functional measures the total curvature of a connection on a principal bundle. Its critical points, the Yang–Mills connections, are the non-abelian generalization of solutions of Maxwell's equations, and in four dimensions the most important among them are the self-dual and anti-self-dual connections (instantons), whose moduli spaces underlie Donaldson theory of smooth four-manifolds. A basic and frequently used fact, recorded as Proposition 3.1.1 in K. Uhlenbeck's lectures Equations of Gauge Theory (notes by L. Fredrickson, Temple University, 2012), is that instantons are not merely critical points: within a fixed topological class and with fixed boundary data they are absolute minimizers of the Yang–Mills energy. The same "energy identity" argument is the template the notes later apply to the Kapustin–Witten equations (Proposition 3.1.5).

Timeline of the ideas involved: Yang and Mills introduce the equations (1954); Belavin, Polyakov, Schwartz and Tyupkin observe the topological lower bound on the energy and its saturation by self-dual fields (1975); Atiyah, Hitchin and Singer study the deformation theory of instantons (1977–78); Donaldson uses the instanton moduli space in four-manifold topology (1983).

Setting

Work on the trivial principal $SU(n)$-bundle over a closed box $\Omega=[a,b]=\prod_{\mu=0}^{3}[a_\mu,b_\mu]\subset\mathbb R^4$ with the Euclidean metric. A connection is $D_A=d+A$ with $A=\sum_\mu A_\mu\,dx^\mu$, where each $A_\mu$ is a smooth map into the Lie algebra $\mathfrak{su}(n)$ of traceless skew-Hermitian $n\times n$ complex matrices. Its curvature is the $\mathfrak{su}(n)$-valued two-form $F_A=dA+A\wedge A$ with coefficients

$$(F_A)_{\mu\nu}=\partial_\mu A_\nu-\partial_\nu A_\mu+[A_\mu,A_\nu].$$

The Hodge star on two-forms is $(\star F)_{\mu\nu}=\tfrac12\sum_{\rho,\sigma}\varepsilon_{\mu\nu\rho\sigma}F_{\rho\sigma}$, with $\varepsilon$ the Levi-Civita symbol. A two-form is self-dual if $\star F=F$ and anti-self-dual if $\star F=-F$. The pointwise norm is $|F|^2=\sum_{\mu<\nu}\operatorname{Re}\operatorname{tr}(F_{\mu\nu}F_{\mu\nu}^{*})$, and the Yang–Mills functional on $\Omega$ is

$$\mathrm{Ym}_\Omega(A)=\int_\Omega |F_A|^2\,d\mathrm{vol}.$$

The Chern–Weil density $\operatorname{tr}(F\wedge F)$ is the coefficient $\tfrac14\sum\varepsilon_{\mu\nu\rho\sigma}\operatorname{tr}(F_{\mu\nu}F_{\rho\sigma})$ of $dx^0\wedge dx^1\wedge dx^2\wedge dx^3$, and the Chern–Simons three-form is $CS(A)=\operatorname{tr}(A\wedge dA+\tfrac23A\wedge A\wedge A)$, with flux components $K^\mu=\sum\varepsilon_{\mu\nu\rho\sigma}\operatorname{tr}(A_\nu\partial_\rho A_\sigma+\tfrac23A_\nu A_\rho A_\sigma)$.

Formalization targets

Goal (Proposition 3.1.1, box version)

If $A$ and $B$ are smooth $SU(n)$-connections on $\Omega$ that agree on $\partial\Omega$, and $F_A$ is self-dual on all of $\Omega$ or anti-self-dual on all of $\Omega$, then

$$\mathrm{Ym}_\Omega(A)\le \mathrm{Ym}_\Omega(B).$$

Milestones

1. Lemma 3.1.2. For an $\mathfrak{su}(n)$-valued two-form $F$: $|F\pm\star F|^2=2|F|^2\mp2\operatorname{tr}(F\wedge F)$.
2. Fact 3.1.3, local form. $\operatorname{tr}(F_A\wedge F_A)=\sum_\mu\partial_\mu K^\mu$, i.e. $\operatorname{tr}(F_A\wedge F_A)=d\,CS(A)$.
3. Fact 3.1.3, box form. $\int_\Omega\operatorname{tr}(F_A\wedge F_A)=\int_{\partial\Omega}CS(A)$ (the topological term vanishes for the trivial bundle).
4. Energy bound (proof of Proposition 3.1.1). $\mathrm{Ym}_\Omega(A)\ge \mp\int_{\partial\Omega}CS(A)$.
5. Equality case (proof of Proposition 3.1.1). On a non-degenerate box, $\mathrm{Ym}_\Omega(A)=-\int_{\partial\Omega}CS(A)$ iff $F_A$ is self-dual on $\Omega$, and $\mathrm{Ym}_\Omega(A)=\int_{\partial\Omega}CS(A)$ iff $F_A$ is anti-self-dual on $\Omega$.

Significance

The energy identity turns a second-order variational problem into a first-order one: any connection satisfying the first-order self-duality equation is automatically a Yang–Mills connection, and in fact a global minimizer in its class. This is the reason instanton moduli spaces are the natural objects of four-dimensional gauge theory, and it is the model for the corresponding minimization statements for the Kapustin–Witten equations treated later in the same notes. The result is classical and its proof is known; the remaining work is formal: a machine-checked development of the curvature, Hodge star, Chern–Simons transgression and the boundary integration on boxes, none of which are currently packaged in this form in Mathlib.

Difficulty

The algebraic identity of Lemma 3.1.2 is a finite computation. The substantive step is the transgression formula $\operatorname{tr}(F_A\wedge F_A)=d\,CS(A)$, a cancellation between derivative terms and cubic terms that depends on cyclicity of the trace and on the antisymmetry of $\varepsilon$, followed by Stokes' theorem on the box with correct face orientations. The naive approach of comparing $|F_A|^2$ and $|F_B|^2$ pointwise fails: the two connections agree only on the boundary, and only the integrated topological term is boundary-determined.

Formalization scope

The general setting of the notes (a $G$-bundle over a compact oriented Riemannian four-manifold with boundary, topological class $c_2(P)=k$) is replaced by the trivial $SU(n)$-bundle over a closed axis-parallel box in Euclidean $\mathbb R^4$, so the topological term $8\pi^2c_2(P)$ is zero. Connections are smooth on all of $\mathbb R^4$ (equivalently, smooth up to the boundary of the box) and every coefficient takes values in $\mathfrak{su}(n)$. Two-forms are stored as antisymmetric $4\times4$ families of matrices; partial derivatives are taken entrywise; integrals are Lebesgue integrals over the box and over its faces. "Fixed boundary data" means $A=B$ at every point of $\partial\Omega$. Self-duality is $\star F=F$, matching $F=\star F$ in Section 2.2 of the notes.

Two sign/normalization corrections relative to the printed notes are made deliberately: Lemma 3.1.2 is stated with the sign obtained in its own proof on p. 32 ($\mp$ rather than the printed $\pm$, because $B^*=-B$ on $\mathfrak{su}(n)$), and the Chern–Simons form uses the standard coefficient $\tfrac23$ in $\operatorname{tr}(A\wedge dA+\tfrac23A^3)$, i.e. $\operatorname{tr}(A\wedge F_A)-\tfrac13\operatorname{tr}(A^3)$, for which $d\,CS=\operatorname{tr}(F\wedge F)$ holds, instead of the printed $\tfrac16$.

A trivializing formalization would make the boundary condition or the self-duality hypothesis unsatisfiable; here the zero connection is self-dual and satisfies every hypothesis, and the statements are not vacuous.

Reusable infrastructure: Levi-Civita symbol and Hodge star on $\Lambda^2\mathbb R^4$ with matrix coefficients, curvature of matrix-valued connections, the Chern–Simons transgression, and Stokes' theorem for flux forms on boxes (Mathlib's divergence theorem on boxes is the natural tool). Contributions to any milestone are welcome.

Selected references

• K. Uhlenbeck, Equations of Gauge Theory, notes by L. Fredrickson, Emil Grosswald Lectures, Temple University, 2012 (the source of all statements; Section 3.1, pp. 29–32).
• C. N. Yang, R. L. Mills, Conservation of isotopic spin and isotopic gauge invariance, Phys. Rev. 96 (1954), 191–195. https://doi.org/10.1103/PhysRev.96.191
• A. A. Belavin, A. M. Polyakov, A. S. Schwartz, Yu. S. Tyupkin, Pseudoparticle solutions of the Yang–Mills equations, Phys. Lett. B 59 (1975), 85–87. https://doi.org/10.1016/0370-2693(75)90163-X
• S. K. Donaldson, An application of gauge theory to four-dimensional topology, J. Differential Geom. 18 (1983), 279–315. https://doi.org/10.4310/jdg/1214437665

Motivation

The Einstein field equations (EFE) are the field equations of general relativity. They relate the curvature of spacetime, encoded in the metric $g_{\mu\nu}$, to its matter–energy content, encoded in the stress–energy tensor $T_{\mu\nu}$:

$$G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu},\qquad \kappa=\frac{8\pi G}{c^4}.$$

They were published by Einstein in 1915. A structural requirement on any such equation is that it be compatible with the local conservation of energy and momentum, $\nabla_\beta T^{\alpha\beta}=0$. For the EFE this compatibility is automatic: the left-hand side is identically divergence-free by the contracted Bianchi identity, so the field equations force conservation of the right-hand side. This mission formalizes that implication together with the standard algebraic reformulations of the equations, following the Wikipedia article Einstein field equations (revision 1374672993).

Setting

Everything is written in one coordinate chart. A point is $x\in\mathbb{R}^D$, where $D$ is the spacetime dimension (not fixed to $4$). A 2-tensor field is a matrix-valued function $x\mapsto T_{ab}(x)$. A metric on an open set $U$ is a 2-tensor field $g$ whose components are $C^\infty$ on $U$ and which is symmetric and nondegenerate at each point of $U$; $g^{ab}$ denotes the inverse matrix. Partial derivatives $\partial_a$ are coordinate (Fréchet) derivatives. Using the Misner–Thorne–Wheeler $(+\,+\,+)$ convention adopted by the source:

• Christoffel symbols $\Gamma^c_{ab}=\tfrac12g^{cs}(\partial_ag_{sb}+\partial_bg_{sa}-\partial_sg_{ab})$;
• Riemann tensor $R^\mu{}_{\alpha\beta\gamma}=\partial_\beta\Gamma^\mu_{\alpha\gamma}-\partial_\gamma\Gamma^\mu_{\alpha\beta}+\Gamma^\mu_{\sigma\beta}\Gamma^\sigma_{\gamma\alpha}-\Gamma^\mu_{\sigma\gamma}\Gamma^\sigma_{\beta\alpha}$;
• Ricci tensor $R_{\mu\nu}=R^\alpha{}_{\mu\alpha\nu}$, scalar curvature $R=g^{\mu\nu}R_{\mu\nu}$, Einstein tensor $G_{\mu\nu}=R_{\mu\nu}-\tfrac12Rg_{\mu\nu}$;
• covariant derivative $\nabla_\lambda T_{\mu\nu}=\partial_\lambda T_{\mu\nu}-\Gamma^\sigma_{\lambda\mu}T_{\sigma\nu}-\Gamma^\sigma_{\lambda\nu}T_{\mu\sigma}$ and divergence $(\operatorname{div}T)_\mu=g^{\nu\lambda}\nabla_\lambda T_{\mu\nu}$, the index-lowered form of $\nabla_\nu T^{\mu\nu}$;
• the field equations on $U$: $G_{\mu\nu}(x)+\Lambda g_{\mu\nu}(x)=\kappa T_{\mu\nu}(x)$ for all $x\in U$.

Formalization targets

Goal: local energy–momentum conservation

For a smooth nondegenerate symmetric metric $g$ on an open $U\subseteq\mathbb{R}^D$, constants $G,c>0$, $\kappa=8\pi G/c^4$, any $\Lambda$, and any $T$ such that the field equations hold on $U$:

$$g^{\beta\lambda}\nabla_\lambda T_{\alpha\beta}=0\quad\text{on }U.$$

Milestones

• Symmetry of the Einstein tensor, $G_{\mu\nu}=G_{\nu\mu}$.
• Metric compatibility, $\nabla_\lambda g_{\mu\nu}=0$.
• The differential Bianchi identity $R^\mu{}_{\alpha[\beta\gamma;\varepsilon]}=0$.
• The contracted Bianchi identity, $G^{\alpha\beta}{}_{;\beta}=0$.
• The trace of the EFE, $R-\tfrac D2R+D\Lambda=\kappa T$.
• Equivalence with the trace-reversed form $R_{\mu\nu}-\tfrac2{D-2}\Lambda g_{\mu\nu}=\kappa(T_{\mu\nu}-\tfrac1{D-2}Tg_{\mu\nu})$ for $D\neq2$.
• The vacuum equations $R_{\mu\nu}=\Lambda g_{\mu\nu}/(\tfrac D2-1)$ when $T=0$, $D\neq2$.
• The cosmological term as vacuum stress–energy $T^{(\mathrm{vac})}_{\mu\nu}=-\tfrac\Lambda\kappa g_{\mu\nu}$, with $\rho_{\mathrm{vac}}=-p_{\mathrm{vac}}=\Lambda/\kappa$.
• Minkowski space $\operatorname{diag}(-1,1,1,1)$ is a vacuum solution.

Significance

Conservation of $T_{\mu\nu}$ is a consistency condition that any relativistic field equation for gravity has to satisfy; it is also the starting point for deriving the motion of matter (for dust, the geodesic equation) from the field equations alone. The trace-reversed and vacuum forms are the ones used in practice to study vacuum solutions such as Schwarzschild and Kerr, and Einstein manifolds in geometry.

All of these results are classical and fully proved in the literature. What is not yet available is a machine-checked development of the Levi-Civita curvature calculus in coordinates suitable for these statements: Mathlib currently has no Riemann or Ricci tensor of a pseudo-Riemannian metric. The mission produces that layer and the proofs on top of it.

Difficulty

The algebraic milestones (trace, trace reversal, vacuum form, vacuum energy) only need matrix algebra and the symmetry of $g$; without symmetry the identity $g^{\mu\nu}g_{\mu\nu}=D$ fails, so symmetry is essential. The analytic core is the contracted Bianchi identity: it needs the symmetry of mixed second and third partial derivatives (Schwarz's theorem on an open set), derivatives of the matrix inverse $g^{-1}$, and lengthy index bookkeeping with sums over $\operatorname{Fin} D$. Since all objects are total functions, every derivative step must be justified by differentiability on the open set $U$, not taken for granted.

Formalization scope

• Coordinates: $\mathbb{R}^D$ is represented as Fin D → ℝ; tensors are Matrix (Fin D) (Fin D) ℝ-valued functions; no manifold structure. $D$ is arbitrary, and no Lorentzian signature is imposed (the results hold for any nondegenerate symmetric metric, which includes the Lorentzian case).
• Regularity: the metric components are $C^\infty$ on the open set $U$; $T$ carries no assumptions, as the field equations determine it on $U$.
• Total-function conventions: the inverse of a singular matrix is $0$ and the derivative of a non-differentiable function is $0$; nondegeneracy on $U$ and openness of $U$ make these junk values irrelevant at points of $U$.
• Divergence is taken on the second index; for symmetric tensors such as $G$ this is the same as the first.
• Not formalized: the Newtonian limit (it rests on approximations), the Einstein–Maxwell system, and the polynomial form.
• Reusable output: coordinate Christoffel/Riemann/Ricci calculus, metric compatibility, Bianchi identities.

Selected references

• Wikipedia, Einstein field equations, revision 1374672993. https://en.wikipedia.org/w/index.php?title=Einstein_field_equations&oldid=1374672993
• C. W. Misner, K. S. Thorne, J. A. Wheeler, Gravitation, W. H. Freeman, 1973.
• S. Carroll, Spacetime and Geometry: An Introduction to General Relativity, Addison Wesley, 2004.

Motivation

The Wheeler–DeWitt equation is the quantum version of the Hamiltonian constraint of general relativity. In the canonical formulation, a spacetime is described by the evolution of the metric $h_{ab}$ of a spatial slice, and Einstein's equations include a constraint: the Hamiltonian density vanishes at every point of space. Quantizing this constraint, as DeWitt did (Phys. Rev. 160, 1967), gives a second-order functional differential equation for a wavefunctional $\Psi[h]$ with no external time parameter.

Three structural facts make the equation distinctive:

• its kinetic term is built from an indefinite metric on the space of metrics, the DeWitt supermetric, so the equation is hyperbolic;
• the timelike direction of that supermetric is the local volume, which serves as an intrinsic time;
• in the limit $\hbar\to0$, a WKB ansatz turns the equation into the Einstein–Hamilton–Jacobi equation, recovering classical general relativity.

A fourth issue is not settled: consistency. In the continuum, the Poisson bracket of two Hamiltonian constraints is a combination of the momentum constraints, so imposing all constraints is consistent (Dirac's first-class condition). Any regularization of the quantum equation, a lattice for instance, must reproduce this. Generic lattice discretizations do not: the constraints become second class (Bander 1987; Dittrich 2008; Bahr–Dittrich 2009). Whether, and with which anomaly, the Hamiltonian-constraint commutators close as the lattice is refined was singled out as an open question by Loll (Living Rev. Rel. 1998, §2.12).

The first three facts are the standard entry points of quantum geometrodynamics, as reviewed by Kiefer (arXiv 0812.0295): Section 2 for the constraints and their quantization, eqs. (3)–(8), and Section 3 for the Hamilton–Jacobi equation, eq. (10), and the semiclassical approximation, eq. (11).

Setting

A spatial metric at a point is a symmetric positive-definite $3\times3$ matrix $h=(h_{ab})$. Write $\sqrt h=\sqrt{\det h}$. The DeWitt supermetric is

$$G_{abcd}(h)=\frac{h_{ac}h_{bd}+h_{ad}h_{bc}-h_{ab}h_{cd}}{2\sqrt h}.$$

It is a quadratic form $G(p,p)=G_{abcd}\,p^{ab}p^{cd}$ on symmetric momenta. Its inverse $G^{abcd}=\tfrac12\sqrt h\,(h^{ac}h^{bd}+h^{ad}h^{bc}-2h^{ab}h^{cd})$ acts on velocities.

Space is represented by a finite set $X$ of sites; this is a lattice regularization. A configuration assigns to each site $x$ a matrix $h(x)$. All nine entries are coordinates, so configuration space is $\mathbb{R}^{9|X|}$, and physical configurations are those that are symmetric and positive definite at every site. A wavefunction is a function $\Psi$ from configurations to $\mathbb{C}$. The functional derivative $\delta/\delta h_{ab}(x)$ is the partial derivative $\partial_{ab}(x)$ with respect to the coordinate $h_{ab}(x)$, with the cell volume normalized to one.

The Wheeler–DeWitt operator at site $x$, with gravitational coupling $\kappa$, cosmological constant $\Lambda$, and a supplied potential $R(h,x)$ playing the role of the spatial scalar curvature, is

$$\widehat{\mathcal H}_x\Psi=-2\kappa\hbar^2\,G_{abcd}(h(x))\,\partial_{ab}(x)\,\partial_{cd}(x)\Psi-\frac{\sqrt{h(x)}}{2\kappa}\,(R-2\Lambda)\,\Psi .$$

Write $V_z(h)=-\tfrac{\sqrt{h(z)}}{2\kappa}(R(h,z)-2\Lambda)$ for the potential at site $z$. On the classical phase space of pairs $(h,p)$, with $p^{ab}(z)$ conjugate to $h_{ab}(z)$, the lattice constraints are

$$H_z(h,p)=2\kappa\,G_{abcd}(h(z))\,p^{ab}(z)\,p^{cd}(z)+V_z(h),$$

with the canonical Poisson bracket. They are first class if each bracket $\{H_x,H_y\}$ vanishes wherever all constraints vanish.

The supermetric stands to the left of both derivatives (Kiefer, eq. (7), vacuum case; the coupling is $\kappa=8\pi G$, so $2\kappa=16\pi G$ as in Kiefer's eq. (10)). The kinetic term involves only derivatives at the same site, as in the continuum; it is ultralocal. The potential may couple neighbouring sites.

Formalization targets

Milestones: geometry of the supermetric

• Signature. $G(p,p)>0$ for every nonzero symmetric $p$ with $\operatorname{tr}(hp)=0$, and $G(h^{-1},h^{-1})<0$.
• Inverse. $G^{abcd}G_{cdef}\,p^{ef}=p^{ab}$ for symmetric $p$.
• Intrinsic time. With $h=s\hat h$, $\det\hat h=1$ and $\tau=\sqrt{32/3}\,s^{3/4}$, the velocity form of the supermetric is $-d\tau^2+\tfrac{3}{32}\tau^2\operatorname{tr}\big((\hat h^{-1}d\hat h)^2\big)$.

Milestone: the conformal sector

For $\Psi=f(\sqrt{\det h(x_0)})$ with $f\in C^2$ and $v=\sqrt{\det h(x_0)}$:

$$G_{abcd}\,\partial_{ab}\partial_{cd}\Psi=-\tfrac38\,\big(vf''(v)+7f'(v)\big).$$

Milestone: the semiclassical limit

For every real $C^2$ function $S$ and $\hbar\neq0$:

$$e^{-iS/\hbar}\,\widehat{\mathcal H}_x\,e^{iS/\hbar}=2\kappa\,G_{abcd}\,\partial_{ab}S\,\partial_{cd}S-\frac{\sqrt h}{2\kappa}(R-2\Lambda)\;-\;i\hbar\,2\kappa\,G_{abcd}\,\partial_{ab}\partial_{cd}S .$$

The $\hbar$-independent part is the Einstein–Hamilton–Jacobi functional of Kiefer's eq. (10), Hamiltonian part, with $S$ the eikonal of the WKB form (11) (amplitude $C=1$). This is the weakest statement exhibiting the classical limit, and it holds for every potential.

Milestone: the lattice commutator

For $\Psi\in C^4$ and sites $x\neq y$:

$$[\widehat{\mathcal H}_x,\widehat{\mathcal H}_y]\Psi=-2\kappa\hbar^2\Big(G_{abcd}(h(x))\big(2\,\partial^{x}_{ab}V_y\,\partial^{x}_{cd}\Psi+\partial^{x}_{ab}\partial^{x}_{cd}V_y\,\Psi\big)-(x\leftrightarrow y)\Big).$$

Milestone: the strong-coupling case

If every $V_z$ depends only on $h(z)$, then $\{H_x,H_y\}=0$ identically.

Goal: lattice constraints are second class

If the symmetric part of $\partial V_y/\partial h_{ab}(x)$ is nonzero at a physical $h$, for some $x\neq y$, then there is a point of the constraint surface over $h$ at which $\{H_x,H_y\}\neq0$.

Every finite-difference curvature couples neighbouring sites, so the goal applies to every such discretization. It is the weakest statement that the discretized constraint algebra is inconsistent, and it holds uniformly in the discretization.

Stronger targets

• The limit form $\hbar\to0$, as a Tendsto statement.
• The same results with the Laplace–Beltrami ordering of the kinetic term on the six-dimensional fibre of symmetric matrices, and an explicit formula for the difference between the two orderings.
• A potential realized as the scalar curvature of a smooth metric field on a coordinate patch, computed from Christoffel symbols, with its scaling law $R[sh]=R[h]/s$ for constant $s>0$.
• The momentum constraints (Kiefer, eq. (8)).
• Open as far as the drafter could determine. Fix a cubic lattice of spacing $\varepsilon$ and a standard finite-difference scalar curvature. Determine the limit $\varepsilon\to0$ of the suitably rescaled commutator $[\widehat{\mathcal H}_x,\widehat{\mathcal H}_y]$, and decide whether it reproduces the continuum Dirac algebra $\{H(x),H(y)\}=(h^{ab}H_b(x)+h^{ab}H_b(y))\,\partial_a\delta(x,y)$ or leaves an anomaly. Give the anomaly explicitly if there is one. This is the metric-variable analogue of the question Loll raised.

Significance

The signature theorem is the mathematical content behind two physical facts: the hyperbolic character of the Wheeler–DeWitt equation, and the instability of the conformal mode (the "conformal factor problem" of Euclidean quantum gravity). DeWitt's cone form identifies the local volume as an intrinsic clock. On this rests the reading of the equation as a wave equation in superspace, with $\tau$ as time. The conformal-sector reduction shows explicitly how the timelike direction appears in the operator, with the sign opposite to the traceless modes. The WKB identity is the precise sense in which the quantum constraint contains classical general relativity: its leading order is the Hamilton–Jacobi form of the Einstein constraint (Peres 1962; Kiefer, eq. (10)), and its next order is the one used in derivations of the Schrödinger equation from quantum gravity.

All of these are classical computations. The drafter knows of no machine-checked version. A formalization fixes conventions that the literature handles loosely:

• the normalization of $G_{abcd}$;
• the treatment of symmetric versus independent metric components;
• the ordering of operators.

It does so with genuine derivatives in place of formal symbols.

The constraint-algebra part turns a phenomenon described qualitatively in the literature into a theorem with exact hypotheses. Lattice constraints are second class as soon as curvature couples sites, and the quantum commutator is given in closed form. It also isolates precisely what a consistent discretization would have to cancel. The continuum-limit target addresses an open question in canonical quantum gravity.

Difficulty

The supermetric statements are finite-dimensional, but none is a single computation. The signature requires a positivity argument for $\operatorname{tr}\big((h^{1/2}ph^{1/2})^2\big)$ on an $h$-traceless subspace. The cone form requires separating the trace part of a velocity in a non-orthonormal frame.

The analytic targets require second derivatives of compositions through the determinant and the matrix inverse. The derivative of $\det$ at $h$ in the direction of a single entry is $\det h\,(h^{-1})_{ba}$, and the derivative of $h^{-1}$ produces terms like $h^{-1}E_{ab}h^{-1}$; a sign or index slip changes the constant $7$. Treating the nine entries as independent coordinates, rather than the six symmetric ones, changes the numerical coefficients; the conventions below fix this.

For the constraint algebra, the quantum commutator involves up to fourth derivatives of $\Psi$, which cancel only by the symmetry of mixed partials. The classical goal needs a point on the constraint surface where the bracket is nonzero. Each constraint fixes the value of an indefinite quadratic form in the momenta, and the bracket is linear in them, so the proof must use the Lorentzian signature to show that the bracket is not constant on that quadric.

A naive formalization that replaces $\partial_{ab}$ by an abstract linear map reduces every target to ring arithmetic, and is ruled out by the definitions.

Formalization scope

• Definitions (module Def_WheelerDeWittSuperspace):
  • metric components as Fin 3 → Fin 3 → ℝ, so that configuration space X → Fin 3 → Fin 3 → ℝ with X a Fintype is a normed space;
  • matrices via Matrix.of;
  • $\partial_{ab}(x)$ as fderiv ℝ Ψ h applied to the coordinate direction of $h_{ab}(x)$;
  • $\sqrt h$ as Real.sqrt of the determinant;
  • the operator with the supermetric on the left.
• Conventions:
  • all nine metric entries are independent coordinates, and statements that need symmetry assume it at the evaluation point (Matrix.PosDef includes symmetry);
  • lattice cell volume equal to $1$;
  • vacuum (no matter term).
• Not formalized; the potential is an interface: the potential $R$ is supplied data on configurations and sites, and every target holds for all such $R$. The continuum limit of the lattice, a Hilbert-space domain for $\widehat{\mathcal H}$, regularization of coincident derivatives in the continuum, and existence of solutions are outside the mission and must not be inferred from it.
• Trivial cases to rule out:
  • the WKB milestone must hold for every $C^2$ phase $S$, not only for $\Psi=0$ or constant $S$;
  • the goal must exhibit a point on the full constraint surface, with every $H_z$ vanishing, not merely a point where the bracket is nonzero;
  • the dependence hypothesis is on the symmetric part, because antisymmetric metric directions are invisible to $G$.
• Phase-space convention: the bracket is the canonical one on all nine components per site. The symmetric reduction changes off-diagonal normalizations but not the first-class property.
• Welcome contributions: the stronger targets, a matter field with its energy density, and minisuperspace reductions (e.g. homogeneous isotropic metrics $h=a^2\delta$) derived from the operator here rather than postulated.

Selected references

• B. S. DeWitt, Quantum Theory of Gravity. I. The Canonical Theory, Phys. Rev. 160 (1967), 1113–1148. https://doi.org/10.1103/PhysRev.160.1113
• C. Kiefer, Quantum Geometrodynamics: whence, whither?, Gen. Relativ. Gravit. 41 (2009), 877–901. https://arxiv.org/abs/0812.0295
• A. Peres, On Cauchy's problem in general relativity – II, Nuovo Cimento 26 (1962), 53–62. https://doi.org/10.1007/BF02754342
• C. Kiefer, Quantum Gravity, 3rd ed., Oxford University Press (2012), Chapter 5. https://doi.org/10.1093/acprof:oso/9780199585205.001.0001
• R. Loll, Discrete approaches to quantum gravity in four dimensions, Living Rev. Relativ. 1 (1998), 13, Section 2.12. https://arxiv.org/abs/gr-qc/9805049
• R. Loll, On the diffeomorphism-commutators of lattice quantum gravity, Class. Quantum Grav. 15 (1998), 799–809. https://arxiv.org/abs/gr-qc/9708025
• P. Renteln, Some results of SU(2) spinorial lattice gravity, Class. Quantum Grav. 7 (1990), 493–502.
• M. Bander, Hamiltonian lattice gravity. Deformations of discrete manifolds, Phys. Rev. D 36 (1987), 2297. https://doi.org/10.1103/PhysRevD.36.2297
• R. Gambini, J. Pullin, Canonical quantization of general relativity in discrete space-times, 2002. https://arxiv.org/abs/gr-qc/0206055
• B. Dittrich, Diffeomorphism symmetry in quantum gravity models, 2008. https://arxiv.org/abs/0810.3594
• B. Bahr, B. Dittrich, (Broken) Gauge symmetries and constraints in Regge calculus, 2009. https://arxiv.org/abs/0905.1670
• C. J. Isham, Some quantum field theory aspects of the superspace quantization of general relativity, Proc. R. Soc. Lond. A 351 (1976), 209.
• K. Pilati, Strong-coupling quantum gravity. I. Solution in a particular gauge, Phys. Rev. D 26 (1982), 2645. https://doi.org/10.1103/PhysRevD.26.2645
• H. W. Hamber, R. M. Williams, Discrete Wheeler–DeWitt equation, 2011. https://arxiv.org/abs/1109.2530