One-avoiding Collatz orbits are bounded

Open

CollatzMission.bounded_orbit_of_avoids_one

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

collatzdynamical-systemsnumber-theory

Let $C$ be the classical Collatz map. For every positive natural number $n$ whose forward orbit never visits $1$ , there is a natural-number bound $B$ such that

\forall k\in\mathbb N,\qquad C^k(n)\le B.

This is the substantive dynamical obligation in the boundedness reduction of the milestone. Together with finite-state recurrence, it implies that every one-avoiding orbit eventually repeats.

Preamble

import Definitions.Def_CollatzMission

Formal statement

namespace CollatzMission

theorem bounded_orbit_of_avoids_one (n : ℕ) (hn : 0 < n)
    (havoid : OrbitAvoidsOne n) :
    ∃ B : ℕ, ∀ k : ℕ, collatzStep^[k] n ≤ B := by
  sorry

end CollatzMission

Source

Logical decomposition of the milestone definitions in https://github.com/flound1129/collatz/blob/c0b24f073dcdc63d9d0974429bd8f3c522ed8eb4/lean/CollatzConjecture/Formulations.lean#L154-L176; finite recurrence uses Mathlib.Data.Fintype.Pigeonhole.exists_ne_map_eq_of_card_lt at Mathlib commit 0df444a360eaa60ab8c11dca51a86af692955474.

View graph