Source and verification

This article explains family 129 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

🏷️ Finite automata and relation products

A two-way finite automaton reads a word between two endmarkers. Its memory consists of a state and the position of one read-only head. Each transition changes the state and moves the head left, right, or not at all. A deterministic machine has at most one successor from each state-symbol pair; a nondeterministic machine may choose among several. A word is accepted if some finite computation reaches an accepting state. An infinite computation that never accepts does not accept.

The resource studied here is the number of states, including initial and accepting states. Neither input length nor computation time is bounded. There are no writable cells, extra heads, random bits, or advice.

Let , with . A binary relation on is a set of directed edges between two copies of . Compose relations in path order:

Use the collection of all relations on as an alphabet. A word describes a layered directed graph, and its product records which initial vertices can reach which final vertices. Define the one-way liveness language

The empty product is the identity relation , so the empty word belongs to .

For example, with , take and . Then , so is live, whereas has empty product. Individual nonempty letters need not form a live word.

A small nondeterministic recognizer guesses an initial vertex and then a path through the layers. It uses path states, an initial state, and an accepting state. At a relation letter it follows one allowed edge; at the right marker it accepts. Missing transitions reject the current branch. Thus states suffice, without any left moves. Adding an explicit rejecting sink gives the companion paper’s -state construction. (OpenAI, 2026) (OpenAI, 2026b)

🏷️ Two exponential state bounds

Complementation and determinization, as stated in the manuscripts

Every two-way nondeterministic recognizer of the complement of has at least

states. Independently, every deterministic two-way recognizer of , with states, satisfies

When an accepting initial configuration counts as acceptance, the second bound improves to on the left. (OpenAI, 2026a) (OpenAI, 2026b)

The first theorem says that even a nondeterministic machine cannot recognize absence of a path with polynomially many states in this family. The second concerns deterministic recognition of the original path-existence language and gives a stronger exponential rate for that task.

There are alphabet symbols. These conclusions exclude polynomial state bounds whose constants are independent of the finite alphabet. They do not establish the same bounds over one fixed alphabet, and they are not lower bounds in terms of transition-table description length. Nor do they separate uniform logarithmic-space complexity classes: the parameter and computational model are different.

Complementing a deterministic machine also requires care. Exchanging accepting and rejecting states does not handle an infinite nonaccepting computation. The complementation paper invokes a separate linear-state deterministic complementation theorem that handles this issue; the companion’s direct proof avoids relying on that consequence for its sharper bound.

🏷️ Boundary summaries and context tests

A two-way computation may cross a cut many times. Recording only the state on its first crossing therefore loses information. The complementation paper instead summarizes an interval by four relations:

  • entries from the left that can exit on the right;
  • entries from the right that can exit on the left;
  • entries from the left that can return to the left;
  • entries from the right that can return to the right.

Boundary labels contain a state and a direction. Gluing two interval diagrams permits arbitrary finite alternation across the shared boundary. This gives an associative composition because expanding or contracting interval paths preserves finite reachability. Adding edges to a diagram can only add possible computations.

Stay moves are included exactly: inside a cell, take any finite sequence of stay transitions, followed by an exit move. An auxiliary success state turns acceptance into a designated rightward exit. This representation uses labels in each direction for an -state machine. It preserves finite acceptance even when other branches loop indefinitely. (OpenAI, 2026a)

The full relation alphabet provides particularly strong tests. Put . For any relation ,

Thus placing two singleton letters around a word tests any chosen entry of its relation product.

Suppose two words have the same computation diagram. Every surrounding context then produces the same acceptance decision. If their relation products differed, a singleton context would distinguish them. Consequently, the relation product is a well-defined function of the diagram. Every relation occurs as a one-letter word, so this function reaches all relations and respects concatenation.

For a machine recognizing emptiness, there is more information. Write when each boundary relation of the first diagram is contained in that of the second. If is absent from , the emptiness machine accepts . Monotonicity of diagram paths implies acceptance of , so is absent from as well. Therefore

This reversal of inclusion is the precise input to the paper’s finite-diagram lower bound. Counting all possible diagrams would not establish the needed exponential number of boundary labels.

🏷️ Amplifying a loss of boundary information

The remaining complementation argument is a structural theorem about these finite path diagrams. Its conclusion is that an inclusion-reversing representation of all relations on points, with labels in each direction, must satisfy

Substituting yields the first automata bound.

The mechanism tracks recurrent classes of boundary labels under a diagram that is unchanged by composition with itself. Restricting attention to diagrams stabilized on both sides by that diagram creates a smaller setting in which the induction can continue. Some operations destroy loops on recurrent classes; those lost classes form a finite budget.

Two estimates are essential. Transport through a fixed surrounding context increases a common loss budget by at most a constant factor. Along a nested sequence of such restrictions, the sum of the successive losses is also controlled by one initial budget. Without the latter estimate, the same destroyed information could be charged afresh at every stage.

The amplification arranges relabeled copies of one relation modification so that they induce additions. Each addition contains a smaller instance of the original representation problem. With , comparing the total required loss with the shared budget produces the exponential recurrence and the decrement in . These transport and nested-loss estimates are substantive source theorems; the elementary context argument alone does not prove them. (OpenAI, 2026a)

🏷️ Deterministic computations as matching diagrams

The deterministic companion uses perfect matchings between boundary ports rather than four arbitrary reachability relations. The reason determinism helps is a simple fact about a finite directed graph in which every vertex has at most one successor.

Sink component lemma

If has no successor, its connected component in the underlying undirected multigraph consists exactly of the vertices whose successor paths reach . That component is a tree.

To prove this, let be the set of vertices reaching . Along any successor edge , membership in is equivalent at the two endpoints. Hence is the component of . Every vertex there except has exactly one outgoing edge, so the connected component with vertices has edges and is a tree. Nonaccepting cycles lie elsewhere.

After routing acceptance to a designated sink, a tour of this tree can encode acceptance by whether two test ports are connected. Choose a cyclic ordering of incidences at each vertex; on arriving along an edge, leave along the next incidence. On a tree this visits each directed edge traversal in one cycle. Removing a leaf and then reinserting its out-and-back excursion proves the assertion inductively. Cutting the tour at two designated leaves gives two paths connecting the cuts.

A further issue is locality: the diagram assigned to a letter must not depend on its neighbors. The construction reserves a slot for each direction and ordered pair of states. The target end of a slot always attaches to the designated target state. At the source end, an actual transition attaches to its source state; an unused candidate attaches to its own separate leaf. This changes neither connectivity between state vertices nor the sink-tree property. Two lanes per slot give boundary ports. (OpenAI, 2026b)

Singleton contexts again imply that the generated matching diagrams represent every relation product faithfully. The companion’s structural theorem then forces at least ports.

Here the loss variable is matching rank: the number of pairs joining opposite boundaries. Restriction to an idempotent diagram of rank reduces the problem to ports, with control of one common support set. The amplification uses relabeled diagrams to generate relation additions; each addition contains a problem on points. The common support budget prevents these additions from being paid for independently. This gives the second exponential recurrence. Its finite-diagram proof is distinct from the nondeterministic recurrent-class argument.

🏷️ Key steps and proof outlines

A relation alphabet makes contextual tests exact

Let be an -element set, and regard each input letter as a binary relation on . The product of a word records all possible paths through its letters. For , write . Then is nonempty exactly when . Thus every individual entry of a relation can be tested by a left and right context. This elementary observation prevents a boundary summary from identifying two relations merely because they agree on the current acceptance test.

For a nondeterministic complementing machine, enlarging its boundary reachability diagram can only add accepting paths. Since acceptance here means that the original relation product is empty, the induced relation map reverses inclusion: more boundary paths must correspond to fewer surviving relation pairs. The lower bound consequently needs an order-reversing diagram theorem, not a bound on the number of arbitrary summaries. Deterministic machines instead yield matching diagrams with a rank invariant. These are distinct structural inputs even though the amplification pattern is shared. (OpenAI, 2026a; OpenAI, 2026b)

Amplifying one defect through a hub

Here is the quantitative mechanism in β€œAn exponential bound for order-reversing images.” For an idempotent boundary diagram , its recurrent classes are the persistent components under repeated composition. Write for the classes missing after inserting a diagram , and let when its relation image is the identity plus one off-diagonal pair. The proof seeks a lower bound on .

Choose disjoint sets and and a hub . Relabeling the original pair supplies diagrams whose relation images add or . Multiplying one of each and restricting away from gives a diagram adding exactly . Thus only initial defects generate distinguishable additions.

The common-set transport lemma charges all these operations to one missing-class set, rather than charging the same class separately at every step. After transport its size is at most . Enumerate the pairs and successively add them, taking idempotent powers after each insertion. No new two-step paths are created among these added edges because . If is the loss at the th nested step, the chain inequality gives

Every step contains a smaller hard instance

To lower-bound a particular , retain only the newly added pair’s two endpoints and the points outside . The retained set has elements. Before this step, its restricted relation is the identity; after the step, it contains the chosen additional pair. The restricted diagrams must still represent all relations on the smaller set, or induction would not apply.

The source ensures this by taking a minimal idempotent preimage of the restricted identity. Sandwiching by that idempotent produces a smaller domain with the correct identity and a surjective relation map. A finite-power argument supplies invertible lifts of relabelings: an element mapping to an invertible relation has an idempotent power, and minimality forces that power to be the domain identity. This verifies the symmetry hypothesis again inside the restricted problem.

Transport into this smaller domain loses at most a factor two. If is the inductive lower bound, then . Combining all steps yields

Taking gives , with base value one, hence . Since a width- diagram has at most recurrent classes, , which converts to the stated state lower bound. The exponential growth comes from quadratic amplification against a linear shared budget.

Why the deterministic exponent is different

The deterministic companion uses the same hub construction with , but measures rank loss rather than missing recurrent classes. Its shared support budget is , while each of the additions costs at least half the smaller-instance bound . Therefore and . The separate machine-to-matching construction has width bounded by for an -state machine, giving the quadratic prefactor in its final inequality. Neither the improved decrement nor that width conversion can be transferred automatically to the nondeterministic proof. (OpenAI, 2026b)

🏷️ Reading connections

Depth-three circuit lower bounds studies a different restricted computational resource: gates rather than finite states. The common lesson is to specify the allowed computations before comparing lower bounds. The constructions here allow unlimited head motion and computation time while keeping finite control small.

🏷️ Manuscripts and verification scope

The family scope page describes selected formalization coverage. Its comparator list covers both the nondeterministic complementation bound and the direct liveness determinization bound, with their distinct state offsets and growing-alphabet conventions. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026a. An exponential state lower bound for two-way nondeterministic complementation.
🐻  OpenAI 2026b. An exponential two-way deterministic state lower bound for one-way liveness.