One-Way Liveness: OpenAI’s Proof That Rereading Cannot Save Exponential States

Give a finite automaton permission to walk back and forth across its input, and it can revisit a choice point as often as it likes. Can that freedom make up for losing nondeterminism? OpenAI’s one-way liveness preprint gives a family for which the answer is no. A nondeterministic machine can recognize the language with $h+3$ states and no left moves, while every equivalent two-way deterministic machine needs exponentially many states in $h$, the number of points underlying each relation. The alphabet is finite for each $h$ and grows with it. The proof turns repeated head motion into products of matching diagrams, then shows that a small diagram cannot preserve everything those relation products can reveal.

1. One-Way Liveness and the 1978 Sakoda–Sipser Problem

Sakoda and Sipser asked how many states it takes to replace nondeterminism with a two-way deterministic finite automaton. The machines recognize regular languages, so the issue is how compactly they can describe the same language. A nondeterministic machine accepts when at least one permitted computation succeeds. A deterministic machine follows a single computation from its initial configuration, with one read-only head and one finite control state at each step.

One-way liveness is the witness family that Sakoda and Sipser showed to be complete for the one-way-source version of the conversion problem. OpenAI’s September 25, 2026 preprint uses this family to prove a lower bound even when the target can reverse anywhere on the input. For another example of separating computational models by their resources, see Binary Verse AI’s coverage of time–space tradeoffs for Turing machines.

2. How One-Way Liveness Works With Binary Relations and Surviving Paths

Write $H=[h]=\{1,\ldots,h\}$ for the point set and $\mathcal{R}_H$ for its binary relation monoid. Each input letter is one subset of $H\times H$. The product is read in path order. If $A$ precedes $B$, a pair $(x,z)$ belongs to $AB$ when some intermediate point $y$ connects the first step $(x,y)\in A$ to the second step $(y,z)\in B$. The operation is associative. Its identity $I_H$ consists of all self-pairs, and $0$ denotes the empty relation.

Here the star denotes all finite words over the relation alphabet, and $\ell$ is the word length. The empty word has product $I_H$ and is accepted. For three points, let $A$ contain the pairs 1 to 2 and 2 to 3, and let $B$ contain only 2 to 3. Only the route $1\to2\to3$ survives both letters, giving $AB=\{(1,\,3)\}$. Reversing the letters gives $BA=0$, since the first step ends at point 3 and the next letter has no outgoing pair there. The question is whether a path crosses every layer.

3. Why a One-Way Nondeterministic Automaton Needs Only Three Extra States

The source automaton uses one state for each point and three more for initialization, acceptance, and rejection. On the left endmarker it moves right into any point state. At a relation letter, it can advance right into any point linked from the current one. If there is no such point, that branch enters the rejecting state with a stay move. A branch that reaches the right endmarker in a point state enters the accepting state with a stay move.

In the example above, the branch starting at point 1 advances to 2, then to 3, and accepts at the marker. The branch starting at point 2 advances to 3 on the first letter and then fails. The initial state handles the choice of starting point even for empty input, where the first right move goes directly to the right endmarker. Each branch tracks a single endpoint. A deterministic one-way machine can track the entire set of reachable endpoints, giving a state upper bound of exponential order.

4. The Previous Quadratic Bound and Why It Was Not Enough

Earlier exponential separations constrained the target’s head. In Sipser’s sweeping model, the machine can reverse only at an endmarker. Kapoutsis obtained an exponential separation with sublinearly many reversals as a function of input length. An unrestricted target may reverse at interior cells and make arbitrarily many reversals as inputs grow.

Chrobak had shown a quadratic lower bound for unrestricted deterministic two-way targets using unary languages. In 2026, Kehinde Adeogun and Christos Kapoutsis established an $\Omega(h^2)$ lower bound for unrestricted 2DFAs recognizing one-way liveness. Kapoutsis had also determined the optimal order $\Theta(h^2/\log h)$ under the promise of exactly three relation letters. That promise limits word length while keeping the full relation alphabet. The new result applies at every word length. Related Binary Verse AI coverage examines the dependence of Weisfeiler–Leman complexity on the computational task being measured.

5. OpenAI’s Exponential State Lower Bound and the Exact Theorem

Theorem 1.1 gives a nondeterministic recognizer with $h+3$ states and no left moves for every integer $h\ge2$. If an equivalent two-way deterministic automaton has $s$ states, the theorem gives the following inequality.

The floor rounds down. Taking a square root and solving for the state count gives the explicit lower bound below.

Because $s$ counts states, any fractional lower bound can be rounded up. The estimate is asymptotically $2^{\Omega(h)}$, although the explicit inequality can be weak for small $h$. The target has a single head, begins at the left endmarker, and respects both boundaries. Stay moves and partial transition rules are allowed. A computation that runs forever without accepting rejects. When the initial configuration itself can count as accepting, the theorem strengthens the left side to $4(s+1)^2$.

6. Why Rereading the Input Cannot Replace Nondeterministic Choices Cheaply

Rereading lets the deterministic head use its position and the symbols it encounters as part of the computation. A proof that simply counts what the machine remembers after a single pass would miss that advantage. OpenAI instead summarizes what a block of input can do when surrounded by other letters. The summary comes from the machine’s configuration graph and accounts for visits from either side.

The language answers one yes-or-no question, but a block’s full relation product can matter later. A context can force the block to start at one particular point and finish at another. If the block summary loses the corresponding entry, the machine cannot distinguish those surrounded inputs. The 1NFA to 2DFA state complexity argument therefore needs a representation that preserves relation products under concatenation.

7. From Two-Way Computations to Trees and Local Matching Diagrams

A configuration consists of a state and a cell position. OpenAI redirects accepting configurations into a new state that moves right to a designated sink at the right endmarker. In the undirected successor graph, the sink component consists exactly of the configurations that reach the sink. Each other vertex in that component has one outgoing successor there, so the connected component has one fewer edge than vertices and is a tree.

A doubled tour traverses each tree edge in both directions. At each vertex, it leaves by the incidence following the one on which it arrived in a fixed cyclic order. The tree produces a single tour. Attach test leaves at the initial configuration and at the sink. In the accepting case, opening the tour at those leaves gives two paths connecting the outer left and right test ports.

For the construction to work letter by letter, the wires at a cell boundary must have the same labels regardless of its neighbors. Reserve a slot for every crossing direction and ordered pair of source and target states. The target end always attaches to its designated state. The source attaches to its own state only for the actual transition and uses a separate fresh leaf otherwise. Stay edges remain within a cell. Two travel lanes per slot give $4N^2$ ports on each side for $N$ normalized states. Contracting internal paths gives a fixed matching for each symbol, including each endmarker. On rejection the two test leaves lie in separate components, so no wire can connect a left test port to a right one. Cycles elsewhere in the graph cannot change this test.

8. Brauer Diagram Monoids, Rank, Support, and Idempotent Corners

A Brauer diagram monoid $D_m$ consists of perfect matchings on $m$ left and $m$ right ports. Multiply by gluing equally indexed ports along the shared boundary and pairing the remaining endpoints along the resulting paths. Internal cycles can be discarded. The rank counts pairs crossing from left to right, and multiplication cannot increase it. The support records the indices where a diagram fails to join a left port directly to its corresponding right port.

An idempotent $e$ satisfies $e^2=e$. The corner $eD_m e$ uses $e$ as its identity. When $e$ has rank $r$, deleting its prescribed outer same-side pairs and renumbering the remaining ports gives a rank-preserving embedding into $D_r$. The renumbering follows the cross pairs of $e$, so they become the identity wires in the smaller diagram. Lemma 2.2 also gives two controls. An idempotent of rank $r$ has support at most $2(m-r)$, and a family with one common support set still has a common set of no larger size after sandwiching and reduction. The latter control keeps the next construction within one port budget.

9. The Key Construction With 32 Conjugates and 256 Relation Additions

Start with an idempotent diagram $a$ that represents the identity relation plus a single off-diagonal pair. Let $c=m-\operatorname{rank}(a)$ be its rank loss. Pick disjoint sets $U$ and $V$ of 16 points each and a separate point $z$. The proof uses permutation-diagram conjugation to produce 16 copies representing an extra edge $u_i\to z$ and 16 representing $z\to v_j$. These copies all have the same rank as $a$.

Multiplying one copy from each family yields a route from $u_i$ through $z$ to $v_j$. Sandwich the product using a lift of the partial identity on $H\setminus\{z\}$. The outer relations remove pairs with endpoint $z$, leaving that partial identity and one extra pair $(u_i,v_j)$. The same 32 conjugates supply all 256 pair choices. Since $U$ and $V$ are disjoint, two added edges cannot compose. Successive additions therefore accumulate by union, with no unintended pairs. The lifted chain uses idempotent powers to preserve those relation images and nest the diagram corners.

10. How the Rank-Loss Induction Produces an Exponential Bound

Let $\Delta_\ell$ be the decrease in rank at addition $\ell$, and write $L$ for the inductive lower bound on rank loss. All 32 conjugates together touch at most $64c$ indices, and reduction at the starting partial-identity lift preserves that common support budget. The rank decreases telescope, so this also caps the sum of the losses across the chain.

At each step, retain the two endpoints of the pair about to be added and every point outside $U\cup V\cup\{z\}$. This leaves $h-31$ points. The previous relation restricts to the identity there because the selected pair is still absent. Lemma 2.4 identifies a corner with the full relation monoid on those points. Choosing a minimum-rank idempotent lift gives permutation lifts in the reduced diagram corner. A suitable power of a permutation lift reaches an idempotent over the corner identity. If the lift had already lost rank, that idempotent would contradict the minimum-rank choice. The addition gives one extra pair on the smaller set. Its reduced diagram lift has support at most $2\Delta_\ell$.

The induction applies on that smaller set. Summing the 256 step bounds gives the comparison below.

For $2\le h<33$, the required loss is at least one because an idempotent of full rank is the identity and cannot represent the added pair under a unital map. For $h\ge33$, the comparison forces $c\ge2L(h-31)$. The resulting lower bound doubles every 31 points.

11. Context Separation Turns Diagram Products Into the Final Lower Bound

Let $d(w)$ be the diagram product of the body letters of a word $w$ and $r(w)$ its relation product. If two words have equal diagram products, the machine gives the same answer in every surrounding context, by associativity and the fixed endmarker diagrams. Suppose their relation products differ at entry $(i,j)$. Prepend the singleton identity relation $I_{\{i\}}$ and append $I_{\{j\}}$. These letters keep precisely that entry when present. Exactly one surrounded word would be accepted, contradicting equality of the diagrams.

Thus the map sending $d(w)$ to $r(w)$ is well-defined and preserves products and identity. It is onto the full binary relation monoid because every relation is available as one letter. Corollary 3.2 uses a minimum-rank corner to obtain permutation lifts and applies the rank-loss bound there. Its lower bound on the diagram degree $k$, combined with the representation in Theorem 4.1, gives $L(h)\le k\le4(s+2)^2$. Proposition 5.1 supplies the small nondeterministic recognizer and completes the separation.

12. What the Proof Establishes, What Lean Checks, and What Remains Open

There are $2^{h^2}$ relation letters, since each of the $h^2$ ordered pairs can independently be present or absent. With $n=h+3$ source states, the lower bound rules out a polynomial state bound uniform over all finite alphabets, even for sources with no left moves. The result leaves the fixed-alphabet determinization question open and measures finite control states. Transition-table size and running time are separate measures.

OpenAI’s math release and the Lean scope notes for family 129 distinguish the liveness theorem from the companion work on complementation. The liveness formalization covers the small source and the deterministic bound under both acceptance conventions, including the sharper bound when an accepting initial configuration counts. The Lean comparator states the target theorem, while the Lean implementation combines the small automaton construction with the deterministic lower bound and formalizes the consequence for polynomial simulation.

One-way liveness gives a concrete reason why revisiting input can leave a deterministic machine exponentially larger. A word that looks like a single yes-or-no test can be surrounded by letters that expose any entry of its relation product, and the machine has to preserve all those distinctions. Follow Binary Verse AI for research explainers on Boolean circuit lower bounds, the Exponential Time Hypothesis, and PCP for PPAD.