Computational Directional Asymmetry: Dissolving the Classical Question Behind P vs NP

We define computational directional asymmetry AM(x) = log2 TM(x)− log2 TV(x, M (x)), the log-ratio of solving time to verification time for a total candidate solver M on instance x. We prove that P= NP if and only if every NP relation admits a solver with worst-case asymmetry O(log n) — equivalently, if and only if a single relation with NP-complete language does — and that no relation-by-relation version holds in general, since search need not reduce to decision. Lifting to the problem level, the asymmetry spectrum ΣNP collects the asymmetry classes (optimal worst-case asymmetry modulo O(log n)) of all NP relations, and P= NP holds exactly when ΣNP = {[0]}. What dissolves is the problem itself. The conceptual problem that P vs NP has been taken to pose — whether finding is fundamentally harder than checking — does not survive as a single problem: it decomposes into relation-, distribution-, and representation-dependent asymmetry questions, and P vs NP is the projection of this richer structure onto one binary degeneracy condition. The formal proposition P= NP is left untouched; it retains a definite truth value, which this paper does not determine and the dissolution does not require. Within the framework, worst-case, average-case, parameterized, and cryptographic hardness appear as statistics of a single distribution, Impagliazzo’s Five Worlds become tail regimes, and global asymmetry accumulates from local information deficits in the search space. We also isolate two conjectures whose conjunction implies P = NP, and analyze them against the relativization, natural proofs, and algebrization barriers. In restricted settings of solvers, namely DPLL and clause-learning solvers, both conjectures become theorems, and extending them to all solvers along the same route would require NP ̸= coNP. Theorem 1 with its search construction, the restricted-setting theorems, and the derivation of the conditional separation from the two conjectures are machine-checked in Lean 4 in a cost model where running time is derived from execution, without custom axioms.