Conditional convergence after a guarded two-burst descent

Proved

CollatzWork.twoBurst_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,l,u,v,m$ be positive natural numbers satisfying $9^k u+1=2^{3l+1}v$ and $2^{k+l}m+5=3\cdot9^l v$ . Put $N=2\cdot8^ku-5$ .

Assume additionally $\mathcal C(a)$ for every natural $a$ with $0<a<N$ . Then

\mathcal C(N).

The convergence conclusion retains both arithmetic guards and the smaller-start induction premise.

Preamble

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

Formal statement

theorem CollatzWork.twoBurst_converges_of_smaller (k l u v m : Nat)
    (hk : 0 < k) (hl : 0 < l) (hu : 0 < u) (hv : 0 < v) (hm : 0 < m)
    (hrecharge : 9 ^ k * u + 1 = 2 ^ (3 * l + 1) * v)
    (hexit : 2 ^ (k + l) * m + 5 = 3 * 9 ^ l * v)
    (ih : ∀ a : Nat, 0 < a → a < 2 * 8 ^ k * u - 5 → Converges a) :
    Converges (2 * 8 ^ k * u - 5) := by sorry

Source

https://github.com/Sodelin/Collatz-Conjecture-Work/blob/026aa4ad4be6453a005ab950b160a9f2204c5271/lean/CollatzWork/TwoBurst.lean#L174-L183

View graph