p_neq_np_conditional
plain-language theorem explainer
Conditional on the uniform topological obstruction hypothesis with fixed k, no polynomial-size Boolean circuit decides unsatisfiability for CNF formulas on sufficiently large n. Complexity researchers examining P versus NP would cite this as the bridge from an exponential size lower bound to a polynomial comparison. The proof scales n by k, invokes exp_dominates_poly to obtain a domination threshold, then applies the hypothesis bound and linarith to reach a contradiction.
Claim. Assume the uniform topological obstruction hypothesis: there exists fixed $k > 0$ such that every unsatisfiable CNF formula on $n$ variables forces any deciding Boolean circuit to have gate count at least $2^{n/k}$. Then for all natural numbers $p_k, p_c$ there exists $n_0$ such that for all $n ≥ n_0$, every unsatisfiable CNF formula $f$ on $n$ variables, and every Boolean circuit $c$ deciding $f$, the gate count of $c$ exceeds $p_c · n^{p_k}$.
background
The module formalizes circuit lower bounds from J-frustration: the d'Alembert functional equation endows the J-cost landscape with multiplicative structure that polynomial circuits cannot exploit. UniformTopologicalObstructionHyp is the strengthened structure fixing a single denominator $k$ and asserting that for every unsatisfiable formula the deciding circuit size is at least $2^{n/k}$ (see REFERENCED_DEFS). BooleanCircuit and CircuitDecides supply the model of feed-forward circuits that decide formulas via an evaluation function (see UPSTREAM_RESULTS).
proof idea
The tactic proof extracts $k$ from the hypothesis and calls exp_dominates_poly on the scaled polynomial coefficient to obtain threshold $m_0$. It sets $n_0 = k · max(m_0, 1)$ and for $n ≥ n_0$ defines $m = n / k$. Nat lemmas establish $m ≥ m_0$ and that the assumed polynomial gate bound is at most the scaled polynomial times $m^{p_k}$, which is strictly less than $2^m$. The hypothesis supplies gate count ≥ $2^m$, so linarith yields the result.
why it matters
This theorem is the direct input to p_neq_np_assembled, which packages the conditional P ≠ NP statement. It completes the SAT instantiation step in the module's three-part argument (algebraic restriction, depth-width tradeoff, SAT instantiation) by converting the uniform exponential lower bound into a statement that no fixed polynomial bound survives for large $n$. The remaining open task is discharge of AlgebraicRestrictionHyp to derive the topological obstruction from the J-functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.