parityOf_filter_split'
plain-language theorem explainer
The lemma shows that the XOR parity of an assignment over a variable list equals the XOR of the parities on the two complementary filtered sublists. SAT backpropagation routines cite this when decomposing XOR constraints to recover missing variable values. The proof is a direct induction on the list that cases on the predicate at the head variable and applies the recursive parity definition together with Boolean XOR reordering.
Claim. Let $a$ be an assignment from variables to Booleans, $vs$ a list of variables, and $p$ a predicate on variables. Then the parity of $a$ over $vs$ equals the XOR of the parity of $a$ over the sublist where $p$ holds and the parity over the complementary sublist.
background
The module treats partial assignments for backpropagation through SAT constraints, where unknown variables are marked none and determined ones carry a Boolean. An Assignment is a total function from Fin n to Bool; parityOf folds Boolean XOR over the values that an assignment takes on a list of variables, starting from false. The companion lemma parityOf_cons states that parity of a cons cell is the head value XORed with the tail parity. The auxiliary xor_comm_assoc' supplies the Boolean identity needed to reorder three-way XORs.
proof idea
Induction on vs. The nil case simplifies directly from the empty-fold definition. For a cons cell the proof cases on whether the head satisfies p, rewrites both filters via filter_cons, applies parityOf_cons to expose the head XOR, invokes the inductive hypothesis on the tail, and closes with either direct associativity or the commutativity-associativity lemma to align the target XOR order.
why it matters
The result is invoked inside the proof of xorMissing_correct, which establishes that the backpropagation routine returns the correct Boolean for the single missing variable in a satisfied XOR constraint. It therefore supplies the algebraic step that lets the solver infer values without enumerating the full assignment. In the broader Recognition Science setting the lemma supports the encoding layer that ultimately feeds into the phi-ladder mass formulas and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.