iteration_bound_from_clauses
The theorem provides an explicit natural-number bound on iterations sufficient to reduce the J-cost of any CNF formula below a threshold, scaling directly with clause count over the positive spectral gap. Analysts of convergence in Boolean landscapes within Recognition Science would invoke it to obtain runtime estimates from the Laplacian spectrum. The proof is a direct term-mode application of the ceiling function together with its elementary lower-bound property.
claimLet $f$ be a CNF formula with $m$ clauses and let $λ > 0$. There exists a natural number $k$ satisfying $k ≥ m / λ$.
background
The Spectral Gap of the J-Cost Laplacian module studies how the second eigenvalue λ₂ of the Laplacian controls the rate at which gradient descent on the J-cost landscape converges to its minimum for CNF-encoded problems. A CNFFormula is a structure consisting of a list of clauses over n variables, as introduced in the RSatEncoding module. This bound complements other results in the module such as the non-negativity of variance and the flat landscape of the empty formula.
proof idea
The proof is a one-line term-mode wrapper. It constructs the witness as the ceiling of the real division of clause count by gap and applies the standard lemma that the ceiling of a real number is at least that number.
why it matters in Recognition Science
The declaration supplies the iteration scaling relation required for convergence analysis in the J-cost spectral gap setting. It directly supports the module's key result that iteration count scales with m over λ, feeding into broader Recognition Science claims about geometric convergence rates. The module documentation flags a remaining Cheeger-type inequality as an open sorry, which this bound would help close once the gap is shown positive for unsatisfiable instances.
scope and limits
- Does not derive the value of the spectral gap from the formula.
- Does not apply to formulas whose gap vanishes.
- Does not extend to non-CNF cost functions.
- Does not yield a tight constant beyond the ceiling construction.
formal statement (Lean)
55theorem iteration_bound_from_clauses {n : ℕ} (f : CNFFormula n)
56 (gap : ℝ) (hgap : 0 < gap) :
57 ∃ iters : ℕ, (iters : ℝ) ≥ f.clauses.length / gap :=
proof body
Term-mode proof.
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). -/