BWD3Model
plain-language theorem explainer
BWD3Model encodes a 3SAT instance as a rational linear system L u = b equipped with an admissibility predicate and three axioms that link satisfiability to feasible witnesses while forcing those witnesses to be Boolean. Researchers studying exact linear relaxations of SAT or Schur-complement techniques for eliminating fractional solutions cite the structure as the interface for the BWD-3 closure route. The declaration is a plain structure definition that bundles the matrix, vector, predicate and the three logical properties without any proof or
Claim. Let $n,N$ be natural numbers and let $φ$ be a CNF formula on $n$ variables. A BWD-3 model consists of a matrix $L∈ℚ^{N×N}$, a vector $b∈ℚ^N$ and a predicate admissible : (Fin $N$ → ℚ) → Prop such that (sound) satisfiability of $φ$ implies existence of an admissible $u$ with $L u = b$, (complete) every admissible solution of $L u = b$ witnesses satisfiability of $φ$, and (schur_pinch) every admissible solution of $L u = b$ satisfies the Boolean phase condition that its first $n$ coordinates lie in {0,1}.
background
BooleanPhaseState is the predicate requiring that the first $n$ coordinates of any vector $u$ are exactly 0 or 1. CNF is the standard structure whose clauses are lists of literals; Satisfiable $φ$ means there exists an assignment that evaluates the conjunction to true. The module works in the linearized log-domain model where 3SAT is represented by a matrix equation together with admissibility constraints drawn from the cost-model layer.
proof idea
The declaration is a structure definition that records the three axioms sound, complete and schur_pinch. No lemmas or tactics are invoked; the structure itself is the interface that downstream results instantiate.
why it matters
BWD3Model supplies the central schema for the BWD-3 closure route. It is instantiated by feasible_implies_boolean to obtain the Boolean-phase property, by LinearFeasible to define the existence predicate, and by sat_decider_classical to produce a classical SAT decider. The structure fills the paper proposition that encodes 3SAT as a linear system plus admissibility constraints, thereby connecting the complexity layer to the rank-test and decision-procedure constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.