Linear budget from an exponential return inequality

Proved

CollatzWork.prefixReturnNumericalBound

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

collatz-work-import

Let $n,d\in\mathbb N$ satisfy $2\cdot32^d<27^d(n+1)$ . Then

10d+27<27n,\qquad d\le\left\lfloor\frac{27n-28}{10}\right\rfloor.

The exponential inequality is an explicit premise; applications to any particular orbit must establish it separately.

Preamble

import Std
import Init.Grind.Ordered.Module
import Definitions.Def_CollatzWork_AffineRepetitionStatement
import Theorems.Thm_CollatzWork_prefixReturnBernoulli

Formal statement

theorem CollatzWork.prefixReturnNumericalBound : PrefixReturnNumericalBoundStatement := by sorry

Source

https://github.com/Sodelin/Collatz-Conjecture-Work/blob/026aa4ad4be6453a005ab950b160a9f2204c5271/lean/CollatzWork/AffineRepetition.lean#L83-L95

View graph