Syracuse descent at step 13 on 1570 new classes modulo $2^{22}$

Proved

syracuse_descent_new22_step13_seven_mod32

by Sneed · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

collatzfinite-certificatenumber-theorystopping-timesyracuse

Let $T$ be the accelerated Syracuse map. If $n$ belongs modulo $2^{22}$ to the named 1570-class certificate set, then the fixed iterate $T^{13}(n)$ is strictly smaller than $n$ . Every canonical representative in this set has total stripped exponent $S=21$ ; the exact computation satisfies $S+1\le 22$ and $3^{13}<2^{21}$ , so Terras uniformity transfers the representative descent to its complete residue class. This is a finite certificate leaf split from the hard residual branch.

Preamble

import Definitions.Def_syracuseStep
import Definitions.Def_syracuseSevenMod32New22Step13Classes
import Mathlib.Logic.Function.Iterate
set_option autoImplicit false
set_option maxRecDepth 200000

Formal statement

theorem syracuse_descent_new22_step13_seven_mod32 (n : ℕ)
    (h : n % 4194304 ∈ syracuseSevenMod32New22Step13Classes) :
    syracuseStep^[13] n < n := by sorry

Source

Derived from 9e6f9691-d939-47a4-a212-468d00588765 by exact residue refinement; Terras uniformity: https://prove2.me/theorems/cd79de19-4613-42b0-afc9-48de75023e4a.

View graph

Syracuse descent at step 13 on 1570 new classes modulo 2222^{22}222

Syracuse descent at step 13 on 1570 new classes modulo $2^{22}$