UNSATGapCondition
plain-language theorem explainer
UNSATGapCondition packages an unsatisfiability witness for a CNF formula with a uniform positive lower bound on every J-cost edge weight. Analysts of convergence rates on the J-cost Laplacian cite it to certify a positive spectral gap for unsatisfiable instances. The declaration is a structure definition that records four fields enforcing the gap condition without performing any computation.
Claim. Let $f$ be a CNF formula on $n$ variables. An UNSAT gap condition on $f$ consists of a proof that $f$ is unsatisfiable together with a positive integer $s$ such that the J-cost edge weight of every variable flip is at least $s$.
background
The J-cost Laplacian is built from the absolute difference in satisfaction cost when one variable is flipped. CNFFormula is a structure holding a list of clauses over $n$ Boolean variables. The module examines how the second eigenvalue of this Laplacian controls the speed of gradient descent on the J-cost landscape toward a minimum. Upstream, jcostEdgeWeight is defined as the absolute difference |satJCost f a - satJCost f (flipBit a k)| and sensitivity_pos extracts positivity from a strictly positive real argument.
proof idea
This is a structure definition. It directly assembles the four fields is_unsat, min_sensitivity, sensitivity_pos, and sensitivity_bound from the supplied data.
why it matters
The structure is the hypothesis type for unsat_has_positive_gap, which extracts the positive real value cond.min_sensitivity. In the spectral-gap analysis it supplies the condition needed to guarantee geometric convergence for unsatisfiable formulas. The module records that a Cheeger-type inequality remains open in unsat_has_spectral_gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.