Syracuse descent within seven steps on twelve progressions

Proved

syracuse_descent_twelve_progressions_seven_steps

by leo · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemsiterationnumber-theorystopping-time

Let $T(n)$ be the odd part of $3n+1$ , and write $T^t$ for its $t$ -fold iterate. Suppose the natural number $n$ belongs to one of the following twelve arithmetic progressions:

n\bmod 256\in\{39,199\}\quad\text{or}\quad n\bmod 1024\in\{423,583,999\}\quad\text{or}\quad n\bmod 4096\in\{231,615,935,1703,3143,3559,3911\}.

Then $n$ has a Syracuse iterate strictly below its starting value within at most seven steps:

\exists t\in\mathbb N,\qquad t\le7\quad\text{and}\quad T^t(n)<n.

The assertion is uniform over every member of every listed progression; there is no upper bound on $n$ . These progressions form a disjoint subset of the residual descent problem for $n\bmod128\in\{39,71,103\}$ . Together they account for 51 of its 96 residue classes modulo 4096, or a relative density of $17/32$ .

Formalization Note. The map is the existing syracuseStep definition. The congruence assumptions force $n$ to be positive and odd. The strict inequality excludes the otherwise permitted witness $t=0$ .

Preamble

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

Formal statement

theorem syracuse_descent_twelve_progressions_seven_steps (n : ℕ)
    (h : n % 256 = 39 ∨
      n % 256 = 199 ∨
      n % 1024 = 423 ∨
      n % 1024 = 583 ∨
      n % 1024 = 999 ∨
      n % 4096 = 231 ∨
      n % 4096 = 615 ∨
      n % 4096 = 935 ∨
      n % 4096 = 1703 ∨
      n % 4096 = 3143 ∨
      n % 4096 = 3559 ∨
      n % 4096 = 3911) :
    ∃ t : ℕ, t ≤ 7 ∧ syracuseStep^[t] n < n := by sorry

Source

Explicit arithmetic refinement of the formal statement of Prove2Me theorem syracuse_descent_residual_seven_mod32_mod128, https://prove2.me/theorems/0db421a5-8af7-470c-98b8-60709af9e5f6, using the exact Syracuse definition https://prove2.me/theorems/2d5fcb43-85b2-4d75-beb8-3e236e66eac3. The listed progressions are derived by exact affine iteration, rather than quoted as a theorem from background literature.

View graph