Eq. (7.30) — bound on the largest principal strain of a deviatoric strain tensor

Proved

Verlinde2016.principal_strain_bound

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

emergent-gravitymathematical-physicsverlinde-2016

Let $d\ge2$ be the spacetime dimension, so space has dimension $d-1$ . Let $\varepsilon'_{ij}$ be a real symmetric, traceless $(d-1)\times(d-1)$ matrix (a deviatoric strain tensor), and let $\varepsilon$ be a principal strain, i.e. an eigenvalue of $\varepsilon'$ with eigenvector $n\neq0$ : $\varepsilon'_{ij}n_j = \varepsilon n_i$ . Then

\varepsilon^2 \le \left(\frac{d-2}{d-1}\right)\varepsilon'^{\,2}_{ij},\qquad \varepsilon'^{\,2}_{ij} = \sum_{i,j}(\varepsilon'_{ij})^2.

The paper states this for the largest principal strain; the bound holds for every eigenvalue, which is what is formalized.

Preamble

import Mathlib
import Definitions.Def_Verlinde2016_Defs

open Real

Formal statement

namespace Verlinde2016

theorem principal_strain_bound (d : ℕ) (hd : 2 ≤ d)
    (E : Matrix (Fin (d - 1)) (Fin (d - 1)) ℝ) (hE : E.IsSymm) (htr : E.trace = 0)
    (ε : ℝ) (v : Fin (d - 1) → ℝ) (hv : v ≠ 0) (hev : E.mulVec v = ε • v) :
    ε ^ 2 ≤ ((d : ℝ) - 2) / ((d : ℝ) - 1) * ∑ i, ∑ j, E i j ^ 2 := by sorry

end Verlinde2016

Source

E. Verlinde, Emergent Gravity and the Dark Universe, SciPost Phys. 2, 016 (2017), arXiv:1611.02269v2, https://arxiv.org/abs/1611.02269, p. 35, eq. (7.30) (with (7.28) for the eigenvector condition)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent as drafter, non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, at the explicit instruction of the account owner. It was not produced blind by an independent auditor, and the author had seen the source paper and the intended meaning while writing it. Reviewers should not treat it as independent evidence of faithfulness and should check the Lean code directly.

Let $d$ be a natural number with $d\ge2$ , and put $m = d-1\ge1$ . Let $E=(E_{ij})$ be a real $m\times m$ matrix with

$E$ symmetric: $E_{ij}=E_{ji}$ for all $i,j$ ;
$\operatorname{tr}E = \sum_i E_{ii} = 0$ .

Let $\varepsilon\in\mathbb R$ and let $v\in\mathbb R^m$ be a nonzero vector with $Ev = \varepsilon v$ (so $\varepsilon$ is a real eigenvalue of $E$ with eigenvector $v$ ; $v$ need not be normalized). Then

\varepsilon^2 \le \frac{d-2}{d-1}\,\sum_{i=1}^{m}\sum_{j=1}^{m} E_{ij}^2 ,

where $d-2$ and $d-1$ are computed as real numbers. Edge case: for $d=2$ the matrix is $1\times1$ , the trace condition forces $E=0$ , hence $\varepsilon=0$ and both sides are $0$ . The eigenvalue $\varepsilon$ is arbitrary: it is not required to be the largest.

View graph