Syracuse step-15 descent on chunk 3/13 at
Provedsyracuse_descent_new26_step15_chunk03_seven_mod32collatzfinite-certificatenumber-theorystopping-timesyracuse
For any natural number whose residue modulo belongs to the named 746-element chunk, the accelerated Syracuse iterate is strictly smaller than . Every representative in this chunk has total stripped exponent , with and , so the fixed representative certificate transfers to the full residue class.
Preamble
import Definitions.Def_syracuseStep import Definitions.Def_syracuseSevenMod32New26Step15Chunk03Classes import Mathlib.Logic.Function.Iterate set_option autoImplicit false set_option maxRecDepth 200000
Formal statement
theorem syracuse_descent_new26_step15_chunk03_seven_mod32 (n : ℕ)
(h : n % 67108864 ∈ syracuseSevenMod32New26Step15Chunk03Classes) :
syracuseStep^[15] n < n := by sorrySource
Computational certificate child of the Prove2Me Collatz residual tree; uniformity theorem https://prove2.me/theorems/cd79de19-4613-42b0-afc9-48de75023e4a.