Formalizing the 15-state Erdős powers-of-two machine (Stérin–Woods) #15

I'd like to add a machine for another conjecture: Erdős's conjecture that $2^n$ has at least
one digit $2$ in base $3$ for every $n > 8$ (Erdős, Some unconventional problems in number
theory, Math. Mag. 52 (1979)).

Stérin and Woods built a 15-state, 2-symbol machine that halts iff this conjecture fails
(arXiv:2107.12475; tables at
powers_of_two_15_2.txt and
powers_of_two_5_4.txt). It simulates
a 5-state, 4-symbol machine, which doubles a reverse-ternary number and counts the three
known exceptions $2^0, 2^2, 2^8$. Their correctness proof is on paper. As far as I can tell
there is no Lean proof yet. Formal Conjectures has the statement with a TODO for the machine
version (FormalConjectures/Arxiv/2107.12475/CollatzLike.lean).

Plan, following the Goldbach files:

• artifacts/erdos_15/machine.txt (relabelled so the start state and blank are 0), with the
  upstream table kept verbatim in baselines/ and its provenance recorded;
• a proof of Halts candidate ↔ ∃ n, 8 < n ∧ 2 ∉ Nat.digits 3 (2 ^ n), aiming for
  propext and Quot.sound only, plus the ¬ ∀ n > 8, … form in Semantics/;
• the matching Challenge.lean statement, comparator config, verify.py entry and docs.

Later I may also look for a machine with fewer states, but that is not part of this.

Three questions before I start:

1. Is that statement form fine, or would you prefer a different definition in
   Propositions.lean?
2. Is it OK to state the 4-symbol machine as a helper (Machine 5 4) and prove the 15-state
   machine simulates it, or would you rather the proof be about the 15-state machine only?
3. Any naming you'd like (erdos_15, ErdosPowersOfTwo, …)?

If someone is already working on this, let me know and I'll pick something else.

AI-usage disclosure: Claude (Anthropic) was used as assistant.