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.

翻译：精确匹配问题要求判定：给定一个边被染成红色和蓝色的二分图，是否存在恰好包含$t$条红边的完美匹配。该问题由Papadimitriou和Yannakakis于1982年提出，尽管自1987年起已通过Schwartz-Zippel引理获得随机化解法，但四十多年来一直缺乏确定性多项式时间算法。我们为所有二分支撑图建立了仿射切片非消失定理：当精确$t$边纤维非空时，Vandermonde加权行列式多项式非零。这通过将二分图紧割分解为支撑图块，为所有二分图上的精确匹配问题给出了确定性$O(n^6)$算法。证明过程沿McCuaig支撑图分解进行结构归纳。我们通过奇偶性解析的圆柱网络正性论证、替换行列式代数以及窄扩张情形（KA, $J3 \to D1$）处理McCuaig例外族。对于多余边步骤，我们引入两种闭包工具：匹配诱导的双额外Hall定理，通过射影坍缩矛盾解决秩$(m-2)$分支；以及区分态$q$-电路引理，通过证明包含多余态的任何极小相关集必然迫使秩为$m-2$，完全消除秩$(m-1)$分支。论文附有Lean 4形式化验证。该形式化将主定理归约为八个显式假设，这些假设对应本文及McCuaig（2001年）中证明的结果，所有代数工具、归纳框架和组合基础设施均经过完全机器检验。