Nondecreasing prefixes of arbitrary finite Mersenne length

Proved

CollatzWork.mersenne_prefix_nondecreasing

by Sodelin · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

collatz-work-import

Let $T:\mathbb N\to\mathbb N$ be the shortcut Collatz map: $T(n)=n/2$ for even $n$ and $T(n)=(3n+1)/2$ for odd $n$ . Write $T^k$ for its $k$ -fold iterate, with $T^0(n)=n$ .

Let $L,q\in\mathbb N$ with $q>0$ , and put $N=2^Lq-1$ . Then

\forall k<L,\quad T^k(N)\le T^{k+1}(N).

The length L is arbitrary, but the conclusion is confined to the finite initial prefix.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_ConvergenceStatement
import Definitions.Def_CollatzWork_InverseWordBoundaryStatement
import Definitions.Def_CollatzWork_RefinedMersenneChild
import Theorems.Thm_CollatzWork_oddRun

Formal statement

theorem CollatzWork.mersenne_prefix_nondecreasing (L q : Nat) (hq : 0 < q) :
    ∀ k, k < L →
      shortcutIter k (2 ^ L * q - 1) ≤
      shortcutIter (k + 1) (2 ^ L * q - 1) := by sorry

Source

https://github.com/Sodelin/Collatz-Conjecture-Work/blob/026aa4ad4be6453a005ab950b160a9f2204c5271/lean/CollatzWork/FinitePaletteObstruction.lean#L84-L107

View graph