STV ODE of order 2: M is a stable rest point with the single eigenvalue -1

Proved

STVFriedmann.corollary1_order2_M_stable

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

cosmologydynamical-systemsgeneral-relativity

Let $DF_2(M)$ be the Jacobian of the order-2 STV ODE (2.48)–(2.51) at the Minkowski rest point $M=(0,1,0,0)$ . Then:

$\boldsymbol R_M=(0,1,0,1)^T$ satisfies $DF_2(M)\boldsymbol R_M=-\boldsymbol R_M$ ;
$\lambda_M=-1$ is the only real eigenvalue of $DF_2(M)$ .

So $M$ is a degenerate stable rest point of the order-2 system.

Formalization Note Corollary 1 also states that $\boldsymbol R_M$ is the only eigenvector. For the explicit system (2.48)–(2.51) this is not correct as stated: at $M$ the eigenspace for $-1$ is spanned by $(0,1,0,0)^T$ and $(0,0,0,1)^T$ , so it is two-dimensional. This statement therefore keeps only the parts of (2.28) that hold for (2.48)–(2.51).

Preamble

import Mathlib
import Definitions.Def_STVFriedmann_basic

open Filter Topology Real

Formal statement

namespace STVFriedmann

/-- Corollary 1 (n = 2), (2.28): at `M = (0,1,0,0)` the vector `R_M = (0,1,0,1)` is an
eigenvector of the Jacobian of the order-2 STV ODE with eigenvalue `-1`, and `-1` is the only
(real) eigenvalue. -/
theorem corollary1_order2_M_stable :
    fderiv ℝ stvField2 restM2 ![0, 1, 0, 1] = (-1 : ℝ) • ![0, 1, 0, 1] ∧
    ∀ (μ : ℝ) (v : Fin 4 → ℝ), v ≠ 0 → fderiv ℝ stvField2 restM2 v = μ • v → μ = -1 := by
  sorry

end STVFriedmann

Source

C. Alexander, B. Temple, Z. Vogler, The Instability of the Critical Friedmann Spacetime at the Big Bang as an Alternative to Dark Energy, arXiv:2510.14228v1 (2025), https://arxiv.org/abs/2510.14228, p. 12, Corollary 1 eq. (2.28); p. 16 (M is a degenerate stable rest point at every order n >= 1 with eigenvalue -1)

Human review

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

View graph