The state lower bound survives arbitrary word encodings

A consequence of OpenAI's crossing-diagram and relation-divisor argument: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata/Syntactic.lean

Replace each relation letter by a word over any target alphabet. Any two-way deterministic machine agreeing with one-way liveness on all encoded words still satisfies the original state lower bound, with exactly the same constants. The theorem imposes no bound on code lengths. Its behavior on other inputs does not enter the hypothesis. In particular, the theorem applies to every language extending the prescribed answers on encoded words.

The proof feeds the product of the encoded word's crossing diagrams into the source's representation theorem. This avoids the extra states of a simulation that explicitly stores the position within a codeword.

theorem Complexity.FiniteAutomaton.encoded_oneWayLiveness_lower_bound {Alpha : Type} (h : ℕ) (hh : 2 ≤ h) (code : Alphabet h → List Alpha) (positive : Bool) (s : ℕ) (D : DMachine Alpha s) (hD : ∀ (w : List (Alphabet h)), D.Accepts positive (List.flatMap code w) ↔ w ∈ oneWayLiveness h) : 2 ^ ((h - 2) / 31) ≤ 4 * (s + if positive = true then 2 else 1) ^ 2

The exact liveness state lower bound transfers through every letter-to-word encoding, independently of the alphabet and of the encoded word lengths.