Exact twelve-step recurrence of the mechanical envelope

Proved

CollatzWork.mechanical_twelve_identity

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 $B,x\in\mathbb N$ , define the normalized twelve-term numerator $N_{12}(B,x)=\sum_{i=0}^{11}3^{11-i}D_i(B,x)$ . Here $f_i=\lfloor\log_2(3^i)\rfloor$ , and $D_i(B,x)$ is $2^{f_i}B$ when $3^i x<2^{f_i+1}B$ , and $2^{f_i+1}B$ otherwise.

For every $s\in\mathbb N$ ,

M(s+12)=3^{12}M(s)+N_{12}\bigl(2^{\lfloor\log_2(3^s)\rfloor},3^s\bigr).

This groups twelve scalar recurrence steps while preserving all dyadic rounding phases.

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_floorPower_mul

Formal statement

theorem CollatzWork.mechanical_twelve_identity (s : Nat) :
    mechanicalMax (s + 12) = 531441 * mechanicalMax s +
      blockNumerator12 (floorPower (3 ^ s)) (3 ^ s) := by sorry

Source

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

View graph