empty_formula_flat_landscape
plain-language theorem explainer
The empty CNF formula over n variables induces a flat J-cost landscape in which every single-bit flip leaves the number of unsatisfied clauses unchanged. Analysts of convergence rates for recognition-based SAT solvers cite this as the base case for a zero-gap Laplacian. The proof is a direct unfolding of the edge-weight definition followed by simplification that the empty clause list forces zero defects on both sides of any flip.
Claim. For the empty formula with no clauses over $n$ variables, and for every assignment $a$ and every variable index $k$, the absolute difference in J-cost (number of unsatisfied clauses) before and after flipping bit $k$ equals zero.
background
A CNFFormula is a structure consisting of a list of clauses together with a variable count. The J-cost of such a formula under an assignment equals the number of clauses left unsatisfied by that assignment, hence is zero precisely on satisfying assignments. The edge weight is defined as the absolute change in this J-cost when a single bit is flipped. The module studies the spectral gap of the associated Laplacian, which governs the rate at which a recognition process modeled as gradient descent on the J-cost surface converges to a minimum.
proof idea
One-line wrapper that introduces the assignment and index, unfolds the edge-weight and J-cost definitions, then applies simp. The empty clause list makes the filter length identically zero for both the original and flipped assignments, so the absolute difference reduces to zero.
why it matters
The result supplies the flat_empty component of the spectralGapCert certificate that anchors the module's variance and convergence-rate theorems. It supplies the zero-defect limit case for the J-cost function, consistent with the non-negativity of recognition costs in the broader framework and with the trivial instance of the Laplacian before any clauses are added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.