parityOf_filter_split'
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not apply when the variable list contains duplicates.
- Does not extend to multisets or sets of variables.
- Does not address infinite lists or non-list collections.
- Does not claim invariance under arbitrary reorderings of the input list.
formal statement (Lean)
146private lemma parityOf_filter_split' {n} (a : Assignment n) (vs : List (Var n)) (p : Var n → Bool) :
147 parityOf a vs = Bool.xor
148 (parityOf a (vs.filter p))
149 (parityOf a (vs.filter (fun v => !p v))) := by
proof body
Tactic-mode proof.
150 induction vs with
151 | nil => simp [parityOf]
152 | cons v vs ih =>
153 simp only [parityOf_cons, List.filter_cons]
154 by_cases hp : p v
155 · have h1 : (if p v then v :: vs.filter p else vs.filter p) = v :: vs.filter p := by simp [hp]
156 have h2 : (if !p v then v :: vs.filter (fun v => !p v) else vs.filter (fun v => !p v)) =
157 vs.filter (fun v => !p v) := by simp [hp]
158 rw [h1, h2, parityOf_cons, ih, Bool.xor_assoc]
159 · have h1 : (if p v then v :: vs.filter p else vs.filter p) = vs.filter p := by simp [hp]
160 have h2 : (if !p v then v :: vs.filter (fun v => !p v) else vs.filter (fun v => !p v)) =
161 v :: vs.filter (fun v => !p v) := by simp [hp]
162 rw [h1, h2, parityOf_cons, ih]
163 exact xor_comm_assoc' _ _ _
164