V-02 general complex frame connection and curvature

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/FrameConn.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.Dmat, ExactVacuumAtlas.EinsteinMaxwell.NP.Fom, ExactVacuumAtlas.EinsteinMaxwell.NP.FrameData, ExactVacuumAtlas.EinsteinMaxwell.NP.GamC, ExactVacuumAtlas.EinsteinMaxwell.NP.Omega, ExactVacuumAtlas.EinsteinMaxwell.NP.Rfr, ExactVacuumAtlas.EinsteinMaxwell.NP.brk, ExactVacuumAtlas.EinsteinMaxwell.NP.cfr, ExactVacuumAtlas.EinsteinMaxwell.NP.coMat, ExactVacuumAtlas.EinsteinMaxwell.NP.fdir, ExactVacuumAtlas.EinsteinMaxwell.NP.frMat, ExactVacuumAtlas.EinsteinMaxwell.NP.gramM, ExactVacuumAtlas.EinsteinMaxwell.NP.omegaC, ExactVacuumAtlas.EinsteinMaxwell.NP.riemC
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_NP_CCalc
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Riemann
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
/-!
# Atlas V-02 (B): connection of a general smooth complex frame, commutators, curvature bridge

B3 local definition layer (`mission/PHYSICS_BOUNDARY.md` §L). A **general** frame on an open set `U ⊆ ℝⁿ`:
complex components `E A μ x = e_A^μ(x)` (frame matrix `frMat E x`, column `A` = vector `e_A`) and a genuine
two-sided dual `Θ C μ x = θ^C_μ(x)` (`coMat Θ x`). No null/orthonormal normalisation, no field equation, no
reality condition. Directional derivatives use V-01's `cpdC` (real slice derivative of complex functions; no
holomorphy). Definitions (class B, transparent; `Γ = christoffel g gi`, first lower index = direction):

* `fdir E A f = Σ_μ e_A^μ ∂_μ f` (`D_A`);
* `omegaC g gi E Θ μ = Θ (∂_μ E + Γ_μ E)`: the connection in coordinate directions, gauge-transformed to the frame;
* `Omega g gi E Θ A = Σ_μ e_A^μ ω_μ`, entries `(Ω_A)^C_B = Σ_ν θ^C_ν (D_A e_B^ν + Σ_{μλ} Γ^ν_{μλ} e_A^μ e_B^λ)`;
* `brk E A B μ = D_A e_B^μ − D_B e_A^μ` and `cfr E Θ C A B = Σ_μ θ^C_μ brk^μ_{AB}` (`c^C_{AB}`);
* `Rfr g gi E Θ A B = D_A Ω_B − D_B Ω_A + Ω_A Ω_B − Ω_B Ω_A − Σ_C c^C_{AB} Ω_C` — **with** the non-coordinate
  term `−Σ_C c^C_{AB} Ω_C`.

Main results on `U` (hypothesis bundle `FrameData`: `MetricData`, `C^∞` frame and dual, duality):
`fdir_comm` (`[D_A, D_B] f = Σ_C c^C_{AB} D_C f`), `cfr_eq_Omega` (torsion-free: `c^C_{AB} = Ω_A^C_B − Ω_B^C_A`),
`pdMC_gramM` / `fdir_gram` (metric compatibility `D_A G = Ω_Aᵀ G + G Ω_A`, `G = Eᵀ g E`), `Fom_eq` (gauge
covariance: the curvature of `ω` is `Θ · R_{μν} · E`), `Rfr_eq` and **`Rfr_eq_riem`**:
`(Rfr A B)^I_J = Σ θ^I_ρ R^ρ_{σμν} e_J^σ e_A^μ e_B^ν` with `R = riem g gi` read off II's `curv`.
-/

open scoped ContDiff Matrix
open Complex

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

variable {n : ℕ}

/-! ### Definitions -/

/-- Frame matrix: `frMat E x μ A = e_A^μ(x)` (column `A` is the vector `e_A`). -/
def frMat (E : Fin n → Fin n → Pt n → ℂ) (x : Pt n) : Matrix (Fin n) (Fin n) ℂ :=
  Matrix.of fun μ A => E A μ x

/-- Coframe matrix: `coMat Θ x C μ = θ^C_μ(x)`. -/
def coMat (Θ : Fin n → Fin n → Pt n → ℂ) (x : Pt n) : Matrix (Fin n) (Fin n) ℂ :=
  Matrix.of fun C μ => Θ C μ x

/-- Kinematic/regularity hypotheses for a general complex frame (no curvature, NP or field equation). -/
structure FrameData (g gi : Metric n) (E Θ : Fin n → Fin n → Pt n → ℂ) (U : Set (Pt n)) : Prop where
  metric : MetricData g gi U
  smooth_E : ∀ A μ, ContDiffOn ℝ ∞ (E A μ) U
  smooth_Θ : ∀ A μ, ContDiffOn ℝ ∞ (Θ A μ) U
  dual : ∀ x ∈ U, coMat Θ x * frMat E x = 1

/-- Frame derivative `D_A f = Σ_μ e_A^μ ∂_μ f`. -/
noncomputable def fdir (E : Fin n → Fin n → Pt n → ℂ) (A : Fin n) (f : Pt n → ℂ) (x : Pt n) : ℂ :=
  ∑ μ, E A μ x * cpdC μ f x

/-- Complexified connection matrices `(Γ_μ)^a_b = Γ^a_{μb}`. -/
noncomputable def GamC (g gi : Metric n) (μ : Fin n) (x : Pt n) : Matrix (Fin n) (Fin n) ℂ :=
  (connMat (christoffel g gi) μ x).map (fun t : ℝ => (t : ℂ))

/-- `ω_μ = Θ (∂_μ E + Γ_μ E)`. -/
noncomputable def omegaC (g gi : Metric n) (E Θ : Fin n → Fin n → Pt n → ℂ) (μ : Fin n) (x : Pt n) :
    Matrix (Fin n) (Fin n) ℂ :=
  coMat Θ x * (pdMC μ (frMat E) x + GamC g gi μ x * frMat E x)

/-- Frame connection `Ω_A = Σ_μ e_A^μ ω_μ`; entry `(C, B)` is `Ω_A^C_B`. -/
noncomputable def Omega (g gi : Metric n) (E Θ : Fin n → Fin n → Pt n → ℂ) (A : Fin n) (x : Pt n) :
    Matrix (Fin n) (Fin n) ℂ :=
  ∑ μ, E A μ x • omegaC g gi E Θ μ x

/-- Coordinate components of the commutator `[e_A, e_B]^μ = D_A e_B^μ − D_B e_A^μ`. -/
noncomputable def brk (E : Fin n → Fin n → Pt n → ℂ) (A B μ : Fin n) (x : Pt n) : ℂ :=
  fdir E A (E B μ) x - fdir E B (E A μ) x

/-- Commutator coefficients `c^C_{AB} = θ^C([e_A, e_B])`. -/
noncomputable def cfr (E Θ : Fin n → Fin n → Pt n → ℂ) (C A B : Fin n) (x : Pt n) : ℂ :=
  ∑ μ, Θ C μ x * brk E A B μ x

/-- Frame derivative of a matrix field, `D_A M = Σ_μ e_A^μ ∂_μ M`. -/
noncomputable def Dmat (E : Fin n → Fin n → Pt n → ℂ) (A : Fin n) (M : Pt n → Matrix (Fin n) (Fin n) ℂ)
    (x : Pt n) : Matrix (Fin n) (Fin n) ℂ :=
  ∑ μ, E A μ x • pdMC μ M x

/-- Frame curvature, **including the non-coordinate term** `−Σ_C c^C_{AB} Ω_C`. -/
noncomputable def Rfr (g gi : Metric n) (E Θ : Fin n → Fin n → Pt n → ℂ) (A B : Fin n) (x : Pt n) :
    Matrix (Fin n) (Fin n) ℂ :=
  Dmat E A (Omega g gi E Θ B) x - Dmat E B (Omega g gi E Θ A) x
    + Omega g gi E Θ A x * Omega g gi E Θ B x - Omega g gi E Θ B x * Omega g gi E Θ A x
    - ∑ C, cfr E Θ C A B x • Omega g gi E Θ C x

/-- Curvature of `ω` in coordinate directions (proof-internal). -/
noncomputable def Fom (g gi : Metric n) (E Θ : Fin n → Fin n → Pt n → ℂ) (μ ν : Fin n) (x : Pt n) :
    Matrix (Fin n) (Fin n) ℂ :=
  pdMC μ (omegaC g gi E Θ ν) x - pdMC ν (omegaC g gi E Θ μ) x
    + omegaC g gi E Θ μ x * omegaC g gi E Θ ν x - omegaC g gi E Θ ν x * omegaC g gi E Θ μ x

/-- Complexified matrix curvature `(R_{μν})^ρ_σ = R^ρ_{σμν}`. -/
noncomputable def riemC (g gi : Metric n) (μ ν : Fin n) (x : Pt n) : Matrix (Fin n) (Fin n) ℂ :=
  (curv (connMat (christoffel g gi)) μ ν x).map (fun t : ℝ => (t : ℂ))

/-- Gram matrix `G = Eᵀ g E` of the frame (complex bilinear, no conjugation). -/
noncomputable def gramM (g : Metric n) (E : Fin n → Fin n → Pt n → ℂ) (x : Pt n) : Matrix (Fin n) (Fin n) ℂ :=
  (frMat E x)ᵀ * cmat g x * frMat E x

/-! ### Basic algebra -/

namespace FrameData

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

end FrameData

/-! ### Commutator of frame derivatives -/

section comm

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

end comm

/-! ### Torsion-freeness -/

/-! ### Gauge covariance of the curvature and the curvature bridge -/

section bridge

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

end bridge

/-! ### Metric compatibility -/

section compat

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

end compat

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