parityOf
plain-language theorem explainer
The parityOf definition computes the iterated XOR of variable values drawn from a Boolean assignment a over a list S of variables. Researchers analyzing mixed CNF-XOR satisfiability or backpropagation through partial assignments in the Recognition Science complexity layer would cite it as the core evaluator for parity constraints. The definition is realized directly as a left fold that applies Bool.xor starting from false.
Claim. For an assignment $a$ of $n$ variables and a list $S$ of variables, the parity is the iterated XOR $a(v_1) ⊕ a(v_2) ⊕ ⋯ ⊕ a(v_k)$ initialized at false.
background
In the Complexity.SAT.XOR module an XOR constraint requires that the parity of a chosen subset of variables equals a prescribed Boolean value. An Assignment n is a total function Fin n → Bool that supplies a truth value for every variable; Var n is simply Fin n. The supplied definition supplies the left-hand side of any such parity equation. Upstream, the same Assignment type appears in RSatEncoding as Fin n → Bool and in CNF as Var n → Bool, establishing the common semantics for evaluating literals and clauses.
proof idea
This is a direct one-line definition that applies List.foldl with the Bool.xor accumulator initialized at false. Related lemmas such as parityOf_cons and parityOf_nil are proved by unfolding the fold and invoking foldl_xor_init for simplification.
why it matters
parityOf supplies the evaluation primitive for every XORConstraint, feeding directly into satisfiesConstraint (PC module) and the backpropagation lemmas knownParity_eq_parityOf_known', parityOf_filter_split', and xorMissing_correct (Backprop module). The latter theorem uses it to recover the unique missing variable value when an assignment satisfies the constraint, confirming linearity of XOR over GF(2). It therefore closes the computational interface needed for the mixed CNF-XOR system without adding hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.