Two guarded growing bursts descend below the original start

Proved

CollatzWork.twoBurstDescent

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 $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$ .

Under these hypotheses,

T^{4(k+l)+2}(N)=m<N.

Both exact arithmetic guards are assumptions. No universal choice of parameters or all-root coverage is asserted.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_ConvergenceStatement
import Definitions.Def_CollatzWork_InverseWordBoundaryStatement
import Definitions.Def_CollatzWork_RefinedMersenneChild
import Definitions.Def_CollatzWork_TwoBurstStatement
import Theorems.Thm_CollatzWork_rootDescentBurst
import Theorems.Thm_CollatzWork_twoBurst_power_margin

Formal statement

theorem CollatzWork.twoBurstDescent : TwoBurstDescentStatement := by sorry

Source

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

View graph