Integral Bernoulli bound for the ratio 32 over 27

Proved

CollatzWork.prefixReturnBernoulli

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

collatz-work-import

For every $d\in\mathbb N$ ,

(27+5d)27^d\le27\cdot32^d.

This is a denominator-cleared Bernoulli estimate used in conditional repetition budgets.

Preamble

import Std
import Init.Grind.Ordered.Module

Formal statement

theorem CollatzWork.prefixReturnBernoulli (d : Nat) :
    (27 + 5 * d) * 27 ^ d ≤ 27 * 32 ^ d := by sorry

Source