Prove2Me

Theorem 9 (n = 2): non-self-similar blow-up at the Big Bang

Proved
STVFriedmann.theorem9_non_self_similar_blowup

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

cosmologydynamical-systemsgeneral-relativity

Fix Δ0>0\Delta_0>0. There is a solution (z2,w0,z4,w2)(tˉ)(z_2,w_0,z_4,w_2)(\bar t), tˉ∈(0,∞)\bar t\in(0,\infty), of the order-2 STV ODE (2.48)–(2.51) such that

  1. it agrees exactly with the k=−1k=-1 Friedmann spacetime at leading order: (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 (notation of (2.41));
  2. it tends to the Minkowski rest point M=(0,1,0,0)M=(0,1,0,0) as tˉ→∞\bar t\to\infty;
  3. it blows up at the Big Bang: ∥(z2,w0,z4,w2)(tˉ)∥→∞\|(z_2,w_0,z_4,w_2)(\bar t)\|\to\infty as tˉ→0+\bar t\to0^+.

So, with time since the Big Bang imposed, solutions in F\mathcal F have a self-similar Big Bang at order n=1n=1 (they tend to SMSM, Theorem 5) but need not at order n=2n=2: such a solution misses SMSM in backward time.

Formalization Note Solutions are functions of log-time τ=ln⁡tˉ\tau=\ln\bar t; ∥⋅∥\|\cdot\| is the sup norm on R4\mathbb R^4.

Preamble
import Mathlib
import Definitions.Def_STVFriedmann_basic

open Filter Topology Real
Formal statement
namespace STVFriedmann

/-- Theorem 9 at order 2: there are solutions of the order-2 STV ODE that agree exactly with
the `k = -1` Friedmann spacetime at leading order and decay to `M` as `t̄ → ∞`, but blow up
(instead of tending to `SM`) as `t̄ → 0⁺`. -/
theorem theorem9_non_self_similar_blowup (Δ₀ : ℝ) (hΔ₀ : 0 < Δ₀) :
    ∃ U : ℝ → Fin 4 → ℝ, IsSTVSolution stvField2 U ∧
      (∀ θ : ℝ, 0 < θ → U (Real.log (Δ₀ * bigBangTime θ)) 0 = friedmannZ2 θ ∧
        U (Real.log (Δ₀ * bigBangTime θ)) 1 = friedmannW0 θ) ∧
      Tendsto U atTop (𝓝 restM2) ∧
      Tendsto (fun τ => ‖U τ‖) atBot atTop := 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. 20, Theorem 9; p. 18 (solutions in F not in the unstable manifold of SM); p. 19, Section 2.8
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