consistent
plain-language theorem explainer
The consistent predicate asserts that a backpropagation state s is compatible with a CNF formula φ and XOR system H. Researchers in SAT complexity and backpropagation would cite it to establish links between partial and total assignments. The definition is realized directly as an existential statement over a total assignment agreeing with s and satisfying both constraints.
Claim. A state $s$ is consistent with CNF $φ$ and XOR system $H$ if there exists an assignment $a$ such that the partial assignment in $s$ agrees with $a$ on all variables, $evalCNF a φ = true$, and $a$ satisfies $H$.
background
BPState is a structure holding a partial assignment over n variables, with each entry either unknown (none) or fixed to a Boolean (some b). CNF is a conjunction of clauses, evaluated by evalCNF which returns true precisely when every clause holds. XORSystem encodes parity constraints checked via satisfiesSystem. The module develops partial assignments for backpropagation in SAT solving, where unknown bits are progressively determined. Upstream, Assignment from RSatEncoding supplies the total Boolean function on variables while CNF and its evaluation functions provide the formula layer.
proof idea
The definition directly encodes the semantic consistency condition via existential quantification over a total assignment. It requires that assignment to extend the partial state in s while satisfying both the CNF evaluation and the XOR system constraints.
why it matters
This predicate supports the BackpropSucceeds definition, which requires every initial state to reach a complete consistent state. It is invoked in the completeness lemmas consistent_completeStateFrom and complete_completeStateFrom. In the Recognition Science framework it bridges the SAT encoding layer to algebraic cost structures, closing the loop from partial states to satisfying assignments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.