Syracuse return period 4961: exclude nontrivial periodic points

Proved

syracuse_period_4961_eq_one

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

collatzcycle-exclusionnumber-theory

Let $T$ be the Syracuse map. For every positive natural number $m$ , prove

T^{4961}(m)=m\quad\Longrightarrow\quad m=1.

No least-period hypothesis is imposed. All smaller return periods have already been excluded by the proved theorem syracuse_period_le_fortyninesixty_eq_one, so this fixed-period obligation isolates the first unsettled return period of the current cycle branch. The existing threshold 1,883,432 does not satisfy the numerical margin at period 4961; this remains an open cycle-exclusion problem.

Preamble

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

Formal statement

theorem syracuse_period_4961_eq_one (m : ℕ) (hm : 0 < m)
    (hcyc : syracuseStep^[4961] 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