Exhaustiveness and verification limits

The matching recursion generates each matching exactly once: the partner of the smallest slot is unique, and induction handles the remainder. The species loop covers all sixteen words. The permutation loop performs full external differentiation. The sparse products enumerate every nonzero component assignment, and the diagonal-metric test is precisely the matching contraction.

Thus the listing reconstructs the complete three-row raw matrix. The analytical completeness proof does not depend on executing it.

The factorization products and final fit are exact:

The substantive facts are that every raw column has zero first entry and that the two pivot columns are original allowed columns. Those facts were proved in the body.