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引理得到随机化解，但四十多年来一直缺乏确定性的多项式时间算法。我们证明了所有二分图支撑的仿射切片非零猜想，并给出了所有二分图上精确匹配问题的确定性O(n^6)算法。该算法通过紧割分解将判定问题归约到支撑块。证明过程基于McCuaig支撑分解的结构归纳法。我们建立了McCuaig例外族、替换行列式代数以及窄扩展情形。对于多余边步骤，我们引入两种封闭工具：一是匹配诱导的双额外Hall定理，通过射影坍缩矛盾解决秩为(m-2)的分支；二是区分态q-圈引理，通过展示包含多余态的任何最小依赖集必然迫使命秩为m-2，从而完全消除秩为(m-1)的分支。整个证明已在Lean 4定理证明器中得到形式化验证。