[Autoplectic]

Summary

The one-step generator equations used throughout (edge law, forward stationarity, summed future-side consistency) are necessary but not sufficient. This PR makes sofic say so and closes the verification gap that follows from it.

• Docs and docstrings. generator_kernel and the generative-models page now say: a positive kernel-LP violation rules a variable out as a generator state; a violation of 0 does not prove it is one. The GenerativeModelResult docstring explains what n_g_optima_generating, separating_variables_generate and cg_exceeds_g actually report.
• Exact verification. _reproduction_error, used by every search that returns a generator, now takes the maximum of the old fixed-length check and a new _equivalence_error. That function runs a difference-automaton equivalence test (Schützenberger / Tzeng): a breadth-first search over words, keeping those whose difference vectors are linearly independent (at most (n_1 + n_2)), and returning the largest word-probability deviation over the visited words. The old cutoff (at most length 8) could accept a candidate that matched short words and drifted later; two HMMs are only guaranteed equal once they agree up to length (n_1 + n_2 - 1).

Why

Future-side consistency constrains a state's belief (R_w) only through its one-step average. Nothing forces (R_w) to be the generated future's actual conditional distribution of (S^-).

Counterexample on survey process ((1,·),(2,0),(1,0)) (cpfci atom_generator_case1.npz): an 11-state ((\pi, Q, R, K)) with kernel-LP violation 0 matches the process's words up to length 3, then drifts (0.0078 at length 4, 0.024 at length 8). _equivalence_error reports 0.023 for it. On three word-verified survey generators it reports (5 \times 10^{-9}) to (6 \times 10^{-8}).

Impact

• Lower bounds (caps, coverage, the ((2,\infty)) certificate) use the equations only as necessary conditions, so they are unaffected.
• Upper bounds were already word-checked; the check now also covers long words.
• Runtime: at most (n_1 + n_2) vector-matrix products per symbol.

Test plan

• tests/test_reproduction_check.py: a fair coin and an alternating process, which agree on single symbols, are told apart even with max_length=1; two presentations of the golden mean (one non-unifilar) agree to (10^{-12}).
• Generator suites (141 passed)
• ruff check, ruff format --check, ty check (no errors), sphinx-build -W