unsat_has_positive_gap
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.