Four-dimensional Lorentzian frames give Mathlib signature $(3,1)$

Proved

ExactVacuumAtlas.sigPos_sigNeg_four

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

coordinate-geometryexact-vacuum-atlasgeneral-relativitylinear-algebralorentzian-signaturequadratic-forms

Let $G$ be a real $4\times4$ matrix which is Lorentzian in the sense of bundle Atlas_Core_Basic (there is $E$ with invertible determinant and $E^{\mathsf T}GE=\mathrm{diag}(-1,1,1,1)$ ) and $Q_G(v)=v^{\mathsf T}Gv$ . Then

\mathrm{sigPos}(Q_G)=3,\qquad \mathrm{sigNeg}(Q_G)=1.

The four-dimensional instance of the signature bridge, fixing the convention $(3,1)$ used throughout the atlas; a release target alongside the goal theorem.

Preamble

import Mathlib
import Definitions.Def_Atlas_Core_Basic
open Matrix

Formal statement

theorem ExactVacuumAtlas.sigPos_sigNeg_four {G : Matrix (Fin 4) (Fin 4) ℝ} (h : IsLorentzian G) :
    sigPos G.toQuadraticForm' = 3 ∧ sigNeg G.toQuadraticForm' = 1 := by sorry

Source

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/Signature.lean#L70-L73 (module Atlas.Core.Signature, file sha256 24deab1b17221c81185dcc9074681eaeb5d9014f73bf1bf6db43099e2f93278d; uploaded stub = platform_mirror/Theorems/Thm_ExactVacuumAtlas_sigPos_sigNeg_four.lean)

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

Four-dimensional Lorentzian frames give Mathlib signature (3,1)(3,1)(3,1)

Four-dimensional Lorentzian frames give Mathlib signature $(3,1)$