A constructive finite separator

For a finite channel, test containment on a complete output algebra basis. If a Hermitian pullback has a nonzero component outside the input algebra, Proposition prop:finiteseparator provides an exact equal-snapshot witness. Kraus completeness, Gauss commutation, regional algebra generation, and equality of complete device actions are separate checks.

A finite numerical agreement is not substituted for an exact containment identity. If approximate arithmetic is used, its validated allowance must enter Proposition prop:approx.