-- 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/SmoothBranch.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.magneticLabel, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.massLabel
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_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

/-! # VII-05 (F2c2): independent smooth extensions at inverse radius zero

The VII-04 pullbacks `pull s f x = f(s + x⁻¹)`, `pullM s m x = x · m(s + x⁻¹)` are total
functions, and Lean's `0⁻¹ = 0` gives the literal value `pullM s m 0 = 0`
(`literal_pullM_zero`). A smooth branch at `x = 0` with `b(0) = 1` therefore can **not** be
phrased with the literal `pullM` (`literal_pullM_not_branch`).

`SmoothBranch I s ε f m a F b A` instead records *independent* real functions `F b A`, `C^∞` on
`U = (-ε, ε)`, equal to the pullbacks **only on `(0, ε)`**, with the three leading values
`F(0) = b(0) = 1`, `A(0) = 0` and the chart tail `(s + ε⁻¹, ∞) ⊆ I`. This is an *additional*
regularity assumption at infinity (a selected smooth branch); it is not derived from
`PaperData` at finite radii or from bare asymptotic flatness. The structure contains no field
equation, no `PaperBVP`/`FactorizedN`, no `G` condition, no Taylor coefficient beyond the three
leading values, and no residual, Γ or `J`/`Q` condition. The labels `M = -F'(0)`, `c = A'(0)`
are definitions, not hypotheses.

On the open set `(0, ε)` the matching transfers values, first and second derivatives
(`Set.EqOn.deriv`), hence the four real compactified residuals and `realGamma`
(`realP*_congr`, `realGamma_congr`). Nothing is transferred at the single point `x = 0`. -/

open scoped ContDiff

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt

open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact

/-- Mass label `M = -F'(0)` (a definition, not an extra hypothesis). -/
noncomputable def massLabel (F : ℝ → ℝ) : ℝ := -deriv F 0
/-- Magnetic label `c = A'(0)` (a definition, not an extra hypothesis). -/
noncomputable def magneticLabel (A : ℝ → ℝ) : ℝ := deriv A 0

/-! ## The literal totalized pullback at zero -/

/-! ## Chart membership and positive-side transfer -/

section Transfer

variable {V : Set ℝ} (hV : IsOpen V) {F b A F' b' A' : ℝ → ℝ}
  (hF : Set.EqOn F F' V) (hb : Set.EqOn b b' V) (hA : Set.EqOn A A' V) {x : ℝ} (hx : x ∈ V)
include hV hF hb hA hx

end Transfer

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt