A fixed binary alphabet still requires exponentially many deterministic states

A consequence of OpenAI's one-way-liveness lower bound and its crossing-diagram proof, combined with the binary scanner constructed here. The full language of the NFA has a two-way deterministic lower bound; this is not a promise problem.

Source: https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata

theorem Complexity.FiniteAutomaton.card_binaryLivenessState (n : ℕ) : Fintype.card (BinaryLivenessState n) = 9 * (n + 2)

The binary scanner uses nine states per original liveness vertex.

theorem Complexity.FiniteAutomaton.binaryLivenessNFA_accepts_code (n : ℕ) (w : List (Alphabet (n + 2))) : List.flatMap binaryLivenessCode w ∈ (binaryLivenessNFA n).accepts ↔ w ∈ oneWayLiveness (n + 2)

On encoded relation words the binary NFA accepts exactly one-way liveness.

theorem Complexity.FiniteAutomaton.binaryLivenessNFA_deterministic_lower_bound (n : ℕ) (positive : Bool) (s : ℕ) (D : DMachine Bool s) (hD : D.Recognizes positive (binaryLivenessNFA n).accepts) : 2 ^ (n / 31) ≤ 4 * (s + if positive = true then 2 else 1) ^ 2

Every equivalent two-way deterministic recognizer has exponential state cost, even though the alphabet is the fixed two-element type Bool.