The two dyadic bins for a product

Proved

CollatzWork.floorPower_mul

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

collatz-work-import

Let $a,x,f,k\in\mathbb N$ satisfy $2^f\le a<2^{f+1}$ and $2^k\le x<2^{k+1}$ . Write $F(y)=2^{\lfloor\log_2 y\rfloor}$ for positive $y$ . Then

F(ax)=\begin{cases}2^{f+k}&ax<2^{f+k+1},\\2^{f+k+1}&ax\ge2^{f+k+1}.\end{cases}

This converts multiplication of dyadic floor powers into one exact threshold test.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_FloorPower

Formal statement

theorem CollatzWork.floorPower_mul {a x f k : Nat}
    (ha : 2 ^ f ≤ a) (ha' : a < 2 ^ (f + 1))
    (hx : 2 ^ k ≤ x) (hx' : x < 2 ^ (k + 1)) :
    floorPower (a * x) =
      if a * x < 2 ^ (f + 1) * 2 ^ k then 2 ^ f * 2 ^ k
      else 2 ^ (f + 1) * 2 ^ k := by sorry

Source

https://github.com/Sodelin/Collatz-Conjecture-Work/blob/026aa4ad4be6453a005ab950b160a9f2204c5271/lean/CollatzWork/FloorPower.lean#L7-L41

View graph