Syracuse step-12 descent on chunk 1/1 at $2^{24}$

Proved

syracuse_descent_new24_step12_chunk01_seven_mod32

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

collatzfinite-certificatenumber-theorystopping-timesyracuse

For any natural number whose residue modulo $2^{24}$ belongs to the named 525-element chunk, the accelerated Syracuse iterate $T^{12}(n)$ is strictly smaller than $n$ . Every representative in this chunk has total stripped exponent $S=23$ , with $S+1\le 24$ and $3^{12}<2^{23}$ , so the fixed representative certificate transfers to the full residue class.

Preamble

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

Formal statement

theorem syracuse_descent_new24_step12_chunk01_seven_mod32 (n : ℕ)
    (h : n % 16777216 ∈ syracuseSevenMod32New24Step12Chunk01Classes) :
    syracuseStep^[12] n < n := by sorry

Source

Computational certificate child of the Prove2Me Collatz residual tree; uniformity theorem https://prove2.me/theorems/cd79de19-4613-42b0-afc9-48de75023e4a.

View graph

Syracuse step-12 descent on chunk 1/1 at 2242^{24}224

Syracuse step-12 descent on chunk 1/1 at $2^{24}$