AlgebraicRestrictionHyp
plain-language theorem explainer
The AlgebraicRestrictionHyp encodes the claim that any circuit deciding an unsatisfiable CNF formula on n variables must obey gate count at least landscape depth times n. Researchers deriving circuit lower bounds from the J-cost landscape in the Recognition Science program would cite this as the algebraic half of the P versus NP argument. The declaration is a named structure whose single field packages the universal quantification over formulas and circuits.
Claim. For any natural number $n$ and CNF formula $f$ on $n$ variables, if $f$ is unsatisfiable then for every Boolean circuit $c$ on $n$ variables that decides $f$, the real number of gates in $c$ is at least the landscape depth of $f$ multiplied by $n$.
background
The module states the core of the P versus NP program as high J-frustration implying super-polynomial circuit size. LandscapeDepth of a formula is the average J-cost over all assignments, where J-cost is the Recognition Science cost function obeying the d'Alembert equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). BooleanCircuit(n) is a feed-forward structure with gate_count and topologically ordered gates; CircuitDecides(c,f) asserts existence of an evaluation function matching the formula's satisfaction predicate.
proof idea
This is a structural definition of the hypothesis with no proof body. The single field directly records the quantified depth-size tradeoff statement for later use in conditional theorems.
why it matters
The hypothesis supplies the algebraic linear lower bound that feeds circuit_lower_bound_algebraic (gate count at least n for unsat formulas) and CircuitLowerBoundCert. It instantiates the d'Alembert multiplicative structure from the forcing chain to force simultaneous access to Omega(n) bits, complementing the topological obstruction hypothesis. The open question it touches is discharging the hypothesis by proving non-separability of the J-multiplier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.