BWD3Model
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
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assert existence of a BWD3Model for an arbitrary CNF.
- Does not supply a polynomial-time construction of L, b or the admissible predicate.
- Does not encode runtime or complexity bounds on any decision procedure.
- Does not connect to the Recognition Science forcing chain or physical constants.
formal statement (Lean)
22structure BWD3Model {n N : ℕ} (φ : CNF n) where
23 L : Matrix (Fin N) (Fin N) ℚ
24 b : Fin N → ℚ
25 admissible : (Fin N → ℚ) → Prop
26 /-- SAT implies existence of an admissible linear witness. -/
27 sound : Satisfiable φ → ∃ u, admissible u ∧ L.mulVec u = b
28 /-- Admissible linear witness gives SAT. -/
29 complete : ∀ u, admissible u → L.mulVec u = b → Satisfiable φ
30 /-- Schur-pinch exclusion: no admissible fractional solutions survive. -/
31 schur_pinch : ∀ u, admissible u → L.mulVec u = b → BooleanPhaseState u
32
33/-- Feasibility of the linearized SAT system under admissibility constraints. -/