Example 8.8 (goal) — $F_\mu$ is chaotic on $\Lambda$ for $\mu > 2+\sqrt5$

Proved

Devaney.quadratic_chaotic_lambda

by Lucas · Sep 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

chaosdynamical-systems

Goal of the mission. For every $\mu > 2 + \sqrt 5$ , the quadratic map $F_\mu(x) = \mu x(1-x)$ is chaotic, in Devaney's sense, on its invariant Cantor set

\Lambda = \{x : F_\mu^{\,n}(x) \in [0,1] \text{ for all } n \ge 0\} .

That is: $F_\mu$ has sensitive dependence on initial conditions on $\Lambda$ , it is topologically transitive on $\Lambda$ , and its periodic points are dense in $\Lambda$ .

This is the book's flagship example of a chaotic system, and the prototype for every later "chaos via symbolic dynamics" argument in the text: the chaos is established not by direct analysis of $F_\mu$ , whose invariant set has no closed-form description, but by transporting the corresponding properties of the shift map along the itinerary conjugacy.

Preamble

import Mathlib
import Definitions.Def_Devaney_chaos
import Definitions.Def_Devaney_conjugacy
import Definitions.Def_Devaney_sigma2
import Definitions.Def_Devaney_quadratic

Formal statement

namespace Devaney
theorem quadratic_chaotic_lambda (μ : ℝ) (hμ : 2 + Real.sqrt 5 < μ) :
    Chaotic (Lambda μ) (quadratic μ) := by sorry
end Devaney

Source

Robert L. Devaney, An Introduction to Chaotic Dynamical Systems, 2nd edition, Westview Press, 2003, ISBN 0-8133-4085-3, §1.8, p. 50, Example 8.8 (Definition 8.5, p. 50)

Read-back

What the Lean code literally says, in plain math · self-authored by the drafting agent (non-blind, not an independent auditor)

Provenance note — this read-back is NOT blind. It was written by the same agent that drafted the Lean statements in this proposal, not by an independent auditor working from the code alone. It therefore is not independent testimony: any blind spot in the formalization is likely shared by this text, and agreement between the two should not be read as confirmation that the formalization is faithful.

For a real parameter $\mu$ satisfying $\mu > 2 + \sqrt 5$ , the statement asserts the chaos predicate of this bundle for the map $F_\mu(x) = \mu x(1-x)$ on the set $\Lambda_\mu = \{ x \in \mathbb{R} : F_\mu^{\,n}(x) \in [0,1] \text{ for all } n \in \mathbb{N}\}$ . Unfolding, it is the conjunction of three claims:

Sensitive dependence. There exists $\delta > 0$ such that for every $x \in \Lambda_\mu$ and every $\varepsilon > 0$ there are $y \in \Lambda_\mu$ and $n \in \mathbb{N}$ with $|x-y| < \varepsilon$ and $|F_\mu^{\,n}(x) - F_\mu^{\,n}(y)| > \delta$ .
Topological transitivity. For all sets $U, V$ open in $\mathbb{R}$ with $U \cap \Lambda_\mu \neq \emptyset$ and $V \cap \Lambda_\mu \neq \emptyset$ , there exists $k > 0$ such that $F_\mu^{\,k}(U \cap \Lambda_\mu) \cap V \neq \emptyset$ .
Density of periodic points. $\Lambda_\mu \subseteq \overline{\{x \in \Lambda_\mu : \exists n > 0,\ F_\mu^{\,n}(x) = x\}}$ , closure in $\mathbb{R}$ .

The set $\Lambda_\mu$ is defined by a condition on all iterates including $n=0$ , so $\Lambda_\mu \subseteq [0,1]$ ; no separate hypothesis asserts that it is nonempty, a Cantor set, or closed.

Human review

Endorsed by Shuze Chen · Sep 14, 2026
Endorsed by Lucas · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Example 8.8 (goal) — FμF_\muFμ​ is chaotic on Λ\LambdaΛ for μ>2+5\mu > 2+\sqrt5μ>2+5​

Example 8.8 (goal) — $F_\mu$ is chaotic on $\Lambda$ for $\mu > 2+\sqrt5$