empty_formula_flat_landscape

formal source

  60/-! ## Landscape Properties -/
  61
  62/-- The empty formula has a flat landscape (all edge weights zero). -/
  63theorem empty_formula_flat_landscape (n : ℕ) :
  64    ∀ (a : Fin n → Bool) (k : Fin n),
  65      jcostEdgeWeight (⟨[], n, rfl⟩ : CNFFormula n) a k = 0 := by
  66  intro a k
  67  unfold jcostEdgeWeight satJCost; simp
  68
  69/-- UNSAT gap condition: structure for formulas where every edge has
  70    positive J-cost weight. -/
  71structure UNSATGapCondition (n : ℕ) (f : CNFFormula n) where
  72  is_unsat : f.isUNSAT
  73  min_sensitivity : ℕ
  74  sensitivity_pos : 0 < min_sensitivity
  75  sensitivity_bound : ∀ (a : Fin n → Bool) (k : Fin n),
  76    jcostEdgeWeight f a k ≥ min_sensitivity
  77
  78/-- From an UNSAT gap condition, we extract a positive gap value. -/
  79theorem unsat_has_positive_gap {n : ℕ} {f : CNFFormula n}
  80    (cond : UNSATGapCondition n f) : (0 : ℝ) < cond.min_sensitivity := by
  81  exact_mod_cast cond.sensitivity_pos
  82
  83/-! ## Certificate -/
  84
  85structure SpectralGapCert where
  86  variance_nonneg_cert : ∀ (n : ℕ) (x : (Fin n → Bool) → ℝ), 0 ≤ Variance x
  87  flat_empty : ∀ (n : ℕ) (a : Fin n → Bool) (k : Fin n),
  88    jcostEdgeWeight (⟨[], n, rfl⟩ : CNFFormula n) a k = 0
  89
  90def spectralGapCert : SpectralGapCert where
  91  variance_nonneg_cert := fun n x => variance_nonneg x
  92  flat_empty := fun n a k => empty_formula_flat_landscape n a k
  93