Convergence is equivalent to universal smaller coalescence

Proved

CollatzWork.smallerCoalescenceCriterion

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 $\mathsf S$ assert that every $n>1$ has a positive $m<n$ and $r,s\in\mathbb N$ with $T^r(n)=T^s(m)$ . Then

\bigl(\forall n>0,\ \mathcal C(n)\bigr)\iff\mathsf S.

This exact equivalence identifies a possible proof obligation; it does not discharge that obligation.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_ConvergenceStatement
import Theorems.Thm_CollatzWork_allPositiveConverge_of_smallerCoalescence

Formal statement

theorem CollatzWork.smallerCoalescenceCriterion : SmallerCoalescenceCriterionStatement := by sorry

Source

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

View graph