V-02 Riemann and Weyl tensors from II's curvature

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/Riemann.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.hessG, ExactVacuumAtlas.EinsteinMaxwell.NP.negMetric, ExactVacuumAtlas.EinsteinMaxwell.NP.quadQ, ExactVacuumAtlas.EinsteinMaxwell.NP.riem, ExactVacuumAtlas.EinsteinMaxwell.NP.riemLow, ExactVacuumAtlas.EinsteinMaxwell.NP.weyl
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Certificate
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
/-!
# Atlas V-02 (A): Riemann and Weyl tensors from the registered matrix curvature

B3 local definition layer (`mission/PHYSICS_BOUNDARY.md` §L). Nothing new is assumed about curvature: the full
Riemann tensor is **read off** II's matrix curvature `curv` of the connection matrices `connMat (christoffel g gi)`
(`Atlas/Transport/Connection.lean`, unchanged; `connMat Γ c y a b = Γ a c b y`, first lower index = direction):

* `riem g gi a b c d x = (curv (connMat (christoffel g gi)) c d x) a b = R^a_{bcd}`
  `= ∂_c Γ^a_{db} − ∂_d Γ^a_{cb} + Σ_e (Γ^a_{ce} Γ^e_{db} − Γ^a_{de} Γ^e_{cb})` (`riem_expand`), i.e.
  `R(∂_c, ∂_d) ∂_b = R^a_{bcd} ∂_a` with `R(X,Y) = [∇_X, ∇_Y] − ∇_{[X,Y]}` — Hintz's operator convention;
* `riemLow g gi a b c d x = Σ_e g_{ae} R^e_{bcd}` (first index lowered with the same `g`);
* `weyl g gi` (4D): `C_{abcd} = R_{abcd} − ½(g_{ac}R_{bd} − g_{ad}R_{bc} − g_{bc}R_{ad} + g_{bd}R_{ac})
  + (R/6)(g_{ac}g_{bd} − g_{ad}g_{bc})` with IV's `ricciOf`, `ricciScalar` (unchanged).

Proved on the open domain of any `MetricData` (symmetric `g`, genuine inverse `gi`, `C^∞`; **no curvature or field
equation**): the contraction is the registered Ricci tensor (`ricciOf_eq_riem_contr`, `ricciOf_eq_riemLow_contr`),
the explicit second-derivative formula (`riemLow_expl`), the four algebraic symmetries, symmetry of `ricciOf`, the
Weyl symmetries and `g^{ac} C_{abcd} = 0` (valid with `Ric ≠ 0`), and smoothness. Einstein–Maxwell algebra:
`tr_g E = −R` and `Ric = 2S + E − ½ g tr_g E` (IV's residual `E`, unchanged). Signature bridge: for
`g' = −g`, `gi' = −gi` the Christoffel symbols, `R^a_{bcd}` and `R_{ab}` are unchanged, while `R`, `R_{abcd}`,
`C_{abcd}` and IV's stress `S` change sign, and `E' = E + 4S` (so `(−g, F)` is **not** an `E = 0` certificate).
-/

open scoped ContDiff
open Matrix

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

variable {n : ℕ}

/-! ### Definitions -/

/-- `R^a_{bcd}`, read off II's matrix curvature of `connMat (christoffel g gi)`. -/
noncomputable def riem (g gi : Metric n) (a b c d : Fin n) (x : Pt n) : ℝ :=
  curv (connMat (christoffel g gi)) c d x a b

/-- `R_{abcd} = Σ_e g_{ae} R^e_{bcd}`. -/
noncomputable def riemLow (g gi : Metric n) (a b c d : Fin n) (x : Pt n) : ℝ :=
  ∑ e, g a e x * riem g gi e b c d x

/-- Weyl tensor (4D), all indices down, built from `riemLow`, IV's `ricciOf` and `ricciScalar`. -/
noncomputable def weyl (g gi : Metric 4) (a b c d : Fin 4) (x : Pt 4) : ℝ :=
  riemLow g gi a b c d x
    - (g a c x * ricciOf g gi b d x - g a d x * ricciOf g gi b c x
        - g b c x * ricciOf g gi a d x + g b d x * ricciOf g gi a c x) / 2
    + ricciScalar g gi x * (g a c x * g b d x - g a d x * g b c x) / 6

/-- Proof-internal notation: second coordinate derivatives of the metric, `∂_i ∂_j g_{kl}`. -/
noncomputable def hessG (g : Metric n) (i j k l : Fin n) (y : Pt n) : ℝ := pd i (pd j (g k l)) y

/-- Proof-internal notation: the quadratic part `Σ_{e f} g^{ef} (Γ_{e,da} Γ_{f,cb} − Γ_{e,ca} Γ_{f,db})`. -/
noncomputable def quadQ (g gi : Metric n) (a b c d : Fin n) (y : Pt n) : ℝ :=
  ∑ e, ∑ f, gi e f y * (chr1 g e d a y * chr1 g f c b y - chr1 g e c a y * chr1 g f d b y)

/-- The metric with reversed sign (signature `(+,−,−,−)` from `(−,+,+,+)`). -/
def negMetric (g : Metric n) : Metric n := fun i j x => -g i j x

/-! ### Unconditional facts -/

/-! ### Metric data: inverse, symmetry, first-kind symbols -/

section metric

variable {g gi : Metric n} {U : Set (Pt n)}

end metric

/-! ### The explicit formula for `R_{abcd}` -/

section formula

variable {g gi : Metric n} {U : Set (Pt n)}

end formula

/-! ### Algebraic symmetries -/

section symm

variable {g gi : Metric n} {U : Set (Pt n)}

end symm

/-! ### Ricci tensor as a contraction -/

section ricci

variable {g gi : Metric n} {U : Set (Pt n)}

end ricci

/-! ### Smoothness -/

section smooth

variable {g gi : Metric n} {U : Set (Pt n)}

end smooth

/-! ### Weyl tensor: symmetries and trace-freeness (4D) -/

section weyl4

variable {g gi : Metric 4} {U : Set (Pt 4)}

end weyl4

/-! ### Einstein–Maxwell algebra: Ricci in terms of the residual -/

section em

variable {g gi : Metric 4} {F : TwoForm 4} {x : Pt 4}

end em

/-! ### Signature bridge `g ↦ −g` -/

section neg

variable (g gi : Metric n)

end neg

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