jfrust_sat_eq_zero

formal source

  43    intro ⟨a, ha⟩; exact absurd ha (by simp [h a])
  44  simp [hns]
  45
  46theorem jfrust_sat_eq_zero {n : ℕ} (f : CNFFormula n) (h : f.isSAT) :
  47    JFrust f = 0 := by
  48  unfold JFrust
  49  haveI := Classical.propDecidable f.isSAT
  50  simp [h]
  51
  52/-! ## Landscape Depth -/
  53
  54/-- The average J-cost across all assignments. -/
  55def LandscapeDepth {n : ℕ} (f : CNFFormula n) : ℝ :=
  56  Finset.univ.sum (fun a : Fin n → Bool => satJCost f a) /
  57  (Finset.univ.card (α := Fin n → Bool) : ℝ)
  58
  59theorem landscapeDepth_nonneg {n : ℕ} (f : CNFFormula n) :
  60    0 ≤ LandscapeDepth f := by
  61  unfold LandscapeDepth
  62  apply div_nonneg
  63  · exact Finset.sum_nonneg (fun a _ => satJCost_nonneg f a)
  64  · exact Nat.cast_nonneg _
  65
  66/-- For UNSAT formulas, landscape depth is ≥ 1. -/
  67theorem landscapeDepth_unsat {n : ℕ} (f : CNFFormula n) (h : f.isUNSAT) :
  68    1 ≤ LandscapeDepth f := by
  69  unfold LandscapeDepth
  70  have hcard_pos : (0 : ℝ) < (Finset.univ.card (α := Fin n → Bool) : ℝ) := by
  71    exact_mod_cast Finset.card_pos.mpr ⟨fun _ => false, Finset.mem_univ _⟩
  72  rw [le_div_iff₀ hcard_pos]
  73  calc (1 : ℝ) * ↑(Finset.univ.card (α := Fin n → Bool))
  74      = Finset.univ.sum (fun _ : Fin n → Bool => (1 : ℝ)) := by
  75          simp [Finset.sum_const, smul_eq_mul]
  76    _ ≤ Finset.univ.sum (fun a : Fin n → Bool => satJCost f a) := by