ConvergenceRate

formal source

  46/-! ## Convergence Rate -/
  47
  48/-- A convergence rate for iterative cost reduction on the J-cost landscape. -/
  49structure ConvergenceRate (n : ℕ) where
  50  rate : ℝ
  51  rate_lt_one : rate < 1
  52  rate_nonneg : 0 ≤ rate
  53
  54/-- The number of iterations needed to reduce cost below ε. -/
  55theorem iteration_bound_from_clauses {n : ℕ} (f : CNFFormula n)
  56    (gap : ℝ) (hgap : 0 < gap) :
  57    ∃ iters : ℕ, (iters : ℝ) ≥ f.clauses.length / gap :=
  58  ⟨Nat.ceil (↑f.clauses.length / gap), Nat.le_ceil _⟩
  59
  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}