Exponential state complexity of nondeterministic complementation

The source is OpenAI's two-way complementation formalization: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/TwoWayAutomata/Main.lean

The public statements use the existing NMachine and ordinary Mathlib NFA. Acceptance here permits a zero-step run (positive = false). The bridge preserves the state count. The source's diagram argument also yields a lower bound through every letter-to-word encoding, independent of codeword lengths.

Combining that bound with the existing binary liveness scanner proves an exponential lower bound for the full complement of a small binary NFA's language. The encoded-word agreement is only the proof method; the binary result concerns a language of all finite binary words. These are checked consequences without any assertion that the source authors were unaware of them.

theorem Complexity.FiniteAutomaton.encoded_oneWayLiveness_complement_lower_bound {Alpha : Type} (h : ℕ) (hh : 2 ≤ h) (code : Alphabet h → List Alpha) (s : ℕ) (M : NMachine Alpha s) (hM : ∀ (w : List (Alphabet h)), M.Accepts false (List.flatMap code w) ↔ w ∉ oneWayLiveness h) : 2 ^ ((h - 2) / 127) ≤ 2 * (s + 1)

Any encoded-word recognizer for the complement of liveness needs exponentially many states, even with two-way nondeterminism and arbitrary codeword lengths.

theorem Complexity.FiniteAutomaton.livenessNFA_complement_lower_bound (h : ℕ) (hh : 2 ≤ h) (s : ℕ) (M : NMachine (Alphabet h) s) (hM : M.Recognizes false (livenessNFA h).acceptsᶜ) : 2 ^ ((h - 2) / 127) ≤ 2 * (s + 1)

The complement of the ordinary h-state liveness NFA requires exponentially many states in every two-way nondeterministic recognizer.

theorem Complexity.FiniteAutomaton.exists_oneWay_nfa_complementation_lower_bound (h : ℕ) (hh : 2 ≤ h) : ∃ (N : NMachine (Alphabet h) (h + 3)), N.NoLeft ∧ ∀ (s : ℕ) (M : NMachine (Alphabet h) s), (∀ (w : List (Alphabet h)), M.Accepts false w ↔ ¬N.Accepts false w) → 2 ^ ((h - 2) / 127) ≤ 2 * (s + 1)

Already a one-way endmarker automaton has an exponentially expensive complement when the complementing machine may use two-way nondeterminism.

theorem Complexity.FiniteAutomaton.binaryLivenessNFA_complement_lower_bound (n s : ℕ) (M : NMachine Bool s) (hM : M.Recognizes false (binaryLivenessNFA n).acceptsᶜ) : 2 ^ (n / 127) ≤ 2 * (s + 1)

The complement of the 9 * (n + 2)-state binary scanner requires an exponential number of states even in a two-way nondeterministic automaton.

theorem Complexity.FiniteAutomaton.no_binary_nfa_polynomial_complementation : ¬∃ (p : Polynomial ℝ), ∀ (Q : Type) [inst : Fintype Q] (A : NFA Bool Q), ∃ (s : ℕ) (M : NMachine Bool s), M.Recognizes false A.acceptsᶜ ∧ ↑s ≤ Polynomial.eval (↑(Fintype.card Q)) p

No polynomial in the source state count bounds complementation of ordinary binary NFAs by two-way NFAs, under zero-step finite-run acceptance.