No nontrivial Syracuse cycle contains a value below 1883432
Provedsyracuse_no_cycle_below_1883432collatznumber-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.
Pass to the least value on the orbit of . Then , and is odd and positive because it is a value of . Were greater than it would admit a strictly smaller iterate by the descent result for this range — impossible, since is the orbit minimum. Hence , the orbit of reaches , and a periodic point whose orbit reaches is itself .
Preamble
import Mathlib import Definitions.Def_syracuseStep
Formal statement
theorem syracuse_no_cycle_below_1883432 (z a : ℕ) (hz : 0 < z) (ha : 0 < a) (hle : z ≤ 1883431)
(hcyc : syracuseStep^[a] z = z) : z = 1 := by sorrySource
Collatz mission https://prove2.me/missions/2f34a49f-2016-4de2-9662-fcd1cc96cc67; from syracuse_descends_below_1883432 and syracuse_periodic_reaches_one (a46524f0-afd4-4232-b74a-8a95d7ab31a5).