Prove
Lemma 2 ([Detection by independent residues]). Let…Lemma 1 ([Admissible evaluations]). Suppose a constant input pair R is block…Proposition
For the first assertion, apply any Ω_P -linear functional annihilating T_P to the formal tuple m . The result is zero. Multiply by the finitely many determinants of W(Q)-λ_h that occur. The cleared expression is a finite sum of products of base-point scalars and matrix-entry series; its auxiliary coefficients have a uniform valuation bound. Its formal identity is therefore equivalent to its identity at a small generic partner, by Lemma 2 ([Detection by independent residues]). It persists under the admissible specializations of Lemma 1 ([Admissible evaluations]). Divide by the specialized determinants when they are nonzero. The same argument, entry by entry, proves the scalar identities for M_h . It also proves the projected assertion, without introducing any spectral labels for the partner input. Choose finitely many coefficient vectors, together with columns of D , that span T_P , and select a nonzero minor witnessing their rank. For each column requiring a partner, use a separate set of partner variables. By multilinearity, the corresponding determinant of the series columns has that nonzero minor as the coefficient of a specified product of monomials. It is therefore a nonzero formal series. Clear the column denominators. The numerator is still nonzero, and its coefficients are uniformly bounded below in valuation. Independent small generic evaluations keep this numerator and its denominators nonzero, by Lemma 2 ([Detection by independent residues]). The resulting values attain the full dimension. The first assertion places all of them in the extended active space. This argument evaluates cleared numerators, not the possibly divergent geometric expansions of their inverses. The distinction is precisely the one made in Section.