Generalized Star Height Problem: How OpenAI’s Two-Split Proof Sets a Three-Level Ceiling

A regular language can require arbitrarily deep repetition in an ordinary regular expression. Add complement, and OpenAI’s September 25, 2026 manuscript gives every regular language a three-level ceiling. Its answer to the Generalized Star Height Problem is a uniform upper bound over the original alphabet, not a proof that three levels are necessary. Whether one level always suffices remains unresolved by this paper.

The mechanism is unusually concrete: split words into episodes, let independent prefix and suffix tests propose information, and make every successful pairing transmit the correct computation. Two split constructions handle both ordinary episodes and their exceptions. The challenge is making disagreement safe without secretly giving either test access to the other’s letters.

1. What Is the Generalized Star Height Problem?

A generalized regular expression builds languages from the empty language, the empty word, and individual letters using union, concatenation, complement, and Kleene star. A star permits any finite number of repetitions, including none. Generalized star height counts the deepest nesting of stars. Union and concatenation take the maximum of their operands’ heights; complement preserves height.

Fix a finite alphabet $\Sigma$. Complement means complement inside $\Sigma^*$, the set of all finite words over that alphabet. Write $h_\Sigma(L)$ for the least height among expressions describing language $L$. The same language can have many expressions, so counting stars in one convenient expression does not establish its minimum.

For example, $\Sigma^*=\neg\emptyset$ has height zero. Over the one-letter alphabet, $(aa)^*$ describes even-length words and has height exactly one: unary star-free languages are finite or cofinite, whereas even-length words are neither. Infinite therefore does not mean star-requiring, but parity does.

2. Why the Original Star-Height Problem Resisted a Solution

Ordinary star height, which forbids complement, is unbounded even over two letters. Its lower-bound techniques constrain a narrower expression language. Adding Boolean negation changes what an expression can say, so those arguments cannot simply be carried across.

The classical algebraic dividing line is useful here. Star-free languages are exactly those recognized by finite aperiodic monoids. Aperiodicity means that powers of each element eventually stabilize, rather than continuing around a nontrivial cycle. This links an expression restriction to a property of its finite recognizing algebra.

Earlier generalized height-one results covered substantial but restricted families, including languages recognized by certain groups and languages counting occurrences of a fixed factor modulo an integer. They did not cover every regular language. The manuscript’s historical discussion distinguishes universal boundedness from the stronger height-one possibility. Confusing those questions would erase the central qualification of the new result.

3. OpenAI’s Proof: Every Regular Language Has Star Height at Most Three

Theorem 1.1 of Generalized Star Height at Most Three states:

The bound is independent of the automaton’s size and the finite alphabet. Expression lengths and construction parameters can still depend on the language. A ceiling on one measure says nothing automatic about another, a distinction also central to our permanent versus determinant explainer.

Two companion manuscripts give independent constructions with bounds thirteen and four. This proof does not assume either numerical theorem. OpenAI included the work in its October mathematics release. This article explains the manuscript’s argument, without presenting publication or repository documentation as an independent correctness audit.

4. Turning Regular Languages Into Finite Monoid Computations

A finite automaton induces a finite monoid $M$ of state transformations. A morphism $T:\Sigma^*\to M$ sends each word to its transformation, preserving concatenation. Membership in a recognized language depends only on this value. It therefore suffices to describe each fiber $T^{-1}(m)$, the words mapped to a particular monoid element.

For positions $a\leq b\leq c$, interval products obey $T_{a,c}=T_{a,b}T_{b,c}$, in reading order. The proof represents these products on the finite vector space $V=\mathbb F_2^M$, with basis vectors indexed by monoid elements. Right multiplication sends $e_m$ to $e_{md}$. Acting on the identity basis vector reveals $d$, so this representation loses no information.

This is finite-state computation, not arbitrary Turing-machine execution. Our Turing-complete fluid computation analysis illustrates the stronger kind of universality that is absent here. The present reduction is powerful because every regular language already has a finite recognizing algebra.

5. Prefix-Code Episodes and the Split Identity

The word is parsed into complete episodes from a prefix code $E$: no episode is a proper prefix of another. Consequently, episode boundaries are unique. Each episode has a deterministic total state update $G_e$. Prefix language $P_x$ tests an input state, and suffix language $Q_y$ tests an output state.

Lemma 2.1 requires two different guarantees. Soundness says every successful pair starting at a true boundary consumes exactly the next episode and satisfies $G_e(x)=y$. Completeness says a pair exists for every input on every episode outside a designated skipped class. Merely exhibiting one good pairing would leave incorrect independent guesses unchecked.

Graph languages for runs of skipped episodes fill the gaps between successful pairs. The split identity joins these runs and pairs with concatenation, union, intersection, and one middle star. If component tests have height at most one and skipped computations have height at most H, then:

The domain’s own star costs at most two levels. The middle star adds one above the skipped computations. An induction from the word’s beginning establishes alignment at every step; the proof does not assume arbitrary interior factors already respect episode boundaries.

6. The Shift-Table Lemma: How the Proof Hides an Unknown Product

A cut may bisect an interval whose product neither side can read. The shift-table lemma replaces knowledge of that product with a certificate covering every possible value. Fix a finite entry set $A$ and finite vector space $S$. A tuple length $\ell$ is chosen using only their sizes. For every table $f:A^\ell\to\operatorname{End}_{\mathrm{lin}}(S)$, choose a correction table $\beta_f:A^\ell\to S$.

Only afterward, for each actual tuple and input vector x, may the proof choose a coordinate whose replacement leaves the corrected output constant. The correction is independent of x. This quantifier order matters: choosing a fresh correction after seeing x would not define one deterministic episode update.

Here $\mathbf a$ is the actual tuple and $y$ the common output. The replacement notation means changing coordinate i while keeping every other entry fixed. The certificate tests all replacements, not a guessed missing value. Once both sides have checked the remaining entries, the actual hidden product is one of those replacements, so the claimed output follows.

The existence argument chooses correction vectors randomly. Failure probability decreases exponentially with tuple length, while the dependency bound grows quadratically. A finite local-lemma argument therefore supplies corrections that work simultaneously for every tuple and input. It is an existence argument, not a measured search algorithm.

Affine corrections can later be removed. For a composite affine map, compare its outputs on x and zero:

Finite intersections enforce both computations on the same word, and finite unions allow every possible translation. No extra star is needed. The homogeneous lift $\widehat F(v,c)=(vL+cb,c)$ also turns affine maps into linear maps on one additional coordinate, without requiring invertibility.

7. The Robust Tag Clock That Coordinates Independent Guesses

Each side independently chooses a tag containing proposed states, products, and indices. The robust clock assigns compatibility sets to these tags in a finite-dimensional torus. At a fixed total time, compatible ordered pairs are either all diagonal or consist of one off-diagonal pair. Crucially, the second alternative permits no competing pair.

With true origin t, cut k, and clock anchor q, the two tests combine through:

Equal tags let the sides verify complementary parts of one certificate. For the unique unequal pair, the episode’s affine translation is defined in advance to carry its prescribed input to its prescribed output. Disagreement is absorbed into a deterministic update whose linear part remains the original monoid action.

Outside exceptional totals, every tag has an interior neighborhood of compatible cuts. These margins let a finite residue grid find a usable cut. A separate sparsity estimate controls exceptional totals across translated candidate positions. The torus constructs finite tables; expressions do not read real-valued clock symbols.

The clock cannot establish that both sides mean the same endpoint. An independent guard compares bounded end searches across all proposed origins and requires exact consumption. Without this guard, correct clock arithmetic could coordinate guesses about different episodes.

8. Local Markers, Periodic Words, and the First Split

Local markers are boundaries chosen by a finite-window rule. They are well separated. If a sufficiently large neighborhood lacks a marker, the letters there have a short period. Overlapping periodic blocks determine a common continuation, making absence of markers usable information rather than a dead end.

When every required marker boundary exists, successive intervals supply a tuple of monoid products. The shift-table lemma selects an ignorable coordinate. The prefix checks earlier products, the suffix checks later ones, and a finite universal certificate covers the product crossing the cut.

When a marker search is absent throughout its extended window, the proof moves the cut through a periodic run. Eventually periodic powers in the finite monoid keep its prefix product fixed along a selected progression. Coprimality of the clock period with the relevant short periods lets these cuts traverse the required clock residues. No monoid cancellation is assumed.

These are local one-dimensional repetitions, rather than the global spatial periodicity discussed in our periodic tiling explainer. The first split succeeds outside an intrinsically defined exceptional episode language D, where clock or marker stability conditions fail. D is fixed by the episode, not selected separately for each input state.

9. Exceptional Episodes: Recovering the True Cut With a Stencil

The exceptional condition becomes a clue. Early candidate cuts form a fixed finite stencil, containing repeated copies of every metadata kind. Given its starting position, the suffix lists all candidate origins implied by those slots. The true origin satisfies the exceptional predicate. The task is preventing false origins from supplying additional witnesses.

Distinct stencil displacements have distinct residues. Marker-search widths indexed by those residues are separated enough that boundary failures cannot cluster freely. Combined with the clock’s uniform sparsity estimate and a bounded roster of clock anchors, the count covers all ordered pairs of different slots, including slots carrying incorrect metadata.

There are fewer ambiguous cuts than copies of any one kind. Therefore every required kind retains a cut where the exceptional witness is unique. Counting only candidates with plausible metadata would not justify that conclusion.

Endpoint handling is equally strict. A smaller end search defines the episode end, while a larger one supplies a bounded clock anchor when available. If some larger search is absent, all relevant smaller searches are absent, and overlapping periodic seeds share a first mismatch. A reference guard verifies that mismatch before uniqueness is tested. After decoding the origin, another check verifies its exact end in both branches. Missing inspection windows cause rejection, never removal of an inconvenient candidate.

10. The Second Split and the Recovery of Every Monoid Value

After the stencil identifies the true slot, prefix and suffix agree on its metadata. One early interval product remains hidden across their cut. The suffix builds a total table ψ describing the later computation for every hypothetical early monoid product, including products that no actual prefix realizes.

For the actual early product, the table returns the homogeneous lift of the first split’s affine update. Composing ψ with the product of early block values gives another table to which the unrestricted shift-table lemma applies. A second affine correction supplies a coordinate that can be omitted for each input.

The prefix verifies earlier entries and the universal missing-coordinate certificate. The suffix verifies later entries and equality of the entire computed table. The stencil guarantees a decodable copy of the needed kind. This split covers every exceptional episode, leaving no further skipped class.

That is why the lemma needed arbitrary tables rather than only feasible product actions. The construction checks a finite algebraic domain, not just examples resembling actual inputs. This universal guarantee differs from empirical evidence, a distinction explored in our Subset Sum proof analysis.

11. Why Two Splits Produce a Three-Level Bound, And What Remains Open

An exact-end check confines component words to finitely many templates $ac^i b$, with fixed words a, b, and c. Accepted exponents are ultimately periodic, so these components need at most one star level. Prefix tests are finite and have height zero. The incomplete remainder also has height-one tests retaining its monoid value.

The inner split begins with height-zero empty skips and produces height two. Affine recovery preserves that bound. Those computations become the outer split’s skips, producing height three:

This final accounting depends on proving height bounds for the individual tests, not merely proving that they are regular. Every standalone suffix must satisfy its own exact-end rule, even under false metadata. That requirement is what allows the periodic-template argument to apply before the split identity combines the components.

Final Boolean recovery and concatenation with the remainder add no star. Tags, states, and residues index finite choices rather than enlarging the input alphabet. This proves the stated uniform generalized star height bound within the manuscript’s construction.

Expression depth, expression size, conversion runtime, and matching performance remain different measures, as our DFT complexity analysis likewise emphasizes. The theorem supplies neither a minimum-height decision procedure nor a direct performance upgrade for programming regex engines.

On verification, the Lean scope note reports theorem coverage, while its linked comparator statement ends with sorry. The comparator is a challenge statement, not the implementation. Its configuration points to a separate solution module, whose main theorem contains proof code. We inspected that entry point but did not rebuild its dependency chain or run the comparator, so independent machine verification is not asserted here. Our Lean formalization explainer provides context for that distinction.

The Generalized Star Height Problem now has a manuscript offering a universal three-level bound, with optimality still open. Follow Binary Verse AI for proof-focused research explainers, and tell us which step deserves a deeper walkthrough: the clock’s controlled disagreement or the stencil’s recovery of exceptional cuts.