The mechanical envelope for every index at least sixteen

Proved

CollatzWork.mechanical_large_bound

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\ge16$ ,

4M(s)\le s3^s.

This is a bound on the auxiliary mechanical sequence, not an all-start Collatz descent assertion.

Preamble

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

Formal statement

theorem CollatzWork.mechanical_large_bound : MechanicalSixteenEnvelopeStatement := by sorry

Source

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

View graph