V-02 covariant frame derivative of the curvature

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/Bianchi.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.bianchiX, ExactVacuumAtlas.EinsteinMaxwell.NP.covX
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_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_Riemann
import Definitions.Def_Atlas_Kerr_InAtoms
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
/-!
# Atlas V-02 (D, general): second Bianchi identity in a general complex frame

For any `FrameData` (no curvature, NP or field equation):

* `gauge_bianchi`: the curvature `Fom` of the coordinate-direction connection `ω_μ` satisfies
  `Σ_cyc(μνλ) (∂_μ F_{νλ} + [ω_μ, F_{νλ}]) = 0` (symmetry of mixed partials + Jacobi identity);
* **`frame_bianchi`**: `Σ_cyc(E,A,B) (D_E R_{AB} + [Ω_E, R_{AB}] − Σ_K c^K_{EA} R_{KB}) = 0` for the frame curvature
  `R_{AB} = Rfr A B` — the non-coordinate term `−c R` is kept;
* `frame_bianchi_cov`: the same in covariant form, `Σ_cyc (∇_E R)_{AB} = 0` with
  `(∇_E R)_{AB} = D_E R_{AB} + [Ω_E, R_{AB}] − Σ_K Ω_E^K_A R_{KB} − Σ_K Ω_E^K_B R_{AK}` (torsion-free).
-/

open scoped ContDiff Matrix
open Complex

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

variable {n : ℕ}

section bianchi

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

/-- The frame Bianchi expression `D_C R_{AB} + [Ω_C, R_{AB}] − Σ_K c^K_{CA} R_{KB}`. -/
noncomputable def bianchiX (g gi : Metric n) (E Θ : Fin n → Fin n → Pt n → ℂ) (C A B : Fin n) (x : Pt n) :
    Matrix (Fin n) (Fin n) ℂ :=
  Dmat E C (Rfr g gi E Θ A B) x + Omega g gi E Θ C x * Rfr g gi E Θ A B x
    - Rfr g gi E Θ A B x * Omega g gi E Θ C x - ∑ K, cfr E Θ K C A x • Rfr g gi E Θ K B x

/-- Covariant frame derivative of the curvature, `(∇_C R)_{AB}` (matrix in the remaining two indices). -/
noncomputable def covX (g gi : Metric n) (E Θ : Fin n → Fin n → Pt n → ℂ) (C A B : Fin n) (x : Pt n) :
    Matrix (Fin n) (Fin n) ℂ :=
  Dmat E C (Rfr g gi E Θ A B) x + Omega g gi E Θ C x * Rfr g gi E Θ A B x
    - Rfr g gi E Θ A B x * Omega g gi E Θ C x
    - ∑ K, Omega g gi E Θ C x K A • Rfr g gi E Θ K B x - ∑ K, Omega g gi E Θ C x K B • Rfr g gi E Θ A K x

end bianchi

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).