-- 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/RadialBVP.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.paperConstraintResidual, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.paperFResidual, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.paperMResidual, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.paperNResidual
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

/-! # VII-03 (F2b): the paper's Eqs. 23a, 24a, 24b, 25 and the four remaining VI residuals

The residuals below are the paper's equations (Fröb et al., EPJC 82:215 (2022), Eqs. 23a, 24a,
24b, 25) written literally as left minus right, with genuine derivatives in the VI radial variable
`R`; `Q`, `J` are parameters (common constants at the BVP level). With `T = 2m²(a')² - f a²`:

* `paperNResidual   = N'' - 2`,
* `paperFResidual   = f²m (m f'/f²)' - m m'(m'/m - 2N'/N) f - (4m²/N - f) f - (8/3)(fm/N) T
                      + (4/3) Q² f²m²/N²`,
* `paperMResidual   = f m (N m'/m)' + (f²N/m² - 2f) m - (4/3) f T - (4/3) Q² f²m/N
                      - 4 (f²m²/N²)(J + 2Qa)²`,
* `paperConstraintResidual = m²(a')² - [f a² - m + fN/(4m) + Q² fm/N + (fm²/N²)(J + 2Qa)²
      + (N m'/8)(f'/f - 2m'/m + 4N'/N) - (N m f'/(8f))(2f'/f - m'/m + 2N'/N)]`.

They are *not* defined as combinations of the VI residuals. The theorems below prove, on any open
`I` with `f, m, N ≠ 0` (no sign, no connectedness, no conservation law), that with the pointwise
values `Q = -q(r)`, `J = -ℓ(r)/2` each actual VI residual `Generic.redE_tt/rr/uu/σσ` on the
paper-gauge dictionary is an explicit combination of the four paper residuals and conversely. -/

open scoped ContDiff Topology
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.D
open ExactVacuumAtlas.EinsteinMaxwell.ES5

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial

/-- Eq. 23a, left minus right: `N'' - 2`. -/
noncomputable def paperNResidual (N : ℝ → ℝ) (r : ℝ) : ℝ := deriv (deriv N) r - 2

/-- Eq. 24a, left minus right. -/
noncomputable def paperFResidual (f m N a : ℝ → ℝ) (Q : ℝ) (r : ℝ) : ℝ :=
  f r ^ 2 * m r * deriv (fun s => m s / f s ^ 2 * deriv f s) r
    - m r * deriv m r * (deriv m r / m r - 2 * deriv N r / N r) * f r
    - (4 * m r ^ 2 / N r - f r) * f r
    - 8 / 3 * (f r * m r / N r) * (2 * m r ^ 2 * deriv a r ^ 2 - f r * a r ^ 2)
    + 4 / 3 * Q ^ 2 * (f r ^ 2 * m r ^ 2 / N r ^ 2)

/-- Eq. 24b, left minus right. -/
noncomputable def paperMResidual (f m N a : ℝ → ℝ) (Q J : ℝ) (r : ℝ) : ℝ :=
  f r * m r * deriv (fun s => N s / m s * deriv m s) r
    + (f r ^ 2 * N r / m r ^ 2 - 2 * f r) * m r
    - 4 / 3 * f r * (2 * m r ^ 2 * deriv a r ^ 2 - f r * a r ^ 2)
    - 4 / 3 * Q ^ 2 * (f r ^ 2 * m r / N r)
    - 4 * (f r ^ 2 * m r ^ 2 / N r ^ 2) * (J + 2 * Q * a r) ^ 2

/-- Eq. 25 (the constraint), left minus right. -/
noncomputable def paperConstraintResidual (f m N a : ℝ → ℝ) (Q J : ℝ) (r : ℝ) : ℝ :=
  m r ^ 2 * deriv a r ^ 2 -
    (f r * a r ^ 2 - m r + f r * N r / (4 * m r) + Q ^ 2 * (f r * m r / N r)
      + f r * m r ^ 2 / N r ^ 2 * (J + 2 * Q * a r) ^ 2
      + N r * deriv m r / 8 * (deriv f r / f r - 2 * deriv m r / m r + 4 * deriv N r / N r)
      - N r * m r * deriv f r / (8 * f r) *
          (2 * deriv f r / f r - deriv m r / m r + 2 * deriv N r / N r))

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

/-- Abbreviations for the four actual VI Einstein residuals on the paper-gauge dictionary. -/
local notation "Ett" => Generic.redE_tt f (Dfun f m N) (Afun f m) (Hfun m N) w p a r
local notation "Err" => Generic.redE_rr f (Dfun f m N) (Afun f m) (Hfun m N) w p a r
local notation "Euu" => Generic.redE_uu f (Dfun f m N) (Afun f m) (Hfun m N) w p a r
local notation "Ess" => Generic.redE_σσ f (Dfun f m N) (Afun f m) (Hfun m N) w p a r
local notation "Qr" => -qFun f N w p a r
local notation "Jr" => -ellFun f m N w p a r / 2

/-! ## Inverse identities: each VI residual from the paper residuals (pointwise `Q`, `J`) -/

/-! ## Forward identities: each paper residual from the VI residuals (pointwise `Q`, `J`) -/

/-! ## Local two-sided equivalence (pointwise `Q = -q(r)`, `J = -ℓ(r)/2`) -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial