CircuitLowerBoundCert
plain-language theorem explainer
CircuitLowerBoundCert packages two conditional statements: algebraic restriction yields a linear gate-count lower bound while topological obstruction yields an exponential one, both for Boolean circuits deciding unsatisfiable CNF formulas. Researchers assembling the Recognition Science P vs NP argument cite this certificate when collecting the lower-bound phase. The declaration is a structure definition that directly records the two implications without further derivation steps.
Claim. If the algebraic restriction hypothesis holds, then for every natural number $n$ and every unsatisfiable CNF formula $f$ on $n$ variables, every Boolean circuit $c$ deciding $f$ satisfies gate count at least $n$. If the topological obstruction hypothesis holds, then for every such $f$, every deciding circuit $c$ satisfies gate count at least $2^{n/k}$ for some positive integer $k$.
background
The module formalizes circuit lower bounds from J-frustration. The d'Alembert equation $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ endows the J-cost landscape with multiplicative structure that polynomial circuits cannot exploit. BooleanCircuit is a feed-forward structure over $n$ variables whose gate_count records total gates in topological order. CircuitDecides $c$ $f$ asserts existence of an evaluation function that matches $f$.satisfiedBy on all assignments. CNFFormula is a list of clauses with var_count $n$ and isUNSAT predicate. AlgebraicRestrictionHyp requires that any deciding circuit for an unsatisfiable $f$ obeys gate_count >= LandscapeDepth $f$ * $n$. TopologicalObstructionHyp requires existence of $k>0$ such that gate_count >= $2^{n/k}$.
proof idea
This is a structure definition that packages the two conditional statements. No tactics or lemmas are applied inside the declaration itself. The concrete implications are supplied by the sibling functions circuit_lower_bound_algebraic and circuit_lower_bound_topological, which are invoked when the structure is instantiated downstream.
why it matters
The certificate is the lower-bound component collected inside PvsNPMasterCert alongside the Laplacian, spectral-gap, frustration and non-naturalness certificates. It operationalizes the module claim that high J-frustration forces super-polynomial circuit size, completing the third step of the Recognition Science P vs NP program. The open question remains discharge of AlgebraicRestrictionHyp and TopologicalObstructionHyp to convert the conditional statements into an unconditional result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.