Propagation of the mechanical envelope by twelve steps

Proved

CollatzWork.mechanical_twelve_propagation

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

Let $s\in\mathbb N$ and assume $4M(s)\le s3^s$ . Then

4M(s+12)\le(s+12)3^{s+12}.

A finite set of consecutive base cases can therefore cover every later index by residue modulo 12.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_BlockArithmetic
import Definitions.Def_CollatzWork_FloorPower
import Definitions.Def_CollatzWork_QuarterGapStatement
import Theorems.Thm_CollatzWork_blockNumerator12_exact_bound
import Theorems.Thm_CollatzWork_mechanical_twelve_identity

Formal statement

theorem CollatzWork.mechanical_twelve_propagation (s : Nat)
    (hstart : 4 * mechanicalMax s ≤ s * 3 ^ s) :
    4 * mechanicalMax (s + 12) ≤ (s + 12) * 3 ^ (s + 12) := by sorry

Source

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

View graph