Exact residue-20 tail to 92 modulo 243

Proved

CollatzWork.residueAncestor_tail92

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

For $a\in\mathbb N$ , put $m=6912a+2612$ and $z=243a+92$ . Then

m>0,\quad m\equiv20\pmod{27},\quad T^{8}(m)=z,\quad 9m+44=256z,\quad m\le64z.

This is one row of the finite tail selector. The bound by 64z is not a claim that the ancestor is smaller than z.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_ConvergenceStatement
import Definitions.Def_CollatzWork_InverseWordBoundaryStatement
import Definitions.Def_CollatzWork_RefinedMersenneChild

Formal statement

theorem CollatzWork.residueAncestor_tail92 (a : Nat) :
    0 < 6912 * a + 2612 ∧
    (6912 * a + 2612) % 27 = 20 ∧
    shortcutIter 8 (6912 * a + 2612) = 243 * a + 92 ∧
    9 * (6912 * a + 2612) + 44 = 256 * (243 * a + 92) ∧
    6912 * a + 2612 ≤ 64 * (243 * a + 92) := by sorry

Source

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

View graph