Sakoda and Sipser asked how many states are needed to replace nondeterminism by determinism when two-way head motion remains available. The canonical target fixes the input alphabet and asks whether the cost is polynomial in the number of source states.

Guillon, Prigioniero, and Taheri describe the general determinization question as open in their STACS 2026 paper. They record an exponential upper bound obtained by eliminating two-way motion and passing to a one-way DFA. Their polynomial construction uses a stronger target device, a 1-limited automaton with a common-guess annotation, so it does not give a 2DFA.

Chrobak's Theorems 6.2 and 6.3 give a tight quadratic tradeoff for unary 1NFAs versus 2DFAs. This already supplies a fixed-alphabet quadratic lower bound for the one-way source subclass. Adeogun and Kapoutsis's arXiv v2, revised 2026-07-06, proves the explicit lower bound \(h(h+1)/4\) for every 2DFA solving one-way liveness of height \(h\), whose source language has an \(h\)-state 1NFA. The fixed-binary transfer recorded in this packet preserves that quadratic order and gives an explicit liveness-based binary family. These bounds remain within a polynomial cost and leave the canonical question unanswered.

The replay uses two independent Boolean-product routines. One evaluates the three nested loops in the definition. The other composes integer row masks. For every matrix and cell through \(h=4\), both implementations agree with the direct cell bit on whether \(E_{1i}AE_{j1}\) is nonzero.

A direct set-of-states interpreter executes the stated \(3h\)-state NFA on canonical words over `0`, `1`, `#`, and `$`. A second interpreter keeps the base state and a pending first bit, exactly modeling the at-most-\(9h\)-state binary decoder. Both answers are compared with Boolean matrix multiplication. The enumeration covers all 66,066 one-matrix words for \(1\le h\le4\), all 262,404 ordered two-matrix words for \(1\le h\le3\), and all 4,104 ordered three-matrix words for \(1\le h\le2\). Every comparison passes. The stable output digest is recorded in the artifact.

These finite checks test the implementation and the stated indexing. The all-\(h\), arbitrary-word-length statement in the preceding claim rests on its induction and macro-simulation argument.

Let \(\Sigma_h=\{0,1\}^{h\times h}\). A word \(A_1\cdots A_m\) is live when the Boolean product \(A_1\cdots A_m\) has a nonzero entry. Equivalently, the layered graph described by the matrices has a path joining its first and last columns. An \(h\)-state 1NFA follows a path by storing its current row index.

Adeogun and Kapoutsis construct \(1+\binom{h+1}{2}\) smooth connectivity properties. Each successive pair is separated by liveness and satisfies the suffix-of-choice condition in their main lemma. The two exit-size sequences of any solving 2DFA must decrease strictly a total of at least \(\binom{h+1}{2}\) times. One sequence therefore has at least half that many strict decreases, which yields \[ |Q|\ge \frac12\binom{h+1}{2}=\frac{h(h+1)}4. \] The alphabet size is \(|\Sigma_h|=2^{h^2}\), so this statement by itself uses an alphabet that grows with \(h\).

Chrobak proves both directions in Section 6. Theorem 6.2 converts any unary \(n\)-state 1NFA to a 2DFA with \(O(n^2)\) states by first placing the NFA in unary normal form, checking the bounded prefix, and using separate passes for the eventual cycles. Theorem 6.3 gives an \(n\)-state unary 1NFA family for which every equivalent 2DFA needs \(\Omega(n^2)\) states.

This settles the tradeoff for one-way nondeterministic source automata over the singleton alphabet. Unary 2NFA determinization and the full fixed-alphabet 2NFA problem remain open. The 2003 erratum is recorded alongside the original article.

Write \(E_{ab}\) for the Boolean matrix with a single one in cell \((a,b)\). Boolean multiplication gives \[ (E_{1i}AE_{j1})_{11}=A_{ij}, \] and every other entry of the product is zero. Hence the product is nonzero exactly when \(A_{ij}=1\).

If \(A\ne B\), choose a cell \((i,j)\) where they differ. Prefixing by \(E_{1i}\) and suffixing by \(E_{j1}\) makes exactly one of the two three-matrix words live. This is the concrete separator behind Lemma 1 of Adeogun and Kapoutsis. The argument also fixes the row and column order used by the replay artifact.

Begin with \(\Gamma=\{0,1,\#,\$\}\). Encode an \(h\) by \(h\) Boolean matrix row by row, put `#` between successive rows, and append `$`. Each matrix block has length \(h^2+h\).

Define a 1NFA \(N_h\) with one start state, \(h-1\) row-skipping states, \(h\) column states, and \(h\) tail states. The total is \(3h\). At the first block it guesses a starting row. In each block it skips to the row stored by the current branch, scans that row, and may choose a `1` in column \(j\). The tail state \(T_j\) carries \(j\) to the next `$`. The start state and the \(h\) states representing block boundaries are final. Thus a branch accepts after the last complete block exactly when it selected one edge in every matrix. Let \(K_h\) be the language accepted by this automaton, including its explicitly determined behavior away from canonical matrix encodings. On every canonical word \[ c_h(A_1)c_h(A_2)\cdots c_h(A_m), \] membership in \(K_h\) is equivalent to the Boolean product \(A_1A_2\cdots A_m\) being nonzero. This follows by induction on the blocks: after each `$`, the live branches store exactly the reachable right-column nodes.

Now suppose an \(s\)-state 2DFA \(D_h\) recognizes \(K_h\). Build a 2DFA for \(\operatorname{owl}_h\) whose ordinary states pair a state of \(D_h\) with the side from which a matrix block was entered. For each large-alphabet symbol \(A\), hardwire the deterministic run of \(D_h\) inside the fixed word \(c_h(A)\) until it exits that block, halts, or repeats an internal state-position configuration. An exit becomes one move to the adjacent matrix symbol with the corresponding entry side. An accepting halt enters a right-sweeping accept state. A rejecting halt or repeated internal configuration enters a right-sweeping reject state. The two sweep states also put the machine into the right-endmarker acceptance convention used by the source lower bound. Endmarker behavior is copied directly. This macro machine has at most \(2s+2\) states and agrees with \(D_h\) on every canonical encoding.

Use the uniform two-bit code \[ 0\mapsto00,\qquad 1\mapsto01,\qquad \#\mapsto10,\qquad \$\mapsto11. \] A binary decoder for \(N_h\) has one boundary copy of each state and two pending-first-bit copies. It therefore uses at most \(9h\) states and accepts exactly the two-bit images of words in \(K_h\). A 2DFA for this binary language can be macro-simulated directly on each length-\(2(h^2+h)\) matrix block, again using two state copies and the two sweep states.

The sourced one-way-liveness lower bound therefore gives \[ 2s+2\ge \frac{h(h+1)}4, \qquad s\ge \frac{h(h+1)}8-1. \] For the four-symbol intermediate family, \(n=3h\) gives \(s\ge n^2/72+n/24-1\). For the binary family, \(n=9h\) gives \(s\ge n^2/648+n/72-1\). These bounds are quadratic. Their exponent matches Chrobak's earlier unary fixed-alphabet lower bound, while the explicit binary family transports the 2026 liveness construction. The canonical polynomial-simulation question remains open.

The production target resolved exactly to problem 2832 with stable ID `tdbc1:15d7ea688e5e5a81d7f338c721357dd630ec5546b578a01981bb896e4d9f5909`. Its digest reported an open, published, actionable problem and no attached research records. Repository searches found the matching v6 candidate and no packet with the same `dataset.problem_ref`.

The source audit read Sakoda and Sipser's 1978 paper, Guillon, Prigioniero, and Taheri's STACS 2026 paper, and Adeogun and Kapoutsis's arXiv v2 dated 2026-07-06. A later-work check also inspected Chrobak's 1986 Theorems 6.2 and 6.3 and paired the article with its 2003 erratum. That check established that the quadratic fixed-alphabet exponent was already known for unary 1NFAs.

Two arXiv API searches were run: `all:Sakoda AND all:Sipser`, and `all:"two-way" AND all:nondeterministic AND all:deterministic AND cat:cs.FL`, both sorted by submission date with up to 100 results. The second query returned 26 records. Its newest relevant determinization paper was the July revision by Adeogun and Kapoutsis. The newer June submission concerned two-dimensional automata and a different problem. Exact-title and phrase searches found no checked primary source claiming a polynomial 2DFA construction or a superpolynomial fixed-alphabet lower bound.

This is a dated search report. Index coverage and terminology can omit relevant work, so the audit does not prove that no later result exists.

The attempted escalation had two parts. First, preserve the one-way-liveness lower bound while replacing \(\Sigma_h\), whose size is \(2^{h^2}\), by one alphabet independent of \(h\). Second, compare the resulting lower bound with the state count of the encoded 1NFA.

The four-symbol construction uses \(3h\) source states. Its uniform binary decoder uses at most \(9h\) states. In either case, a hypothetical \(s\)-state 2DFA for the encoded language yields a \((2s+2)\)-state 2DFA for \(\operatorname{owl}_h\). Substitution into the July 2026 theorem gives a lower bound of order \(h^2\), hence order \(n^2\) in either source-state normalization.

A quadratic lower bound fits the polynomial alternative in the canonical question. The encoding cannot amplify the imported exponent because every state transformation costs a constant factor. A superpolynomial conclusion from this route would require a superpolynomial source lower bound for one-way liveness or another hard family. Neither appears in the checked sources. Another run of the same encoding with larger finite \(h\) cannot cross this boundary.

Adeogun and Kapoutsis obtain their bound from a chain of \(1+\binom{h+1}{2}\) smooth connectivity properties. Their conclusion conjectures that \(\binom{h+1}{2}\) transitions are maximal for any chain satisfying the main lemma's successive-pair conditions.

A useful next computation would formalize those conditions for connectivity properties \(P(C)\), enumerate or solve them with a certificate-producing SAT model for \(h=2,3,4\), and compare the exact maximum with the proposed value. The first run should restrict to idempotent matrices and should emit every adjacency witness used in the chain. A longer chain would sharpen this lower-bound method. Agreement at small \(h\) would delimit the method and provide test instances for a proof of maximality.

The program represents every Boolean matrix as a row-major integer. It compares a dense Boolean product, an integer-row-mask product, and direct cell extraction for the separator identity. Separate transition interpreters read the canonical four-symbol encoding and its uniform binary image, then compare both answers with the matrix-product oracle.

The default command enumerates all dimensions and word lengths stated in the bounded computation claim. It uses exact integer and Boolean operations, one process, no pseudorandom choices, no network, and no external service. A successful run prints one stable JSON document ending with `all_exact_checks_passed`.