`SpectralGapCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.SpectralGap
domain: Complexity
line: 85 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.SpectralGap on GitHub at line 85.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.