The radial heat equation for the outer mass

For $f_0$ smooth on $S^2$, $m\in\mathbb R$, $R>0$ and a chart point $x=(r,\theta,\varphi)$ with $r\ge 3R$ and $\sin\theta\ne 0$, the function $F=$ outerMass f₀ m R satisfies

where $\zeta_R=$ bendingZeta R, $v_R=$ bendingV R, and $\Delta_{S^2}F$ is the sphere Laplacian computed from the mass jet in the chart.

The last term is the padding density. The heat term cancels the Laplacian term that the mass aspect would otherwise contribute to the energy.

Formal statement. In the scope of the preamble:

theorem outerMass_heat (f₀ : C(Sphere,ℝ)) (hf₀ : SmoothSphere f₀) (m : ℝ)
    {R : ℝ} (hR : 0 < R) {x : Point} (hr : 3*R ≤ x 0) (hs : Real.sin (x 1) ≠ 0) :
    D (basis 0) (outerMass f₀ m R) x =
      bendingZeta R (x 0) * (massJet (outerMass f₀ m R) x).laplace
        (Real.sin (x 1)) (Real.cos (x 1)) / (2*x 0*A (bendingV R (x 0))) +
      1/(x 0*Real.sqrt (x 0))

Formalization Note The statement is verbatim from lean/OAI/Geometry/Relativity/CKS/HeatRadial.lean, lines 75-91, in OpenAI's openai/math at commit adc7f12 (Apache-2.0), formalizing part of the construction in the preprint Area-controlled end replacement and the Bondi–Penrose inequality in the CKS class (OpenAI, September 27, 2026). It is a supporting lemma for OAI.CKSSourceExterior.area_controlled_end_replacement. The definitions it mentions are those of Definitions.Def_CKSBondiPenrose and Definitions.Def_CKSEndReplacementSupport.