Prove2Me

Signatures (+−−−)(+---), (+++++)(+++++), (++−−)(++--): hyperbolic, elliptic, ultrahyperbolic

Proved
TegmarkDimensionality.signature_examples

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

linear-algebramathematical-physicspde

The field equations with coefficient matrix A=g−1A=g^{-1} are

  1. hyperbolic for the metric g=diag⁡(1,−1,−1,−1)g=\operatorname{diag}(1,-1,-1,-1) of signature (+−−−)(+---), i.e. (n,m)=(3,1)(n,m)=(3,1);
  2. elliptic for g=diag⁡(1,1,1,1,1)g=\operatorname{diag}(1,1,1,1,1) of signature (+++++)(+++++);
  3. ultrahyperbolic for g=diag⁡(1,1,−1,−1)g=\operatorname{diag}(1,1,-1,-1) of signature (++−−)(++--).

These are the three examples the paper gives for the classification.

Preamble
import Mathlib
import Definitions.Def_tegmark_pde_classification
Formal statement
namespace TegmarkDimensionality

/-- The field equations are hyperbolic for the metric of signature `(+ - - -)`, elliptic
for `(+ + + + +)` and ultrahyperbolic for `(+ + - -)`. -/
theorem signature_examples :
    IsHyperbolic (Matrix.diagonal (![1, -1, -1, -1] : Fin 4 → ℝ))⁻¹ ∧
      IsElliptic (Matrix.diagonal (![1, 1, 1, 1, 1] : Fin 5 → ℝ))⁻¹ ∧
      IsUltrahyperbolic (Matrix.diagonal (![1, 1, -1, -1] : Fin 4 → ℝ))⁻¹ := 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 ('hyperbolic in a metric of the signature (+---), ... elliptic in a metric of the signature (+++++), and ultrahyperbolic in a metric of the signature (++--)')
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.

The theorem asserts three facts about specific real diagonal matrices and their matrix inverses:

  1. the inverse of the 4×44\times4 diagonal matrix diag⁡(1,−1,−1,−1)\operatorname{diag}(1,-1,-1,-1) is hyperbolic: symmetric with (N+=1N_+=1, N−=3N_-=3) or (N−=1N_-=1, N+=3N_+=3);
  2. the inverse of the 5×55\times5 identity matrix diag⁡(1,1,1,1,1)\operatorname{diag}(1,1,1,1,1) is elliptic: symmetric with N+=5N_+=5 or N−=5N_-=5;
  3. the inverse of the 4×44\times4 diagonal matrix diag⁡(1,1,−1,−1)\operatorname{diag}(1,1,-1,-1) is ultrahyperbolic: symmetric with N+≥2N_+\ge2 and N−≥2N_-\ge2.

Here N±N_\pm count positive and negative real roots of the characteristic polynomial with multiplicity.

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