-- 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/KSRicci.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.mOf, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.qTerm
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_CoordinateAcceleration
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_KSConnection
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_KSMetric
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_MaxwellFrame
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_PaperGauge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVP
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVPEquivalence
import Definitions.Def_Atlas_Transport_Connection

/-! # VII-08 (3/5): actual contracted Ricci difference for a same-coordinate KS metric

**Generic helper** (`ricci_contract_diff`): for two connection families `Γ, Γ̄` on an open `U`,
with `C = Γ − Γ̄` symmetric in its lower indices on `U`, genuinely differentiable `Γ, Γ̄` and `K`
at `x ∈ U`, and the identities `Σ_{pq} C^a_{pq} K^p K^q = 0`, `Σ_a C^a_{pa} = 0` holding on the
whole open `U` (so that they may be differentiated), the registered `ricci` satisfies

  `Σ_{pq} (Ric_Γ − Ric_Γ̄)_{pq} K^p K^q = −2 Σ_{ap} M^a_p B_a^p − Σ_{ap} M^a_p M^p_a`,

`M^a_p = Σ_q C^a_{pq} K^q`, `B_a^p = ∂_a K^p + Σ_c Γ̄^p_{ac} K^c` (`covD`). No curvature library,
no background flatness, no Lorentz signature.

**Main root** (`vii08_ks_ricci_contraction`): for raw `KSData b bi v k U` (non-constant
background allowed) and `x ∈ U`,

  `Ric_g(k,k) = Ric_b(k,k) − v · b(A, A)`,  `A = accel b bi k` (actual VII-07 acceleration),

all with the registered `ricciOf`/`christoffel`/`pd`. In the 2009 convention `v = −2H` this is
`Ric_g(k,k) = Ric_b(k,k) + 2H b(A,A)`. Consequences: actual pregeodesic `k` ⇒
`Ric_g(k,k) = Ric_b(k,k)`; an independent actual background `VacuumCertificate` (Ricci-flat, not
Riemann-flat) ⇒ `Ric_g(k,k) = 0`; and the constructor of the VII-07 `RicciNullPregeodesicField`
(constructed in `KSTailObstruction`) whose `ricci_null` field is an **output** of this
derivation. No converse is claimed (`v = 0`).
-/

open scoped ContDiff Topology Matrix
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.ES5
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections (contract2)
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry

/-- `M^a_p = Σ_q C^a_{pq} K^q`. -/
noncomputable def mOf (C : Fin 5 → Fin 5 → Fin 5 → Pt 5 → ℝ) (K : Pt 5 → Fin 5 → ℝ) (x : Pt 5)
    (a p : Fin 5) : ℝ :=
  ∑ q, C a p q x * K x q

/-- The quadratic connection-difference terms of `ricci Γ − ricci Γ̄` (fixed `p q i j`). -/
noncomputable def qTerm (Γb C : Fin 5 → Fin 5 → Fin 5 → Pt 5 → ℝ) (x : Pt 5) (p q i j : Fin 5) :
    ℝ :=
  Γb i i j x * C j p q x + C i i j x * Γb j p q x + C i i j x * C j p q x
    - Γb i q j x * C j p i x - C i q j x * Γb j p i x - C i q j x * C j p i x

section Helper

variable {Γ Γb : Fin 5 → Fin 5 → Fin 5 → Pt 5 → ℝ} {K : Pt 5 → Fin 5 → ℝ} {U : Set (Pt 5)}
  {x : Pt 5}

end Helper

variable {b bi : Metric 5} {v : Pt 5 → ℝ} {k : Pt 5 → Fin 5 → ℝ} {U : Set (Pt 5)}

namespace KSData

variable (hD : KSData b bi v k U)
include hD

end KSData

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry