Cycle and non-cyclic counterexample reduction

Proved

CollatzMission.collatz_of_no_cycles_and_no_divergence

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

collatzdynamical-systemsnumber-theory

Let $T$ be the classical Collatz map. Assume there is no positive orbit which avoids $1$ and eventually repeats, and no positive orbit which avoids $1$ without eventually repeating. Then every positive integer reaches $1$ under iteration of $T$ .

Here the second branch means precisely a one-avoiding, non-eventually-cyclic orbit; it does not assert that the orbit is unbounded.

Preamble

import Definitions.Def_CollatzMission

Formal statement

namespace CollatzMission

theorem collatz_of_no_cycles_and_no_divergence :
    NoEventualCycleCounterexamples →
      NoDivergentCounterexamples →
        ∀ n : ℕ, 0 < n → ∃ m : ℕ, collatzStep^[m] n = 1 := by
  sorry

end CollatzMission

Source

https://github.com/flound1129/collatz/blob/c0b24f073dcdc63d9d0974429bd8f3c522ed8eb4/lean/CollatzConjecture/Formulations.lean#L154-L198

View graph