Prove2Me

Uniform coefficient margin for two burst lengths

Proved
CollatzWork.twoBurst_power_margin

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

collatz-work-import

For every j,l∈Nj,l\in\mathbb N,

3⋅9j+l+1+3⋅9l+10⋅8l2j+l+1<4⋅16j+l+1.3\cdot9^{j+l+1}+3\cdot9^l+10\cdot8^l2^{j+l+1}<4\cdot16^{j+l+1}.

This numerical inequality supplies slack for the guarded original-root comparison.

Preamble
import Std
import Init.Grind.Ordered.Module
Formal statement
theorem CollatzWork.twoBurst_power_margin (j l : Nat) :
    3 * 9 ^ (j + l + 1) + 3 * 9 ^ l +
        10 * 8 ^ l * 2 ^ (j + l + 1) < 4 * 16 ^ (j + l + 1) := by sorry
Source
https://github.com/Sodelin/Collatz-Conjecture-Work/blob/026aa4ad4be6453a005ab950b160a9f2204c5271/lean/CollatzWork/TwoBurst.lean#L40-L69

View graph