-- 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/RicciNullDirections.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.kMinus, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.kPlus, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.principalCoord
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_ScalarCertificate
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_SmoothBranch

/-!
# VII-06 (F3a, part B): actual ES5 Ricci-null directions

The Ricci tensor is always the actual `ricciOf (esMetric …) (esInverse …)` of the candidate,
connected to its own Einstein–Maxwell equations through the VI identity
`ricciOf_of_einstein_zero` (total dimension 5: `R_ab = 2 F_ac g^cd F_bd - g_ab F²/3`). It is
contracted with actual coordinate vectors `k`; the frame enters only through the pointwise
pullback `k = esFrame v` (`frameInv`), never by applying `ricciOf` to a frame metric.

* `ricci_contract2_actual`: on the field equations, `Ric(k,k) = 2 g(z,z) - g(k,k) F²/3` with the
  actual mixed vector `z = (g⁻¹ F) k`.
* `vii06_ricci_null_directions`: at a positive point (`f, m, N > 0`, `0 < u < 1`) with
  `alphaSq > 0`, the nonzero actual null Ricci-null vectors are exactly the nonzero multiples of
  the two actual principal vectors `kPlus`, `kMinus`, which are eigenvectors of the actual
  `g⁻¹ F` with eigenvalues `±√alphaSq`.
* `vii06_charged_tail_ricci_null_directions` (actual `PaperBVP`) and
  `vii06_certificate_tail_directions` (the candidate's own `EMCertificateD`): A + B on the actual
  charged tail.

Not proved here (pending): Kerr–Schild ⇒ Ricci-null, geodesic principal field ⇒ `G = 0`.
-/

open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.ES5
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt
open ExactVacuumAtlas.EinsteinMaxwell.D (einsteinMaxwellD EMCertificateD)
open scoped Matrix

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections

/-! ## Contraction of the trace-reversed field equations -/

section Contraction

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

end Contraction

/-! ## The two actual principal null directions (paper dictionary) -/

/-- Actual coordinate principal vector `𝒦_λ = esFrame · K_λ` of the paper dictionary. -/
noncomputable def principalCoord (f m N w p a : ℝ → ℝ) (lam : ℝ) (x : Pt 5) : Fin 5 → ℝ :=
  esFrame w x *ᵥ
    principalFrame (f (x 1)) (Hfun m N (x 1)) (eFun w p a (x 1)) (deriv a (x 1)) lam

/-- `k₊ = 𝒦_{+√alphaSq}`. -/
noncomputable def kPlus (f m N w p a : ℝ → ℝ) (x : Pt 5) : Fin 5 → ℝ :=
  principalCoord f m N w p a (Real.sqrt (alphaSq f m N w p a (x 1))) x

/-- `k₋ = 𝒦_{-√alphaSq}`. -/
noncomputable def kMinus (f m N w p a : ℝ → ℝ) (x : Pt 5) : Fin 5 → ℝ :=
  principalCoord f m N w p a (-Real.sqrt (alphaSq f m N w p a (x 1))) x

section Pointwise

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

end Pointwise

/-! ## A + B on the actual charged tail -/

section Tail

variable {I : Set ℝ} {f m N w p a F b A : ℝ → ℝ} {s h ε : ℝ}

end Tail

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections