V-02 lowered covariant curvature derivative

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/NPBianchi.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.covL
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Lift
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_KN_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_KN_Domain
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Bianchi
import Definitions.Def_Atlas_EinsteinMaxwell_NP_CCalc
import Definitions.Def_Atlas_EinsteinMaxwell_NP_FrameConn
import Definitions.Def_Atlas_EinsteinMaxwell_NP_FrameNull
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNFrame
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPMaxwell
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPRicci
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPScalars
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Riemann
import Definitions.Def_Atlas_Kerr_InAtoms
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
/-!
# Atlas V-02 (D): lowered frame Bianchi identity and the Weyl/Ricci decomposition under frame derivatives

General (any null frame; no field equation):

* `bianchi_low`: the covariant second Bianchi identity `Σ_cyc(C,A,B) (∇_C R)_{IJAB} = 0` with the first index lowered,
  written with the connection components `omL`, `Ω` and the frame curvature `riemFL`:
  `(∇_C R)_{IJAB} = D_C R_{IJAB} + Σ_L ω_{ICL} Σ_M η_{LM} R_{MJAB} − Σ_L R_{ILAB} Ω_C^L_J − Σ_K Ω_C^K_A R_{IJKB}
  − Σ_K Ω_C^K_B R_{IJAK}`;
* `riemFL_decomp`, `fdir_riemFL_decomp`: `R_{IJAB} = C_{IJAB} + ½(η_{IA}R_{JB} − η_{IB}R_{JA} − η_{JA}R_{IB}
  + η_{JB}R_{IA}) − (R/6)(η_{IA}η_{JB} − η_{IB}η_{JA})`, also under a frame derivative (the Ricci tensor and the
  scalar curvature are kept as source terms; with IV's residual they are `2S + E − ½ g tr E`).
-/

open scoped ContDiff Matrix
open Complex

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

variable {g gi : Metric 4} {E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ} {U : Set (Pt 4)}

/-! ### Smoothness of frame curvature, Weyl and Ricci components -/

/-! ### Lowered covariant Bianchi identity -/

/-- The lowered covariant frame derivative of the curvature, `(∇_C R)_{IJAB}`. -/
noncomputable def covL (g gi : Metric 4) (E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ) (I J C A B : Fin 4) (x : Pt 4) : ℂ :=
  fdir E C (riemFL g gi E Θ I J A B) x
    + ∑ L, omL g gi E Θ I C L x * ∑ M, etaNull L M * riemFL g gi E Θ M J A B x
    - ∑ L, riemFL g gi E Θ I L A B x * Omega g gi E Θ C x L J
    - ∑ K, Omega g gi E Θ C x K A * riemFL g gi E Θ I J K B x
    - ∑ K, Omega g gi E Θ C x K B * riemFL g gi E Θ I J A K x

/-! ### Weyl + Ricci decomposition of the frame curvature -/

end ExactVacuumAtlas.EinsteinMaxwell.NP

• Endorsed by Shuze Chen · Oct 24, 2026

  Confirmed by the moderator at approval.

• Endorsed by He Wang · Oct 24, 2026

  Confirmed by the mission captain (proposal self-audit).