LandscapeDepth
plain-language theorem explainer
LandscapeDepth computes the mean J-cost of a CNF formula by averaging satJCost over every one of the 2^n Boolean assignments. Complexity researchers deriving circuit size lower bounds from algebraic restrictions cite this average when establishing positive depth for unsatisfiable instances. The definition is a direct normalization of the total sum of per-assignment J-costs by the cardinality of the assignment space.
Claim. For a CNF formula $f$ on $n$ variables, the landscape depth is defined by $LandscapeDepth(f) = 2^{-n} sum_{a} J(f,a)$, where the sum runs over all assignments $a$ and $J(f,a)$ equals the number of unsatisfied clauses under $a$.
background
In the J-Frustration module, J-cost is the number of unsatisfied clauses under a given assignment, as introduced in satJCost: J equals zero precisely when the assignment satisfies every clause and equals the count of unsatisfied clauses otherwise. CNFFormula encodes a k-CNF formula as a list of clauses together with a variable count. LandscapeDepth averages this per-assignment cost over the full hypercube of assignments, yielding a global measure of landscape frustration. The module states that J-frustration quantifies the topological depth of the J-cost barrier around a formula's satisfying region.
proof idea
This is a direct definition that sums satJCost over Finset.univ of all assignments and divides by the cardinality of that Finset, expressed in real numbers.
why it matters
LandscapeDepth supplies the quantitative depth used inside JFrustrationCert to certify that every unsatisfiable formula has depth at least one. It is invoked by AlgebraicRestrictionHyp and circuit_lower_bound_algebraic to obtain size lower bounds of the form gate_count >= n for circuits deciding unsatisfiable formulas. The quantity therefore bridges the Recognition Science J-cost construction to concrete circuit-complexity statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.