$g^{-1}$ has the eigenvalue signs of the metric $g$

Proved

TegmarkDimensionality.coefficient_matrix_eigenvalue_signs

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

linear-algebramathematical-physics

Let $g$ be a real symmetric square matrix with $\det g\neq0$ . Then $g^{-1}$ has the same number of positive eigenvalues and the same number of negative eigenvalues as $g$ , counted with multiplicity:

N_+(g^{-1})=N_+(g),\qquad N_-(g^{-1})=N_-(g).

For the covariant field equations the coefficient matrix is $A=g^{-1}$ . The paper's remark that " $A$ has the same eigenvalues as the metric" is used for their signs only, which is what determines the PDE type.

Formalization Note The eigenvalues of $g^{-1}$ are the reciprocals of those of $g$ , so the statement is about signs and not about equality of eigenvalues.

Preamble

import Mathlib
import Definitions.Def_tegmark_pde_classification

Formal statement

namespace TegmarkDimensionality

/-- The coefficient matrix `A = g⁻¹` of the covariant field equations has the same numbers
of positive and of negative eigenvalues as the (nondegenerate, symmetric) metric `g`. -/
theorem coefficient_matrix_eigenvalue_signs {ι : Type*} [Fintype ι] [DecidableEq ι]
    (g : Matrix ι ι ℝ) (hg : g.IsSymm) (hdet : g.det ≠ 0) :
    numPosEigenvalues g⁻¹ = numPosEigenvalues g ∧
      numNegEigenvalues g⁻¹ = numNegEigenvalues g := 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')

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 $\iota$ be a finite index type with decidable equality and $g$ a real $\iota\times\iota$ matrix that is symmetric with $\det g\neq0$ . Let $g^{-1}$ be its matrix inverse. The theorem asserts $N_+(g^{-1})=N_+(g)$ and $N_-(g^{-1})=N_-(g)$ , where $N_+$ and $N_-$ are the numbers of positive and negative real roots of the characteristic polynomial, counted with multiplicity. The index type may be empty, in which case both sides are $0$ .

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

g−1g^{-1}g−1 has the eigenvalue signs of the metric ggg

$g^{-1}$ has the eigenvalue signs of the metric $g$