No bounded-time descent rank from a finite monotone palette

Proved

CollatzWork.finitePaletteObstruction

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 $r,B\in\mathbb N$ , let $f_0,\ldots,f_{r-1}:\mathbb N\to\mathbb N$ be nondecreasing on inputs at least $B$ , and let $\sigma:\mathbb N\to\{0,\ldots,r-1\}$ . Let $V:\mathbb N\to\mathbb N$ satisfy $V(n)=f_{\sigma(n)}(n)$ for $n\ge B$ .

For any further natural threshold $B'$ and time bound $H$ , the following uniform rank-descent assertion is false:

\neg\bigl(\forall n\ge B',\ \exists j,\ 1\le j\le H\ \land\ V(T^j(n))<V(n)\bigr).

The obstruction concerns this finite-palette, uniformly bounded-time proof architecture. It does not imply nontermination of any Collatz orbit.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_ConvergenceStatement
import Definitions.Def_CollatzWork_FinitePaletteObstructionStatement
import Definitions.Def_CollatzWork_InverseWordBoundaryStatement
import Definitions.Def_CollatzWork_RefinedMersenneChild
import Theorems.Thm_CollatzWork_finitePalette_path_obstruction
import Theorems.Thm_CollatzWork_mersenne_prefix_nondecreasing

Formal statement

theorem CollatzWork.finitePaletteObstruction : FinitePaletteObstructionStatement := by sorry

Source

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

View graph