Residual Syracuse descent inside $n \equiv 27 \pmod{32}$ modulo $2^{16}$

Open

syracuse_descent_residual_twentyseven_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$ with

n\equiv 27\pmod{32},

satisfying the exclusions inherited from syracuse_descent_residual_twentyseven_mod32_mod8192_excl8,

\begin{aligned} n\bmod 128&\ne 59,\\ n\bmod 256&\notin\{123,219\},\\ n\bmod 1024&\notin\{347,507,923\},\\ n\bmod 4096&\notin\{1019,1435,1787,2203,2587,2907,3675\},\\ n\bmod 8192&\notin\{539,1563,2075,3483,3835,4507,4859,5371,5723,6747,7259\},\\ n\bmod 8192&\notin\{2331,3067,4091,4251,4955,5275,5787,5979\}, \end{aligned}

and the two further exclusions

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

where the residue sets are:

$S_{15}$ consists of the following $37$ residues modulo $2^{15}=32768$ : 411, 1275, 2299, 3163, 3611, 4187, 6907, 7163, 8187, 8347, 8795, 9051, 9371, 10075, 12571, 12827, 13851, 16027, 16123, 17147, 18011, 19035, 20507, 22811, 22939, 23803, 23835, 25691, 26267, 27291, 29467, 30715, 30747, 31771, 31899, 32155, 32603.
$S_{16}$ consists of the following $99$ residues modulo $2^{16}=65536$ : 603, 859, 1179, 1627, 4379, 4635, 6555, 7451, 7835, 7931, 9819, 10907, 11035, 13339, 14363, 14747, 15515, 15643, 15771, 16411, 16635, 17659, 18523, 19099, 19547, 19707, 21595, 22555, 23707, 23963, 24571, 24731, 25371, 25851, 26459, 26619, 27675, 27739, 28507, 30235, 30971, 32283, 32763, 32859, 32923, 33531, 34651, 35419, 35579, 36635, 36891, 37467, 38171, 38427, 39195, 40187, 41243, 41627, 41723, 42075, 42651, 43611, 44699, 45083, 45851, 47099, 47387, 48155, 48379, 48987, 49563, 50267, 50843, 51451, 51611, 52507, 52763, 53339, 54043, 55291, 55963, 56059, 56315, 56347, 57179, 57755, 57947, 58203, 58523, 59643, 60571, 60955, 61531, 61723, 61979, 64251, 64507, 65179, 65275.

The open assertion is

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

This is the residual subproblem of syracuse_descent_residual_twentyseven_mod32_mod8192_excl8 left after separating the $136$ arithmetic progressions of syracuse_descent_progressions_twentyseven_mod32_mod65536, on which descent holds within ten Syracuse steps. The admissible $n$ form $395$ of the $568$ residue classes modulo $2^{16}$ lying over the $71$ classes modulo $8192$ of the parent statement, about $69.5\%$ 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 seven hypotheses are copied verbatim from syracuse_descent_residual_twentyseven_mod32_mod8192_excl8; the two new exclusions are negated memberships in explicit Finset ℕ literals. No oddness or positivity hypothesis is needed, since $n\equiv27\pmod{32}$ forces both.

Preamble

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

Formal statement

theorem syracuse_descent_residual_twentyseven_mod32_mod65536 (n : ℕ)
    (h : n % 32 = 27)
    (h128 : n % 128 ≠ 59)
    (h256 : n % 256 ≠ 123 ∧ n % 256 ≠ 219)
    (h1024 : n % 1024 ≠ 347 ∧ n % 1024 ≠ 507 ∧ n % 1024 ≠ 923)
    (h4096 : n % 4096 ≠ 1019 ∧ n % 4096 ≠ 1435 ∧ n % 4096 ≠ 1787 ∧
      n % 4096 ≠ 2203 ∧ n % 4096 ≠ 2587 ∧ n % 4096 ≠ 2907 ∧
      n % 4096 ≠ 3675)
    (h8192 : n % 8192 ≠ 539 ∧ n % 8192 ≠ 1563 ∧ n % 8192 ≠ 2075 ∧
      n % 8192 ≠ 3483 ∧ n % 8192 ≠ 3835 ∧ n % 8192 ≠ 4507 ∧
      n % 8192 ≠ 4859 ∧ n % 8192 ≠ 5371 ∧ n % 8192 ≠ 5723 ∧
      n % 8192 ≠ 6747 ∧ n % 8192 ≠ 7259)
    (h8192b : n % 8192 ≠ 2331 ∧ n % 8192 ≠ 3067 ∧ n % 8192 ≠ 4091 ∧
      n % 8192 ≠ 4251 ∧ n % 8192 ≠ 4955 ∧ n % 8192 ≠ 5275 ∧
      n % 8192 ≠ 5787 ∧ n % 8192 ≠ 5979)
    (h32768 : n % 32768 ∉ ({411, 1275, 2299, 3163, 3611, 4187, 6907, 7163, 8187, 8347,
      8795, 9051, 9371, 10075, 12571, 12827, 13851, 16027, 16123, 17147,
      18011, 19035, 20507, 22811, 22939, 23803, 23835, 25691, 26267, 27291,
      29467, 30715, 30747, 31771, 31899, 32155, 32603} : Finset ℕ))
    (h65536 : n % 65536 ∉ ({603, 859, 1179, 1627, 4379, 4635, 6555, 7451, 7835, 7931,
      9819, 10907, 11035, 13339, 14363, 14747, 15515, 15643, 15771, 16411,
      16635, 17659, 18523, 19099, 19547, 19707, 21595, 22555, 23707, 23963,
      24571, 24731, 25371, 25851, 26459, 26619, 27675, 27739, 28507, 30235,
      30971, 32283, 32763, 32859, 32923, 33531, 34651, 35419, 35579, 36635,
      36891, 37467, 38171, 38427, 39195, 40187, 41243, 41627, 41723, 42075,
      42651, 43611, 44699, 45083, 45851, 47099, 47387, 48155, 48379, 48987,
      49563, 50267, 50843, 51451, 51611, 52507, 52763, 53339, 54043, 55291,
      55963, 56059, 56315, 56347, 57179, 57755, 57947, 58203, 58523, 59643,
      60571, 60955, 61531, 61723, 61979, 64251, 64507, 65179, 65275} : Finset ℕ)) :
    ∃ t : ℕ, syracuseStep^[t] n < n := by sorry

Source

Explicit refinement of Prove2Me theorem syracuse_descent_residual_twentyseven_mod32_mod8192_excl8, https://prove2.me/theorems/90428acc-af53-4bb4-8fb3-36a19c10aef5, 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 inside n≡27(mod32)n \equiv 27 \pmod{32}n≡27(mod32) modulo 2162^{16}216

Residual Syracuse descent inside $n \equiv 27 \pmod{32}$ modulo $2^{16}$