unsat_has_positive_gap
The theorem shows that any UNSAT gap condition on a CNF formula forces its minimum sensitivity to be strictly positive. Researchers analyzing convergence rates of gradient descent on J-cost landscapes would cite it to guarantee a nonzero gap for unsatisfiable instances. The proof is a direct cast from the positivity hypothesis embedded in the UNSATGapCondition structure.
claimLet $f$ be a CNF formula on $n$ variables. If $f$ satisfies the UNSAT gap condition (i.e., $f$ is unsatisfiable and every edge weight $jcostEdgeWeight(f,a,k)$ is at least a positive integer $m$), then $0 < m$.
background
The module examines the spectral gap of the J-cost Laplacian on the hypercube. This gap controls the convergence speed of gradient descent on the J-cost landscape for a given formula. UNSATGapCondition is the structure requiring that the formula is unsatisfiable and that the minimum J-cost edge weight over all assignments and bit flips is a positive integer, with the bound holding uniformly. The result imports the CNFFormula definition (a list of clauses over $n$ variables) and the sensitivity_pos lemma, which proves positivity of a sensitivity function whenever its input is positive.
proof idea
The proof is a one-line wrapper that applies the sensitivity_pos field of the UNSATGapCondition hypothesis via exact_mod_cast.
why it matters in Recognition Science
This supplies the positivity ingredient required for spectral-gap arguments on unsatisfiable formulas, supporting downstream claims on iteration bounds and geometric convergence rates. It directly addresses the spectral gap λ₂ of the J-cost Laplacian described in the module. The module records an open sorry for the Cheeger-type inequality in unsat_has_spectral_gap, which this positivity result prepares.
scope and limits
- Does not establish a quantitative lower bound on the spectral gap.
- Does not apply to satisfiable CNF formulas.
- Does not compute explicit gap values in terms of clause count.
- Does not prove the full Cheeger inequality relating gap to conductance.
formal statement (Lean)
79theorem unsat_has_positive_gap {n : ℕ} {f : CNFFormula n}
80 (cond : UNSATGapCondition n f) : (0 : ℝ) < cond.min_sensitivity := by
proof body
Term-mode proof.
81 exact_mod_cast cond.sensitivity_pos
82
83/-! ## Certificate -/
84