Erdős similarity for distance sets: finite patterns, a pinned obstruction, and an open window

For a compact set E ⊂ ℝ^d let Δ(E) = {|x − y| : x, y ∈ E} be its distance set. We ask whether, for d ≥ 2 and dim_H E > d/2, the distance set must contain a nontrivial affine copy x + s{2^(−n) : n ≥ 1} of the dyadic sequence, a distance-set version of the Erdős similarity problem. We combine two recent results announced by OpenAI: the Falconer distance theorem in all dimensions and the dyadic case of the Erdős similarity conjecture. Assuming these, we show: (A) Δ(E) contains affine copies of every finite set, for a positive-measure family of translations at every small scale. (B) For every d ≥ 1 there is a compact set K ∋ 0 of nearly full volume in the unit ball of ℝ^d whose distance set from the origin contains no affine copy of the dyadic sequence, while Δ(K) does contain one and, for d ≥ 2, so does the distance set from every other point. (C) A counterexample must have Δ(E) of positive measure but empty interior, so by the Mattila–Sjölin theorem the question is open exactly for d/2 < dim_H E ≤ (d+1)/2. A positive answer would follow if Δ(E) had nonempty interior in this range, itself an open problem; a negative answer would, to our knowledge, give the first sets of dimension > d/2 whose distance sets have empty interior. Every lemma, proposition and theorem of this note has a Lean 4 proof with Mathlib. The OpenAI results and the Mattila–Sjölin theorem enter as explicit hypotheses, and we checked with the Lean kernel that OpenAI's Lean proofs and a separate formalization of the Mattila–Sjölin theorem prove exactly these hypotheses. So Theorems A and B, Proposition C and the window are machine-checked down to the standard axioms. The spherical maximal theorem, which is not formalized, is used only in one clearly marked remark. Lean 4 formalization, paper source and verification scripts: https://github.com/haraldschilly/math-distance-set-similarity (commit 31317f2). The Mattila–Sjölin theorem is formalized in https://github.com/haraldschilly/math-mattila-sjolin. Use of AI: this note builds on AI-generated results released by OpenAI (https://github.com/openai/math). It was prepared with substantial assistance from Claude (Anthropic), including the Lean formalization.