bp_step_monotone
plain-language theorem explainer
Monotonicity of backpropagation steps ensures that once a variable receives a value, later steps cannot revoke it. Researchers formalizing SAT solvers or constraint propagation in the Recognition Science setting cite this when establishing termination or completeness of the process. The proof performs case analysis on the BPStep constructors and applies setVar lemmas to verify that known assignments survive each update.
Claim. Let $n$ be a natural number, let $φ$ be a CNF formula over $n$ variables, and let $H$ be an XOR system. For partial assignments $s$ and $t$, if $t$ is obtained from $s$ by one application of the backpropagation step relation, then every variable assigned a value in $s$ remains assigned a value in $t$.
background
The module treats partial assignments as maps from variables to optional booleans, with none denoting unknown and some $b$ denoting a determined value. BPState packages such an assignment. BPStep is the inductive relation whose constructors include xor_push (setting a missing variable to satisfy an XOR constraint), clause_unit (unit propagation on a clause), and several identity rules (and_one, and_zero, or_one, or_zero, not_flip, wire_prop) that leave the assignment unchanged. The auxiliary setVar updates the assignment at one variable while preserving all others.
proof idea
The term proof introduces the step hypothesis and the variable, then performs case analysis on the BPStep constructors. For xor_push and clause_unit it branches on whether the variable equals the pushed variable, invoking setVar_same or setVar_ne to reduce to the hypothesis. For the six identity constructors the assignment is untouched, so the hypothesis transfers directly.
why it matters
The lemma supplies the monotonicity property required to argue that repeated backpropagation steps accumulate information without loss, supporting the claim that every legal start reaches a complete consistent state. It therefore belongs to the formalization of the backpropagation procedure inside the SAT module. No downstream theorems are yet recorded, and the result does not invoke the Recognition Science forcing chain or the RCL directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.