# Exponential state costs for two-way automata

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [An exponential state lower bound for two-way nondeterministic complementation](../../preprints/An-exponential-state-lower-bound-for-two-way-nondeterministic-complementation-September-25-2026/paper.pdf)
- [An exponential two-way deterministic state lower bound for one-way liveness](../../preprints/An-exponential-two-way-deterministic-state-lower-bound-for-one-way-liveness-September-25-2026/main.pdf)

## Scope

The paper asks how many states are needed to complement or determinize two-way nondeterministic finite automata. The formalization gives, for every $n\ge4$, an explicit $n$-state automaton whose complement requires at least $\tfrac12 2^{\lfloor(n-4)/127\rfloor}-1$ states. For the same family of relational languages and every $n\ge131$, every equivalent deterministic two-way automaton requires at least $\tfrac12 2^{\lfloor(n-4)/127\rfloor}$ states.

The alphabet grows with $n$, so neither complementation nor determinization has a polynomial state bound uniform over alphabets. The model has two endmarkers, left, right, and stay moves, and acceptance by a finite run. The separate results about one-way liveness and the Sakoda–Sipser problem are outside this scope.

The formalization gives a family of one-way nondeterministic automata with $h+3$ states whose languages require exponentially many states for two-way deterministic recognition. For every $h\ge2$, a deterministic recognizer with $s$ states satisfies $2^{\lfloor(h-2)/31\rfloor}\le4(s+2)^2$ under both acceptance conventions considered in the paper; one convention has the sharper factor $4(s+1)^2$. The alphabet may grow with $h$, so no alphabet-independent polynomial simulation bound holds.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Two-way nondeterministic complementation lower bound | [TwoWayComplementation.lean](../ComparatorChallenges/TwoWayComplementation.lean) |
| Same-family determinization lower bound | [TwoWayDeterminization.lean](../ComparatorChallenges/TwoWayDeterminization.lean) |
| Exponential deterministic state lower bound for liveness | [OneWayLiveness.lean](../ComparatorChallenges/OneWayLiveness.lean) |