Every odd number above one and below 1166400 has a strictly smaller Syracuse iterate
Provedsyracuse_descends_below_1166400collatznumber-theory
Let be the Syracuse map, sending to the odd part of . For every odd with , some iterate of falls strictly below .
This is a descent statement, deliberately weaker than convergence, and exactly the strength cycle exclusion requires: the minimum of a nontrivial cycle can never descend.
Below the result is inherited from the previous descent bound. Above it, the statement comes from a ladder of mutually independent range lemmas, each following orbits only until their first drop below that range's own lower bound. Half of every range needs no orbit data at all: if then , so in a single step.
Preamble
import Mathlib import Definitions.Def_syracuseStep
Formal statement
theorem syracuse_descends_below_1166400 (m : ℕ) (h1 : 1 < m) (hlt : m < 1166400) (hodd : Odd m) :
∃ t : ℕ, syracuseStep^[t] m < m := by sorrySource
Collatz mission https://prove2.me/missions/2f34a49f-2016-4de2-9662-fcd1cc96cc67; assembled from syracuse_descends_below_860564 and 77 independent descent range lemmas covering [860564, 1166399].