Characterizing Language Generation in the Limit: Finite Witnesses and a Separation-Width Hierarchy

Language generation in the limit—producing valid, unseen elements from an exhaustive stream of an unknown language—now has an exact characterization. The authors establish that generation is solvable across countable universes if and only if each target language admits a finite positive witness ensuring an infinite intersection among all activated candidates. Beyond this equivalence, the paper defines a positive separation-width hierarchy reflecting witness size constraints and formalizes the complete theoretical framework and normalization lemmas within Lean.