IndisputableMonolith.Complexity.SAT.BWD3SchurPinch

   1import Mathlib
   2import IndisputableMonolith.Complexity.SAT.CNF
   3
   4namespace IndisputableMonolith
   5namespace Complexity
   6namespace SAT
   7
   8/--
   9A Boolean phase state in the linearized log-domain model.
  10
  11In the paper language this is the "no fractional witnesses" condition:
  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
  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). -/
  53theorem feasible_implies_boolean {n N : ℕ} {φ : CNF n}
  54    (M : BWD3Model (n := n) (N := N) φ) :
  55    ∀ u, M.admissible u → M.L.mulVec u = M.b → BooleanPhaseState u :=
  56  M.schur_pinch
  57
  58/--
  59Optional algorithmic interface: a rank/null-space test can be plugged in as a
  60single Boolean oracle. This is intentionally abstract at scaffold stage.
  61-/
  62def RankTestExact {n N : ℕ} {φ : CNF n}
  63    (M : BWD3Model (n := n) (N := N) φ) : Prop :=
  64  ∃ decideLinear : Bool, decideLinear = true ↔ LinearFeasible M
  65
  66/--
  67Classical existence of an exact linear-feasibility decider.
  68
  69This theorem is purely logical (`decide` over a proposition) and does not provide
  70any complexity guarantee.
  71-/
  72theorem rankTestExact_classical {n N : ℕ} {φ : CNF n}
  73    (M : BWD3Model (n := n) (N := N) φ) : RankTestExact M := by
  74  classical
  75  refine ⟨decide (LinearFeasible M), ?_⟩
  76  simpa using (decide_eq_true_iff (p := LinearFeasible M))
  77
  78/--
  79If an exact linear-feasibility test is available, it immediately yields an
  80exact SAT decision predicate for the same instance.
  81-/
  82theorem sat_decider_from_rank_test {n N : ℕ} {φ : CNF n}
  83    (M : BWD3Model (n := n) (N := N) φ) (hRank : RankTestExact M) :
  84    ∃ decideSAT : Bool, decideSAT = true ↔ Satisfiable φ := by
  85  rcases hRank with ⟨d, hd⟩
  86  refine ⟨d, ?_⟩
  87  constructor
  88  · intro hdtrue
  89    have hlin : LinearFeasible M := (hd.mp hdtrue)
  90    exact (satisfiable_iff_linearFeasible M).2 hlin
  91  · intro hsat
  92    have hlin : LinearFeasible M := (satisfiable_iff_linearFeasible M).1 hsat
  93    exact hd.mpr hlin
  94
  95/--
  96Classical end-to-end SAT decider existence for any instantiated `BWD3Model`.
  97
  98As above, this does not encode runtime bounds; it closes only the logical existence
  99of an exact decider.
 100-/
 101theorem sat_decider_classical {n N : ℕ} {φ : CNF n}
 102    (M : BWD3Model (n := n) (N := N) φ) :
 103    ∃ decideSAT : Bool, decideSAT = true ↔ Satisfiable φ :=
 104  sat_decider_from_rank_test M (rankTestExact_classical M)
 105
 106end SAT
 107end Complexity
 108end IndisputableMonolith
 109