landscapeDepth_nonneg

formal source

  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
  77          apply Finset.sum_le_sum; intro a _
  78          exact unsat_cost_lower_bound f h a
  79
  80/-! ## Certificate -/
  81
  82structure JFrustrationCert where
  83  unsat_ge_one : ∀ (n : ℕ) (f : CNFFormula n), f.isUNSAT → JFrust f ≥ 1
  84  sat_eq_zero : ∀ (n : ℕ) (f : CNFFormula n), f.isSAT → JFrust f = 0
  85  depth_nonneg : ∀ (n : ℕ) (f : CNFFormula n), 0 ≤ LandscapeDepth f
  86  depth_unsat : ∀ (n : ℕ) (f : CNFFormula n), f.isUNSAT → 1 ≤ LandscapeDepth f
  87
  88def jfrustrationCert : JFrustrationCert where
  89  unsat_ge_one := fun n f h => jfrust_unsat_ge_one f h