STV ODE of order 1: M is a degenerate stable rest point

Proved

STVFriedmann.corollary1_order1_M_degenerate

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

cosmologydynamical-systemsgeneral-relativity

Let $DF_1(M)$ be the Jacobian of the order-1 STV ODE (2.34)–(2.35) at the Minkowski rest point $M=(0,1)$ . Then:

$\boldsymbol R_M=(0,1)^T$ is an eigenvector with eigenvalue $\lambda_M=-1$ ;
every (real) eigenpair $(\mu, v)$ , $v\ne0$ , of $DF_1(M)$ has $\mu=-1$ and $v$ a multiple of $\boldsymbol R_M$ .

That is, $M$ is a degenerate stable rest point with one eigenvalue and one eigenvector.

Preamble

import Mathlib
import Definitions.Def_STVFriedmann_basic

open Filter Topology Real

Formal statement

namespace STVFriedmann

/-- Corollary 1 (n = 1), (2.28): at `M = (0,1)` the Jacobian of the order-1 STV ODE has the
single eigenvalue `-1` with the single eigenvector direction `R_M = (0, 1)`. -/
theorem corollary1_order1_M_degenerate :
    fderiv ℝ stvField1 restM1 ![0, 1] = (-1 : ℝ) • ![0, 1] ∧
    ∀ (μ : ℝ) (v : Fin 2 → ℝ), v ≠ 0 → fderiv ℝ stvField1 restM1 v = μ • v →
      μ = -1 ∧ ∃ c : ℝ, v = c • ![0, 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 has repeated eigenvalue -1 and single eigenvector R_M = (0,1)^T at n = 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