Erdős 261 greedy carry: closed form for a block of doubling steps

Proved

Erdos261.doubling_block

by Ethan Cheung Wang · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

erdos-problemsnumber-theory

Let $g_j$ be the greedy carry for Erdős Problem 261 started at $(n,n)$ : $g_0=n$ , and $g_{j+1}=2g_j-(n+j+1)$ if $2g_j\ge n+j+1$ (a subtracting step), otherwise $g_{j+1}=2g_j$ (a doubling step). The greedy algorithm for $n/2^n=\sum a_k/2^{a_k}$ terminates iff some $g_j=0$ . Theorem. If steps $j,\dots,j+t-1$ are all doubling, then

g_{j+t}=2^t g_j.

Together with subtracting_block this gives the exact phase calculus of the greedy orbit: every phase acts by an explicit affine map, so termination after a fixed phase pattern is an exponential Diophantine condition.

Preamble

import Mathlib
import Definitions.Def_Erdos261_defs
open Finset

Formal statement

namespace Erdos261

theorem doubling_block (n j t : ℕ)
    (h : ∀ i < t, 2 * greedy n (j + i) < ((n + j + i + 1 : ℕ) : ℤ)) :
    greedy n (j + t) = 2 ^ t * greedy n j := by sorry

end Erdos261

Source

Erdős Problem 261 (https://www.erdosproblems.com/261); greedy carry as in Borwein–Loring 1990 / Tengely–Ulas–Zygadło 2020 (platform def Def_Erdos261_defs); (A.8) of claim from GPT 6.1 Sol (fourth answer, Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)

View graph