module module high

`IndisputableMonolith.Complexity.SAT.Backprop`

This module defines partial assignments and backpropagation states for SAT instances that combine CNF clauses with XOR parity constraints. It supplies update operations and evaluation functions that track determined values under incomplete information. Completeness arguments in the SAT development cite these structures to propagate assignments from total solutions. The module consists entirely of definitions and basic supporting lemmas built on the CNF and XOR foundations.

claimA partial assignment over $n$ variables is a map from Fin $n$ to Option Bool. The backpropagation state tracks determined values for a CNF formula together with an XOR constraint set, with operations to set a variable and to evaluate literals, clauses, and parity expressions.

background

The module sits inside the SAT complexity layer of Recognition Science and imports variable indexing from the CNF module, where variables are elements of Fin n for a problem of size n. It also imports the XOR module, whose constraints require that the parity of a designated subset equals a fixed parity bit. PartialAssignment encodes incomplete knowledge by mapping each variable to none when unknown and to some b when its boolean value has been fixed. The sibling definitions then supply setVar for updating the assignment, valueOfLit for literal evaluation, valueOfClause for clause satisfaction, and valueOfXOR for parity checks.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The structures supply the assignment-propagation layer required by the Completeness module, which constructs fully-determined backpropagation states from total assignments. This placement supports the SAT completeness argument inside the Recognition framework by furnishing the concrete mechanism that turns partial information into determined values for both CNF and XOR constraints.

scope and limits

Does not implement a full SAT solver or search procedure.
Does not handle constraints outside CNF clauses and XOR parities.
Does not address counting, optimization, or approximate solving.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Complexity.SAT.Completeness module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Complexity.SAT.CNF module_import
IndisputableMonolith.Complexity.SAT.XOR module_import

declarations in this module (31)

abbrev PartialAssignment L10
structure BPState L13
def setVar L17
lemma setVar_same L20
lemma setVar_ne L24
def valueOfLit L32
def valueOfClause L38
def valueOfXOR L47
def xorMissing L55
def clauseUnit L66
inductive BPStep L79
def complete L105
def consistent L109
def compatible L114
lemma compatible_setVar L118
lemma not_isSome_eq_isNone' L137
lemma xor_comm_assoc' L140
lemma xor_comm_cancel' L143
lemma parityOf_filter_split' L146
lemma getD_of_compat_isSome' L165
lemma knownParity_eq_parityOf_known' L177
lemma list_singleton_of_length_one' L197
theorem xorMissing_correct L213
lemma not_isSome_iff_isNone' L260
lemma singleton_eq_get_zero' L263
lemma mem_zip_of_getElem' L270
lemma known_lit_false'' L277
theorem clauseUnit_correct L311
lemma bp_step_sound L399
lemma bp_step_monotone L431
def BackpropSucceeds L455