Prove2Me

Theorem 5 (n = 1): the k < 0 Friedmann spacetime is the trajectory from SM to M

Proved
STVFriedmann.theorem5_kneg_friedmann_order1

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

cosmologydynamical-systemsgeneral-relativity

Fix Δ0>0\Delta_0>0. For θ>0\theta>0 put

tˉΔ0=12(sinh⁡2θ−2θ),z~2(θ)=6(sinh⁡2θ−2θ)2(cosh⁡2θ−1)3,w~0(θ)=(sinh⁡2θ−2θ)sinh⁡2θ(cosh⁡2θ−1)2.\frac{\bar t}{\Delta_0}=\frac12\bigl(\sinh 2\theta-2\theta\bigr),\qquad \tilde z_2(\theta)=\frac{6(\sinh2\theta-2\theta)^2}{(\cosh2\theta-1)^3},\qquad \tilde w_0(\theta)=\frac{(\sinh2\theta-2\theta)\sinh2\theta}{(\cosh2\theta-1)^2}.

Then there is a solution (z2,w0)(tˉ)(z_2,w_0)(\bar t), tˉ∈(0,∞)\bar t\in(0,\infty), of the order-1 STV ODE (2.34)–(2.35) such that

  1. (z2,w0)(tˉ)=(z~2(θ),w~0(θ))(z_2,w_0)(\bar t)=(\tilde z_2(\theta),\tilde w_0(\theta)) whenever tˉ=Δ02(sinh⁡2θ−2θ)\bar t=\tfrac{\Delta_0}2(\sinh2\theta-2\theta), θ>0\theta>0;
  2. (z2,w0)(tˉ)→SM=(43,23)(z_2,w_0)(\bar t)\to SM=(\tfrac43,\tfrac23) as tˉ→0+\bar t\to0^+;
  3. (z2,w0)(tˉ)→M=(0,1)(z_2,w_0)(\bar t)\to M=(0,1) as tˉ→∞\bar t\to\infty.

So the leading-order part of the p=0p=0, k=−1k=-1 Friedmann spacetime with parameter Δ0\Delta_0 is the trajectory of the 2×22\times2 phase portrait connecting SMSM to MM; Δ0\Delta_0 enters only as a log-time translation.

Formalization Note The STV ODE tˉ U˙=F(U)\bar t\,\dot U=F(U) is written in log-time τ=ln⁡tˉ\tau=\ln\bar t as dU/dτ=F(U)dU/d\tau=F(U) for all τ∈R\tau\in\mathbb R; so tˉ→0+\bar t\to0^+ is τ→−∞\tau\to-\infty and tˉ→∞\bar t\to\infty is τ→+∞\tau\to+\infty.

Preamble
import Mathlib
import Definitions.Def_STVFriedmann_basic

open Filter Topology Real
Formal statement
namespace STVFriedmann

/-- Theorem 5, (2.40)–(2.41): for every `Δ₀ > 0`, the leading-order `k = -1` Friedmann curve
`(z̃₂, w̃₀)(θ)`, with `t̄ = Δ₀ (sinh 2θ - 2θ)/2`, is a solution of the order-1 STV ODE taking
`SM` (as `t̄ → 0`) to `M` (as `t̄ → ∞`). -/
theorem theorem5_kneg_friedmann_order1 (Δ₀ : ℝ) (hΔ₀ : 0 < Δ₀) :
    ∃ U : ℝ → Fin 2 → ℝ, IsSTVSolution stvField1 U ∧
      (∀ θ : ℝ, 0 < θ → U (Real.log (Δ₀ * bigBangTime θ)) = friedmannCurve1 θ) ∧
      Tendsto U atBot (𝓝 restSM1) ∧ Tendsto U atTop (𝓝 restM1) := 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. 14, Theorem 5 eqs. (2.40)-(2.42); p. 13, Section 2.5
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