The infiltration coincidence theorem (paper §7): a series is infiltration-finite (an infiltration polynomial in a finite tuple of series closed under the left derivatives) if and only if it is recognised by an infiltration automaton. The "finite implies recognisable" direction extends the witnessing tuple by the series itself and builds the automaton from the closure under left derivatives; the "recognisable implies finite" direction reads off the generator tuple $A.sem (X_i)$, closed under left derivatives by the derivation property.