satisfiesXOR
satisfiesXOR declares that a Boolean assignment meets a single XOR constraint exactly when the parity of the listed variables equals the constraint's target bit. SAT analysts and linear-system modelers over GF(2) would invoke this predicate when checking consistency of parity equations. The definition is a direct one-line wrapper that delegates to the parityOf fold.
claimAn assignment $a$ satisfies XOR constraint $c$ if and only if the iterated XOR of $a$ over the variables in $c$ equals the prescribed parity of $c$.
background
Assignment n denotes total maps from variables (Fin n or Var n) to Bool. XORConstraint n is the structure holding a list of variables together with a target parity Boolean. parityOf a S folds Bool.xor across the values a(v) for v in list S, beginning from false.
proof idea
One-line wrapper that applies parityOf to the constraint's variable list and compares the result to the stored parity field.
why it matters in Recognition Science
This predicate supplies the atomic check lifted by satisfiesSystem to full XOR systems. It is called inside the soundness lemma for belief-propagation steps and inside the theorem establishing that xorMissing recovers the correct value for a missing variable. The construction embeds linear equations over GF(2) into the SAT library, aligning with parity operations appearing in ledger and kinship modules.
scope and limits
- Does not prove existence of any satisfying assignment.
- Does not incorporate CNF clauses or mixed clause-XOR systems.
- Does not count the number of solutions.
- Does not operate on partial assignments.
formal statement (Lean)
22def satisfiesXOR {n} (a : Assignment n) (c : XORConstraint n) : Prop :=
proof body
Definition body.
23 parityOf a c.vars = c.parity
24
25/-- An assignment satisfies an XOR system when all constraints hold. -/