feasible_implies_boolean
plain-language theorem explainer
Any admissible feasible witness for the BWD3 linear encoding of a CNF formula must be a Boolean phase state, so its first n coordinates are exactly 0 or 1. Researchers studying linear relaxations of 3SAT would cite the result to exclude fractional solutions from admissible sets. The proof is a direct one-line extraction of the schur_pinch field from the supplied BWD3Model.
Claim. Let $M$ be a BWD3Model for CNF formula $φ$ with $n$ variables. For any vector $u$ such that $u$ is admissible and $L u = b$, the first $n$ coordinates of $u$ satisfy $u_i = 0$ or $u_i = 1$.
background
BWD3Model packages a linear system $L u = b$ over rationals, an admissibility predicate on vectors, and three axioms: sound (SAT implies an admissible witness), complete (admissible feasible witness implies SAT), and schur_pinch (admissible feasible witness is Boolean). BooleanPhaseState is the predicate requiring that the first $n$ coordinates of any such $u$ are exactly 0 or 1. The module places this inside the linearized log-domain model for SAT, where the no-fractional-witnesses condition recovers discrete solutions from the relaxation.
proof idea
One-line wrapper that applies the schur_pinch field of the supplied BWD3Model.
why it matters
The declaration supplies the exclusion property that admissible linear witnesses cannot be fractional, which is required for the BWD-3 closure route to map 3SAT exactly onto linear feasibility. It supports the sat_decider_from_rank_test and rankTestExact_classical constructions in the same module. In the Recognition Science setting it enforces discreteness on the variable coordinates, consistent with the forcing chain's emphasis on exact projection from linear models back to Boolean states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.