Prove2Me

Binary-carry characterisation of ∑j=1Ncj2N−j=0\sum_{j=1}^N c_j2^{N-j}=0

Proved
Erdos261.carry_iff

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

erdos-problemsnumber-theory

Theorem. For integers c1,…,cNc_1,\dots,c_N,

∑j=1Ncj 2N−j=0  ⟺  ∃ r1,…,rN+1∈Z: rN+1=0, r1=0, 2rj=cj+rj+1 (1≤j≤N).\sum_{j=1}^{N}c_j\,2^{N-j}=0\iff \exists\, r_1,\dots,r_{N+1}\in\mathbb Z:\ r_{N+1}=0,\ r_1=0,\ 2r_j=c_j+r_{j+1}\ (1\le j\le N).

This is the exact signed carry formulation of Erdős Problem 261 (applied with cj=j[j∈S]−n[j=n]c_j=j[j\in S]-n[j=n]): a representation is the same as a finite carry run that starts and ends at 00. No limiting process is involved.

Formalization Note. c,rc,r are functions N→Z\mathbb N\to\mathbb Z; only the values on [1,N+1][1,N+1] matter.

Preamble
import Mathlib
import Definitions.Def_Erdos261_defs
open Finset
Formal statement
namespace Erdos261

theorem carry_iff (N : ℕ) (c : ℕ → ℤ) :
    ∑ j ∈ Icc 1 N, c j * 2 ^ (N - j) = 0 ↔
      ∃ r : ℕ → ℤ, r (N + 1) = 0 ∧ r 1 = 0 ∧ ∀ j ∈ Icc 1 N, 2 * r j = c j + r (j + 1) := by sorry

end Erdos261
Source
Erdős Problem 261 (https://www.erdosproblems.com/261); definitions from Formal Conjectures 261.lean; Theorem A3 of GPT 6.1 Sol; lemma proposed by GPT 6.1 Sol (Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)

View graph