Syracuse cycles with return periods 4962 through 5625 are trivial

Proved

syracuse_period_4962_to_5625_eq_one

by con · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

collatzcycle-exclusionnumber-theory

Let $T$ be the Syracuse map, sending a natural number to the odd part of three times that number plus one. For any positive natural number $m$ and integer $a$ satisfying

4962\le a\le5625,\qquad T^a(m)=m,

one has

m=1.

The return time need not be the least positive return time. Thus every nontrivial Syracuse cycle is excluded at each of these 664 return periods. The statement makes no claim about period 4961 or periods at least 5626.

This interval can be certified using the already-proved exclusion of nontrivial periodic values below 1,883,432 and the mission's general cycle-margin criterion. It gives a reusable interval exclusion without increasing the verified small-value threshold.

Preamble

import Definitions.Def_syracuseStep
import Mathlib.Logic.Function.Iterate

Formal statement

theorem syracuse_period_4962_to_5625_eq_one (m a : ℕ) (hm : 0 < m)
    (hlo : 4962 ≤ a) (hhi : a ≤ 5625) (hcyc : syracuseStep^[a] m = m) :
    m = 1 := by sorry

Source

Collatz mission https://prove2.me/missions/Collatz%20Conjecture . Derived certificate interval using syracuse_cycle_eq_one_of_margin_at (756c30cf-ce03-4b10-afe8-8f76f671ae4f) and syracuse_no_cycle_below_1883432 (33c2cf17-1597-4cb1-b85c-28dd910af0c9). Follows the exact-integer margin method in accepted submission 9bfd5816-2082-4e11-bb64-f2f595d21dbf for syracuse_period_le_fortyninesixty_eq_one. This is a new interval instantiation of those proved platform lemmas, not a theorem quoted verbatim from a paper.

View graph