The classical coincidence lemma (paper §4): a series is recognisable if and only if it is linearly finite. The forward direction ($LF_of_recognisable$) takes the finite-dimensional range of the representation's $semLin$ map as the finite generator space; the reverse direction ($recognisable_of_linearly_finite$) builds a representation from a left-derivative-closed finite generator space, reading off the matrices, initial vector, and final vector from a basis of that space.