Atlas VII definitions: PrincipalGeodesic

Definition

Atlas_EinsteinMaxwell_ES5_KerrSchild_PrincipalGeodesic

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.PrincipalGeodesic (kept exactly as in the accepted source, skeleton subtraction).

VII-07 (F3b): exact actual acceleration of the principal null fields

Paper dictionary g = esMetric f D A H w, D = m/(4fN), A = m/f, H = N/m, actual inverse esInverse, e = p' + w a', Z = p'' + w a'', G = a' p'' - p' a'' (Gfun). For a radial function λ the field principalField λ = (x ↦ principalCoord … (λ (x 1)) x) has coordinate components (e/f, λ, 0, w e/f - a'/H, w e/f - a'/H); VII-06's kPlus/kMinus are literally principalField (±√alphaSq) (rfl). All derivatives are genuine; λ varies with R and its derivative is eliminated only through the eventual identity λ² = alphaSq near the point.

Main results (no Einstein, Maxwell, BVP, conservation or G = 0 input):

principal_lowered_accel: g·accel(K_λ) = (-λp'', (e/f) Z - a'a''/H, 0, -uλa'', -(1-u)λa'');
principal_accel_decomp: accel(K_λ) - (λZ/e) K_λ = (G/e) (0, a'/(DH), 0, λ/H, λ/H) (e ≠ 0);
vii07_principal_acceleration (both actual k±) and vii07_principal_pregeodesic_iff_G (k₊ pregeodesic ⇔ G(R) = 0 ⇔ k₋ pregeodesic), and the nonzero-rescaling corollary.

Constants in this bundle: principalField.

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/PrincipalGeodesic.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic.principalField
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_ChargedTail
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedBridge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedResiduals
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CoordinateAcceleration
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_MaxwellFrame
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_RicciNullDirections
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_SmoothBranch

/-! # VII-07 (F3b): exact actual acceleration of the principal null fields

Paper dictionary `g = esMetric f D A H w`, `D = m/(4fN)`, `A = m/f`, `H = N/m`, actual inverse
`esInverse`, `e = p' + w a'`, `Z = p'' + w a''`, `G = a' p'' - p' a''` (`Gfun`). For a radial
function `λ` the field `principalField λ = (x ↦ principalCoord … (λ (x 1)) x)` has coordinate
components `(e/f, λ, 0, w e/f - a'/H, w e/f - a'/H)`; VII-06's `kPlus`/`kMinus` are literally
`principalField (±√alphaSq)` (`rfl`). All derivatives are genuine; `λ` varies with `R` and its
derivative is eliminated only through the **eventual** identity `λ² = alphaSq` near the point.

Main results (no Einstein, Maxwell, BVP, conservation or `G = 0` input):
* `principal_lowered_accel`: `g·accel(K_λ) = (-λp'', (e/f) Z - a'a''/H, 0, -uλa'', -(1-u)λa'')`;
* `principal_accel_decomp`: `accel(K_λ) - (λZ/e) K_λ = (G/e) (0, a'/(DH), 0, λ/H, λ/H)` (`e ≠ 0`);
* `vii07_principal_acceleration` (both actual `k±`) and `vii07_principal_pregeodesic_iff_G`
  (`k₊` pregeodesic ⇔ `G(R) = 0` ⇔ `k₋` pregeodesic), and the nonzero-rescaling corollary. -/

open scoped ContDiff Topology Matrix
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.ES5
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic

/-- The actual principal coordinate field with a radial function `lam` in the `r`-slot. -/
noncomputable def principalField (f m N w p a lam : ℝ → ℝ) : Pt 5 → Fin 5 → ℝ :=
  fun x => principalCoord f m N w p a (lam (x 1)) x

variable {I : Set ℝ} {f m N w p a : ℝ → ℝ}

/-! ## Genuine radial derivatives -/

/-! ## Actual lowering of the principal vector (pointwise algebra) -/

/-! ## The lowered actual acceleration of `principalField λ` -/

/-! ## Exact decomposition and the pregeodesic criterion -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic

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/PrincipalGeodesic.lean; SHA-256 5452b99cefb6ce9580bc3a7cd3b092cf372b1834cc7796fc323f927c83b7b637. 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