circuit_lower_bound_topological
plain-language theorem explainer
The theorem asserts that under TopologicalObstructionHyp, any Boolean circuit deciding an unsatisfiable CNF formula on n variables has gate count at least 2^{n/k} for some positive integer k. Complexity researchers assembling the Recognition Science P versus NP certificate would cite this result when combining algebraic and topological bounds. The proof is a one-line wrapper applying the exponential_lower_bound field of the hypothesis structure.
Claim. Assuming the topological obstruction hypothesis on the J-cost landscape, for every natural number $n$, every unsatisfiable CNF formula $f$ on $n$ variables, and every Boolean circuit $c$ that decides $f$, there exists a positive integer $k$ such that the gate count of $c$ satisfies $c.gate_count >= 2^{n/k}$.
background
The module formalizes circuit lower bounds from J-frustration. BooleanCircuit is a feed-forward structure with gate_count and gates in topological order, representing a restricted sub-ledger without global coupling across the lattice. CircuitDecides holds when there exists an evaluation function matching the formula's satisfiedBy predicate. CNFFormula is a k-CNF given by a list of clauses with var_count equal to n. TopologicalObstructionHyp is the structural hypothesis that the J-cost landscape for UNSAT formulas has a defect moat (J-cost >=1) creating a topological barrier that any deciding circuit must encode, forcing exponential size.
proof idea
The proof is a one-line wrapper that applies the exponential_lower_bound field of the TopologicalObstructionHyp hypothesis directly to the parameters n, f, hunsat, c, and hdec.
why it matters
This supplies the topological exponential lower bound inside circuitLowerBoundCert, which bundles algebraic and topological components for the overall certificate. It fills the topological step in the module's argument: algebraic restriction from the Recognition Composition Law, depth-width tradeoff, and SAT instantiation with high clause-to-variable ratio. The result sits at the research frontier where discharging the named hypotheses completes the P versus NP proof in the Recognition Science program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.