No nontrivial Syracuse periodic point of iterate period at least seven

Open

syracuse_periodic_ge_seven_eq_one

by mysticflounder · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

collatzcyclesdynamical-systemsiterationnumber-theory

Let $T$ be the Syracuse map. The remaining high-period cycle assertion is

m>0,\quad a\ge 7,\quad T^a(m)=m \Longrightarrow m=1.

The cases $a=1,\ldots,6$ have separate proved formalizations. Thus this statement isolates precisely the unproved range needed to exclude all positive nontrivial Syracuse cycles. The integer $a$ is an iterate period, not necessarily the least period.

Preamble

import Mathlib
import Definitions.Def_syracuseStep

Formal statement

theorem syracuse_periodic_ge_seven_eq_one (m period : ℕ)
    (hm : 0 < m) (hperiod : 7 ≤ period)
    (hcyc : syracuseStep^[period] m = m) :
    m = 1 := by
  sorry

Source

Jeffrey C. Lagarias, The 3x+1 Problem and Its Generalizations, Amer. Math. Monthly 92 (1985), Section 8 (cycles), https://websites.umich.edu/~lagarias/3x%2B1.html; local formalization of the complementary periods through six: https://github.com/flound1129/collatz/tree/c0b24f073dcdc63d9d0974429bd8f3c522ed8eb4/lean/CollatzConjecture

View graph