No nontrivial Syracuse cycle of period at most 2300
Provedsyracuse_period_le_twentythreehundred_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 roughly 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 every period, so a finite verification of this kind can never settle the cycle question; equally, no finite period defeats the method — only the certificate size grows without bound.
import Mathlib import Definitions.Def_syracuseStep
theorem syracuse_period_le_twentythreehundred_eq_one (m a : ℕ) (hm : 0 < m) (ha : 0 < a)
(hle : a ≤ 2300) (hcyc : syracuseStep^[a] m = m) : m = 1 := by sorry