IndisputableMonolith.Complexity.SAT.BWD3SchurPinch
This module defines the BWD3 Schur pinch structures for reducing SAT to linear feasibility checks in the log-domain model of Recognition Science. Researchers studying complexity reductions would cite it for the BooleanPhaseState condition that enforces discrete assignments. It consists of definitions establishing equivalences such as satisfiable_iff_linearFeasible together with rank-test predicates.
claimDefines BooleanPhaseState as the condition that admissible linear solutions project to discrete Boolean states on variable coordinates (no fractional witnesses). Introduces BWD3Model, LinearFeasible, RankTestExact, and the equivalences satisfiable_iff_linearFeasible together with sat_decider_from_rank_test.
background
The module imports the CNF module, where variable indices are Fin n for a given problem size. It introduces BooleanPhaseState in the linearized log-domain model. Per the module documentation, this encodes the paper condition that admissible linear solutions must project to discrete Boolean states on the variable coordinates.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module supplies the BWD3 model and phase-state definitions that support the SAT decider constructions appearing among its sibling declarations, including sat_decider_from_rank_test and sat_decider_classical. It supplies the complexity-side interface between CNF problems and the rank-test machinery inside the Recognition framework.
scope and limits
- Does not implement a numerical SAT solver or runtime.
- Does not treat general NP-complete problems outside SAT.
- Does not address non-linear or higher-order extensions of the model.
- Does not supply concrete problem instances or benchmarks.