-- 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/CompactifiedBridge.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.FactorizedN, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.eq24cResidual, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.pull, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.pullM
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_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-04 (F2c1): the real change of variables `x = 1/(R - s)` on the factorized-N branch

Real paper-gauge data `f m N w p a` on an open `I` (`PaperData`, VII-02) with the **explicit branch
hypothesis** `FactorizedN I N s h : ∀ R ∈ I, N R = (R - s)(R - s - h)` (not derived from
`N'' = 2`; `s`, `s + h` are not claimed to be horizons, squared radii or non-extremal).
The pulled-back functions of `x` are

  `F = pull s f : x ↦ f(s + 1/x)`, `b = pullM s m : x ↦ x m(s + 1/x)`, `A = pull s a`.

At every `x ≠ 0` with `s + 1/x ∈ I` (the chart is invertible only there; `x = 0` is not in it) the
genuine chain rule gives (`realPF_eq` … `realPC_eq`)

  `realPF = 3 F u² · paperFResidual`, `realPM = (3 x b u²/F) · paperMResidual`,
  `realPA = u² · eq24cResidual`, `realPC = 4 x b F² u² · paperConstraintResidual`

with the *existing* VII-03 residuals and `u = 1 - h x ≠ 0`, and from VII-02's on-shell `G` formula
`u² G(s + 1/x) = realGamma …(x)` (`realGamma_eq`). Root `vii04_compactified_bridge`: `PaperBVP`
on `I` ⇒ all four real compactified residuals vanish and the `G` identity holds on the chart.
Nothing here concerns `x = 0`, Taylor coefficients or asymptotics (F2c2). -/

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

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact

/-- `F(x) = f(s + 1/x)`. -/
noncomputable def pull (s : ℝ) (g : ℝ → ℝ) : ℝ → ℝ := fun x => g (s + x⁻¹)
/-- `b(x) = x · m(s + 1/x)`, i.e. `m(R) = b(x)/x`. -/
noncomputable def pullM (s : ℝ) (g : ℝ → ℝ) : ℝ → ℝ := fun x => x * g (s + x⁻¹)

/-- Eq. 24c, left minus right, exactly as it appears in `PaperBVP`. -/
noncomputable def eq24cResidual (f m N a : ℝ → ℝ) (Q J : ℝ) (r : ℝ) : ℝ :=
  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)

/-- The factorized-N branch (explicit hypothesis). -/
def FactorizedN (I : Set ℝ) (N : ℝ → ℝ) (s h : ℝ) : Prop :=
  ∀ R ∈ I, N R = (R - s) * (R - s - h)

variable {I : Set ℝ} {s h x : ℝ}

/-! ## Chain rule for the chart `x ↦ s + 1/x` -/

section Second

variable {g : ℝ → ℝ} (hI : IsOpen I) (hgd : ∀ R ∈ I, HasDerivAt g (deriv g R) R)
  (hg2 : HasDerivAt (deriv g) (deriv (deriv g) (s + x⁻¹)) (s + x⁻¹)) (hx : x ≠ 0)
  (hxI : s + x⁻¹ ∈ I)
include hI hgd hx hxI

include hg2

end Second

/-! ## Values on the chart for paper-gauge data -/

section Paper

variable {f m N w p a : ℝ → ℝ} (hP : PaperData I f m N w p a) (hx : x ≠ 0) (hxI : s + x⁻¹ ∈ I)
include hP hx hxI

variable (hN : FactorizedN I N s h)
include hN

/-! ## The four compactified residual identities (genuine chain rule) -/

end Paper

/-! ## The real geodesic defect on the chart -/

section Gamma

variable {f m N w p a : ℝ → ℝ} (hP : PaperData I f m N w p a) (hx : x ≠ 0) (hxI : s + x⁻¹ ∈ I)
  (hN : FactorizedN I N s h)
include hP hx hxI hN

end Gamma

/-! ## Roots: `PaperBVP` on `I` ⇒ the compactified system on the chart -/

section Roots

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

end Roots

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact