p_neq_np_assembled
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.
claimAssume 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 in Recognition Science
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.
scope and limits
- Does not prove the uniform topological obstruction hypothesis.
- Does not address the unconditional dissolution path.
- Does not apply to quantum or non-Boolean circuit models.
- Does not bound circuit depth or other restricted classes.
formal statement (Lean)
53theorem p_neq_np_assembled (pkg : PneqNPConditional) :
54 ∀ (poly_k poly_c : ℕ), ∃ (n₀ : ℕ),
55 ∀ n : ℕ, n₀ ≤ n →
56 ∀ (f : CNFFormula n), f.isUNSAT →
57 ∀ (c : BooleanCircuit n), CircuitDecides c f →
58 ¬ (c.gate_count ≤ poly_c * n ^ poly_k) :=
proof body
Term-mode proof.
59 p_neq_np_conditional pkg.phase3_hypothesis
60
61/-! ## Path B: Dissolution (Unconditional RS Position) -/
62
63/-- The RS dissolution argument. -/