Exclusion of an infinitely repeated affine block

Proved

CollatzWork.noInfiniteExpandingAffineBlocks

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

collatz-work-import

Let $b,d,c\in\mathbb N$ with $\gcd(b,b+d)=1$ and $b>1$ , and let $x:\mathbb N\to\mathbb N$ satisfy $d x_0+c>0$ . Then

\neg\bigl(\forall i\in\mathbb N,\ b x_{i+1}=(b+d)x_i+c\bigr).

Only the displayed fixed block is excluded; this does not exclude every nonconvergent Collatz itinerary.

Preamble

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

Formal statement

theorem CollatzWork.noInfiniteExpandingAffineBlocks : NoInfiniteExpandingAffineBlocksStatement := by sorry

Source

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

View graph