Rudin PMA X: Integration of Differential FormsTextbook
## 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.
18 thms4 active usersReviewed
🏆Completed
Captain: He Wang
Kerr Vacuum Solution Verification in Boyer–Lindquist CoordinatesResearch Paper
## Why a coordinate verification of Kerr
The Kerr metric (Kerr, 1963) is the exact solution of the vacuum Einstein equations that describes the exterior gravitational field of a rotating mass. It is the working model for astrophysical black holes: gravitational-wave templates, black-hole imaging and the classification results of the uniqueness theorems all take it as their starting point. Its form in the coordinates of Boyer and Lindquist (1967) is the one found in every textbook, and the statement that this line element has vanishing Ricci tensor is the single most-cited computation of the subject. That computation is long, it is almost never printed, and in practice it is trusted because computer-algebra systems agree on it. The parent project of this mission builds a certified-discovery pipeline for exact solutions of Einstein's equations in which a symbolic verifier is the oracle; this mission asks for the Kerr instance of that oracle's verdict to be re-established inside a proof assistant, so that the pipeline's benchmark result rests on a kernel-checked proof rather than on a simplification routine.
Timeline: Kerr (1963) found the metric in Kerr-Schild and in his original coordinates; Boyer and Lindquist (1967) introduced the coordinates $(t,r,\theta,\varphi)$ in which the metric below is written and described its maximal analytic extension; Carter (1968) established the separability structure that underlies the closed-form inverse. None of these results has, to the authors' knowledge, a machine-checked proof.
## Setting
Fix real parameters $M$ and $a$. A point of $\mathbb R^4$ is written $x=(x_0,x_1,x_2,x_3)=(t,r,\theta,\varphi)$; in Lean it is a function `Pt := Fin 4 → ℝ`. Write $s=\sin\theta$, $c=\cos\theta$ and
$$\Sigma := r^2+a^2\cos^2\theta,\qquad \Delta := r^2-2Mr+a^2 .$$
The **Boyer-Lindquist Kerr metric** is the symmetric $4\times4$ matrix of functions
$$g_{tt}=-\Big(1-\frac{2Mr}{\Sigma}\Big),\quad g_{rr}=\frac{\Sigma}{\Delta},\quad g_{\theta\theta}=\Sigma,\quad g_{\varphi\varphi}=\Big(r^2+a^2+\frac{2Mra^2\sin^2\theta}{\Sigma}\Big)\sin^2\theta,\quad g_{t\varphi}=-\frac{2Mar\sin^2\theta}{\Sigma},$$
with all other entries zero (signature $(-,+,+,+)$, $G=c=1$). Its **closed-form inverse** $\hat g$ has $\hat g^{rr}=\Delta/\Sigma$, $\hat g^{\theta\theta}=1/\Sigma$ and a $(t,\varphi)$ block with denominator $\Sigma\Delta\sin^2\theta$. The **regular coordinate domain** is
$$\mathrm{Reg}_{M,a}(x)\ :\Longleftrightarrow\ \Sigma\neq0\ \wedge\ \Delta\neq0\ \wedge\ \sin\theta\neq0 .$$
For any matrix of functions $g$ with candidate inverse $\hat g$, the **coordinate partial derivative** $\partial_i f(x)$ is the one-variable derivative at $u=x_i$ of the slice $u\mapsto f(x[i\mapsto u])$, and the **coordinate Christoffel symbols** and **coordinate Ricci tensor** are
$$\Gamma^a_{bc}=\tfrac12\sum_k\hat g^{ak}\big(\partial_c g_{kb}+\partial_b g_{kc}-\partial_k g_{bc}\big),\qquad R_{bd}=\sum_i\Big(\partial_i\Gamma^i_{bd}-\partial_d\Gamma^i_{bi}+\sum_j\big(\Gamma^i_{ij}\Gamma^j_{bd}-\Gamma^i_{dj}\Gamma^j_{bi}\big)\Big).$$
These four definitions (`pd`, `christoffel`, `ricci`, `ricciOf`) form the definition bundle `KerrBL_CoordGeometry`; the metric, its inverse and the regular domain form `KerrBL_Kerr_Metric`.
## Formalization targets
### Goal: Kerr vacuum theorem in Boyer-Lindquist coordinates (`KerrBL.vacuum_Kerr`)
For all real $M,a$ and every $x$ with $\mathrm{Reg}_{M,a}(x)$:
$$\sum_k\hat g^{ik}(x)g_{kj}(x)=\delta_{ij},\qquad u\mapsto g_{ij}(x[l\mapsto u])\ \text{and}\ u\mapsto\Gamma^i_{jk}(x[l\mapsto u])\ \text{are differentiable at } x_l,\qquad R_{bd}(x)=0\ \ \forall\,b,d .$$
The goal deliberately bundles the inverse identity and the two differentiability clauses with Ricci-flatness. Without the first, `ricciOf g ĝ` with a wrong $\hat g$ could vanish trivially; without the other two, the derivative in the definition of $R_{bd}$ could be Mathlib's default value $0$ at a non-differentiable slice. With them, the last clause is a statement about the genuine coordinate Ricci tensor.
### Supporting targets
The milestones follow the three layers of the proof: (I) the inverse identity; (II) the bridge from the generic definitions to explicit closed forms, through derivative certification of the metric, the Christoffel bridge, derivative certification of the generic Christoffel symbols, and the Ricci bridge $R_{bd}(x)=\mathrm{RicciKerr}_{bd}(x)$; (III) the vanishing of the explicit expression for each of the eight components that are not structurally zero, as rational identities in the seven variables $(M,a,r,s,c,S,D)$ under $s^2+c^2=1$, $S=\Sigma$, $D=\Delta$, and finally the vanishing of all sixteen generic components.
## Significance
The result itself is classical: the Boyer-Lindquist Kerr family is a vacuum solution wherever the coordinates are regular. What the mission adds is a proof in which the trusted base is explicit and small: a 45-line generic layer defining $\partial_i$, $\Gamma$ and $R$, and the transcription of five metric components from a hash-locked source file, with source-lock lemmas proving that the compact definitions equal the transcriptions. Everything else, including roughly 120 kB of generated closed forms, is bridged by proof; a wrong closed form can make a bridge theorem unprovable but never a false theorem provable. The generic layer and the bridge pattern are reusable for any coordinate metric in four dimensions, and the pattern of certifying a computer-algebra derivation through polynomial witnesses checked by `linear_combination` is reusable for any rational-function identity.
Status: the theorem is proved in the classical sense since 1963 and verified by every computer-algebra system; the machine-checked coordinate proof is what this mission records. At launch every node of the mission carries an accepted proof.
## Difficulty
The obvious argument is to compute. The difficulty is size and control, not ideas. The Ricci components of Kerr are rational functions whose numerators have up to a few hundred monomials in seven variables; a normalisation tactic applied to the raw expression does not terminate in practice, and a naive $\mathrm{simp}$-based unfolding of the double sums over $\mathrm{Fin}\,4$ produces terms whose elaboration alone exceeds the server budget. The proof therefore has to be organised: opaque atoms for $\Sigma$ and $\Delta$ so that denominators are monomials, per-term clearing lemmas over a common denominator, and a single polynomial identity per component certified by explicit quotient witnesses of the relations $s^2+c^2=1$, $S=\Sigma$, $D=\Delta$. Mathlib's derivative also needs care: `deriv` returns $0$ where a function is not differentiable, so every derivative used in the Ricci formula must be accompanied by a `HasDerivAt` witness, and the differentiability of the generic Christoffel symbols has to be transferred from their closed forms by a locality argument on the open regular domain.
## Formalization scope
The Lean representation commits to the following. Points are `Fin 4 → ℝ` with $0=t$, $1=r$, $2=\theta$, $3=\varphi$; there is no manifold, no chart, no periodicity of $\varphi$ and no range restriction on $r$. Derivatives are Mathlib's `deriv` of coordinate slices. The candidate inverse is data; its correctness is a theorem. The parameters $M,a$ are arbitrary reals: the mission proves Ricci-flatness of the Boyer-Lindquist Kerr family on the regular coordinate domain used by the formalization, not a global Lorentzian-manifold theorem and not a statement restricted to the black-hole regime $M>0$, $|a|\le M$. The axis $\sin\theta=0$ is excluded (the inverse carries $1/\sin^2\theta$) although the metric is smooth there; the loci $\Sigma=0$ and $\Delta=0$ are excluded. Nothing is asserted about signature, uniqueness, symmetry of $R_{bd}$ (all sixteen components are proved separately) or any coordinate-independent curvature quantity. A trivialising formalization is ruled out by the goal's first clause: the Ricci tensor of the specification layer takes the inverse as an argument, and the goal certifies that argument.
Independent blind read-back of the definitions and main statements, performed by a separate agent that saw only the Lean text, returned the following honest statement, recorded here verbatim: "For every pair of real numbers $M$, $a$ and every point $(t,r,\theta,\varphi)\in\mathbb R^4$ at which $r^2+a^2\cos^2\theta\neq0$, $r^2-2Mr+a^2\neq0$ and $\sin\theta\neq0$, all sixteen numbers $R_{bd}$ obtained by evaluating the explicit coordinate formula [...] vanish, where $g$ is the explicitly transcribed Boyer-Lindquist Kerr component matrix, $\hat g$ is an explicitly transcribed matrix that (by `ginv_mul_g_Kerr`, under the same hypothesis) satisfies $\hat g g=I$ at that point, and $\partial_i$ is Mathlib's one-variable `deriv` of the coordinate slice." The two should-fix findings of that read-back (inverse coupling; junk derivative values) are addressed by the first three clauses of the goal.
Infrastructure: three definition bundles (`KerrBL_CoordGeometry`, hand-written; `KerrBL_Kerr_Metric`, generated from the source file and human-auditable; `KerrBL_Kerr_ClosedForms`, generated and untrusted). Reusable beyond the mission: the generic layer, the locality lemma, and the bridge pattern. Natural extensions welcome after release: the two-sided inverse, the $a=0$ reduction to Schwarzschild, and curvature invariants such as the Kretschmann scalar.
## Selected references
- R. P. Kerr, *Gravitational field of a spinning mass as an example of algebraically special metrics*, Phys. Rev. Lett. 11 (1963) 237-238. https://doi.org/10.1103/PhysRevLett.11.237
- R. H. Boyer and R. W. Lindquist, *Maximal analytic extension of the Kerr metric*, J. Math. Phys. 8 (1967) 265-281. https://doi.org/10.1063/1.1705193
- B. Carter, *Global structure of the Kerr family of gravitational fields*, Phys. Rev. 174 (1968) 1559-1571. https://doi.org/10.1103/PhysRev.174.1559
- S. Chandrasekhar, *The Mathematical Theory of Black Holes*, Oxford University Press, 1983, Chapter 6.
- S. M. Carroll, *Spacetime and Geometry*, Cambridge University Press, 2019, Section 6.6.