No nontrivial Syracuse cycle contains a value below 330750
Provedsyracuse_no_cycle_below_330750collatznumber-theory
Let be the Syracuse map, sending to the odd part of . If is a positive integer with and for some , then . The return time is arbitrary; no minimality is assumed.
The argument is the natural one for cycles. Passing to the least value on the orbit of , one has , and is odd and positive because it is a value of . If were greater than it would admit a strictly smaller iterate, by the descent result for this range — but is the orbit minimum, so no iterate of can lie below it. Hence , the orbit of reaches , and a periodic point whose orbit reaches is itself .
Note that only descent is needed, never convergence. That is what makes the threshold cheap to raise.
Preamble
import Mathlib import Definitions.Def_syracuseStep
Formal statement
theorem syracuse_no_cycle_below_330750 (z a : ℕ) (hz : 0 < z) (ha : 0 < a) (hle : z ≤ 330749)
(hcyc : syracuseStep^[a] z = z) : z = 1 := by sorrySource
Collatz mission https://prove2.me/missions/2f34a49f-2016-4de2-9662-fcd1cc96cc67; from syracuse_descends_below_330750 and syracuse_periodic_reaches_one (a46524f0-afd4-4232-b74a-8a95d7ab31a5). Supersedes syracuse_no_cycle_below_99781 (bb9842e2-a1a4-46c0-be27-ea9e7d8a90a5).