Bounded one-avoiding Collatz orbits eventually repeat

Proved

CollatzMission.eventualCycleCounterexample_of_bounded_orbit

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

collatzdynamical-systemsnumber-theory

Let $C$ be the classical Collatz map. Fix natural numbers $n$ and $B$ . Assume the forward orbit of $n$ avoids $1$ and that every iterate is bounded by $B$ :

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

Then the orbit eventually repeats with a positive period, so $n$ is an eventual-cycle counterexample in the mission terminology.

This theorem isolates the finite-state recurrence step that converts a bounded one-avoiding orbit into eventual periodicity.

Preamble

import Definitions.Def_CollatzMission

Formal statement

namespace CollatzMission

theorem eventualCycleCounterexample_of_bounded_orbit (n B : ℕ)
    (havoid : OrbitAvoidsOne n)
    (hbound : ∀ k : ℕ, collatzStep^[k] n ≤ B) :
    EventualCycleCounterexample n := 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