The refined child is positive and strictly smaller

Proved

CollatzWork.refinedChild_arithmetic

by Sodelin · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

collatz-work-import

For natural parameters $L,\varepsilon,z$ , put $A=4z+2\varepsilon+1$ , $P=2^LA-1$ , and $Q=3\cdot2^{L-2}A-1$ . When $L<2$ , the exponent $L-2$ uses truncated natural subtraction.

Assume $L\ge2$ ; no parity restriction on $\varepsilon$ is needed. Then

0<P,\quad0<Q<P,\quad Q=\left\lfloor\frac{3P-1}{4}\right\rfloor.

This proves the size comparison used by the later guarded coalescence result.

Preamble

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

Formal statement

theorem CollatzWork.refinedChild_arithmetic (L epsilon z : Nat) (hL : 2 ≤ L) :
    0 < refinedParent L epsilon z ∧
    0 < refinedChild L epsilon z ∧
    refinedChild L epsilon z < refinedParent L epsilon z ∧
    refinedChild L epsilon z = (3 * refinedParent L epsilon z - 1) / 4 := by sorry

Source

https://github.com/Sodelin/Collatz-Conjecture-Work/blob/026aa4ad4be6453a005ab950b160a9f2204c5271/lean/CollatzWork/RefinedMersenneChild.lean#L128-L147

View graph