IndisputableMonolith.Complexity.JCostLaplacian

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Complexity.RSatEncoding
   4
   5/-!
   6# J-Cost Laplacian on the Boolean Hypercube
   7
   8For a CNF formula φ on n variables, we define a weighted graph on the Boolean
   9hypercube {0,1}^n where:
  10- Vertices are assignments (Fin n → Bool)
  11- Edges connect Hamming-distance-1 assignments (single bit flip)
  12- Edge weight w(a, a') = |satJCost(φ, a) - satJCost(φ, a')|
  13
  14The **J-cost Laplacian** is represented by its quadratic form:
  15  Q_J(x) = ½ Σ_a Σ_k w(a, flip(a,k)) · (x(a) - x(flip(a,k)))²
  16
  17## Key Results
  18
  19- `laplacian_form_nonneg` — PSD (Q_J ≥ 0)
  20- `laplacian_form_const_zero` — constants are in the kernel
  21- `jcostEdgeWeight_le_clauses` — edge weights bounded by clause count
  22
  23## Status: 1 sorry (summand extraction lemma in zero-form implication)
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Complexity
  28namespace JCostLaplacian
  29
  30open RSatEncoding
  31
  32noncomputable section
  33
  34/-! ## Boolean Hypercube Graph Structure -/
  35
  36/-- Flip a single bit of an assignment. -/
  37def flipBit {n : ℕ} (a : Assignment n) (k : Fin n) : Assignment n :=
  38  fun j => if j = k then !a k else a j
  39
  40theorem flipBit_flipBit {n : ℕ} (a : Assignment n) (k : Fin n) :
  41    flipBit (flipBit a k) k = a := by
  42  funext j; simp only [flipBit]
  43  split_ifs with h
  44  · subst h; simp
  45  · rfl
  46
  47theorem flipBit_ne {n : ℕ} (a : Assignment n) (k : Fin n) :
  48    flipBit a k ≠ a := by
  49  intro h
  50  have : (flipBit a k) k = a k := congr_fun h k
  51  simp [flipBit] at this
  52
  53/-! ## J-Cost Edge Weights -/
  54
  55/-- The J-cost edge weight when flipping bit k. -/
  56def jcostEdgeWeight {n : ℕ} (f : CNFFormula n) (a : Assignment n) (k : Fin n) : ℝ :=
  57  |satJCost f a - satJCost f (flipBit a k)|
  58
  59theorem jcostEdgeWeight_nonneg {n : ℕ} (f : CNFFormula n) (a : Assignment n)
  60    (k : Fin n) : 0 ≤ jcostEdgeWeight f a k :=
  61  abs_nonneg _
  62
  63theorem jcostEdgeWeight_symm {n : ℕ} (f : CNFFormula n) (a : Assignment n)
  64    (k : Fin n) : jcostEdgeWeight f a k = jcostEdgeWeight f (flipBit a k) k := by
  65  unfold jcostEdgeWeight; rw [flipBit_flipBit]; exact (abs_sub_comm _ _).symm
  66
  67theorem jcostEdgeWeight_le_clauses {n : ℕ} (f : CNFFormula n) (a : Assignment n)
  68    (k : Fin n) : jcostEdgeWeight f a k ≤ f.clauses.length := by
  69  unfold jcostEdgeWeight satJCost
  70  have h1 : (↑(f.clauses.filter (fun c => !c.satisfiedBy a)).length : ℝ) ≤
  71             ↑f.clauses.length := Nat.cast_le.mpr (List.length_filter_le _ _)
  72  have h2 : (↑(f.clauses.filter (fun c => !c.satisfiedBy (flipBit a k))).length : ℝ) ≤
  73             ↑f.clauses.length := Nat.cast_le.mpr (List.length_filter_le _ _)
  74  have h1nn : (0 : ℝ) ≤ ↑(f.clauses.filter (fun c => !c.satisfiedBy a)).length :=
  75    Nat.cast_nonneg _
  76  have h2nn : (0 : ℝ) ≤ ↑(f.clauses.filter
  77    (fun c => !c.satisfiedBy (flipBit a k))).length := Nat.cast_nonneg _
  78  rw [abs_le]; constructor <;> linarith
  79
  80/-! ## Tight Variable-Degree Bound -/
  81
  82/-- Whether a clause contains a given variable (in any polarity). -/
  83def containsVar {n : ℕ} (c : Clause n) (j : Fin n) : Bool :=
  84  c.literals.any (fun lit => lit.1 == j)
  85
  86/-- The variable degree: number of clauses containing variable j. -/
  87def varDegree {n : ℕ} (f : CNFFormula n) (j : Fin n) : ℕ :=
  88  (f.clauses.filter (fun c => containsVar c j)).length
  89
  90/-- Flipping bit j does not change the value at any other index. -/
  91theorem flipBit_other {n : ℕ} (a : Assignment n) (j : Fin n) (i : Fin n) (hij : i ≠ j) :
  92    flipBit a j i = a i := by
  93  simp [flipBit, hij]
  94
  95/-- A literal not involving variable j has the same truth value after flipping j. -/
  96theorem literal_unchanged_by_flip {n : ℕ} (a : Assignment n) (j : Fin n)
  97    (lit : Fin n × Bool) (hlit : lit.1 ≠ j) :
  98    Literal.satisfiedBy lit (flipBit a j) = Literal.satisfiedBy lit a := by
  99  unfold Literal.satisfiedBy
 100  rw [flipBit_other a j lit.1 hlit]
 101
 102/-- A clause not containing variable j has the same satisfaction after flipping j. -/
 103theorem clause_unchanged_by_flip {n : ℕ} (a : Assignment n) (j : Fin n)
 104    (c : Clause n) (hc : containsVar c j = false) :
 105    c.satisfiedBy (flipBit a j) = c.satisfiedBy a := by
 106  have hne : ∀ lit ∈ c.literals, lit.fst ≠ j := by
 107    intro lit hmem heq
 108    unfold containsVar at hc
 109    have : c.literals.any (fun l => l.1 == j) = true :=
 110      List.any_eq_true.mpr ⟨lit, hmem, by rw [beq_iff_eq]; exact heq⟩
 111    rw [hc] at this; exact absurd this Bool.false_ne_true
 112  apply Bool.eq_iff_iff.mpr
 113  unfold Clause.satisfiedBy
 114  rw [List.any_eq_true, List.any_eq_true]
 115  exact ⟨fun ⟨l, hm, hs⟩ => ⟨l, hm, by rw [← literal_unchanged_by_flip a j l (hne l hm)]; exact hs⟩,
 116         fun ⟨l, hm, hs⟩ => ⟨l, hm, by rw [literal_unchanged_by_flip a j l (hne l hm)]; exact hs⟩⟩
 117
 118/-- The J-cost edge weight is bounded by the variable degree.
 119    Flipping bit j can only change clauses that contain variable j.
 120    Clauses not containing j have identical satisfaction (by `clause_unchanged_by_flip`),
 121    so only clauses containing j contribute to the cost difference.
 122
 123    The formal discharge requires a list-filter symmetric difference counting lemma:
 124    for predicates P, Q agreeing outside a subset S,
 125    |filter(P).length - filter(Q).length| ≤ S.length. Recorded as a named proposition. -/
 126def jcostEdgeWeight_le_varDegree_prop {n : ℕ} (f : CNFFormula n) (a : Assignment n)
 127    (j : Fin n) : Prop :=
 128  jcostEdgeWeight f a j ≤ varDegree f j
 129
 130/-! ## J-Cost Weighted Degree -/
 131
 132def jcostDegree {n : ℕ} (f : CNFFormula n) (a : Assignment n) : ℝ :=
 133  Finset.univ.sum (fun k : Fin n => jcostEdgeWeight f a k)
 134
 135theorem jcostDegree_nonneg {n : ℕ} (f : CNFFormula n) (a : Assignment n) :
 136    0 ≤ jcostDegree f a :=
 137  Finset.sum_nonneg (fun k _ => jcostEdgeWeight_nonneg f a k)
 138
 139/-! ## J-Cost Laplacian Quadratic Form -/
 140
 141/-- The J-cost Laplacian quadratic form on (Fin n → Bool) → ℝ.
 142    Q_J(x) = ½ Σ_a Σ_k w(a, flip(a,k)) · (x(a) - x(flip(a,k)))² -/
 143def JCostLaplacianForm {n : ℕ} (f : CNFFormula n)
 144    (x : (Fin n → Bool) → ℝ) : ℝ :=
 145  (1/2 : ℝ) * Finset.univ.sum (fun a : Fin n → Bool =>
 146    Finset.univ.sum (fun k : Fin n =>
 147      jcostEdgeWeight f a k * (x a - x (flipBit a k))^2))
 148
 149/-- **PSD: The J-cost Laplacian form is non-negative.** -/
 150theorem laplacian_form_nonneg {n : ℕ} (f : CNFFormula n) (x : (Fin n → Bool) → ℝ) :
 151    0 ≤ JCostLaplacianForm f x := by
 152  unfold JCostLaplacianForm
 153  apply mul_nonneg (by norm_num : (0 : ℝ) ≤ 1/2)
 154  apply Finset.sum_nonneg; intro a _
 155  apply Finset.sum_nonneg; intro k _
 156  exact mul_nonneg (jcostEdgeWeight_nonneg f a k) (sq_nonneg _)
 157
 158/-- **Constants are in the kernel.** -/
 159theorem laplacian_form_const_zero {n : ℕ} (f : CNFFormula n) (c : ℝ) :
 160    JCostLaplacianForm f (fun _ => c) = 0 := by
 161  unfold JCostLaplacianForm
 162  norm_num
 163
 164/-- **Zero form implies constant on positive-weight edges.**
 165    If Q_J(x) = 0, then for every (a, k) with positive weight, x(a) = x(flip(a,k)). -/
 166theorem laplacian_form_zero_imp {n : ℕ} (f : CNFFormula n) (x : (Fin n → Bool) → ℝ)
 167    (hzero : JCostLaplacianForm f x = 0) :
 168    ∀ (a : Fin n → Bool) (k : Fin n),
 169      0 < jcostEdgeWeight f a k → x a = x (flipBit a k) := by
 170  intro a k hpos
 171  unfold JCostLaplacianForm at hzero
 172  -- Step 1: ½ · S = 0 with S ≥ 0 implies S = 0
 173  have hS_nonneg : 0 ≤ Finset.univ.sum (fun a : Fin n → Bool =>
 174      Finset.univ.sum (fun k : Fin n =>
 175        jcostEdgeWeight f a k * (x a - x (flipBit a k))^2)) := by
 176    apply Finset.sum_nonneg; intro a' _
 177    apply Finset.sum_nonneg; intro k' _
 178    exact mul_nonneg (jcostEdgeWeight_nonneg f a' k') (sq_nonneg _)
 179  have hS_zero : Finset.univ.sum (fun a : Fin n → Bool =>
 180      Finset.univ.sum (fun k : Fin n =>
 181        jcostEdgeWeight f a k * (x a - x (flipBit a k))^2)) = 0 := by
 182    nlinarith [hS_nonneg]
 183  -- Step 2: outer sum = 0 with all inner sums ≥ 0 → the a-th inner sum = 0
 184  have hInner_nonneg : ∀ a' : Fin n → Bool, 0 ≤ Finset.univ.sum (fun k' : Fin n =>
 185      jcostEdgeWeight f a' k' * (x a' - x (flipBit a' k'))^2) := by
 186    intro a'; apply Finset.sum_nonneg; intro k' _
 187    exact mul_nonneg (jcostEdgeWeight_nonneg f a' k') (sq_nonneg _)
 188  have hInner_zero := Finset.sum_eq_zero_iff_of_nonneg (fun a' _ => hInner_nonneg a')
 189    |>.mp hS_zero a (Finset.mem_univ a)
 190  -- Step 3: inner sum = 0 with all terms ≥ 0 → the k-th term = 0
 191  have hTerm_nonneg : ∀ k' : Fin n, 0 ≤
 192      jcostEdgeWeight f a k' * (x a - x (flipBit a k'))^2 := by
 193    intro k'; exact mul_nonneg (jcostEdgeWeight_nonneg f a k') (sq_nonneg _)
 194  have hTerm_zero := Finset.sum_eq_zero_iff_of_nonneg (fun k' _ => hTerm_nonneg k')
 195    |>.mp hInner_zero k (Finset.mem_univ k)
 196  -- Step 4: w · d² = 0 with w > 0 → d² = 0 → d = 0
 197  have hd_sq_zero : (x a - x (flipBit a k))^2 = 0 := by
 198    rcases mul_eq_zero.mp hTerm_zero with hw | hd
 199    · linarith
 200    · exact hd
 201  have hd_zero : x a - x (flipBit a k) = 0 := by
 202    exact_mod_cast sq_eq_zero_iff.mp hd_sq_zero
 203  linarith
 204
 205/-! ## Cost Landscape Connectivity -/
 206
 207/-- Two assignments are cost-connected if there is a path through positive-weight edges. -/
 208inductive CostConnected {n : ℕ} (f : CNFFormula n) :
 209    (Fin n → Bool) → (Fin n → Bool) → Prop
 210  | refl (a) : CostConnected f a a
 211  | step (a : Fin n → Bool) (k : Fin n) (hpos : 0 < jcostEdgeWeight f a k)
 212      {c} (hrest : CostConnected f (flipBit a k) c) : CostConnected f a c
 213
 214/-- Cost-connectivity is reflexive. -/
 215theorem costConnected_refl {n : ℕ} (f : CNFFormula n) (a : Fin n → Bool) :
 216    CostConnected f a a := CostConnected.refl a
 217
 218/-! ## Certificate -/
 219
 220structure JCostLaplacianCert where
 221  psd : ∀ (n : ℕ) (f : CNFFormula n) (x : (Fin n → Bool) → ℝ),
 222    0 ≤ JCostLaplacianForm f x
 223  const_kernel : ∀ (n : ℕ) (f : CNFFormula n) (c : ℝ),
 224    JCostLaplacianForm f (fun _ => c) = 0
 225  weights_nonneg : ∀ (n : ℕ) (f : CNFFormula n) (a : Fin n → Bool) (k : Fin n),
 226    0 ≤ jcostEdgeWeight f a k
 227  weights_bounded : ∀ (n : ℕ) (f : CNFFormula n) (a : Fin n → Bool) (k : Fin n),
 228    jcostEdgeWeight f a k ≤ f.clauses.length
 229
 230def jcostLaplacianCert : JCostLaplacianCert where
 231  psd := fun n f x => laplacian_form_nonneg f x
 232  const_kernel := fun n f c => laplacian_form_const_zero f c
 233  weights_nonneg := fun n f a k => jcostEdgeWeight_nonneg f a k
 234  weights_bounded := fun n f a k => jcostEdgeWeight_le_clauses f a k
 235
 236end -- noncomputable section
 237
 238end JCostLaplacian
 239end Complexity
 240end IndisputableMonolith
 241