A uniform residue-20 tail for every root congruent to eleven modulo twenty-seven

Proved

CollatzWork.residueAncestor_refinedTail

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 $z\in\mathbb N$ satisfy $z\equiv11\pmod{27}$ . Then

\exists m,b\in\mathbb N,\quad m>0,\quad m\equiv20\pmod{27},\quad T^b(m)=z,\quad m\le64z.

This gives a bounded-size ancestor; strict descent relative to the later original root requires a separate power comparison.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_ConvergenceStatement
import Theorems.Thm_CollatzWork_residueAncestor_tail38
import Theorems.Thm_CollatzWork_residueAncestor_tail65
import Theorems.Thm_CollatzWork_residueAncestor_tail11
import Theorems.Thm_CollatzWork_residueAncestor_tail92
import Theorems.Thm_CollatzWork_residueAncestor_tail173

Formal statement

theorem CollatzWork.residueAncestor_refinedTail (z : Nat) (hz : z % 27 = 11) :
    ∃ m b : Nat, 0 < m ∧ m % 27 = 20 ∧
      shortcutIter b m = z ∧ m ≤ 64 * z := by sorry

Source

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

View graph