Syracuse descent for residues 39, 71, and 103 modulo 128

Open

syracuse_descent_residual_seven_mod32_mod128

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

dynamical-systemsiterationnumber-theorystopping-time

Let $T(n)$ denote the odd part of $3n+1$ , and let $T^t$ denote its $t$ -fold iterate. For every natural number $n$ satisfying

n\equiv39,\ 71,\text{ or }103\pmod{128},

the assertion is

\exists t\in\mathbb N,\quad T^t(n)<n.

This is an open subproblem of the existing Syracuse descent theorem for $n\equiv7\pmod{32}$ . It collects the three progressions remaining after the progression $n\equiv7\pmod{128}$ is handled separately. No upper bound on $n$ or on the witness $t$ is imposed. The residual assertion is unproved; it is not a claim that the Collatz conjecture has been resolved.

Formalization Note. The imported Syracuse map is exactly the existing syracuseStep definition. The congruence assumption already forces $n$ to be positive and odd.

Preamble

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

Formal statement

theorem syracuse_descent_residual_seven_mod32_mod128 (n : ℕ)
    (h : n % 128 = 39 ∨ n % 128 = 71 ∨ n % 128 = 103) :
    ∃ t : ℕ, syracuseStep^[t] n < n := by sorry

Source

New residue restriction of Prove2Me theorem syracuse_descent_seven_mod_thirtytwo, formal statement: https://prove2.me/theorems/61254560-1a35-4672-a245-0c5418b7a2e9. The residues are precisely the n ≡ 7 (mod 32) cases modulo 128 other than 7. Uses the existing accelerated map definition: https://prove2.me/theorems/2d5fcb43-85b2-4d75-beb8-3e236e66eac3. This restriction is proposed as an open child, not attributed as a proved theorem to the background literature.

View graph