empty_formula_flat_landscape
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply to any formula that contains at least one clause.
- Does not compute or bound the spectral gap value itself.
- Does not address numerical stability or floating-point issues.
- Does not extend to weighted or soft-clause variants of the cost.
Lean usage
flat_empty := fun n a k => empty_formula_flat_landscape n a kformal statement (Lean)
63theorem empty_formula_flat_landscape (n : ℕ) :
64 ∀ (a : Fin n → Bool) (k : Fin n),
65 jcostEdgeWeight (⟨[], n, rfl⟩ : CNFFormula n) a k = 0 := by
proof body
Term-mode proof.
66 intro a k
67 unfold jcostEdgeWeight satJCost; simp
68
69/-- UNSAT gap condition: structure for formulas where every edge has
70 positive J-cost weight. -/