No one-avoiding eventual cycles
OpenCollatzMission.no_eventual_cycle_counterexamplescollatzdynamical-systemsnumber-theory
No positive integer has a Collatz orbit that both avoids at every iterate and eventually repeats with a positive period.
This is the cycle branch of the counterexample split.
Preamble
import Definitions.Def_CollatzMission
Formal statement
namespace CollatzMission theorem no_eventual_cycle_counterexamples : NoEventualCycleCounterexamples := by sorry end CollatzMission
Source