p_neq_np_assembled
plain-language theorem explainer
The theorem packages a conditional separation of P from NP under the uniform topological obstruction. Complexity theorists working inside Recognition Science would cite it when assembling the full argument from J-frustration non-naturalness to circuit-size lower bounds. The proof is a one-line wrapper that feeds the phase-3 hypothesis from the input package into the upstream conditional lower-bound theorem.
Claim. Assume the uniform topological obstruction holds. Then for every pair of natural numbers $k,c$ there exists $n_0$ such that, for all $ngeq n_0$, every unsatisfiable CNF formula on $n$ variables, and every Boolean circuit that decides it, the circuit contains more than $c n^k$ gates.
background
PneqNPConditional is the structure that bundles four certificates (J-cost Laplacian, spectral gap, J-frustration, non-naturalness) together with the UniformTopologicalObstructionHyp and the CircuitLowerBoundCert. The module states two resolution paths: Path A derives P ≠ NP once the obstruction is granted; Path B dissolves the question by distinguishing recognition time from Turing-machine simulation overhead. Upstream, BooleanCircuit is the feed-forward structure whose gate_count is the size measure, while CircuitDecides asserts existence of an evaluation function that matches the formula's satisfiability predicate. The key upstream result is the theorem that the obstruction directly yields the stated polynomial-size prohibition.
proof idea
The proof is a one-line wrapper that applies the upstream theorem p_neq_np_conditional to the field pkg.phase3_hypothesis extracted from the supplied package.
why it matters
It completes the conditional Path A inside the P-vs-NP assembly module, supplying the final link from the phase-3 hypothesis to the explicit circuit-size statement. The module doc-comment positions this as the step that converts non-natural J-frustration into an exponential lower bound once the topological obstruction is assumed. In the broader framework the result sits between the Recognition Composition Law and the distinction between recognition time and classical circuit complexity; it leaves open whether the obstruction itself can be discharged unconditionally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.