Fix átomaton construction and decide reverse ε-machine finiteness

[Autoplectic]

Carries the five átomaton / time-reversal commits that were merged into cursor/wheeler-automata via #10 after #9 had already landed, so they never reached main. cursor/wheeler-automata has a byte-identical tree to this branch (e636fdb) — it is just these five commits plus the merge commit from #10 — so this single PR covers all the unmerged work on both branches, and both can be deleted once it lands.

What's here

Átomaton construction and atomicity (sofic/automata/atomaton.py, algorithms.py) — atomaton_from_language ended in a spurious determinize(), which collapsed the átomaton back to the minimal DFA of the language, i.e. Brzozowski's minimization rather than the átomaton. The átomaton is the reverse of the minimal DFA of the reverse language (Brzozowski & Tamm 2014, Theorem 2), so the pipeline now stops at the reversal. On the paper's three-state example that is the difference between 3 states and the correct 6 states with 3 initial.

The AtomicAutomaton.validate stub is filled in with Theorem 4: a state is atomic iff the set of N^{RD} states containing it is a union of Nerode classes of N^{RD}. nerode_partition is extracted from minimize_moore via a shared _moore_refine, and deliberately does not trim — states with an empty right language have to survive as their own class or the atomicity test reports a false positive.

Explosion is propagated, not swallowed (sofic/generators/epsilon_machine.py, mixed_state_construction.py, sofic/exceptions.py) — a finite forward ε-machine does not imply a finite reverse one. When the reverse belief set never closed, from_time_reversed caught the generic StochasticValidationError raised by the max_states cap and fell back to _row_normalized_presentation, which row-normalizes the reversed HMM without determinizing. On a three-state witness that returns a non-unifilar machine whose state entropy equals the forward C_μ exactly, so causal_irreversibility() reported 0.0 — "perfectly reversible" — for a process whose true ΔC_μ is -∞.

The cap now raises its own MixedStateExplosionError (a StochasticValidationError, so existing handlers keep working) and from_time_reversed re-raises it. Genuine UnifilarityError still falls back as before.

Deciding reverse finiteness (sofic/generators/reversal.py) — the new reverse_is_finite. Because the seed belief is uniform and the machine unifilar, the retrodictive causal states are exactly the normalized vectors (Pr(x|s))_s, so the reverse machine is finite iff every log-likelihood ratio takes finitely many values. Reading a symbol moves the pair (s, s') to (δ(s,a), δ(s',a)) and multiplies the ratio by p(a|s)/p(a|s'), giving:

the reverse ε-machine is finite iff every cycle of that pair graph has weight one.

That is the twins property of weighted-automata determinization, so the O(|Q|²+|E|²) test of Allauzen & Mohri (2003) applies.

Verification

1031 tests pass (21 more than main), ruff clean, merges cleanly into main.

reverse_is_finite was validated against exact-rational brute force on all 432 strongly connected 3-state binary machines (432/432), plus 4-state and ternary samples, and adversarial tuned probabilities where a cycle weight is 1 by coincidence — those come out finite despite sharing structure with explosive machines, so this is not a structural test in disguise.

Two implementation details that validation caught are worth knowing about: the pair graph must be a MultiDiGraph, since two symbols can carry a pair to the same successor with different ratios and collapsing them hides the inconsistency; and weights accumulate in log space, because products of ratios underflow and make any absolute tolerance meaningless.

The explosion regression test uses a witness whose infinitude has a closed form — the block map multiplies the posterior ratio z/y by exactly 9/7, so the futures (01)^k have pairwise distinct posteriors for every k.

Citations

Per the repo's literature-references rule, Ellison et al. (2011) is cited where the explosion behavior is introduced (MixedStateExplosionError, from_time_reversed, reverse_is_finite, and the two docs pages); Chaos 21 037107 Sec. VI B 3 gives a ternary process with two recurrent forward causal states and countably infinitely many reverse ones. Ellison2011 was already in references.bib as an arXiv preprint and is upgraded to the published Chaos entry with its DOI.

The docs also carried a wrong claim, now corrected: an infinite reverse presentation does not make C_μ^- infinite. C_μ^- is the entropy of the retrodictive stationary distribution, which converges when the weights decay geometrically, as they do in that example. What explodes is the cardinality of the presentation, which is the actual reason there is nothing to return.

The twins citation is stated precisely: the pair-graph cycle-weight criterion is Theorem 5 of Allauzen & Mohri (2003), with Theorem 6 the per-SCC potential algorithm actually implemented. The hypothesis is cycle-unambiguous, not unambiguous — weaker, and the one that actually holds, since unifilarity gives one path per state/word. Their "twins iff determinizable" equivalence is explicitly not invoked: it is for trim unambiguous automata over the tropical semiring, and full-support seeding makes every state initial, so this automaton is |S|-ambiguous over the real semiring. The equivalence used here comes from the direct log-ratio argument instead.

Made with Cursor