circuit_lower_bound_algebraic
plain-language theorem explainer
Algebraic restriction from the d'Alembert equation yields a linear circuit lower bound: any deciding circuit for an unsatisfiable n-variable CNF formula requires gate count at least n. Complexity researchers would cite it when establishing baseline size requirements from J-cost multiplicative structure. The proof chains the hypothesis depth-size tradeoff directly to the landscape depth lower bound of 1 via multiplication and simplification.
Claim. Assuming the hypothesis that the d'Alembert equation forces any circuit for a function with J-frustration to obey gate count $S$ satisfying $S d$ trade-off with landscape depth, for any $n$, unsatisfiable CNF formula $f$ on $n$ variables, and Boolean circuit $c$ deciding $f$, one has $c$.gate_count $geq n$.
background
In the Complexity.CircuitLowerBound module, circuit lower bounds are derived from J-frustration on the phi-ladder. BooleanCircuit models a feed-forward network with gate_count gates in topological order. CircuitDecides asserts existence of an assignment evaluation matching the formula's satisfiedBy predicate. LandscapeDepth averages the satJCost over all 2^n assignments, and landscapeDepth_unsat proves this average is at least 1 precisely when the formula is unsatisfiable.
proof idea
The tactic proof first invokes the depth_size_tradeoff field of AlgebraicRestrictionHyp to obtain gate_count >= LandscapeDepth f * n. It then applies landscapeDepth_unsat to establish LandscapeDepth f >= 1. Finally, mul_le_mul_of_nonneg_right and one_mul reduce the product to n.
why it matters
This result populates the algebraic_linear field of CircuitLowerBoundCert, which aggregates the linear algebraic bound with the exponential topological bound. It fills the algebraic restriction step in the module's three-step P versus NP argument, leveraging the Recognition Composition Law to impose multiplicative structure on the J-cost landscape. The declaration advances the framework's claim that high J-frustration triggers super-polynomial circuit size, though the full exponential bound remains conditional on the topological hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.