Failure of the normalized mechanical envelope at index fifteen

Proved

CollatzWork.mechanical_fifteen_failure

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

At the single index $s=15$ ,

15\cdot3^{15}<4M(15).

Together with the separate theorem for all indices at least 16, this identifies the smallest eventual threshold. This theorem alone states only the failure at 15.

Preamble

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

Formal statement

set_option maxRecDepth 100000 in
set_option maxHeartbeats 0 in

theorem CollatzWork.mechanical_fifteen_failure : MechanicalFifteenFailureStatement := by sorry

Source

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

View graph