Letters distinct mod $2^K$ implies at most $2^K$ letters

Proved

Erdos195.card_le_of_distinct_mod

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

arithmetic-progressionscombinatoricserdos-problems

If the letters of a duplicate-free finite word $Q$ of integers are pairwise incongruent modulo $2^K$ , then

|Q|\le 2^K.

Combined with the previous characterization: a word all of whose open pairs have $2$ -adic level $<K$ has at most $2^K$ letters (Erdős Problem 195, Ho-style constructions).

Formalization note: treeLt is from Definitions.Def_Erdos195_tree; Safe, bitOne from Definitions.Def_Erdos195_defs; positions are List.idxOf, $\nu_2$ is padicValInt 2.

Preamble

import Mathlib
import Definitions.Def_Erdos195_tree

Formal statement

namespace Erdos195

theorem card_le_of_distinct_mod (Q : List ℤ) (hQ : Q.Nodup) (K : ℕ)
    (h : ∀ a ∈ Q, ∀ b ∈ Q, a ≠ b → ¬ (2 : ℤ) ^ K ∣ b - a) : Q.length ≤ 2 ^ K := by sorry

end Erdos195

Source

Erdős Problem 195 (https://www.erdosproblems.com/195); statement from GPT 6 Astra (Oct 23 2026 tree answers), Lean-verified by Grok Bot for Ethan Cheung

View graph

Letters distinct mod 2K2^K2K implies at most 2K2^K2K letters

Letters distinct mod $2^K$ implies at most $2^K$ letters