sat_decider_classical
plain-language theorem explainer
The theorem asserts existence of a classical Boolean decision procedure that returns true exactly on satisfiable 3SAT instances encoded as BWD-3 models. Researchers studying exact decision procedures obtained from linear feasibility tests would cite the result. The proof is a one-line term composition of the classical rank-test existence lemma with the decider extraction lemma.
Claim. Let $φ$ be a conjunctive normal form formula with $n$ variables. For any BWD-3 model $M$ of $φ$, there exists a Boolean value $d$ such that $d = true$ if and only if $φ$ is satisfiable.
background
A BWD-3 model encodes a 3SAT instance as a linear system $L u = b$ over the rationals together with an admissibility predicate on candidate solutions. The structure supplies three key properties: satisfiability of the formula implies existence of an admissible solution vector, every admissible solution vector yields satisfiability, and every admissible solution satisfying the equation must be a Boolean phase state (the Schur-pinch condition that excludes fractional witnesses). Satisfiability of a CNF means there exists a Boolean assignment that evaluates the entire formula to true.
proof idea
The proof is a one-line term that applies the decider extraction lemma to the supplied BWD-3 model and the classical rank-test exactness result for that model.
why it matters
The declaration closes the logical existence of an exact SAT decider for any BWD-3 model, completing the chain that begins with the linear encoding and the Schur-pinch exclusion of fractional solutions. It supplies the final step that converts an exact linear-feasibility test into a Boolean SAT predicate. No downstream results are recorded; the result stands as a terminal existence statement within the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.