The Exact Matching problem asks whether a bipartite graph with edges colored red and blue admits a perfect matching with exactly $t$ red edges. Introduced by Papadimitriou and Yannakakis in 1982, the problem has resisted deterministic polynomial-time algorithms for over four decades, despite admitting a randomized solution via the Schwartz-Zippel lemma since 1987. We establish the Affine-Slice Nonvanishing Theorem (ASNC) for all bipartite braces: a Vandermonde-weighted determinant polynomial is nonzero whenever the exact-$t$ fiber is nonempty. This yields a deterministic $O(n^6)$ algorithm for Exact Matching on all bipartite graphs via the tight-cut decomposition into brace blocks. The proof proceeds by structural induction on McCuaig's brace decomposition. We handle the McCuaig exceptional families via a parity-resolved cylindric-network positivity argument, the replacement determinant algebra, and the narrow-extension cases (KA, $J3 \to D1$). For the superfluous-edge step, we introduce two closure tools: a matching-induced Two-extra Hall theorem that resolves the rank-$(m-2)$ branch via projective-collapse contradiction, and a distinguished-state $q$-circuit lemma that eliminates the rank-$(m-1)$ branch entirely by showing that any minimal dependent set containing the superfluous state forces rank $m-2$. A Lean 4 formalization accompanies the paper. The formalization reduces the main theorem to eight explicit hypotheses corresponding to results proved here and in McCuaig (2001), with all algebraic tools, the induction skeleton, and the combinatorial infrastructure fully machine-checked.