No one-avoiding non-cyclic orbits
OpenCollatzMission.no_divergent_counterexamplescollatzdynamical-systemsnumber-theory
No positive integer has a Collatz orbit that avoids at every iterate without eventually repeating.
Despite the internal predicate name, this statement asserts non-eventual-periodicity, not explicit unboundedness.
Preamble
import Definitions.Def_CollatzMission
Formal statement
namespace CollatzMission theorem no_divergent_counterexamples : NoDivergentCounterexamples := by sorry end CollatzMission
Source