V-02 null-frame objects

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/FrameNull.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.FfrF, ExactVacuumAtlas.EinsteinMaxwell.NP.NullFrameData, ExactVacuumAtlas.EinsteinMaxwell.NP.NullFrameData.FfrM, ExactVacuumAtlas.EinsteinMaxwell.NP.cL, ExactVacuumAtlas.EinsteinMaxwell.NP.ccontr4, ExactVacuumAtlas.EinsteinMaxwell.NP.fvec, ExactVacuumAtlas.EinsteinMaxwell.NP.omL, ExactVacuumAtlas.EinsteinMaxwell.NP.ricF, ExactVacuumAtlas.EinsteinMaxwell.NP.riemFL, ExactVacuumAtlas.EinsteinMaxwell.NP.weylF
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_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 (B, null frames): lowered connection, Koszul formula, frame Riemann and Weyl components

Four-dimensional specialisation of `FrameConn` to frames whose (complex-bilinear) Gram matrix is V-01's constant
`etaNull` (`g(l,n) = −1`, `g(m,m̄) = 1`, signature `(−,+,+,+)`); index order `0 = l, 1 = n, 2 = m, 3 = m̄`.
`NullFrameData` adds only this kinematic normalisation to `FrameData` (no curvature, NP or field equation).
Class B definitions:

* `omL C A B = Σ_K η_{CK} Ω_A^K_B = g(e_C, ∇_{e_A} e_B)` and `cL C A B = Σ_K η_{CK} c^K_{AB} = g(e_C, [e_A, e_B])`;
* `ccontr4 T x u v w z = Σ T_{abcd} u^a v^b w^c z^d` (complex-multilinear, no conjugation);
* `riemFL I J A B = Σ_K η_{IK} (Rfr A B)^K_J` (frame curvature with the first index lowered);
* `ricF A B = Ric(e_A, e_B)`, `weylF I J A B = C(e_I, e_J, e_A, e_B)`, `FfrF A B = F(e_A, e_B)`.

Proved: `coMat_eq` (`Θ = η Eᵀ g`), `cmat_gi_eq` (`g⁻¹ = E η Eᵀ`), `omL_antisymm` (metric compatibility),
`cL_eq_omL` (torsion), **`omL_koszul`** (`2 omL_{CAB} = cL_{CAB} − cL_{ABC} + cL_{BCA}`), `cL_eq_ccontr`
(`cL_{CAB} = g(e_C, brk_{AB})`), **`riemFL_eq`** (frame curvature = `R_{abcd}` contracted with the frame), the frame
Weyl decomposition `weylF_eq`, frame symmetries and trace-freeness of `weylF`, and the frame form of IV's stress
`emStressF_eq`.
-/

open scoped ContDiff Matrix
open Complex

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

/-- A null frame: `FrameData` with Gram matrix `etaNull` on `U`. -/
structure NullFrameData (g gi : Metric 4) (E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ) (U : Set (Pt 4)) : Prop
    extends FrameData g gi E Θ U where
  gram : ∀ x ∈ U, gramM g E x = etaNull

/-- `g(e_C, ∇_{e_A} e_B)`. -/
noncomputable def omL (g gi : Metric 4) (E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ) (C A B : Fin 4) (x : Pt 4) : ℂ :=
  ∑ K, etaNull C K * Omega g gi E Θ A x K B

/-- `g(e_C, [e_A, e_B])`. -/
noncomputable def cL (E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ) (C A B : Fin 4) (x : Pt 4) : ℂ :=
  ∑ K, etaNull C K * cfr E Θ K A B x

/-- Complex-multilinear contraction of a real 4-index field with four complex vectors. -/
noncomputable def ccontr4 {n : ℕ} (T : Fin n → Fin n → Fin n → Fin n → Pt n → ℝ) (x : Pt n)
    (u v w z : Fin n → ℂ) : ℂ :=
  ∑ a, ∑ b, ∑ c, ∑ d, (T a b c d x : ℂ) * u a * v b * w c * z d

/-- Frame curvature with the first index lowered by `etaNull`. -/
noncomputable def riemFL (g gi : Metric 4) (E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ) (I J A B : Fin 4) (x : Pt 4) : ℂ :=
  ∑ K, etaNull I K * Rfr g gi E Θ A B x K J

/-- The frame vector `e_A` at `x` as a coordinate vector. -/
def fvec (E : Fin 4 → Fin 4 → Pt 4 → ℂ) (A : Fin 4) (x : Pt 4) : Fin 4 → ℂ := fun μ => E A μ x

/-- `Ric(e_A, e_B)`. -/
noncomputable def ricF (g gi : Metric 4) (E : Fin 4 → Fin 4 → Pt 4 → ℂ) (A B : Fin 4) (x : Pt 4) : ℂ :=
  ccontr (ricciOf g gi) x (fvec E A x) (fvec E B x)

/-- `C(e_I, e_J, e_A, e_B)`. -/
noncomputable def weylF (g gi : Metric 4) (E : Fin 4 → Fin 4 → Pt 4 → ℂ) (I J A B : Fin 4) (x : Pt 4) : ℂ :=
  ccontr4 (weyl g gi) x (fvec E I x) (fvec E J x) (fvec E A x) (fvec E B x)

/-- `F(e_A, e_B)`. -/
noncomputable def FfrF (F : TwoForm 4) (E : Fin 4 → Fin 4 → Pt 4 → ℂ) (A B : Fin 4) (x : Pt 4) : ℂ :=
  ccontr F x (fvec E A x) (fvec E B x)

/-! ### `etaNull` and index bookkeeping -/

namespace NullFrameData

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

/-! ### Lowered connection: metric compatibility, torsion, Koszul -/

/-! ### Lowered frame Riemann tensor -/

end NullFrameData

/-! ### Symmetries of 4-index contractions -/

section c4

variable {T : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Pt 4 → ℝ} {x : Pt 4}

end c4

namespace NullFrameData

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

/-! ### Frame Weyl tensor -/

/-! ### Frame components of a real 2-tensor; IV's stress in the frame -/

/-- Matrix of frame components `F(e_A, e_B)`. -/
noncomputable def FfrM (F : TwoForm 4) (E : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℂ :=
  (frMat E x)ᵀ * cmat F x * frMat E x

end NullFrameData

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