landscapeDepth_unsat
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.