-- 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/NullRicciEnergy.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy.betaSq, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy.coeff0, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy.coeff2, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy.coeff4, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy.misalign, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy.muCoeff, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy.nullSOS, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy.resL
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_ChargedTail
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedBridge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedResiduals
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_MaxwellFrame
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_RicciNullDirections
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_SmoothBranch

/-! # VII-09 (1/3): exact actual null-Ricci sum of squares and a homogeneous lower bound

For the actual ES5 candidate `gA = esMetric f (Dfun f m N) (Afun f m) (Hfun m N) w`, its actual
inverse `giA = esInverse …` and actual Faraday `esFaraday p a`, at a point `x` of `esDomain I`
where the **actual** Einstein–Maxwell equations `einsteinMaxwellD gA giA F = 0` hold, the frozen
VII-06 contraction `ricci_contract2` and frame identity `frame_sum_of_squares` give, for every
coordinate vector `k` with frame components `ξ = frameInv w x k`,

`Ric(k,k) + (F²/3 + 2·alphaSq)·g(k,k) = c₀ L² + c₂ ξ₂² + c₄ ξ₄²`,

with `L = f a' ξ₀ + H e ξ₃`, `c₀ = 2/(D f H)`, `c₂ = 2(alphaSq+betaSq) A/(4U)`,
`c₄ = 2(alphaSq+betaSq) A U`, `U = u(1-u)`, `betaSq = 4a²/A²`. For an actually null `k` the trace
term drops and `Ric(k,k)` equals the weighted sum of squares (`c₀ = 8` on the paper dictionary).

`Ric` here is the Core `ricciOf gA giA` of the actual metric and inverse; no new curvature object
is defined. `mu = min c₀ (min c₂ c₄)` and `misalign = L² + ξ₂² + ξ₄²` compare unweighted residuals
in the fixed coordinate chart and numerical units: `misalign` is not an invariant distance, angle
or physical observable, and `mu` depends on the point (no uniform lower bound is claimed).
-/

open scoped Matrix
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.ES5
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections
open ExactVacuumAtlas.EinsteinMaxwell.D (einsteinMaxwellD)

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy

/-! ## Residuals and coefficients (transparent notation, Class B) -/

/-- Fiber/time residual `L = f a' ξ₀ + H e ξ₃` of `ξ = frameInv w x k`. -/
noncomputable def resL (f m N w p a : ℝ → ℝ) (x : Pt 5) (k : Fin 5 → ℝ) : ℝ :=
  f (x 1) * deriv a (x 1) * frameInv w x k 0 + Hfun m N (x 1) * eFun w p a (x 1) * frameInv w x k 3

/-- Magnetic discriminant `betaSq = 4a²/A²` on the paper dictionary. -/
noncomputable def betaSq (f m a : ℝ → ℝ) (r : ℝ) : ℝ := betaSqFrame (Afun f m r) (a r)

/-- `c₀ = 2/(D f H)`. -/
noncomputable def coeff0 (f m N : ℝ → ℝ) (r : ℝ) : ℝ := 2 / (Dfun f m N r * f r * Hfun m N r)

/-- `c₂ = 2(alphaSq+betaSq) A/(4U)`, `U = u(1-u)`. -/
noncomputable def coeff2 (f m N w p a : ℝ → ℝ) (x : Pt 5) : ℝ :=
  2 * (alphaSq f m N w p a (x 1) + betaSq f m a (x 1)) * Afun f m (x 1) / (4 * (x 2 * (1 - x 2)))

/-- `c₄ = 2(alphaSq+betaSq) A U`. -/
noncomputable def coeff4 (f m N w p a : ℝ → ℝ) (x : Pt 5) : ℝ :=
  2 * (alphaSq f m N w p a (x 1) + betaSq f m a (x 1)) * Afun f m (x 1) * (x 2 * (1 - x 2))

/-- The weighted sum of squares `c₀ L² + c₂ ξ₂² + c₄ ξ₄²`. -/
noncomputable def nullSOS (f m N w p a : ℝ → ℝ) (x : Pt 5) (k : Fin 5 → ℝ) : ℝ :=
  coeff0 f m N (x 1) * resL f m N w p a x k ^ 2 + coeff2 f m N w p a x * frameInv w x k 2 ^ 2 +
    coeff4 f m N w p a x * frameInv w x k 4 ^ 2

/-- `mu = min c₀ (min c₂ c₄)` (depends on the point only, not on `k`). -/
noncomputable def muCoeff (f m N w p a : ℝ → ℝ) (x : Pt 5) : ℝ :=
  min (coeff0 f m N (x 1)) (min (coeff2 f m N w p a x) (coeff4 f m N w p a x))

/-- Unweighted residual square sum `L² + ξ₂² + ξ₄²` (fixed-chart numerical comparison only). -/
noncomputable def misalign (f m N w p a : ℝ → ℝ) (x : Pt 5) (k : Fin 5 → ℝ) : ℝ :=
  resL f m N w p a x k ^ 2 + frameInv w x k 2 ^ 2 + frameInv w x k 4 ^ 2

/-! ## Homogeneity -/

/-! ## Elementary positivity and the lower bound (finite algebra) -/

section Identity

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

end Identity

/-! ## Roots -/

section Roots

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

end Roots

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy