-- 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/MaxwellFrame.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.alphaSq, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.alphaSqFrame, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.betaSqFrame, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.contract2, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.frameInv, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.frameQ, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.frameZ, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.principalFrame
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_PaperGauge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVP
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVPEquivalence

/-!
# VII-06 (F3a): the actual ES5 Maxwell frame

Pointwise algebra in the existing frame `esFrame` (columns `E₀ = ∂t + W(∂φ + ∂ψ)`, `E₁ = ∂R`,
`E₂ = ∂u`, `E₃ = ∂φ + ∂ψ`, `E₄ = (1-u)∂φ - u∂ψ`), where the actual metric is
`d = Eᵀ g E = diag(-B, D, A/(4u(1-u)), H, A u(1-u))` (`esFrame_spec`).

* Scalar layer (Class B, finite algebra): the frame quadratic form `frameQ`, the frame Faraday
  matrix `frameFaraday`, the frame mixed vector `frameZ = d⁻¹ (Eᵀ F E) v`, the raw discriminant
  `alphaSqFrame = (e²/B - (Ψ')²/H)/D` (no square root), the sum-of-squares identity and the two
  principal vectors `K_λ = (e/B, λ, 0, -Ψ'/H, 0)`.
* Actual layer: the explicit inverse `frameInv` of `esFrame` (both compositions), and the binding of
  the actual `esMetric`, `esInverse`, `esFaraday = extD esPotential` to the scalar layer (via the
  VI table `Generic.bind_F`). The frame is only a pointwise tensor pullback: no connection or
  curvature of the frame is computed here.

Paper dictionary (`PaperGauge`): `B = f`, `D = m/(4fN)`, `A = m/f`, `H = N/m`, `Φ = p`, `Ψ = a`,
`e = p' + w a'`; `alphaSq = 4((N/m) e² - f (a')²)`.
-/

open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.ES5
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial
open scoped Matrix

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections

/-! ## Scalar frame algebra -/

/-- Frame quadratic form `q(v) = vᵀ d v`, `d = diag(-f, D, A/(4u(1-u)), H, A u(1-u))`. -/
noncomputable def frameQ (f D A H u : ℝ) (v : Fin 5 → ℝ) : ℝ :=
  -f * v 0 ^ 2 + D * v 1 ^ 2 + A / (4 * u * (1 - u)) * v 2 ^ 2 + H * v 3 ^ 2 +
    A * u * (1 - u) * v 4 ^ 2

/-- Frame components of the mixed vector `z = d⁻¹ (Eᵀ F E) v`. -/
noncomputable def frameZ (f D A H u e a1 a0 : ℝ) (v : Fin 5 → ℝ) : Fin 5 → ℝ :=
  ![e / f * v 1, (e * v 0 + a1 * v 3) / D, 4 * u * (1 - u) * a0 / A * v 4,
    -(a1 / H) * v 1, -(a0 / (A * u * (1 - u))) * v 2]

/-- Raw electric discriminant `(e²/f - (a')²/H)/D` (no square root taken). -/
noncomputable def alphaSqFrame (f D H e a1 : ℝ) : ℝ := (e ^ 2 / f - a1 ^ 2 / H) / D

/-- Magnetic discriminant `4a²/A²` (no signed eigenvalue chosen). -/
noncomputable def betaSqFrame (A a0 : ℝ) : ℝ := 4 * a0 ^ 2 / A ^ 2

/-- Raw-frame principal vector `K_λ = (e/f, λ, 0, -a'/H, 0)` (no normalisation, no `1/α`). -/
noncomputable def principalFrame (f H e a1 lam : ℝ) : Fin 5 → ℝ := ![e / f, lam, 0, -(a1 / H), 0]

/-! ## The actual frame: explicit inverse and bindings to the actual tensors -/

/-- Coordinate → frame components, the explicit inverse of `esFrame` (no square roots):
`v = (k⁰, k¹, k², u k³ + (1-u) k⁴ - W k⁰, k³ - k⁴)`. -/
noncomputable def frameInv (W : ℝ → ℝ) (x : Pt 5) (k : Fin 5 → ℝ) : Fin 5 → ℝ :=
  ![k 0, k 1, k 2, x 2 * k 3 + (1 - x 2) * k 4 - W (x 1) * k 0, k 3 - k 4]

/-- Actual contraction `T(k,k) = Σ_ab T_ab(x) k^a k^b` of a covariant 2-tensor. -/
noncomputable def contract2 (T : Fin 5 → Fin 5 → Pt 5 → ℝ) (x : Pt 5) (k : Fin 5 → ℝ) : ℝ :=
  ∑ a, ∑ b, T a b x * k a * k b

variable {R : Set ℝ} {B D A H W Φ Ψ : ℝ → ℝ}

/-! ## The paper-dictionary discriminant -/

/-- **Actual electric discriminant** on the paper dictionary, without a square root:
`alphaSq(R) = 4((N/m) e² - f (a')²)`, `e = p' + w a'` (genuine `deriv`). -/
noncomputable def alphaSq (f m N w p a : ℝ → ℝ) (r : ℝ) : ℝ :=
  4 * (N r / m r * eFun w p a r ^ 2 - f r * deriv a r ^ 2)

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections