landscapeDepth_nonneg
landscapeDepth_nonneg establishes that the average J-cost over all assignments is nonnegative for any CNF formula. Complexity researchers analyzing SAT landscapes and frustration barriers cite it to anchor basic bounds before proving stricter results for UNSAT instances. The term proof reduces directly to nonnegativity of the defining sum and its normalization factor.
claimFor any natural number $n$ and any CNF formula $f$ on $n$ variables, the average J-cost satisfies $0 ≤ (1/2^n) ∑_a satJCost(f,a)$, where the sum is over all $2^n$ assignments and satJCost counts unsatisfied clauses.
background
The J-Frustration module quantifies the topological depth of the J-cost landscape barrier around satisfying assignments. LandscapeDepth is the average J-cost across all assignments, defined explicitly as the sum of satJCost values divided by the number of assignments (Finset.univ.card). J-cost itself is the number of unsatisfied clauses under a given assignment. The upstream theorem satJCost_nonneg asserts that this count is always nonnegative, which is the key fact imported here. CNFFormula is the standard structure of a list of clauses over n variables.
proof idea
The term proof unfolds LandscapeDepth, then applies div_nonneg. Nonnegativity of the numerator follows from Finset.sum_nonneg applied pointwise to satJCost_nonneg. The denominator is nonnegative by Nat.cast_nonneg on the cardinality of the assignment space.
why it matters in Recognition Science
The result is invoked inside jfrustrationCert to supply the depth_nonneg field of the JFrustrationCert bundle. It supports the module's core classification results, including jfrust_sat_eq_zero and landscapeDepth_unsat (which gives depth ≥1 for UNSAT formulas). Within Recognition Science this anchors the nonnegativity side of the J-cost landscape before linking to the forcing chain and phi-ladder structures.
scope and limits
- Does not establish a positive lower bound for satisfiable formulas.
- Does not bound depth in terms of clause density or variable count.
- Does not address computational cost of evaluating the average.
- Does not extend to weighted clauses or probabilistic assignments.
Lean usage
theorem use_example {n : ℕ} (f : CNFFormula n) : 0 ≤ LandscapeDepth f := landscapeDepth_nonneg fformal statement (Lean)
59theorem landscapeDepth_nonneg {n : ℕ} (f : CNFFormula n) :
60 0 ≤ LandscapeDepth f := by
proof body
Term-mode proof.
61 unfold LandscapeDepth
62 apply div_nonneg
63 · exact Finset.sum_nonneg (fun a _ => satJCost_nonneg f a)
64 · exact Nat.cast_nonneg _
65
66/-- For UNSAT formulas, landscape depth is ≥ 1. -/