Collatz mission predicates
DefinitionCollatzMissioncollatzdynamical-systemsnumber-theory
Defines the classical Collatz map and three mission interfaces: the conjecture restricted to positive odd inputs, one-avoiding eventually cyclic counterexamples, and one-avoiding non-eventually-cyclic counterexamples. The latter is a logical non-cycle branch and does not by itself assert unbounded growth.
Definition code
import Mathlib
namespace CollatzMission
/-- The classical Collatz step used by the mission's supporting reductions. -/
def collatzStep (n : ℕ) : ℕ :=
if Even n then n / 2 else 3 * n + 1
/-- The Collatz claim restricted to positive odd starting values. -/
def OddInputsConjecture : Prop :=
∀ n : ℕ, 0 < n → ¬Even n → ∃ m : ℕ, collatzStep^[m] n = 1
/-- The forward orbit of `n` never visits `1`. -/
def OrbitAvoidsOne (n : ℕ) : Prop :=
∀ k : ℕ, collatzStep^[k] n ≠ 1
/-- A one-avoiding orbit which eventually repeats. -/
def EventualCycleCounterexample (n : ℕ) : Prop :=
OrbitAvoidsOne n ∧
∃ start period : ℕ,
0 < period ∧ collatzStep^[period] (collatzStep^[start] n) = collatzStep^[start] n
/-- A one-avoiding orbit which is not eventually cyclic. -/
def DivergentCounterexample (n : ℕ) : Prop :=
OrbitAvoidsOne n ∧ ¬EventualCycleCounterexample n
/-- No positive starting value has a one-avoiding eventually cyclic orbit. -/
def NoEventualCycleCounterexamples : Prop :=
∀ n : ℕ, 0 < n → ¬EventualCycleCounterexample n
/-- No positive starting value has a one-avoiding non-cyclic orbit. -/
def NoDivergentCounterexamples : Prop :=
∀ n : ℕ, 0 < n → ¬DivergentCounterexample n
end CollatzMission
Source