Variable ancestor prefix of length k plus 2

Proved

CollatzWork.residueAncestor_prefix_two

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,u,r\in\mathbb N$ with $u>0$ and $3^{k+3}u=4r+1$ . Then

T^{k+2}(9\cdot2^k u-1)=r.

This computes a guarded forward prefix without claiming that its starting value is smaller than r.

Preamble

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

Formal statement

theorem CollatzWork.residueAncestor_prefix_two (k u r : Nat) (hu : 0 < u)
    (hguard : 3 ^ (k + 3) * u = 4 * r + 1) :
    shortcutIter (k + 2) (9 * (2 ^ k * u) - 1) = r := by sorry

Source

https://github.com/Sodelin/Collatz-Conjecture-Work/blob/026aa4ad4be6453a005ab950b160a9f2204c5271/lean/CollatzWork/ResidueAncestor.lean#L70-L84

View graph