BWD3Model

formal source

  19Schema for the BWD-3 closure route:
  203SAT is encoded as a linear system `L * u = b` plus admissibility constraints.
  21-/
  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. -/
  34def LinearFeasible {n N : ℕ} {φ : CNF n} (M : BWD3Model (n := n) (N := N) φ) : Prop :=
  35  ∃ u, M.admissible u ∧ M.L.mulVec u = M.b
  36
  37/--
  38Conditional BWD-3 closure theorem:
  39under exact linearization + admissibility + Schur pinch, SAT is exactly
  40the linear feasibility problem.
  41-/
  42theorem satisfiable_iff_linearFeasible {n N : ℕ} {φ : CNF n}
  43    (M : BWD3Model (n := n) (N := N) φ) :
  44    Satisfiable φ ↔ LinearFeasible M := by
  45  constructor
  46  · intro hsat
  47    exact M.sound hsat
  48  · intro hlin
  49    rcases hlin with ⟨u, hadm, hu⟩
  50    exact M.complete u hadm hu
  51
  52/-- Any admissible feasible witness is Boolean (no fractional witness survives). -/