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 prove the Affine-Slice Nonvanishing Conjecture (ASNC) for all bipartite braces and give a deterministic O(n^6) algorithm for Exact Matching on all bipartite graphs. The algorithm follows via the tight-cut decomposition, which reduces the decision problem to brace blocks. The proof proceeds by structural induction on McCuaig's brace decomposition. We establish the McCuaig exceptional families, 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. The entire proof has been formally verified in the Lean 4 proof assistant.

翻译：精确匹配问题询问：一个边被染成红色和蓝色的二分图是否存在恰好包含t条红边的完美匹配。该问题由Papadimitriou和Yannakakis于1982年提出，尽管自1987年以来通过Schwartz-Zippel引理存在随机化解，但四十多年来一直未能找到确定性多项式时间算法。我们证明了所有二分braces上的仿射切片非消失猜想（ASNC），并给出了所有二分图上精确匹配的确定性O(n^6)算法。该算法通过紧割分解实现，将决策问题归约到brace块。证明过程基于McCuaig的brace分解进行结构归纳。我们建立了McCuaig例外族、替换行列式代数以及窄扩展情形（KA、J3到D1）。对于多余边步骤，我们引入了两个闭包工具：一个由匹配诱导的二部额外Hall定理，通过射影坍缩矛盾解决了秩(m-2)分支；以及一个区分态q-电路引理，通过证明任何包含多余态的最小相关集强制秩为m-2，彻底消除了秩(m-1)分支。整个证明已在Lean 4证明助手中得到形式化验证。