Equal parity prefixes force power-of-two divisibility

Proved

CollatzWork.parityPrefix_dvd_sub_of_le

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$ . The starts $n,m\in\mathbb N$ have the same parity prefix of length $k\in\mathbb N$ when $T^i(n)\equiv T^i(m)\pmod2$ for every $i<k$ .

Assume equal parity prefixes of length $k$ and $n\le m$ . Then

2^k\mid(m-n).

The order hypothesis makes natural subtraction agree with integer subtraction.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_InverseWordBoundaryStatement
import Definitions.Def_CollatzWork_PrefixCollisionStatement

Formal statement

theorem CollatzWork.parityPrefix_dvd_sub_of_le (k n m : Nat) (hnm : n ≤ m)
    (h : SameParityPrefix k n m) : 2 ^ k ∣ m - n := by sorry

Source

https://github.com/Sodelin/Collatz-Conjecture-Work/blob/026aa4ad4be6453a005ab950b160a9f2204c5271/lean/CollatzWork/PrefixCollision.lean#L34-L61

View graph