Conditional convergence transfer from guarded burst descent

Proved

CollatzWork.rootDescent_converges_of_smaller

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$ . Write $\mathcal C(n)$ for the assertion that $T^j(n)=1$ for some $j\in\mathbb N$ .

Let $k,u,m>0$ be natural numbers with $2^k m+5=9^k u$ , and put $N=8^k u-5$ . Assume $\mathcal C(a)$ for every natural $a$ with $0<a<N$ . Then

\mathcal C(N).

This is a strong-induction transfer for a guarded family; the hypothesis on all smaller starts remains explicit.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_ConvergenceStatement
import Theorems.Thm_CollatzWork_converges_shortcutIter_iff
import Theorems.Thm_CollatzWork_rootDescent

Formal statement

theorem CollatzWork.rootDescent_converges_of_smaller (k u m : Nat)
    (hk : 0 < k) (hu : 0 < u) (hm : 0 < m)
    (hguard : 2 ^ k * m + 5 = 9 ^ k * u)
    (ih : ∀ a : Nat, 0 < a → a < 8 ^ k * u - 5 → Converges a) :
    Converges (8 ^ k * u - 5) := by sorry

Source

https://github.com/Sodelin/Collatz-Conjecture-Work/blob/026aa4ad4be6453a005ab950b160a9f2204c5271/lean/CollatzWork/RootDescent.lean#L121-L129

View graph