Atlas VII definitions: RadialBVPEquivalence
DefinitionAtlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVPEquivalenceDefinitions of the Atlas VII module Atlas.EinsteinMaxwell.ES5.KerrSchild.RadialBVPEquivalence (kept exactly as in the accepted source, skeleton subtraction).
VII-03 (F2b): the actual reduced system is equivalent to the paper's radial BVP
PaperBVP I f m N w p a Q J lists the paper's seven radial field equations with one common pair of
constants Q, J on all of I: the two conservation laws q = -Q, ℓ = -2J, Eq. 23a N'' = 2,
Eqs. 24a, 24b, 24c and the constraint Eq. 25. It is a statement about the field equations only (no
regularity, no jet, no Kerr–Schild or J³Q⁵ content).
On an open preconnected I with base point r₀ and real paper data (C^∞, f, m, N ≠ 0):
Generic.ReducedSystem <dictionary> I ↔ ∃ Q J, Q = -q(r₀) ∧ J = -ℓ(r₀)/2 ∧ PaperBVP … Q J.
Forward: VII-02 gives the common constants and Eq. 24c from the actual residuals; the four
forward identities give 23a, 24a, 24b, 25. Reverse: q' = ℓ' = 0 from the conservation laws on the
open set (derivative transfer), the VII-02 residual identities give redJ_t = redE_tσ = 0, Eq. 24c
gives redJ_σ = 0, and the four inverse identities give the remaining Einstein residuals.
From N'' = 2 on a preconnected open I: N R = R² + βR + γ with explicit real β, γ. No
statement about real roots, horizons or non-extremality is made (N = R² + 1 satisfies N'' = 2).
Constants in this bundle: PaperBVP.
Registered B3 definition layer (Mathlib at the pinned revision has no Lorentzian metric / Ricci API): mission/PHYSICS_BOUNDARY.md, Atlas VII sections P–XVII.
-- 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/RadialBVPEquivalence.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.PaperBVP
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_PaperGauge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVP
/-! # VII-03 (F2b): the actual reduced system is equivalent to the paper's radial BVP
`PaperBVP I f m N w p a Q J` lists the paper's seven radial field equations with one common pair of
constants `Q`, `J` on all of `I`: the two conservation laws `q = -Q`, `ℓ = -2J`, Eq. 23a `N'' = 2`,
Eqs. 24a, 24b, 24c and the constraint Eq. 25. It is a statement about the field equations only (no
regularity, no jet, no Kerr–Schild or `J³Q⁵` content).
On an open preconnected `I` with base point `r₀` and real paper data (`C^∞`, `f, m, N ≠ 0`):
`Generic.ReducedSystem <dictionary> I ↔ ∃ Q J, Q = -q(r₀) ∧ J = -ℓ(r₀)/2 ∧ PaperBVP … Q J`.
Forward: VII-02 gives the common constants and Eq. 24c from the actual residuals; the four
forward identities give 23a, 24a, 24b, 25. Reverse: `q' = ℓ' = 0` from the conservation laws on the
open set (derivative transfer), the VII-02 residual identities give `redJ_t = redE_tσ = 0`, Eq. 24c
gives `redJ_σ = 0`, and the four inverse identities give the remaining Einstein residuals.
From `N'' = 2` on a preconnected open `I`: `N R = R² + βR + γ` with explicit real `β`, `γ`. No
statement about real roots, horizons or non-extremality is made (`N = R² + 1` satisfies `N'' = 2`). -/
open scoped ContDiff Topology
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.D
open ExactVacuumAtlas.EinsteinMaxwell.ES5
namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial
/-- The paper's radial BVP with common constants `Q`, `J` on `I` (field equations only). -/
def PaperBVP (I : Set ℝ) (f m N w p a : ℝ → ℝ) (Q J : ℝ) : Prop :=
∀ r ∈ I, qFun f N w p a r = -Q ∧ ellFun f m N w p a r = -2 * J ∧
deriv (deriv N) r = 2 ∧
paperFResidual f m N a Q r = 0 ∧
paperMResidual f m N a Q J r = 0 ∧
m r * deriv (fun s => m s * deriv a s) r - f r * a r =
2 * Q * f r * m r ^ 2 / N r ^ 2 * (J + 2 * Q * a r) ∧
paperConstraintResidual f m N a Q J r = 0
variable {I : Set ℝ} {f m N w p a : ℝ → ℝ} {r : ℝ}
/-! ## The two directions -/
/-! ## `N'' = 2` gives a real quadratic (no root or horizon statement) -/
/-! ## Roots and certificate layer -/
end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial