landscapeDepth_unsat
For any unsatisfiable CNF formula on n variables, the average J-cost across all 2^n assignments is at least 1. Researchers deriving circuit size lower bounds from algebraic restrictions cite this to obtain a depth lower bound of 1 for unsatisfiable instances. The proof unfolds the average definition, rewrites the target inequality via cardinality positivity, and sums the per-assignment lower bound of 1 over the full assignment space.
claimLet $f$ be an unsatisfiable CNF formula on $n$ variables. Then $1$ is at most the average J-cost over all assignments: $1 ≤ (1/2^n) ∑_a J(f,a)$, where $J(f,a)$ equals the number of unsatisfied clauses under assignment $a$.
background
J-cost of a formula under an assignment equals the number of unsatisfied clauses, hence zero precisely on satisfying assignments. LandscapeDepth averages this J-cost over the full set of 2^n assignments. The module establishes J-frustration as a topological measure of the barrier around satisfying regions for CNF formulas.
proof idea
The proof unfolds the LandscapeDepth definition to expose the sum of satJCost values divided by the assignment cardinality. It establishes positivity of the cardinality, rewrites the target inequality as a comparison of sums, and applies the unsat_cost_lower_bound lemma pointwise to bound the sum from below by the cardinality itself.
why it matters in Recognition Science
This theorem supplies the depth_unsat component of the JFrustrationCert certificate. It is invoked in circuit_lower_bound_algebraic to conclude that any circuit deciding an unsatisfiable formula has gate count at least n, under the AlgebraicRestrictionHyp. Within the Recognition framework it contributes to classifying complexity via J-frustration, a non-natural property separating SAT from UNSAT instances.
scope and limits
- Does not establish a lower bound on the minimum J-cost (handled by unsat_cost_lower_bound).
- Does not apply when the formula is satisfiable.
- Does not quantify the exact depth beyond the inequality.
- Does not address formulas outside CNF encoding.
Lean usage
have hld := landscapeDepth_unsat f hunsatformal statement (Lean)
67theorem landscapeDepth_unsat {n : ℕ} (f : CNFFormula n) (h : f.isUNSAT) :
68 1 ≤ LandscapeDepth f := by
proof body
Tactic-mode proof.
69 unfold LandscapeDepth
70 have hcard_pos : (0 : ℝ) < (Finset.univ.card (α := Fin n → Bool) : ℝ) := by
71 exact_mod_cast Finset.card_pos.mpr ⟨fun _ => false, Finset.mem_univ _⟩
72 rw [le_div_iff₀ hcard_pos]
73 calc (1 : ℝ) * ↑(Finset.univ.card (α := Fin n → Bool))
74 = Finset.univ.sum (fun _ : Fin n → Bool => (1 : ℝ)) := by
75 simp [Finset.sum_const, smul_eq_mul]
76 _ ≤ Finset.univ.sum (fun a : Fin n → Bool => satJCost f a) := by
77 apply Finset.sum_le_sum; intro a _
78 exact unsat_cost_lower_bound f h a
79
80/-! ## Certificate -/
81