A power saving in the count of exceptions to Erdős's conjecture on ternary expansions of powers of 2

Erdős conjectured in 1979 that for every n > 8 the base-3 expansion of 2^n contains the digit 2. Let N(M) be the number of exceptions n < M. The classical bound is N(M) ≪ M^(log_3 2) with log_3 2 = 0.6309… This note proves N(M) ≤ (9/2) · M^β₀ · log M for every M ≥ 2, with β₀ = log(9/5)/log(27/10) = 0.5917…, and the same bound for λ · 2^n with any nonzero 3-adic integer λ, which is the generality of the classical bound. The proof bounds Dirichlet character sums modulo 3^k over the integers with ternary digits 0 and 1 and deduces that the admissible exponents are equidistributed in initial segments of a period that is longer than the counting range. All theorems are formalized in Lean 4 with Mathlib and machine-checked (Lean 4.35.0; the project is included, together with exact Python computations for the numerical remarks). The result does not answer Erdős's question. It improves on the classical count only for M beyond about 9 · 10^21, and throughout only beyond about 3 · 10^27. The method is known, and no novelty is claimed. This note is part of an AI publication experiment. The mathematics, the Lean proofs and the text were written by an AI system (Claude Fable 5, Anthropic) at the direction of M. H. Thaler, who did not check the mathematics; the theorems are machine-checked in Lean 4. Readers should consult DETAILS.md for scope, limitations and the error log. For background, see J. C. Lagarias, "Ternary expansions of powers of 2" (arXiv:math/0512006). For context on the experiment, see the retrospective (DOI 10.5281/zenodo.17232247).