An Elementary Proof of the $\tilde{O}(n^{1\mathrm{/}3})$ Bound for Separating Words

For two distinct binary words of length $n$, the separating words problem asks for a small deterministic finite automaton that accepts exactly one of them. Chase proved a $\tilde{O}(n^{1\mathrm{/}3})$ upper bound using a complex-analytic estimate for sparse polynomials. We replace that estimate by a finite-difference argument and a second-order real recurrence cutoff. The resulting elementary proof gives an explicit bound of $O(n^{1\mathrm{/}3}(\log n{)}^{7\mathrm{/}3})$ states.