-- 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/KSConnection.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.accL, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.cdiffOf, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.chrL, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.covD, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.covL, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.dprof, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.ksC, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.nablaH
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_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 (2/5): actual Kerr–Schild difference connection and acceleration transfer

Same chart, open `U`, raw `KSData b bi v k U`. With the **registered** `christoffel`:

* `Γ̄ = christoffel b bi` (background, non-constant in general), `Γ = christoffel g gi` for the
  Kerr–Schild pair `g = ksMetric b v k`, `gi = ksInverse bi v k`;
* `C = Γ − Γ̄` (`ksC`), `(∇̄_c k)^a = ∂_c k^a + Σ_l Γ̄^a_{cl} k^l` (`covD`, an explicit finite sum),
  `A = accel b bi k` (VII-07 actual acceleration), `a_d = Σ_j b_dj A^j`, `k(v) = Σ_c k^c ∂_c v`.

Proved on `U` from the raw data only (no geodesic, flatness, `v ≠ 0` or `k ≠ 0` hypothesis):

1. differentiated nullity / background metric compatibility: `Σ_a ℓ_a (∇̄_c k)^a = 0`;
2. lowered difference connection `Σ_i g_di C^i_{pq} = ½(∇̄_q h_{dp} + ∇̄_p h_{dq} − ∇̄_d h_{pq})`
   with `∇̄_c h_{pq}` (`nablaH`) written explicitly for `h = v ℓ ⊗ ℓ`;
3. `M^a_p = Σ_q C^a_{pq} k^q = ½[k(v) k^a ℓ_p + v A^a ℓ_p + v k^a a_p]`;
4. `Σ_{pq} C^a_{pq} k^p k^q = 0`, `Σ_a C^a_{aq} = 0` (trace of the **difference** connection);
5. `accel g gi k = accel b bi k`, hence actual pregeodesic / affine conditions are equivalent
   (same multiplier; non-affine parametrisation allowed).

All derivative facts are genuine (`pd_mul`, `pd_sum`, `pd_congr_of_eqOn` on the open `U`); the
nullity identity is differentiated only because it holds on the whole open `U`.
-/

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

/-- Explicit covariant-derivative expression `(∇_c K)^a = ∂_c K^a + Σ_l Γ^a_{cl} K^l`. -/
noncomputable def covD (Γ : Fin 5 → Fin 5 → Fin 5 → Pt 5 → ℝ) (K : Pt 5 → Fin 5 → ℝ)
    (x : Pt 5) (c a : Fin 5) : ℝ :=
  pd c (fun y => K y a) x + ∑ l, Γ a c l x * K x l

/-- Difference of two connection families, `C = Γ − Γ̄`. -/
def cdiffOf (Γ Γb : Fin 5 → Fin 5 → Fin 5 → Pt 5 → ℝ) : Fin 5 → Fin 5 → Fin 5 → Pt 5 → ℝ :=
  fun a p q y => Γ a p q y - Γb a p q y

/-- Actual Kerr–Schild difference connection `C = Γ(g, gi) − Γ(b, bi)`. -/
noncomputable def ksC (b bi : Metric 5) (v : Pt 5 → ℝ) (k : Pt 5 → Fin 5 → ℝ) :
    Fin 5 → Fin 5 → Fin 5 → Pt 5 → ℝ :=
  cdiffOf (christoffel (ksMetric b v k) (ksInverse bi v k)) (christoffel b bi)

/-- Lowered background derivative `β_{cd} = Σ_j b_{dj} (∇̄_c k)^j`. -/
noncomputable def covL (b bi : Metric 5) (k : Pt 5 → Fin 5 → ℝ) (x : Pt 5) (c d : Fin 5) : ℝ :=
  ∑ j, b d j x * covD (christoffel b bi) k x c j

/-- Lowered background Christoffel contraction `Σ_e Γ̄^e_{cd} ℓ_e`. -/
noncomputable def chrL (b bi : Metric 5) (k : Pt 5 → Fin 5 → ℝ) (x : Pt 5) (c d : Fin 5) : ℝ :=
  ∑ e, christoffel b bi e c d x * lowerK b k x e

/-- Lowered actual background acceleration `a_d = Σ_j b_dj (accel b bi k)^j`. -/
noncomputable def accL (b bi : Metric 5) (k : Pt 5 → Fin 5 → ℝ) (x : Pt 5) (d : Fin 5) : ℝ :=
  ∑ j, b d j x * accel b bi k x j

/-- Profile derivative along the KS vector, `k(v) = Σ_c k^c ∂_c v`. -/
noncomputable def dprof (v : Pt 5 → ℝ) (k : Pt 5 → Fin 5 → ℝ) (x : Pt 5) : ℝ :=
  ∑ c, k x c * pd c v x

/-- `∇̄_c h_{pq}` for `h = v ℓ ⊗ ℓ`: `∂_c v ℓ_p ℓ_q + v β_{cp} ℓ_q + v ℓ_p β_{cq}`. -/
noncomputable def nablaH (b bi : Metric 5) (v : Pt 5 → ℝ) (k : Pt 5 → Fin 5 → ℝ) (x : Pt 5)
    (c p q : Fin 5) : ℝ :=
  pd c v x * lowerK b k x p * lowerK b k x q + v x * covL b bi k x c p * lowerK b k x q
    + v x * lowerK b k x p * covL b bi k x c q

/-! ### Generic facts (no Kerr–Schild data) -/

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

/-! ### Genuine first derivatives on the open `U` -/

/-! ### The lowered difference connection -/

/-! ### Acceleration transfer -/

end KSData

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry