A fixed coprime denominator cannot recur forever

Proved

CollatzWork.noInfinitePositiveRecurrence

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

collatz-work-import

Let $a,b\in\mathbb N$ satisfy $\gcd(b,a)=1$ and $b>1$ , and let $y:\mathbb N\to\mathbb N$ satisfy $y_0>0$ . Then

\neg\bigl(\forall i\in\mathbb N,\ b y_{i+1}=a y_i\bigr).

This excludes an infinite sequence obeying this single recurrence, rather than arbitrary sequences of different affine blocks.

Preamble

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

Formal statement

theorem CollatzWork.noInfinitePositiveRecurrence : NoInfinitePositiveRecurrenceStatement := by sorry

Source

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

View graph