No nontrivial Syracuse cycle of period at most ninety-three
Provedsyracuse_period_le_ninetythree_eq_oneLet be the Syracuse map, sending to the odd part of . If is a positive integer with for some with , then .
Equivalently, every Syracuse cycle of length at most is the trivial cycle . The return time need not be minimal.
The proof is uniform across the ninety-three periods. For each one checks the single numerical inequality
where is the least exponent with , and feeds it to the margin criterion; the threshold is available because no nontrivial cycle contains a value below .
The bound is exactly where this method stops: the inequality holds for every and fails first at . Raising the verified small-value range would move the bound further — but never to all periods, since comes arbitrarily close to along the convergents of , most sharply at .
import Mathlib import Definitions.Def_syracuseStep
theorem syracuse_period_le_ninetythree_eq_one (m a : ℕ) (hm : 0 < m) (ha : 0 < a) (hle : a ≤ 93)
(hcyc : syracuseStep^[a] m = m) : m = 1 := by sorry