A mechanical quarter certificate at every positive odd count

Proved

CollatzWork.universalMechanicalQuarterCertificate

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

collatz-work-import

For $s\in\mathbb N$ , define $M(0)=0$ , $M(s+1)=3M(s)+2^{\lfloor\log_2(3^s)\rfloor}$ , and $e(s)=\lfloor\log_2(3^s)\rfloor+1$ .

For every $s\in\mathbb N$ with $s\ge1$ ,

4M(s)\le s2^{e(s)}.

This numerical certificate supplies the hypothesis for the actual-orbit quarter-gap result.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_QuarterGapStatement
import Definitions.Def_CollatzWork_QuarterGapUniversalStatement
import Theorems.Thm_CollatzWork_mechanical_large_bound

Formal statement

theorem CollatzWork.universalMechanicalQuarterCertificate :
    UniversalMechanicalQuarterCertificateStatement := by sorry

Source

https://github.com/Sodelin/Collatz-Conjecture-Work/blob/026aa4ad4be6453a005ab950b160a9f2204c5271/lean/CollatzWork/QuarterGapUniversal.lean#L137-L145

View graph