IndisputableMonolith.Complexity.SAT.BWD3SchurPinch
This module defines the Boolean phase state for the BWD3 Schur pinch in SAT complexity analysis. It encodes the no fractional witnesses condition that admissible linear solutions in the log-domain must project to discrete Boolean states on variable coordinates. The module builds directly on Fin n indexing from the CNF import and supplies the sibling objects for feasibility and rank tests.
claimThe central object is the Boolean phase state predicate $BPS(x)$ on a linear solution $x$, requiring that the projection of $x$ onto each variable coordinate $i$ satisfies $x_i = 0$ or $x_i = 1$ for all $i$ in the finite set of size $n$.
background
The module resides in the Complexity.SAT hierarchy and imports the CNF module, which indexes variables by Fin n for a problem of given size. It introduces the linearized log-domain model together with BWD3Model, LinearFeasible, and RankTestExact to support the Schur pinch reduction. The BooleanPhaseState definition enforces the discrete projection condition on admissible solutions.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the core objects that feed sat_decider_from_rank_test and sat_decider_classical. It supplies the interface between linear feasibility in the log-domain and Boolean satisfiability, closing one step in the Recognition Science treatment of complexity via the forcing chain.
scope and limits
- Does not prove equivalence of linear feasibility and Boolean satisfiability.
- Does not implement numerical rank tests or solvers.
- Does not extend the CNF indexing or clause structure.
- Does not address multi-variable interactions beyond the phase state predicate.