Exclude nontrivial Syracuse cycles of least period at least 5626

Open

syracuse_minimal_period_ge_5626_eq_one

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

collatzcycle-exclusionnumber-theory

Let $T$ be the Syracuse map. Suppose a positive natural number $m$ has least positive return time $p$ , meaning

T^p(m)=m,\qquad T^k(m)\ne m\quad\text{for every }0<k<p.

Under the additional assumption

5626\le p,

prove that $m=1$ . Since one is fixed, the hypotheses would in fact be inconsistent. This is the remaining unbounded cycle obligation after separately isolating return period 4961 and excluding the interval 4962 through 5625. Period 4961 remains a separate open obligation; this statement does not claim that all smaller periods have been settled.

Preamble

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

Formal statement

theorem syracuse_minimal_period_ge_5626_eq_one (m p : ℕ) (hm : 0 < m)
    (hp : 5626 ≤ p) (hcyc : syracuseStep^[p] m = m)
    (hmin : ∀ k : ℕ, 0 < k → k < p → syracuseStep^[k] m ≠ m) :
    m = 1 := by sorry

Source

Collatz mission https://prove2.me/missions/Collatz%20Conjecture . Subcase of the exact open frontier syracuse_minimal_period_ge_fortyninesixtyone_eq_one (39d44aec-e63d-4fb4-96a6-2ec1636ad877), separated by the proved interval syracuse_period_4962_to_5625_eq_one. For the fixed-period case, smaller return times are covered by syracuse_period_le_fortyninesixty_eq_one (1f75404a-e93a-4c58-8dca-d6a968bed177). These are explicitly open subproblems of the mission, not established source theorems.

View graph