IndisputableMonolith.Complexity.SAT.Isolation
This module defines XOR families for SAT instances of size n, along with isolating families and deterministic isolation structures. Researchers modeling SAT completeness or backpropagation would cite these definitions when extending parity constraints. The module consists of definitions that layer on top of CNF variable indexing and XOR parity constraints.
claimAn XOR family over $n$ variables consists of a collection of XOR constraints, each specifying that the parity of a subset of variables indexed by Fin $n$ equals a fixed parity value. An isolating family selects subsets of such constraints that determine a unique total assignment.
background
The module sits in the SAT complexity layer and imports the CNF module (variables indexed by Fin $n$ for a given problem size) and the XOR module (an XOR constraint over $n$ variables requires that the parity of a variable subset equals a given parity). These supply the basic objects for constructing families that isolate deterministic assignments.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the isolation primitives required by the downstream Completeness module, which builds a fully-determined backpropagation state from a total assignment. It therefore closes the definitional gap between raw XOR constraints and deterministic isolation in the SAT setting.
scope and limits
- Does not contain theorems or proofs.
- Does not address general CNF satisfiability beyond XOR families.
- Does not define algorithms or numerical procedures.