Theorem 10.2 (goal) — Sarkovskii's theorem

Proved

Devaney.sarkovskii_of_precedes

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

dynamical-systemsperiodic-points

Goal of the mission. Let $f : \mathbb{R} \to \mathbb{R}$ be continuous. If $f$ has a periodic point of prime period $k$ , and $k \triangleright \ell$ in the Sarkovskii ordering

3 \triangleright 5 \triangleright 7 \triangleright \cdots \triangleright 2\cdot3 \triangleright 2\cdot5 \triangleright \cdots \triangleright 2^2\cdot3 \triangleright \cdots \triangleright 2^3 \triangleright 2^2 \triangleright 2 \triangleright 1,

then $f$ also has a periodic point of prime period $\ell$ .

Continuity is the only hypothesis. Since $3$ heads the ordering, the theorem contains "period three implies all periods" as its first corollary, and since the powers of two come last, it explains why a map with finitely many periodic points can only have dyadic periods.

Preamble

import Mathlib
import Definitions.Def_Devaney_sarkovskii

Formal statement

namespace Devaney
theorem sarkovskii_of_precedes (f : ℝ → ℝ) (hf : Continuous f) (k l : ℕ)
    (h : ∃ x, HasPrimePeriod f x k) (hkl : SarkovskiiPrecedes k l) :
    ∃ x, HasPrimePeriod f x l := 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.10, p. 62, Theorem 10.2 (Sarkovskii's theorem)

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 continuous $f : \mathbb{R}\to\mathbb{R}$ and natural numbers $k$ and $\ell$ , under the hypotheses that some real number has prime period exactly $k$ for $f$ (i.e. $k > 0$ , $f^{k}(x) = x$ , and $f^{m}(x) \ne x$ for $0 < m < k$ ) and that $\mathrm{SarkovskiiPrecedes}(k,\ell)$ holds, the statement asserts that some real number has prime period exactly $\ell$ for $f$ .

Unfolding the relation: writing $v_2$ for the $2$ -adic valuation and $\mathrm{odd}(n) = n/2^{v_2(n)}$ , the hypothesis on $k$ and $\ell$ is the disjunction of (i) $\mathrm{odd}(k) > 1$ , $\mathrm{odd}(\ell) > 1$ and $(v_2(k), \mathrm{odd}(k))$ lexicographically below $(v_2(\ell), \mathrm{odd}(\ell))$ ; (ii) $\mathrm{odd}(k) > 1$ , $\ell > 0$ a power of two; (iii) $k, \ell$ both positive powers of two with $v_2(\ell) < v_2(k)$ . The relation is irreflexive and fails when either argument is $0$ , so no claim is made for $\ell = k$ or $\ell = 0$ .

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