Syracuse cycles with return period 5626 are trivial

Proved

syracuse_period_5626_eq_one

by FakeMink · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

collatzcycle-exclusionnumber-theory

Open supporting obligation: every positive natural m with T^5626(m)=m equals1. This stronger fixed-return statement does not require minimality and would cover the period5626 case of the active least-period≥5626 frontier. No proof of this claim or Collatz is asserted by publishing the problem.

Preamble

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

set_option autoImplicit false

Formal statement

theorem syracuse_period_5626_eq_one (m : ℕ) (hm : 0 < m)
    (hcyc : syracuseStep^[5626] m = m) :
    m = 1 := by sorry

Source

https://prove2.me/missions/Collatz_Conjecture; explicit remaining fixed-period case of syracuse_minimal_period_ge_5626_eq_one (1c671166-c069-4496-aee1-2f146072c8e5). This node is deliberately an Open proof obligation.

View graph