rankTestExact_classical
plain-language theorem explainer
Given a BWD-3 model M that encodes a CNF formula as a linear system L u = b together with admissibility constraints, there exists a Boolean value d such that d equals true exactly when an admissible solution u exists. Researchers studying exact reductions from 3SAT to linear feasibility would cite this result to close classical decidability. The argument is a one-line wrapper that applies the decide tactic to LinearFeasible and equates the outcome via decide_eq_true_iff.
Claim. Let $M$ be a BWD-3 model for a CNF formula on $n$ variables with $N$ equations. Then there exists a Boolean $d$ such that $d = true$ if and only if there exists an admissible vector $u$ satisfying $L u = b$.
background
BWD3Model is the structure that encodes 3SAT as the linear system $L u = b$ over rationals together with an admissibility predicate on solution vectors; it carries soundness (SAT implies an admissible witness), completeness (admissible witness implies SAT), and the Schur-pinch condition that admissible solutions must be Boolean phase states. LinearFeasible is the proposition asserting existence of an admissible $u$ with $L$ mulVec $u$ equal to $b$. RankTestExact is the interface that packages this feasibility question as the existence of a Boolean oracle deciding it exactly. The module setting is the linearized log-domain model in which admissible linear solutions are required to project to discrete Boolean states on the variable coordinates, i.e., the no-fractional-witnesses condition.
proof idea
The proof is a one-line wrapper. It invokes classical to refine the pair consisting of decide (LinearFeasible M) together with the equivalence decide (LinearFeasible M) = true ↔ LinearFeasible M, obtained by simpa on decide_eq_true_iff.
why it matters
This theorem supplies the classical existence of the rank-test oracle that sat_decider_classical consumes to produce an exact Boolean decider for Satisfiable φ. It therefore closes the logical existence half of the BWD-3 closure route without supplying runtime bounds. The result sits downstream of BWD3Model and LinearFeasible and is invoked directly by sat_decider_from_rank_test.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.