xorMissing_correct
plain-language theorem explainer
xorMissing_correct asserts that when a partial assignment agrees with a total satisfying assignment on an XOR constraint and the detector reports exactly one unknown variable v together with candidate value b, then b equals the assignment's value at v. Implementers of backpropagation in SAT solvers that handle parity constraints cite the result to justify unit propagation steps. The proof splits on the length of the unknown-variable list, decomposes the parity computation, substitutes the satisfaction hypothesis, and reduces to XOR cancellation
Claim. Let $n$ be a natural number, let $σ$ be a partial assignment over $n$ variables, let $a$ be a total assignment, let $X$ be an XOR constraint, let $v$ be a variable and let $b$ be a boolean. If $σ$ agrees with $a$ on every determined bit, $a$ satisfies the parity condition of $X$, and the detector that returns the unique missing variable-value pair under $σ$ yields the pair $(v,b)$, then $b$ equals $a(v)$.
background
A partial assignment maps each variable to either none (unknown) or some boolean (determined). Compatibility requires that every determined bit in the partial assignment matches the corresponding bit of the total assignment. An XOR constraint consists of a list of variables together with a required parity bit. The upstream lemma knownParity_eq_parityOf_known' equates the parity obtained by folding the known bits under the partial assignment to the parity computed directly from the total assignment on those variables. The sibling result clauseUnit_correct establishes the analogous correctness statement for ordinary clauses.
proof idea
The tactic proof unfolds xorMissing, simplifies, and splits on whether the filtered list of unknown variables has length one. In the affirmative branch it extracts the variable and value, proves the unknown list equals the singleton containing v, invokes parityOf_filter_split' to separate known and unknown contributions, substitutes the satisfaction hypothesis, replaces the known parity via knownParity_eq_parityOf_known', and finishes with the cancellation lemma xor_comm_cancel'. The negative branch is discharged by simplification.
why it matters
The theorem supplies the semantic correctness of the xorMissing detector and is invoked by bp_step_sound to establish that a single backpropagation step preserves compatibility with any model. It replaces an earlier axiom with a proved statement, ensuring unit propagation on XOR constraints remains faithful. Within the Recognition Science treatment of complexity encodings the result guarantees that backpropagation on parity constraints does not introduce spurious models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.