Atlas VII definitions: VII17Analysis

Definition

Atlas_EinsteinMaxwell_ES5_KerrSchild_VII17Analysis

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

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

Definitions of the Atlas VII module Atlas.EinsteinMaxwell.ES5.KerrSchild.VII17Analysis (kept exactly as in the accepted source, skeleton subtraction).

VII17 — finite-regularity analysis tools (B3 coordinate certificate, analysis layer)

Generic one-variable tools for the finite C⁶ bootstrap at the compactified endpoint x = 0⁺:

PS g — g is C^∞ on a right neighbourhood of 0; RL k g — g, …, g⁽ᵏ⁾ have finite right limits; ExtV k g L — an independent Cᵏ extension across 0 agreeing with g on the positive side, value L.
extV_of_RL — right limits ⇒ extension (accepted VII16 glue); ExtV.RL — the converse.
euler_lim (L'Hôpital), euler_RL — x M′ + (n+1) M = φ, x M → 0 transfers right limits from φ to M.
hadamard — G ∈ Cᵏ⁺¹, G(0)=0 ⇒ G/x ∈ Cᵏ (loses one order).
euler_gain — x g′ + 2 g = x H, g → 0, H ∈ Cᵏ ⇒ g ∈ Cᵏ⁺¹ (gains one order: g′ = H − 2g/x). The endpoint condition g → 0 excludes the homogeneous c/x² mode. No physics input.

Constants in this bundle: ExtV, PS, RL.

Registered B3 definition layer (Mathlib at the pinned revision has no Lorentzian metric / Ricci API): mission/PHYSICS_BOUNDARY.md, Atlas VII sections P–XVII.

Definition code

-- Generated by scripts/vii24r/publish/gen_platform_tree_unitA.py (Atlas VII Unit A; copy of the RELEASE06 generator, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/ES5/KerrSchild/VII17Analysis.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.ExtV, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.PS, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.RL
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

/-!
# VII17 — finite-regularity analysis tools (B3 coordinate certificate, analysis layer)

Generic one-variable tools for the finite `C⁶` bootstrap at the compactified endpoint `x = 0⁺`:
* `PS g` — `g` is `C^∞` on a right neighbourhood of `0`; `RL k g` — `g, …, g⁽ᵏ⁾` have finite right limits;
  `ExtV k g L` — an independent `Cᵏ` extension across `0` agreeing with `g` on the positive side, value `L`.
* `extV_of_RL` — right limits ⇒ extension (accepted VII16 `glue`); `ExtV.RL` — the converse.
* `euler_lim` (L'Hôpital), `euler_RL` — `x M′ + (n+1) M = φ`, `x M → 0` transfers right limits from `φ` to `M`.
* `hadamard` — `G ∈ Cᵏ⁺¹`, `G(0)=0` ⇒ `G/x ∈ Cᵏ` (loses one order).
* `euler_gain` — `x g′ + 2 g = x H`, `g → 0`, `H ∈ Cᵏ` ⇒ `g ∈ Cᵏ⁺¹` (gains one order: `g′ = H − 2g/x`).
The endpoint condition `g → 0` excludes the homogeneous `c/x²` mode. No physics input.
-/

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17

open Filter Set Topology
open scoped ContDiff

/-- Positive-side germ smoothness. -/
def PS (g : ℝ → ℝ) : Prop := ∀ᶠ x in 𝓝[>] (0:ℝ), ContDiffAt ℝ ∞ g x

/-- Right limits at `0⁺` of `g, g′, …, g⁽ᵏ⁾` (recursive form). -/
def RL : ℕ → (ℝ → ℝ) → Prop
  | 0, g => ∃ L, Tendsto g (𝓝[>] (0:ℝ)) (𝓝 L)
  | k + 1, g => (∃ L, Tendsto g (𝓝[>] (0:ℝ)) (𝓝 L)) ∧ RL k (deriv g)

/-- An independent `Cᵏ` extension across `0`, agreeing with `g` on the positive side, value `L`. -/
def ExtV (k : ℕ) (g : ℝ → ℝ) (L : ℝ) : Prop :=
  ∃ G : ℝ → ℝ, ContDiffAt ℝ k G 0 ∧ G =ᶠ[𝓝[>] (0:ℝ)] g ∧ G 0 = L

section Closure
variable {f g : ℝ → ℝ} {k : ℕ} {a c L : ℝ}

end Closure

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17

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/VII17Analysis.lean; SHA-256 0a0c3533c95c6059ee4eda802b5cb0a725724deff290d14db36b008a7839e766. 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