The infiltration closure theorem (paper §7): the infiltration-finite series are closed under addition, scalar multiplication, the infiltration product, and right derivatives. Addition, scalar multiplication, and the infiltration product follow by concatenating the witnessing tuples (the infiltration algebra is not the pointwise ring, so the evaluation is an infiltration-algebra homomorphism; the tuple is extended and the polynomial embedded at the front or back, and the closure under left derivatives is preserved by the concatenation). The right derivative is handled at the semantic level: the letter endomorphism $S_a = id + Δ_a$ is $ℚ$-linear but not a ring homomorphism, so the right derivative cannot be read off an automaton with the same transitions (unlike the Hadamard case); instead the witnessing tuple is extended to the "augmented" tuple $(fs, fun i => fs i + rightDeriv a (fs i))$, and the right derivative of the evaluation is the evaluation of $embedBack p − embedFront p$ in the extended tuple. The class is stated in terms of the semantic definition $IsInfiltrationFinite$; the proof proceeds at the semantic level, working directly with the witnessing tuples.