BooleanPhaseState
plain-language theorem explainer
BooleanPhaseState is the predicate on a rational vector u requiring its first n coordinates to equal exactly 0 or 1. Researchers encoding 3SAT as linear systems over the rationals cite it to enforce the no-fractional-witnesses condition on admissible solutions. The definition is a direct universal quantifier over the initial segment of coordinates with no auxiliary lemmas.
Claim. Let $u : {Q}^N$. The vector $u$ is a Boolean phase state when $forall i < n$, $u_i = 0 lor u_i = 1$.
background
In the BWD-3 closure route, 3SAT instances are encoded as linear systems $L u = b$ together with admissibility constraints on rational vectors. The BooleanPhaseState predicate isolates the integrality requirement on the first $n$ coordinates, which correspond to the original Boolean variables in the linearized log-domain model. This matches the paper-language description of the no-fractional-witnesses condition: admissible linear solutions must project to discrete Boolean states on the variable coordinates.
proof idea
The declaration is a direct definition consisting of the single predicate forall i, i.1 < n -> u i = 0 or u i = 1. No lemmas or tactics are applied; it serves as the primitive statement of the integrality filter.
why it matters
BooleanPhaseState supplies the integrality filter used inside BWD3Model to link satisfiability to the existence of admissible linear witnesses. It is invoked by the feasible_implies_boolean theorem, which shows that any feasible solution must satisfy the predicate. The definition closes the gap between the continuous relaxation and the discrete SAT problem, supporting the BWD-3 route within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.