Type of the covariant field equations in an $(n+m)$ -dimensional spacetime

Proved

TegmarkDimensionality.field_equation_type_by_signature

by Lucas · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebramathematical-physicspde

Let $n,m\ge0$ and let $g$ be a real symmetric $(n+m)\times(n+m)$ matrix (a spacetime metric at a point) with exactly $m$ positive and $n$ negative eigenvalues, counted with multiplicity. Then $g$ is invertible. The covariant field equations $g^{\mu\nu}\partial_\mu\partial_\nu u+(\text{lower order})=0$ (wave, Klein–Gordon, …) have coefficient matrix $A=g^{-1}$ , and their type is determined by $(n,m)$ :

\begin{aligned} A\ \text{elliptic}&\iff n=0\ \text{or}\ m=0,\\ A\ \text{hyperbolic}&\iff n=1\ \text{or}\ m=1,\\ A\ \text{ultrahyperbolic}&\iff n\ge2\ \text{and}\ m\ge2. \end{aligned}

This is the paper's classification of spacetimes by the causal structure of their field equations (Figure 1). Only hyperbolic equations admit well-posed initial-value problems, so this result singles out $m=1$ (and the tachyonic mirror case $n=1$ ).

Formalization Note The eigenvalue counts and the three types are those of the definition tegmark_pde_classification. The metric is taken at a single point and $g^{-1}$ is the matrix inverse.

Preamble

import Mathlib
import Definitions.Def_tegmark_pde_classification

Formal statement

namespace TegmarkDimensionality

/-- In an `(n+m)`-dimensional spacetime whose metric `g` has `m` positive (time-like)
and `n` negative (space-like) eigenvalues, the covariant field equations
`g^{μν} ∂_μ ∂_ν u + (lower order) = 0`, whose coefficient matrix is `g⁻¹`, are elliptic iff
`n = 0` or `m = 0`, hyperbolic iff `n = 1` or `m = 1`, and ultrahyperbolic iff `n ≥ 2` and
`m ≥ 2`. -/
theorem field_equation_type_by_signature (n m : ℕ)
    (g : Matrix (Fin (n + m)) (Fin (n + m)) ℝ) (hg : g.IsSymm)
    (hpos : numPosEigenvalues g = m) (hneg : numNegEigenvalues g = n) :
    (IsElliptic g⁻¹ ↔ (n = 0 ∨ m = 0)) ∧
      (IsHyperbolic g⁻¹ ↔ (n = 1 ∨ m = 1)) ∧
      (IsUltrahyperbolic g⁻¹ ↔ (2 ≤ n ∧ 2 ≤ m)) := by sorry

end TegmarkDimensionality

Source

M. Tegmark, *On the dimensionality of spacetime*, Class. Quantum Grav. 14 (1997) L69–L75, https://doi.org/10.1088/0264-9381/14/4/002, p. L73 (second paragraph: 'the matrix A will clearly have the same eigenvalues as the metric tensor') and Figure 1

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor, so it may share the drafter's blind spots. Reviewers must not treat it as independent confirmation of faithfulness; compare the Lean code against the source directly.

Let $n,m$ be natural numbers (zero allowed) and let $g$ be a real square matrix of size $(n+m)\times(n+m)$ . Assume:

$g$ is symmetric ( $g^{\mathsf T}=g$ );
$N_+(g)=m$ , the characteristic polynomial of $g$ has exactly $m$ positive real roots counted with multiplicity;
$N_-(g)=n$ , it has exactly $n$ negative real roots counted with multiplicity.

Let $g^{-1}$ be the matrix inverse of $g$ . By Lean's convention this is the zero matrix if $g$ is singular; the hypotheses do not explicitly state invertibility. The theorem asserts three equivalences:

$g^{-1}$ is elliptic $\iff$ $n=0$ or $m=0$ ;
$g^{-1}$ is hyperbolic $\iff$ $n=1$ or $m=1$ ;
$g^{-1}$ is ultrahyperbolic $\iff$ $n\ge2$ and $m\ge2$ .

The three types are defined as follows, with $d=n+m$ . Elliptic: symmetric and ( $N_+(g^{-1})=d$ or $N_-(g^{-1})=d$ ). Hyperbolic: symmetric and ( $N_+(g^{-1})=1$ , $N_-(g^{-1})=d\mathbin{\dot-}1$ ) or ( $N_-(g^{-1})=1$ , $N_+(g^{-1})=d\mathbin{\dot-}1$ ). Ultrahyperbolic: symmetric, $N_+(g^{-1})\ge2$ and $N_-(g^{-1})\ge2$ . Here $N_\pm$ count positive and negative real roots of the characteristic polynomial with multiplicity.

Edge cases: $n=m=0$ gives the empty matrix, and the claim then is that it is elliptic, not hyperbolic and not ultrahyperbolic. $(n,m)=(1,0)$ and $(0,1)$ fall under both "elliptic" and "hyperbolic".

Human review

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

View graph

Type of the covariant field equations in an (n+m)(n+m)(n+m)-dimensional spacetime

Type of the covariant field equations in an $(n+m)$ -dimensional spacetime