IndisputableMonolith.Complexity.SAT.Isolation
The Isolation module defines XOR families and isolating families for SAT instances of size n, supplying deterministic isolation primitives. Researchers working on SAT completeness or backpropagation constructions would cite it when building fully determined assignment states. It is a definition module containing no theorems or proofs.
claimFor natural number $n$, an XOR family consists of parity constraints over variables indexed by $Fin n$. The module defines $XORFamily(n)$, $IsolatingFamily$, and $DeterministicIsolation$ as collections of such constraints that isolate solutions.
background
This module sits inside the SAT complexity layer of Recognition Science and imports the CNF module (variables indexed by $Fin n$) together with the XOR module (parity of a variable subset equals a given parity). It introduces XORFamily as an XOR family for instances of size n, plus the sibling definitions IsolatingFamily and DeterministicIsolation that encode isolation via parity constraints.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the isolation layer required by the downstream Completeness module, which builds a fully-determined backpropagation state from a total assignment. It therefore completes the deterministic isolation step inside the SAT completeness argument.
scope and limits
- Does not implement any SAT decision procedure or solver.
- Does not prove NP-completeness or hardness results.
- Does not address general CNF formulas beyond XOR-based isolation.
- Does not connect to phi-ladder, forcing chain, or physical constants.