BooleanPhaseState

formal source

  12admissible linear solutions must project to discrete Boolean states on the
  13variable coordinates.
  14-/
  15def BooleanPhaseState {n N : ℕ} (u : Fin N → ℚ) : Prop :=
  16  ∀ i, i.1 < n → u i = 0 ∨ u i = 1
  17
  18/--
  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