No nontrivial Syracuse cycle of period at most 1635
Provedsyracuse_period_le_sixteenthirtyfive_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 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 it. At one has and the comparison is between integers of about digits.
Period is the first not covered. Writing for the least threshold covering every period up to , the sequence runs as passes , with jumps at denominators of convergents of . Since , no single threshold covers all periods, so this argument cannot settle the cycle question — but no finite period defeats it either; only the certificate size grows without bound.
import Mathlib import Definitions.Def_syracuseStep
theorem syracuse_period_le_sixteenthirtyfive_eq_one (m a : ℕ) (hm : 0 < m) (ha : 0 < a)
(hle : a ≤ 1635) (hcyc : syracuseStep^[a] m = m) : m = 1 := by sorry