Complementary carry of the Erdős 261 greedy algorithm

Proved

Erdos261.compl_carry_step

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). Equivalently $(N,R)\mapsto(N+1,\,2R\bmod(N+1))$ with $N_j=n+j$ , $R_j=g_j$ ; the greedy algorithm terminates iff some $g_j=0$ . Theorem. Put $D_j=(n+j+2)-g_j$ . Then

D_{j+1}=\begin{cases}2D_j,&\text{step } j \text{ subtracting},\\ 2D_j-(n+j+1),&\text{step } j \text{ doubling}.\end{cases}

So on doubling runs $R=g$ doubles and on subtracting runs the complementary carry $D=N+2-R$ doubles.

Preamble

import Mathlib
import Definitions.Def_Erdos261_defs
open Finset

Formal statement

namespace Erdos261

theorem compl_carry_step (n j : ℕ) :
    ((n + (j + 1) + 2 : ℕ) : ℤ) - greedy n (j + 1) =
      if ((n + j + 1 : ℕ) : ℤ) ≤ 2 * greedy n j
      then 2 * (((n + j + 2 : ℕ) : ℤ) - greedy n j)
      else 2 * (((n + j + 2 : ℕ) : ℤ) - greedy n j) - ((n + j + 1 : ℕ) : ℤ) := 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); Claim A1 of claim from a GPT answer relayed by Ethan Cheung (third round, Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)

View graph