dissolution_holds
plain-language theorem explainer
dissolution_holds certifies the unconditional RS dissolution path for P versus NP by exhibiting the three required properties of the PvsNPDissolution structure. Complexity researchers comparing recognition time to Turing-machine simulation would cite it when separating R̂-polytime SAT from classical overhead. The proof is a direct term construction that populates each field by invoking the upstream recognition-time bound, the J-cost obstruction for unsatisfiability, and the adversarial parity failure lemma.
Claim. In the recognition structure, every satisfiable CNF formula on $n$ variables admits an assignment of zero J-cost reachable in at most $n$ recognition steps; every unsatisfiable formula has J-cost at least 1 for every assignment; and every local decoder on a proper subset of variables fails to recover the hidden global bit.
background
The module assembles two resolution paths for P versus NP. Path B (dissolution) is unconditional and rests on three properties collected in the PvsNPDissolution structure: R̂-polytime recognition for SAT formulas, a positive J-cost lower bound for UNSAT formulas, and local blindness under restricted decoders. The upstream theorem sat_recognition_time_bound states that the recognition time for a satisfiable formula is ≤ n (variable count). The upstream theorem unsat_cost_lower_bound states that for UNSAT formulas the minimum J-cost over all assignments is positive (bounded away from zero).
proof idea
Term-mode record construction. The rhat_polytime field is filled by the pair returned from sat_recognition_time_bound. The unsat_obstruction field is filled by unsat_cost_lower_bound. The local_blindness field is filled by BalancedParityHidden.adversarial_failure.
why it matters
This theorem supplies the unconditional dissolution argument (Path B) and is referenced by pvsNPMasterCert. It supports the claim that P versus NP conflates two distinct complexity measures by exhibiting polynomial R̂ recognition for SAT while preserving the obstruction for UNSAT. The result closes the assembly of the dissolution path without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.