PDE type (elliptic / hyperbolic / ultrahyperbolic) via eigenvalue signs

Definition

tegmark_pde_classification

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

linear-algebramathematical-physicspde

Let $A$ be a real $d\times d$ matrix. Write $N_+(A)$ and $N_-(A)$ for the number of positive and the number of negative real roots of the characteristic polynomial $\det(X I-A)$ , each counted with multiplicity. For symmetric $A$ these are the numbers of positive and of negative eigenvalues.

The second-order linear PDE

\sum_{i,j=1}^d A_{ij}\,\partial_i\partial_j u+\sum_{i=1}^d b_i\,\partial_i u+c\,u=0

with symmetric coefficient matrix $A$ is called

elliptic if $A$ is symmetric and $N_+(A)=d$ or $N_-(A)=d$ (all eigenvalues positive or all negative);
hyperbolic if $A$ is symmetric and either $N_+(A)=1,\ N_-(A)=d-1$ or $N_-(A)=1,\ N_+(A)=d-1$ (one eigenvalue of one sign, the rest of the other);
ultrahyperbolic if $A$ is symmetric, $N_+(A)\ge2$ and $N_-(A)\ge2$ .

The paper uses this classification to sort spacetime dimensionalities $(n,m)$ by the causal structure of their field equations.

Formalization Note The type depends only on the constant matrix $A$ , i.e. the classification is taken at a single point. A symmetric matrix with a zero eigenvalue is never elliptic or hyperbolic, but it is ultrahyperbolic as soon as it has at least two positive and two negative eigenvalues (the paper's 'remaining case'). For $d=1$ a nonzero matrix is both elliptic and hyperbolic, exactly as the paper's wording permits. $d-1$ is natural-number subtraction.

Definition code

import Mathlib

namespace TegmarkDimensionality

/-- The number of positive eigenvalues of a real square matrix `A`, counted with
multiplicity: the number of positive real roots of the characteristic polynomial of `A`,
counted with multiplicity. -/
noncomputable def numPosEigenvalues {ι : Type*} [Fintype ι] [DecidableEq ι]
    (A : Matrix ι ι ℝ) : ℕ :=
  Multiset.card (A.charpoly.roots.filter (fun x : ℝ => 0 < x))

/-- The number of negative eigenvalues of a real square matrix `A`, counted with
multiplicity: the number of negative real roots of the characteristic polynomial of `A`,
counted with multiplicity. -/
noncomputable def numNegEigenvalues {ι : Type*} [Fintype ι] [DecidableEq ι]
    (A : Matrix ι ι ℝ) : ℕ :=
  Multiset.card (A.charpoly.roots.filter (fun x : ℝ => x < 0))

/-- A second-order linear PDE `∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼ u + ∑ᵢ bᵢ ∂ᵢ u + c u = 0` with symmetric
coefficient matrix `A` (at a point) is *elliptic* if all eigenvalues of `A` are positive
or all are negative. -/
def IsElliptic {ι : Type*} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) : Prop :=
  A.IsSymm ∧ (numPosEigenvalues A = Fintype.card ι ∨ numNegEigenvalues A = Fintype.card ι)

/-- The PDE is *hyperbolic* if one eigenvalue of `A` is positive and the rest are
negative, or vice versa. -/
def IsHyperbolic {ι : Type*} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) : Prop :=
  A.IsSymm ∧
    ((numPosEigenvalues A = 1 ∧ numNegEigenvalues A = Fintype.card ι - 1) ∨
      (numNegEigenvalues A = 1 ∧ numPosEigenvalues A = Fintype.card ι - 1))

/-- The PDE is *ultrahyperbolic* if at least two eigenvalues of `A` are positive and at
least two are negative. -/
def IsUltrahyperbolic {ι : Type*} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) : Prop :=
  A.IsSymm ∧ 2 ≤ numPosEigenvalues A ∧ 2 ≤ numNegEigenvalues A

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. L72–L73, classification of the PDE (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.

This file introduces four notions for a real square matrix $A$ indexed by a finite type $\iota$ with decidable equality, where $d=|\iota|$ is the number of indices.

$N_+(A)$ is the cardinality of the multiset of real roots of the characteristic polynomial of $A$ , counted with multiplicity, filtered to the strictly positive ones. $N_-(A)$ is the same count for the strictly negative roots. Nothing requires $A$ to be symmetric here, so for a non-symmetric $A$ these count only the real roots. For the zero polynomial, which cannot occur as a characteristic polynomial, the root multiset would be empty.
Elliptic $(A)$ : $A$ equals its transpose, and $N_+(A)=d$ or $N_-(A)=d$ .
Hyperbolic $(A)$ : $A$ equals its transpose, and either ( $N_+(A)=1$ and $N_-(A)=d\mathbin{\dot-}1$ ) or ( $N_-(A)=1$ and $N_+(A)=d\mathbin{\dot-}1$ ). Here $\dot-$ is truncated subtraction, so $0\mathbin{\dot-}1=0$ .
Ultrahyperbolic $(A)$ : $A$ equals its transpose, $N_+(A)\ge2$ and $N_-(A)\ge2$ .

Edge cases: for $d=0$ the empty matrix is elliptic, because $N_+=0=d$ , and it is neither hyperbolic nor ultrahyperbolic. For $d=1$ with $A=(a)$ , $a\ne0$ , the matrix is both elliptic and hyperbolic. A symmetric matrix with a zero eigenvalue is never elliptic or hyperbolic, but it can be ultrahyperbolic, e.g. with $N_+=N_-=2$ and $d=5$ .

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