-- 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/VII17Algebra.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.c1E, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.d1E, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.rdE, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.rhoE, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.rootE, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.zrhsE
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

/-!
# VII17 — exact identities on the real compactified residuals (3A–3D)

State variables (positive side, `u = 1 - h x`): `Z = uF′/F`, `V = A/x`, `W = bA′`, `D = (b² - F)/x`, `r = b′/b`,
`B = J + 2QxV`. Proved on the real `pcE`/`paE`/`pfE` (including the `J`-term of `pcE`):
`quad_pcE` (constraint as `x u r² + (2 - xZ) r + ρ = 0`), `root_eq` (small-root selection without `1/x`),
`dmode_id` (`x D′ + 2(D + h) = x RD`), `zprime_id` (`Z′`), `maxwell_id` (`S = V + W`, `T = V - W` modes).
-/

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17

open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact

/-- 3A remainder `ρ` (state values `F b Z V W D`; `u = 1 - h x`, `B = J + 2 Q x V`). -/
noncomputable def rhoE (h Q J x F b Z V W D : ℝ) : ℝ :=
  x * Z ^ 2 / (1 - h * x) - Z / (1 - h * x) + D / b ^ 2 + h * (b ^ 2 + F) / b ^ 2
    + 4 * x ^ 2 * W ^ 2 / b - 4 * F * x ^ 2 * V ^ 2 / b - 4 * Q ^ 2 * F * x / (1 - h * x)
    - 4 * F * b * x ^ 2 * (J + 2 * Q * x * V) ^ 2 / (1 - h * x) ^ 2

/-- 3A small root of `x u r² + (2 - x Z) r + ρ = 0`, written without a `1/x`. -/
noncomputable def rootE (h Q J x F b Z V W D : ℝ) : ℝ :=
  -2 * rhoE h Q J x F b Z V W D /
    (2 - x * Z + √((2 - x * Z) ^ 2 - 4 * (1 - h * x) * x * rhoE h Q J x F b Z V W D))

/-- 3B right-hand side of `Z′`. -/
noncomputable def zrhsE (h Q J x F b V W : ℝ) : ℝ :=
  4 * x / (3 * b) * (W ^ 2 + F * V ^ 2) + 8 * Q ^ 2 * F / (3 * (1 - h * x))
    + 4 * F * b * x * (J + 2 * Q * x * V) ^ 2 / (1 - h * x) ^ 2

/-- 3D right-hand side `RD`; `P` stands for the Hadamard quotient `(F - 1)/x`. -/
noncomputable def rdE (h Q J x F b Z V W D r P : ℝ) : ℝ :=
  -b ^ 2 * Z ^ 2 / (1 - h * x) + D * Z / (1 - h * x) - h * (D + 2 * P)
    - 4 * b * x * W ^ 2 + 4 * F * b * x * V ^ 2 + 4 * Q ^ 2 * F * b ^ 2 / (1 - h * x)
    + 4 * F * b ^ 3 * x * (J + 2 * Q * x * V) ^ 2 / (1 - h * x) ^ 2
    + b ^ 2 * Z * r - (1 - h * x) * b ^ 2 * r ^ 2

/-- 3C coefficient `c1`; `P1` stands for `(F/b - 1)/x`. -/
noncomputable def c1E (h Q x F b P1 : ℝ) : ℝ := P1 + 4 * Q ^ 2 * F * b * x / (1 - h * x) ^ 2
/-- 3C source `d1`. -/
noncomputable def d1E (h Q J x F b : ℝ) : ℝ := 2 * Q * J * F * b / (1 - h * x) ^ 2

section Alg
variable (x h Q J F F₁ F₂ b b₁ b₂ A A₁ A₂ : ℝ)

end Alg

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17