Residual Syracuse descent after twelve certified progressions

Open

syracuse_descent_residual_mod4096

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$ . Consider a natural number $n$ satisfying

n\bmod128\in\{39,71,103\},

and all three exclusions

\begin{aligned} n\bmod 256&\notin\{39,199\}\\ n\bmod 1024&\notin\{423,583,999\}\\ n\bmod 4096&\notin\{231,615,935,1703,3143,3559,3911\} \end{aligned}.

The open assertion is

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

This is the residual subproblem left after separating twelve arithmetic progressions with certified descent within seven Syracuse steps. It consists of 45 of the previous 96 residue classes modulo 4096. Both the starting value and the descent time are unbounded; the assertion remains unproved.

Formalization Note. The imports use the existing syracuseStep definition. Positivity and oddness already follow from the first congruence hypothesis.

Preamble

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

Formal statement

theorem syracuse_descent_residual_mod4096 (n : ℕ)
    (h : n % 128 = 39 ∨ n % 128 = 71 ∨ n % 128 = 103)
    (h256 : n % 256 ≠ 39 ∧ n % 256 ≠ 199)
    (h1024 : n % 1024 ≠ 423 ∧ n % 1024 ≠ 583 ∧ n % 1024 ≠ 999)
    (h4096 : n % 4096 ≠ 231 ∧ n % 4096 ≠ 615 ∧ n % 4096 ≠ 935 ∧ n % 4096 ≠ 1703 ∧ n % 4096 ≠ 3143 ∧ n % 4096 ≠ 3559 ∧ n % 4096 ≠ 3911)
    : ∃ t : ℕ, 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