parityOf_singleton
plain-language theorem explainer
The lemma shows that the parity of a singleton variable list under an assignment equals the Boolean value assigned to that variable. Workers formalizing XOR-SAT encodings or parity-based constraints cite it to collapse trivial cases during larger reductions. The argument is a direct simplification that unfolds the foldl definition of parityOf.
Claim. Let $n$ be a natural number, $a$ an assignment of Boolean values to the $n$ variables, and $v$ a variable index. Then the parity of the list containing only $v$ equals the value $a(v)$.
background
The module defines XOR constraints over $n$ variables as requiring that the parity of a chosen subset equals a target parity. The function parityOf computes this parity by folding the Boolean XOR operation across the list of variables, beginning from false. An Assignment is a total function from variables (Fin $n$ indices) to Bool, as introduced in the RSatEncoding and CNF modules.
proof idea
The proof is a one-line wrapper that applies simplification using the definitions of parityOf and List.foldl.
why it matters
This reduction supplies a basic case for singleton XOR constraints inside the SAT.XOR module. It supports sibling definitions such as satisfiesXOR and SatisfiableXOR by allowing direct substitution of single-variable parities. The result sits in the complexity layer and does not connect directly to the T0-T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.