UNSATGapCondition
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of an UNSAT gap condition for any concrete formula.
- Does not compute the numerical value of the spectral gap λ₂.
- Does not apply to satisfiable formulas.
- Does not incorporate the full Cheeger inequality.
formal statement (Lean)
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. -/