theorem
proved
unsat_has_positive_gap
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.SpectralGap on GitHub at line 79.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
94end -- noncomputable section
95
96end SpectralGap
97end Complexity
98end IndisputableMonolith