Prove2Me

Lemma 8.7 — Lorenz equation with r≤1r \le 1 — the origin is the only fixed point and attracts every solution

Proved
TeschlODE.HigherDim.lorenz_tendsto_origin

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemslorenz-equationp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1stability

Consider the Lorenz equation (8.13), x˙=−σ(x−y)\dot x = -\sigma(x - y), y˙=rx−y−xz\dot y = r x - y - x z, z˙=xy−bz\dot z = x y - b z, with σ,r,b>0\sigma, r, b > 0, and suppose r≤1r \le 1. Then

  1. the origin is the only fixed point: f(v)=0  ⟺  v=0f(v) = 0 \iff v = 0 for the Lorenz vector field ff;
  2. all solutions converge to the origin as t→∞t \to \infty: for the flow Φ\Phi of (8.13) on R3\mathbb{R}^3 and every v∈R3v \in \mathbb{R}^3, the solution through vv exists for all t≥0t \ge 0 and
lim⁡t→∞Φ(t,v)=0.\lim_{t \to \infty} \Phi(t, v) = 0 .

For r>1r > 1 two further fixed points appear and the dynamics becomes the famous strange attractor; this lemma is the simple regime.

Formalization Note. σ,r,b>0\sigma, r, b > 0 is the standing assumption of §8.2 and appears as binders. "All solutions converge as t→∞t \to \infty" includes that they exist for all t≥0t \ge 0; this is stated explicitly ([0,∞)⊆Iv[0, \infty) \subseteq I_v). The flow is quantified universally: any pair (I,Φ)(I, \Phi) that is the maximal flow of (8.13) on R3\mathbb{R}^3 (it exists and is unique since the field is polynomial). The second paragraph after the lemma on the page (r>1r > 1) is not part of it.

Preamble
import Mathlib
import Definitions.Def_TeschlODE_HigherDim_IsIntegralCurve
import Definitions.Def_TeschlODE_HigherDim_IsMaximalFlow
import Definitions.Def_TeschlODE_HigherDim_lorenzField
Formal statement
namespace TeschlODE.HigherDim

/-- Teschl, Lemma 8.7, p. 235: for the Lorenz equation (8.13) with `σ, r, b > 0` and `r ≤ 1`,
the origin is the only fixed point, and every solution exists for all `t ≥ 0` and converges to
the origin as `t → ∞`. -/
theorem lorenz_tendsto_origin (σ r b : ℝ) (hσ : 0 < σ) (hr : 0 < r) (hb : 0 < b)
    (hr1 : r ≤ 1) :
    (∀ v : EuclideanSpace ℝ (Fin 3), lorenzField σ r b v = 0 ↔ v = 0) ∧
      ∀ (I : EuclideanSpace ℝ (Fin 3) → Set ℝ)
        (Φ : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)),
        IsMaximalFlow (lorenzField σ r b) Set.univ I Φ →
          ∀ x : EuclideanSpace ℝ (Fin 3), Set.Ici (0 : ℝ) ⊆ I x ∧
            Filter.Tendsto (fun t => Φ t x) Filter.atTop (nhds 0) := by sorry

end TeschlODE.HigherDim
Source
Teschl, Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012), p. 235, Lemma 8.7
Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Inputs and hypotheses. Let σ,r,b\sigma, r, b be real numbers with

σ>0,b>0,0<r≤1.\sigma > 0, \quad b > 0, \quad 0 < r \le 1 .

Let F(v)=(−σ(v0−v1), rv0−v1−v0v2, v0v1−bv2)F(v) = \big(-\sigma(v_0 - v_1),\ r v_0 - v_1 - v_0 v_2,\ v_0 v_1 - b v_2\big) for v=(v0,v1,v2)∈R3v = (v_0,v_1,v_2) \in \mathbb{R}^3 (Euclidean).

Conclusion. Both of the following hold:

  1. For every v∈R3v \in \mathbb{R}^3: F(v)=0F(v) = 0 if and only if v=0v = 0.
  2. For every pair (I,Φ)(I,\Phi) that is a maximal flow of FF on all of R3\mathbb{R}^3, and for every starting point x∈R3x \in \mathbb{R}^3:
    • [0,∞)⊆I(x)[0,\infty) \subseteq I(x);
    • Φ(t,x)→0\Phi(t,x) \to 0 as the real variable t→+∞t \to +\infty.

Here (I,Φ)(I,\Phi) being a maximal flow of FF on R3\mathbb{R}^3 means that for every xx all of the following hold:

  • I(x)⊆RI(x) \subseteq \mathbb{R} is open, order-connected and contains 00;
  • Φ(0,x)=x\Phi(0,x) = x;
  • ∂tΦ(t,x)=F(Φ(t,x))\partial_t \Phi(t,x) = F(\Phi(t,x)) for all t∈I(x)t \in I(x);
  • every curve ψ\psi with ψ(0)=x\psi(0) = x and ψ′=F(ψ)\psi' = F(\psi) on an open order-connected J∋0J \ni 0 satisfies J⊆I(x)J \subseteq I(x) and ψ=Φ(⋅,x)\psi = \Phi(\cdot,x) on JJ.

Degenerate cases.

  • The boundary value r=1r = 1 is included.
  • The values σ=0\sigma = 0, b=0b = 0 and r≤0r \le 0 are excluded.
  • Part 2 quantifies over all maximal flows, so if no maximal flow of FF existed it would hold vacuously. The statement itself does not assert that a maximal flow exists.
Human review

  • Endorsed by Shuze Chen · Oct 2, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 2, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph