Minkowski metric in Cartesian coordinates, any dimension $n+1$

Definition

Atlas_Minkowski_Cartesian

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

cartesian-coordinatescoordinate-geometryexact-vacuum-atlasgeneral-relativityminkowski-space

For a natural number $n$ , the coordinate metric $g^{\rm cart}_n$ on $\mathbb R^{n+1}$ with constant components $\eta_n=\mathrm{diag}(-1,1,\dots,1)$ (line element $ds^2=-dt^2+dx_1^2+\dots+dx_n^2$ ), and its candidate inverse, the same constant matrix. The atlas uses $n=3$ .

Row 1 data.

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Minkowski.Cartesian; declarations: ExactVacuumAtlas.Minkowski.gCart, ExactVacuumAtlas.Minkowski.giCart. 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/Minkowski/Cartesian.lean
-- definition bundle: kept ExactVacuumAtlas.Minkowski.gCart, ExactVacuumAtlas.Minkowski.giCart
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
/-!
# Minkowski space in Cartesian coordinates, any dimension `n + 1`

`ds² = -dt² + dx₁² + … + dxₙ²` (Müller–Grave, *Catalogue of Spacetimes*, eq. minkCart, `c = 1`).
Certified on all of `ℝⁿ⁺¹`. For release 0.1 the catalogue row is `n = 3`.
-/

open scoped ContDiff

namespace ExactVacuumAtlas.Minkowski

/-- Cartesian Minkowski metric, constant components `diag(-1, 1, …, 1)`. -/
def gCart (n : ℕ) : Metric (n + 1) := fun i j _ => eta n i j

/-- Its inverse (the same matrix). -/
def giCart (n : ℕ) : Metric (n + 1) := fun i j _ => eta n i j

end ExactVacuumAtlas.Minkowski

Source

Müller–Grave catalogue eqs. minkCart and minkSph; Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Minkowski/Cartesian.lean (source module Atlas.Minkowski.Cartesian, file sha256 e28e443043a8e2e209d525d5f88daacb33777a03c2df47b8ab5051bdff7c110b; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Minkowski_Cartesian.lean, sha256 2e0389d322df7eb10e35bffc45cece6413353c82519d45103d7f480ad8fc872e)

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

Minkowski metric in Cartesian coordinates, any dimension n+1n+1n+1

Minkowski metric in Cartesian coordinates, any dimension $n+1$