xor_comm_assoc'
plain-language theorem explainer
The lemma establishes that exclusive-or on booleans satisfies a commuted associativity: a XOR (b XOR c) equals b XOR (a XOR c) for any booleans a, b, c. Researchers modeling SAT solvers or boolean parity in backpropagation would cite this identity when decomposing parity computations over variable lists. The proof is a one-line wrapper that exhausts all eight truth-value combinations via case analysis and closes by reflexivity.
Claim. For all boolean values $a, b, c$, $aoplus(boplus c)=boplus(aoplus c)$, where $oplus$ denotes exclusive or.
background
The module treats partial assignments for SAT backpropagation, where each variable is either unknown or fixed to a concrete boolean. Parity over a list of variables is computed by iterated exclusive-or. The lemma supplies the specific rearrangement of three XORs needed to split a parity calculation into two filtered sublists.
proof idea
This is a one-line wrapper proof that performs exhaustive case analysis on a, b, and c, then discharges the resulting boolean equalities by reflexivity.
why it matters
It is invoked by parityOf_filter_split' to show that the parity of a variable list equals the XOR of the parities over a predicate filter and its complement. This decomposition supports the backpropagation steps that update partial assignments during SAT search. Within the Recognition Science framework the result contributes to the complexity module that models boolean constraint propagation alongside the phi-ladder and eight-tick structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.