TopologicalObstructionHyp
plain-language theorem explainer
The TopologicalObstructionHyp structure encodes the assumption that any Boolean circuit deciding an unsatisfiable CNF formula on n variables must have gate count at least 2^{n/k} for some positive integer k. Circuit complexity researchers working on conditional P ≠ NP results inside the Recognition Science framework would cite this named hypothesis. It is realized as a structure whose single field directly states the exponential size requirement without derivation.
Claim. The hypothesis asserts that for every natural number $n$ and every unsatisfiable CNF formula $f$ on $n$ variables, every Boolean circuit $c$ on $n$ inputs that decides $f$ satisfies: there exists $k > 0$ such that the gate count of $c$ is at least $2^{n/k}$.
background
The module develops circuit lower bounds from J-frustration using the Recognition Composition Law and d'Alembert equation. A BooleanCircuit is a feed-forward structure recording gate_count together with gates in topological order over n inputs. CircuitDecides holds precisely when there exists an evaluation function on assignments that matches the formula's satisfiedBy predicate. The sibling AlgebraicRestrictionHyp supplies a related linear lower bound via a depth-size tradeoff whenever landscape depth is positive.
proof idea
This declaration is a structural definition of the hypothesis. It introduces the exponential_lower_bound field with no proof body, as the content is an assumption. The structure is applied verbatim in the downstream conditional theorem circuit_lower_bound_topological.
why it matters
The structure supplies the topological component that enables the conditional theorem circuit_lower_bound_topological establishing exponential circuit size for unsatisfiable formulas. It complements AlgebraicRestrictionHyp, which yields only a linear bound. In the Recognition Science framework it advances the claim that high J-frustration implies super-polynomial circuit size as part of the conditional P ≠ NP program. The open question is discharge of the hypothesis by proving the required topological invariant from the J-cost landscape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.