Conditional convergence of a guarded refined parent

Proved

CollatzWork.refinedParent_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$ . For natural parameters $L,\varepsilon,z$ , put $A=4z+2\varepsilon+1$ , $P=2^LA-1$ , and $Q=3\cdot2^{L-2}A-1$ . When $L<2$ , the exponent $L-2$ uses truncated natural subtraction.

Assume $L\ge2$ , $\varepsilon\le1$ , and $\varepsilon\equiv L\pmod2$ . Assume additionally $\mathcal C(m)$ for every natural $m$ with $0<m<P$ . Then

\mathcal C(P).

This is a strong-induction application with the smaller-start hypothesis retained.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_ConvergenceStatement
import Definitions.Def_CollatzWork_RefinedMersenneChild
import Theorems.Thm_CollatzWork_refinedParent_converges_iff_child
import Theorems.Thm_CollatzWork_refinedChild_arithmetic

Formal statement

theorem CollatzWork.refinedParent_converges_of_smaller (L epsilon z : Nat)
    (hL : 2 ≤ L) (hepsilon : epsilon ≤ 1)
    (hparity : epsilon % 2 = L % 2)
    (ih : ∀ m : Nat, 0 < m → m < refinedParent L epsilon z → Converges m) :
    Converges (refinedParent L epsilon z) := by sorry

Source

https://github.com/Sodelin/Collatz-Conjecture-Work/blob/026aa4ad4be6453a005ab950b160a9f2204c5271/lean/CollatzWork/Convergence.lean#L126-L135

View graph