pith. sign in
module module high

IndisputableMonolith.Complexity.SAT.Backprop

show as:
view Lean formalization →

Module supplies partial assignment types and backpropagation state for SAT instances mixing CNF clauses with XOR parity constraints. Researchers working on propagation invariants or completeness arguments in the Recognition Science complexity layer would cite these definitions. Content consists of type definitions for assignments and states together with basic update lemmas.

claimA partial assignment over $n$ variables is a map from indices in $Fin n$ to $Option B$, where $none$ marks an undetermined variable and $some b$ records a fixed boolean value. The backpropagation state augments this map with derived evaluations of clauses and XOR constraints.

background

The module operates inside the SAT complexity subdomain. It imports variable indexing from the CNF module, where each variable is an element of $Fin n$ for a fixed problem size, and parity constraints from the XOR module, where each constraint specifies that the parity of a chosen subset equals a target bit. Partial assignments track known versus unknown values during propagation steps. Derived operations compute clause satisfaction and XOR parity under the current partial information.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the state representation consumed by the Completeness module to construct fully-determined backpropagation states from total assignments. This supports the larger claim that SAT instances mixing CNF and XOR can be resolved through systematic value propagation inside the Recognition framework.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (31)