dissolution_holds
plain-language theorem explainer
The dissolution_holds theorem verifies the three axioms of the RS dissolution structure for the P versus NP problem by confirming polynomial recognition time for SAT instances, a positive J-cost obstruction for UNSAT formulas, and local blindness under partial decoders. Complexity researchers working in the Recognition Science framework cite it for the unconditional dissolution route that separates recognition measures from Turing-machine simulation. The proof is a direct term-mode assembly that supplies each field of the target structure from
Claim. The dissolution theorem asserts that 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$ and satJCost$(f,a)=0$; if $f$ is unsatisfiable then satJCost$(f,a)$ is at least 1 for every assignment $a$; and for every proper subset $M$ of the $n$ variables and every decoder from the restricted domain to Bool, there exist a hidden bit $b$ and full assignment $R$ such that the decoder disagrees with $b$ on the balanced-parity encoding of $b$ and $R$.
background
In the P vs NP Assembly module the dissolution path supplies an unconditional argument that the classical P versus NP question conflates two distinct complexity measures. The central definitions are satJCost, the natural-number length of unsatisfied clauses after recognition, and the recognition time bound that counts steps until zero J-cost is reached. The structure PvsNPDissolution packages three properties: polynomial-time recognition for satisfiable formulas, a strict positive lower bound on J-cost for unsatisfiable formulas, and local blindness for any decoder that sees only a proper subset of variables.
proof idea
The proof is a term-mode construction that directly populates the three fields of PvsNPDissolution. The rhat_polytime field invokes sat_recognition_time_bound to extract the witness steps and assignment. The unsat_obstruction field applies unsat_cost_lower_bound to obtain the positive J-cost guarantee. The local_blindness field delegates to BalancedParityHidden.adversarial_failure on the given subset and decoder.
why it matters
This theorem completes the unconditional dissolution path inside the P vs NP assembly and supplies the missing piece for the master certificate pvsNPMasterCert. It realizes the RS claim that recognition time for SAT is linear while Turing-machine simulation incurs structural overhead, thereby dissolving the classical question rather than resolving it via circuit lower bounds. The result sits downstream of the recognition-time and J-cost bounds and upstream of any global complexity certificate that invokes the dissolution route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.