PvsNPDissolution
plain-language theorem explainer
The PvsNPDissolution structure encodes the unconditional RS dissolution of P versus NP by requiring linear-step recognition of satisfying assignments for SAT formulas, a unit J-cost lower bound on all assignments to UNSAT formulas, and failure of any local decoder on masked parity encodings. Researchers assembling RS-native complexity certificates cite it when separating recognition time from Turing-machine simulation cost. The structure is populated by direct appeal to upstream satJCost bounds and the balanced parity hiding construction.
Claim. Let $f$ range over CNF formulas on $n$ variables and $a$ over assignments (maps from variables to truth values). The structure asserts: (i) every satisfiable $f$ admits steps $sleq n$ and assignment $a$ with J-cost zero; (ii) every unsatisfiable $f$ has J-cost at least 1 under every assignment; (iii) for any index set $M$ with $|M|<n$, no decoder on the restriction of a masked encoding recovers the hidden bit.
background
The module presents two resolution paths for P versus NP. Path B (dissolution) is unconditional and treats the classical question as a mismatch between recognition time and Turing-machine cost. Supporting definitions include Assignment as a map Fin n to Bool, CNFFormula as a list of clauses with var_count, and satJCost as the count of unsatisfied clauses under an assignment (hence zero exactly on satisfying assignments). The local blindness clause invokes the hidden mask encoder (bit b with mask R yields R or its negation) and its restriction to a queried index set.
proof idea
Structure definition with empty proof body. Fields are instantiated downstream by direct substitution of the recognition time bound for satisfiable formulas, the cost lower bound for unsatisfiable formulas, and the local blindness property of the parity hiding construction.
why it matters
Supplies the three axioms required by dissolution_holds and is embedded inside PvsNPMasterCert. It realizes the unconditional Path B of the module, which separates R-hat recognition time (linear for SAT) from TM simulation overhead and thereby dissolves the P versus NP distinction inside Recognition Science. No open scaffolding remains in the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.