Coordinate geometry core: points, metrics, slice derivative, Christoffel symbols, Ricci tensor, Lorentzian signature

Definition

Atlas_Core_Basic

by He Wang · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

christoffel-symbolscoordinate-geometryexact-vacuum-atlasgeneral-relativitylorentzian-signaturericci-tensor

Dimension-parametric coordinate objects on $\mathbb R^n$ (points are functions $\{0,\dots,n-1\}\to\mathbb R$ ; nothing is a manifold). A coordinate metric is a matrix $g=(g_{ij})$ of real functions of the point; a second such matrix $\hat g$ is a candidate inverse. The slice derivative is $\partial_i f(x)=\frac{d}{du}f(x[x_i:=u])\big|_{u=x_i}$ (Mathlib's deriv, which returns $0$ where the slice is not differentiable; the full certificates prove the required $C^\infty$ smoothness, and derivative bridge lemmas establish the genuine-derivative interpretation on the relevant open domains; auxiliary algebraic identities need not each carry a separate smoothness hypothesis). The coordinate Christoffel symbols and coordinate Ricci tensor are

\Gamma^a_{bc}=\tfrac12\sum_k\hat g^{ak}\big(\partial_c g_{kb}+\partial_b g_{kc}-\partial_k g_{bc}\big),\qquad R_{bd}=\sum_i\Big(\partial_i\Gamma^i_{bd}-\partial_d\Gamma^i_{bi}+\sum_j\big(\Gamma^i_{ij}\Gamma^j_{bd}-\Gamma^i_{dj}\Gamma^j_{bi}\big)\Big),

with ricciOf g ĝ the Ricci tensor built from christoffel g ĝ; first index of $\Gamma$ up, contraction of the Riemann tensor on its first and third index. Also defined: the matrix $g(x)=(g_{ij}(x))$ , the Minkowski form $\eta_n=\mathrm{diag}(-1,1,\dots,1)$ in dimension $n+1$ , and Lorentzian: $G$ is Lorentzian if $E^{\mathsf T}GE=\eta_n$ for some matrix $E$ with invertible determinant.

Class-A definition layer of the atlas (registered in the project's physics boundary): the pinned Mathlib has no Levi-Civita connection or Ricci tensor for indefinite metrics, so these coordinate formulas are supplied here. For $n=4$ they coincide with the earlier platform definition KerrBL_CoordGeometry (proved by rfl in the source, bundle Atlas.Compat.KerrBL, not uploaded).

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Core.Basic; declarations: ExactVacuumAtlas.IsLorentzian, ExactVacuumAtlas.Metric, ExactVacuumAtlas.Pt, ExactVacuumAtlas.christoffel, ExactVacuumAtlas.eta, ExactVacuumAtlas.metricMatrix, ExactVacuumAtlas.pd, ExactVacuumAtlas.ricci, ExactVacuumAtlas.ricciOf. No theorem is proved inside the bundle; it imports only Mathlib and other Definitions.Def_* bundles.

Definition code

-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Core/Basic.lean
-- definition bundle: kept ExactVacuumAtlas.IsLorentzian, ExactVacuumAtlas.Metric, ExactVacuumAtlas.Pt, ExactVacuumAtlas.christoffel, ExactVacuumAtlas.eta, ExactVacuumAtlas.metricMatrix, ExactVacuumAtlas.pd, ExactVacuumAtlas.ricci, ExactVacuumAtlas.ricciOf
import Mathlib
/-!
# Exact Vacuum Atlas — coordinate geometry core

Dimension-parametric (`Fin n`) coordinate objects. Nothing here is a manifold: a metric is a
matrix of real functions on points of `ℝⁿ`, and every theorem about these objects states its
coordinate domain explicitly.

* `pd i f x` is the partial derivative `∂ᵢ f (x)`, defined as Mathlib's `deriv` of the
  one-variable slice `u ↦ f (x with xᵢ := u)`. Where the slice is not differentiable `deriv`
  returns the junk value `0`; certificates therefore carry explicit smoothness hypotheses, and
  `Atlas.Core.Pd` proves that under them every `pd` used is a genuine derivative.
* `christoffel g ginv a b c = Γᵃ_{bc} = ½ Σ_k ginv^{ak} (∂_c g_{kb} + ∂_b g_{kc} − ∂_k g_{bc})`.
* `ricci Γ b d = R_{bd} = Σ_i (∂_i Γⁱ_{bd} − ∂_d Γⁱ_{bi} + Σ_j (Γⁱ_{ij} Γʲ_{bd} − Γⁱ_{dj} Γʲ_{bi}))`.

Formulas, index order and signs are those of the specification layer `KerrBL_CoordGeometry`
of the earlier Kerr mission; `Atlas.Compat.KerrBL` proves they coincide for `n = 4`.
-/

namespace ExactVacuumAtlas

/-- A coordinate point of `ℝⁿ`. -/
abbrev Pt (n : ℕ) := Fin n → ℝ

/-- Components `g_{ij}` of a coordinate metric (or any rank-2 field) as functions of the point. -/
abbrev Metric (n : ℕ) := Fin n → Fin n → Pt n → ℝ

/-- Partial derivative `∂ᵢ f (x)` as the derivative of the slice through `x` along `xᵢ`. -/
noncomputable def pd {n : ℕ} (i : Fin n) (f : Pt n → ℝ) (x : Pt n) : ℝ :=
  deriv (fun u : ℝ => f (Function.update x i u)) (x i)

/-- Coordinate Christoffel symbols `Γᵃ_{bc}` of `g` with candidate inverse `ginv`. -/
noncomputable def christoffel {n : ℕ} (g ginv : Metric n) (a b c : Fin n) (x : Pt n) : ℝ :=
  (∑ k : Fin n, ginv a k x * (pd c (g k b) x + pd b (g k c) x - pd k (g b c) x)) / 2

/-- Coordinate Ricci tensor `R_{bd}` built from a family of Christoffel symbols. -/
noncomputable def ricci {n : ℕ} (Γ : Fin n → Fin n → Fin n → Pt n → ℝ) (b d : Fin n)
    (x : Pt n) : ℝ :=
  ∑ i : Fin n, (pd i (Γ i b d) x - pd d (Γ i b i) x
    + ∑ j : Fin n, (Γ i i j x * Γ j b d x - Γ i d j x * Γ j b i x))

/-- Ricci tensor of a metric `g` with candidate inverse `ginv`. -/
noncomputable def ricciOf {n : ℕ} (g ginv : Metric n) : Fin n → Fin n → Pt n → ℝ :=
  ricci (christoffel g ginv)

/-- The matrix `(g_{ij}(x))`. -/
def metricMatrix {n : ℕ} (g : Metric n) (x : Pt n) : Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun i j => g i j x

/-- Minkowski form `diag(-1, 1, …, 1)` in dimension `n+1`. -/
def eta (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ :=
  Matrix.diagonal fun i => if i = 0 then -1 else 1

/-- Lorentzian signature `(-,+,…,+)`: congruent to `eta n` through an invertible frame matrix
`E` (columns = an orthonormal frame). By Sylvester's law of inertia this is the usual notion;
the law itself is not needed for, and not used by, the certificates. -/
def IsLorentzian {n : ℕ} (G : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ) : Prop :=
  ∃ E : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ, IsUnit E.det ∧ E.transpose * G * E = eta n

end ExactVacuumAtlas

Source

coordinate Christoffel symbols and Ricci tensor: Müller–Grave catalogue.tex lines 277–281 (eq. ChristoffelSymbols), 287–290 (eq. RiemannTensor), 305–307 (R_{μν}=R^ρ_{μρν}), verified by the independent review 2026-10-13; R. M. Wald, General Relativity (1984) eqs. (3.1.30), (3.4.4)–(3.4.5) author-cited (not reviewer-verified); same formulas as platform definition KerrBL_CoordGeometry (id bbec007a-159a-4623-916d-f1cafab3e353); Sylvester's law of inertia (standard linear algebra); Mathlib LinearAlgebra/QuadraticForm/Signature.lean (pinned 0df444a3) for sigPos/sigNeg; Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Core/Basic.lean (source module Atlas.Core.Basic, file sha256 43706e42e842f504fb4061a3f4b115ddca174fbb987ff6b644b66a6034d189e0; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Core_Basic.lean, sha256 7feabbbc1a90bd7b95589ac2da59a8330cad5e39403b6fa65cbaaec46b8bce0e)

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by He Wang · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph