Every positive periodic Collatz orbit visits 1

Open

CollatzMission.periodic_point_reaches_one

by Yuning · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

collatzdynamical-systemsiterationnumber-theoryopen-problem

Let $C$ be the classical Collatz map. If a positive integer $x$ is periodic with some positive period $p$ , so that $C^p(x)=x$ , then its forward orbit visits $1$ :

\exists k\in\mathbb N,\qquad C^k(x)=1.

Equivalently, the only positive periodic Collatz orbit is the familiar cycle containing $1,4,2$ . This is an open cycle-exclusion target, not a claim that nontrivial cycles have already been ruled out. It isolates the arithmetic core from an arbitrary transient prefix: an eventually periodic counterexample first enters a genuinely periodic orbit, and this theorem excludes that periodic tail.

Preamble

import Definitions.Def_CollatzMission

Formal statement

namespace CollatzMission

/-- Every positive periodic point of the Collatz map belongs to a cycle that visits `1`. -/
theorem periodic_point_reaches_one (x period : ℕ)
    (hx : 0 < x) (hperiod : 0 < period)
    (hfix : collatzStep^[period] x = x) :
    ∃ k : ℕ, collatzStep^[k] x = 1 := by
  sorry

end CollatzMission

Source

Open periodic-orbit formulation of the Collatz cycle problem; Jeffrey C. Lagarias, The 3x+1 Problem and Its Generalizations, American Mathematical Monthly 92 (1985), 3–23, Section 2, https://websites.umich.edu/~lagarias/3x%2B1.html. Reduction child for Prove2Me theorem CollatzMission.no_eventual_cycle_counterexamples.

View graph