-- 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/CoordinateAcceleration.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic.PregeodesicAt, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic.accel
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_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

/-! # VII-07 (F3b): actual coordinate acceleration of a vector field

For a coordinate metric `g` with candidate inverse `ginv` on `Pt n` (total coordinate dimension
`n`) and a vector field `K : Pt n → (Fin n → ℝ)`, the **actual** acceleration `∇_K K` is

  `accel g ginv K x ^ i = Σ_j K^j(x) ∂_j(K^i)(x) + Σ_{j,l} Γ^i_{jl}(x) K^j(x) K^l(x)`,

built from the registered class-A `pd` and `christoffel` (no replacement formula). A field is
**pregeodesic** at `x` if `accel = κ • K` for some real `κ` (non-affine parametrisation allowed),
and **affinely geodesic** if `accel = 0`. Proved here, under genuine (Fréchet) differentiability:
the product/sum rules for `pd` (no junk values), locality of `accel` on open neighbourhoods, the
lowered-index identity
  `(g·accel)_b = Σ_j K^j ∂_j(g K)_b - ½ Σ_{j,l} ∂_b(g_{jl}) K^j K^l`  (from `g·ginv = 1` only),
and the scaling law `accel(σK) = σ² accel K + σ (K·∂σ) K` for an arbitrary differentiable scalar
`σ` (any coordinate dependence). The ES5 part: the actual metric slices along `t, φ, ψ` are
constant, and the metric contraction with a frozen vector has the derivative of its slice. -/

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

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic

variable {n : ℕ}

/-- **Actual coordinate acceleration** `(∇_K K)^i` (registered `pd`, `christoffel`). -/
noncomputable def accel (g ginv : Metric n) (K : Pt n → Fin n → ℝ) (x : Pt n) : Fin n → ℝ :=
  fun i => ∑ j, K x j * pd j (fun y => K y i) x +
    ∑ j, ∑ l, christoffel g ginv i j l x * K x j * K x l

/-- Pregeodesic (non-affinely parametrised geodesic) at `x`: `∇_K K = κ K` for some `κ`. -/
def PregeodesicAt (g ginv : Metric n) (K : Pt n → Fin n → ℝ) (x : Pt n) : Prop :=
  ∃ κ : ℝ, accel g ginv K x = κ • K x

/-! ## Genuine product and sum rules for `pd` -/

/-! ## The lowered-index identity (from `g · ginv = 1` only) -/

/-! ## Scaling by an arbitrary differentiable scalar -/

/-! ## Metric contraction with a frozen vector -/

/-! ## ES5: the actual metric slices (coordinates `x = (t, r, u, φ, ψ)`, dimension 5) -/

section ES5

open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections

variable (B D A H W : ℝ → ℝ)

variable {B D A H W}

end ES5

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic