BPStep
plain-language theorem explainer
BPStep defines the single-step backpropagation relation over a CNF formula augmented by an XOR system. Researchers proving monotonicity or soundness of propagation algorithms cite it when building completeness results for SAT instances with unique solutions. The declaration enumerates guarded constructors for XOR push and clause unit rules together with identity steps for gate types.
Claim. Let $n$ be a natural number, let $φ$ be a CNF formula over $n$ variables, and let $H$ be an XOR system. The inductive relation BPStep($φ$, $H$, $s$, $t$) holds when the partial assignment of state $t$ is obtained from that of state $s$ by setting a variable according to a missing XOR constraint from $H$, or by unit propagation on a clause from $φ$, or by an identity step on a gate.
background
The module works with partial assignments in which none denotes an unknown value and some b a determined Boolean. BPState is the structure that packages such an assignment. clauseUnit returns the variable and required value precisely when exactly one literal of a clause remains unknown and all known literals evaluate to false. xorMissing plays the analogous role for XOR constraints.
proof idea
This is an inductive definition. The two substantive constructors are xor_push (requiring X in H and xorMissing to return a pair) and clause_unit (requiring C in φ.clauses and clauseUnit to return a pair). The remaining six constructors are identity rules that leave the state unchanged.
why it matters
BPStep supplies the step relation used by bp_step_monotone and bp_step_sound. It appears in the hypotheses of backprop_succeeds_of_unique, determined_values_correct, and geometric_isolation_enables_propagation_thm. The definition therefore closes the interface between local propagation rules and the global isolation invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.