circuitLowerBoundCert
plain-language theorem explainer
The circuitLowerBoundCert packages two conditional lower bounds on Boolean circuit size for unsatisfiable CNF formulas: a linear bound from algebraic restrictions on the J-cost landscape and an exponential bound from topological obstructions. Researchers formalizing the P versus NP separation in the Recognition Science framework would cite this certificate when assembling the master proof. The definition is a direct one-line wrapper that delegates each field to the corresponding conditional theorem.
Claim. The certificate for circuit lower bounds is the structure whose algebraic linear field applies the algebraic restriction theorem to give gate count at least $n$ and whose topological exponential field applies the topological obstruction theorem to give gate count at least $2^{n/k}$ for some positive integer $k$, for any unsatisfiable formula on $n$ variables decided by the circuit.
background
The module formalizes circuit lower bounds from J-frustration, where the J-cost satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. High J-frustration for unsatisfiable formulas forces circuits to have large size through algebraic restrictions that prevent local computation and topological obstructions that require global access. The upstream theorem circuit_lower_bound_algebraic states that given AlgebraicRestrictionHyp any circuit deciding an UNSAT formula on $n$ variables has size at least $n$. Its companion circuit_lower_bound_topological states that given TopologicalObstructionHyp any such circuit has exponential size.
proof idea
The definition constructs the CircuitLowerBoundCert structure by assigning the algebraic_linear field to the direct application of circuit_lower_bound_algebraic and the topological_exp field to the direct application of circuit_lower_bound_topological. Each assignment is a one-line wrapper that passes the hypothesis, the formula, the unsatisfiability witness, the circuit, and the decision proof to the respective conditional theorem.
why it matters
This declaration supplies the lower_bound component to pvsNPMasterCert in the PvsNPAssembly module, completing the assembly of the full P versus NP certificate that also includes Laplacian, spectral gap, frustration, and non-naturalness components. It realizes the core claim of the module that high J-frustration implies super-polynomial circuit size, advancing the Recognition Science program toward P ≠ NP. The open hypotheses AlgebraicRestrictionHyp and TopologicalObstructionHyp remain to be discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.