Which Regular Languages Admit Provably Correct RNN Implementations? A Lattice-Theoretic Characterisation via Forward-Invariant Sets

We study which regular languages can be recognised by recurrent neural networks with a forward-invariant certificate of length generalisation. An Elman RNN defines a switched dynamical system $h_{t+1} = \tanh(W_{hh} h_t + u_{x_t})$; we prove that length generalisation under such a certificate is equivalent to the existence of a forward-invariant positive-margin set (Theorem 2.1, if-and-only-if). We then establish a precise connection to automata theory: the class of regular languages admitting forward-invariant RNN implementations is contained within the class of absorbing-state languages, those whose minimal DFA has an accept state $q_a$ with $\delta(q_a, \sigma) = q_a$ for all $\sigma \in \Sigma$. This class is closed under union and intersection (but not complement in general). Non-absorbing languages (modular counting, last-$k$, alternating patterns) provably cannot admit forward-invariant sets of this form, and empirically show near-zero (0--7%) success with our training protocol (vs. 63--100% baseline). We verify the characterisation computationally: Kleene iteration on the complete lattice of axis-aligned boxes converges in $\sim 14$ iterations ($\rho_\mathcal{T} \approx 0.12$), and CQLF certificates via LMI verify 109/110 models up to $H = 70$. Across 42 absorbing patterns and 12 non-absorbing patterns: 350/350 vs $\leq 7$%, a near-perfect separation predicted by the lattice-theoretic characterisation. The gap formula $\mathrm{gap}_d \approx \operatorname{sech}^2(\bar{z}_d) \cdot |\Delta z_d|$ connects the automaton structure to an analytic sufficient condition ($r = +0.743$, F1 $= 0.872$). The result is a one-directional characterisation of the expressibility-verifiability boundary for recurrent networks on formal languages: necessity is proven, while the converse is supported empirically across the 42 absorbing patterns we tested.