Main regularity theorem (sufficiency direction)

Proved

ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16.contDiffOn_flatExt

by He Wang · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

einstein-maxwellexact-spacetime-atlas-viiexact-vacuum-atlasfive-dimensional-gravitygeneral-relativitykerr-schild

Main regularity theorem (sufficiency direction). If the germ h is Cⁿ on (0, ε) and its iterated derivatives of every order k ≤ n have right limit 0 at the origin, then the flat extension is Cⁿ on (-ε, ε).

The hypothesis is on the actual derivatives, not on function values: this is exactly the gap the paper's Eq. 30/33 do not fill.

Scope. Supporting result in the formal proof chain of Atlas VII Unit A: the restricted geodesic Kerr–Schild obstruction on the actual asymptotic branch of the five-dimensional, $\Lambda = 0$ , source-free Einstein–Maxwell radial system with two equal-magnitude angular momenta. It asserts exactly the Lean statement of this node for the data stated there; it does not claim the existence of a solution, a horizon or a black hole.

Preamble

import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_D_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Cert
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Data
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Reduced
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Tables
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedBridge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedResiduals
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_FiniteJetObstruction
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_FiniteTaylorJet
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_JetRecursion
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_OneSidedExtraction
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_PaperGauge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_PolynomialJet
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVP
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVPEquivalence
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_SmoothBranch
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_VII13FiniteBranchSpec
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_VII16AsymptoticBridge
open Filter Set
open scoped Topology ContDiff
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact (pull pullM)
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec (FiniteBranch6)
-- (open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.Controls: no listed name exists here)
-- (open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial: no listed name exists here)

Formal statement

theorem ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16.contDiffOn_flatExt (n : ℕ) :
    ∀ {h : ℝ → ℝ} {ε : ℝ}, 0 < ε → ContDiffOn ℝ n h (Ioo (0:ℝ) ε) →
      (∀ k ≤ n, Tendsto (iteratedDeriv k h) (𝓝[>] (0:ℝ)) (𝓝 0)) →
      ContDiffOn ℝ n (flatExt h) (Ioo (-ε) ε) := by sorry

Source

He Wang, Exact Spacetime Atlas VII, Unit A (restricted Kerr–Schild obstruction on the actual asymptotic branch, VII17). Local source, no public repository; commit f64ba9c823ec; Atlas/EinsteinMaxwell/ES5/KerrSchild/VII16AsymptoticBridge.lean#L223-L274; SHA-256 4eaa449e244a96eb98e0a117308c07eff0f4f640fba2fcee9d527fee281fb022. Registered definitions: mission/PHYSICS_BOUNDARY.md (Atlas VII sections P–XVII). Physical Kerr–Schild obstruction: Fröb–Khavkine–Málek–Pravda, Eur. Phys. J. C 82 (2022) 215, arXiv:2112.13266 (Eqs. 23–25, 33, 59–60).

View graph