parityOf_nil
plain-language theorem explainer
The parity computation over the empty list of variables returns false for any assignment. Researchers encoding SAT instances with XOR constraints in Recognition Science cite this as the base case for inductive arguments on parity. The proof is a direct reflexivity step from the foldl definition of parityOf.
Claim. For any natural number $n$ and any assignment $a$ of boolean values to the $n$ variables, the parity of the empty subset is false: parity$(a,[]) = false$.
background
An assignment maps each of $n$ variables to a boolean value. The parity function on a list of variables is defined by folding left with boolean XOR, starting from false. The module treats an XOR constraint as the requirement that this parity equals a prescribed boolean target. Upstream definitions of Assignment appear in both the RSatEncoding and CNF modules as total functions from variables to booleans.
proof idea
One-line term proof that applies reflexivity directly to the definition of parityOf on the empty list.
why it matters
This base case anchors the inductive development of parityOf, parityOf_cons and related lemmas inside the XOR encoding of SAT. It supplies the zero-length foundation needed for any recursive argument about parity preservation under list operations. Within the Recognition Science framework the lemma contributes to the complexity layer that sits above the phi-ladder and eight-tick octave structure, even though no downstream use is recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.