PvsNPDissolution
plain-language theorem explainer
The PvsNPDissolution structure packages three properties that together dissolve the P versus NP question inside the recognition framework: SAT instances admit zero J-cost assignments in at most n steps, UNSAT instances carry J-cost at least 1 under every assignment, and any decoder on a proper subset of variables fails to recover a hidden parity bit. Researchers comparing recognition time to Turing-machine simulation overhead would cite it to separate the two complexity measures. The definition assembles the three claims directly from upstreamJ
Claim. A structure asserting: for every natural number $n$ and CNF formula $f$ on $n$ variables, if $f$ is satisfiable then there exist steps $s$ and assignment $a$ with $s$ at most $n$ such that the number of unsatisfied clauses under $a$ is zero; if $f$ is unsatisfiable then every assignment yields at least one unsatisfied clause; and for every proper subset $M$ of the $n$ variables and every decoder from the restricted hidden-parity encoding to a Boolean, there exists a hidden bit $b$ and mask $R$ such that the decoder disagrees with $b$.
background
J-cost of a CNF formula under an assignment equals the number of unsatisfied clauses, hence zero precisely when the assignment satisfies the formula. CNFFormula packages a list of clauses together with a variable count; Assignment is a Boolean function on the $n$ variables. The local-blindness clause invokes the hidden-parity encoder that flips a random mask $R$ according to bit $b$ and the restrictor that projects any full word onto the queried index set $M$. The module sets this structure inside the unconditional dissolution path that distinguishes recognition time from Turing-machine overhead.
proof idea
One-line definition that packages three independent properties drawn from upstream results on satJCost bounds and the balanced-parity hiding construction.
why it matters
It supplies the dissolution structure instantiated by dissolution_holds and referenced inside PvsNPMasterCert. The module doc-comment positions it as the unconditional RS claim that P versus NP conflates recognition time (bounded by $n$) with TM simulation overhead, consistent with the framework's separation of J-cost from classical circuit size.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.