consistent
plain-language theorem explainer
The consistent predicate declares that a backward-propagation state s matches a CNF formula φ and XORSystem H precisely when a total Boolean assignment exists that agrees with s on every determined variable, satisfies φ under evalCNF, and satisfies H. Researchers establishing completeness of SAT backpropagation steps within Recognition Science would cite this definition when linking partial states to total solutions. The definition is a direct existential quantification over completing assignments.
Claim. A partial assignment state $s$ over $n$ variables is consistent with CNF formula $φ$ and XOR system $H$ if there exists a total assignment $a$ such that $s$ agrees with $a$ on all determined variables, $a$ evaluates $φ$ to true, and $a$ satisfies $H$.
background
In the SAT.Backprop module, BPState is a structure containing a PartialAssignment that marks variables as unknown (none) or determined (some Bool). CNF is a structure whose clauses list is evaluated by evalCNF, which returns true exactly when every clause holds. Assignment from RSatEncoding is the type Fin n → Bool; the CNF module supplies its own Assignment alias Var n → Bool together with evalCNF. satisfiesSystem and XORSystem are imported from the XOR module to encode parity constraints.
proof idea
Direct definition. The body is an existential quantifier over an Assignment n that simultaneously extends the partial map in s, satisfies the CNF via evalCNF, and satisfies the XORSystem via satisfiesSystem.
why it matters
BackpropSucceeds quantifies over consistent states to assert that every initial BPState reaches a complete consistent state. The completeness lemmas consistent_completeStateFrom and complete_completeStateFrom rely on this predicate to show that any satisfying total assignment yields a consistent state. Downstream uses appear in CircuitLedger and in derivations for ElectroweakVEVStructure and CosmologicalConstant, placing the predicate inside the chain that connects SAT encodings to physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.