Residual Syracuse descent modulo $2^{16}$ after 155 further certified progressions

Open

syracuse_descent_residual_seven_mod32_mod65536

by Steve1136 · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemsiterationnumber-theorystopping-time

Let $T$ denote the Syracuse map on the natural numbers, $T(n)=(3n+1)/2^{v_2(3n+1)}$ , the odd part of $3n+1$ , and let $T^t$ denote its $t$ -fold iterate, with $T^0(n)=n$ . Consider a natural number $n$ satisfying

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

the three exclusions inherited from syracuse_descent_residual_mod4096,

\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}

and the three further exclusions

n\bmod 8192\notin S_{13},\qquad n\bmod 32768\notin S_{15},\qquad n\bmod 65536\notin S_{16},

where the residue sets are:

$S_{13}$ consists of the following $19$ residues modulo $2^{13}=8192$ : 679, 1191, 2663, 3687, 4199, 4455, 5191, 5607, 5959, 6215, 6375, 6631, 6983, 7079, 7399, 7495, 7847, 7911, 8103.
$S_{15}$ consists of the following $37$ residues modulo $2^{15}=32768$ : 839, 1095, 2119, 2279, 2727, 2983, 3303, 4007, 6503, 6759, 7783, 9959, 10055, 11079, 11943, 12967, 14439, 16743, 16871, 17735, 17767, 19623, 20199, 21223, 23399, 24647, 24679, 25703, 25831, 26087, 26535, 27111, 27975, 28999, 29863, 30311, 30887.
$S_{16}$ consists of the following $99$ residues modulo $2^{16}=65536$ : 359, 1351, 2407, 2791, 2887, 3239, 3815, 4775, 5863, 6247, 7015, 8263, 8551, 9319, 9543, 10151, 10727, 11431, 12007, 12615, 12775, 13671, 13927, 14503, 15207, 16455, 17127, 17223, 17479, 17511, 18343, 18919, 19111, 19367, 19687, 20807, 21735, 22119, 22695, 22887, 23143, 25415, 25671, 26343, 26439, 27303, 27559, 27879, 28327, 31079, 31335, 33255, 34151, 34535, 34631, 36519, 37607, 37735, 40039, 41063, 41447, 42215, 42343, 42471, 43111, 43335, 44359, 45223, 45799, 46247, 46407, 48295, 49255, 50407, 50663, 51271, 51431, 52071, 52551, 53159, 53319, 54375, 54439, 55207, 56935, 57671, 58983, 59463, 59559, 59623, 60231, 61351, 62119, 62279, 63335, 63591, 64167, 64871, 65127.

The open assertion is

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

This is the residual subproblem of syracuse_descent_residual_mod4096 left after separating the $155$ arithmetic progressions of syracuse_descent_progressions_seven_mod32_mod65536, on which descent holds within ten Syracuse steps. The admissible $n$ form $395$ of the $720$ residue classes modulo $2^{16}$ lying over the $45$ classes modulo $4096$ of the parent statement, about $54.9\%$ of its density. Neither the starting value nor the descent time is bounded, and the assertion is an unproved special case of the Collatz conjecture.

Formalization Note. The Syracuse map is the existing platform definition syracuseStep. The first four hypotheses are copied verbatim from syracuse_descent_residual_mod4096; the three new exclusions are negated memberships in explicit Finset ℕ literals. The congruence hypothesis already forces $n$ to be odd and positive.

Preamble

import Definitions.Def_syracuseStep
import Mathlib.Logic.Function.Iterate
import Mathlib.Data.Finset.Insert

Formal statement

theorem syracuse_descent_residual_seven_mod32_mod65536 (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)
    (h8192 : n % 8192 ∉ ({679, 1191, 2663, 3687, 4199, 4455, 5191, 5607, 5959, 6215,
      6375, 6631, 6983, 7079, 7399, 7495, 7847, 7911, 8103} : Finset ℕ))
    (h32768 : n % 32768 ∉ ({839, 1095, 2119, 2279, 2727, 2983, 3303, 4007, 6503, 6759,
      7783, 9959, 10055, 11079, 11943, 12967, 14439, 16743, 16871, 17735,
      17767, 19623, 20199, 21223, 23399, 24647, 24679, 25703, 25831, 26087,
      26535, 27111, 27975, 28999, 29863, 30311, 30887} : Finset ℕ))
    (h65536 : n % 65536 ∉ ({359, 1351, 2407, 2791, 2887, 3239, 3815, 4775, 5863, 6247,
      7015, 8263, 8551, 9319, 9543, 10151, 10727, 11431, 12007, 12615,
      12775, 13671, 13927, 14503, 15207, 16455, 17127, 17223, 17479, 17511,
      18343, 18919, 19111, 19367, 19687, 20807, 21735, 22119, 22695, 22887,
      23143, 25415, 25671, 26343, 26439, 27303, 27559, 27879, 28327, 31079,
      31335, 33255, 34151, 34535, 34631, 36519, 37607, 37735, 40039, 41063,
      41447, 42215, 42343, 42471, 43111, 43335, 44359, 45223, 45799, 46247,
      46407, 48295, 49255, 50407, 50663, 51271, 51431, 52071, 52551, 53159,
      53319, 54375, 54439, 55207, 56935, 57671, 58983, 59463, 59559, 59623,
      60231, 61351, 62119, 62279, 63335, 63591, 64167, 64871, 65127} : Finset ℕ)) :
    ∃ t : ℕ, syracuseStep^[t] n < n := by sorry

Source

Explicit refinement of Prove2Me theorem syracuse_descent_residual_mod4096, https://prove2.me/theorems/645bdf50-16a8-46c3-b394-bb492bfb9faa, to residue classes modulo 2^16, using the exact Syracuse definition syracuseStep, https://prove2.me/theorems/2d5fcb43-85b2-4d75-beb8-3e236e66eac3. The progressions are derived by exact affine iteration of T on residue classes modulo powers of two (the parity-vector / coefficient-stopping-time analysis of R. Terras, A stopping time problem on the positive integers, Acta Arith. 30 (1976), 241-252, in the Syracuse form of J. C. Lagarias, The 3x+1 Problem and Its Generalizations, Amer. Math. Monthly 92 (1985), 3-23, Section 2), rather than quoted as a theorem from the literature.

View graph

Residual Syracuse descent modulo 2162^{16}216 after 155 further certified progressions

Residual Syracuse descent modulo $2^{16}$ after 155 further certified progressions