LinearFeasible
plain-language theorem explainer
LinearFeasible encodes the existence of an admissible vector u satisfying the linear equation L u = b for a BWD-3 model of a CNF formula. Researchers reducing SAT to linear feasibility would cite this predicate as the target condition inside the BWD-3 closure theorem. The definition is a direct existential statement drawn from the model's admissible predicate and matrix-vector product.
Claim. Let $M$ be a BWD3Model for CNF formula $φ$ with matrix $L$ and right-hand side $b$. Then LinearFeasible($M$) holds if and only if there exists a vector $u$ such that $M$.admissible($u$) and $L u = b$.
background
The BWD3Model structure encodes a 3SAT instance as a linear system $L u = b$ over the rationals together with an admissibility predicate on candidate solution vectors. The module setting places this construction inside the linearized log-domain model, where the no-fractional-witnesses condition requires that admissible solutions project to discrete Boolean phase states on the variable coordinates. The upstream BWD3Model supplies the sound and complete properties that link satisfiability of $φ$ to the existence of such witnesses, plus the Schur-pinch clause that excludes fractional solutions.
proof idea
This is a one-line definition that directly packages the existential quantification over admissible vectors satisfying the linear constraint extracted from the BWD3Model fields.
why it matters
LinearFeasible supplies the target predicate for the biconditional in satisfiable_iff_linearFeasible, the conditional BWD-3 closure theorem. It is referenced by RankTestExact, rankTestExact_classical, and sat_decider_from_rank_test to abstract an exact decision procedure for SAT. In the Recognition framework this definition completes the linearization step that reduces combinatorial satisfiability to linear algebra over the rationals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.