Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ ZENODOarrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Preprint . 2026
License: CC BY
Data sources: ZENODO
addClaim

P = NP, A Proof That Travels: Receipt-Based Verification by Transport, Not Search

Authors: Figurelli, Rogério;

P = NP, A Proof That Travels: Receipt-Based Verification by Transport, Not Search

Abstract

When claims become long, toolchain-dependent, numerically mediated, or operationally complex, “accepted by consensus” stops being sufficient as a closure mode: trust must travel. This paper specifies a receipt-based protocol for transporting verification of candidate P vs NP artifacts across machines, institutions, and time, without relying on hidden environments, informal assumptions, or non-replayable judgment calls. The protocol enforces canonicalization of inputs and transformations; explicit move ledgers (receipts) with hash-chaining; admissibility rules that separate untrusted context from action; a numeric policy that certifies only consumed values (otherwise halting with a typed, checkable HOLD-certificate); and terminal anchoring in widely checkable clausal certificates (SAT witnesses and UNSAT DRAT/LRAT). The result is a governance-grade verification contract: either a claim closes under replayable receipts and bounded resources, or the system halts with a typed, checkable HOLD that localizes the missing obligation. Failure becomes a transportable scientific object. This manuscript additionally provides (i) a typed HOLD taxonomy with per-type receipt schemas, (ii) an operational refutation budget parameter B(·), (iii) a canonical attempt policy object, (iv) explicit schema objects that bind validation rules to object types, and (v) an end-to-end anchored soundness statement for receipt acceptance. 

Keywords

certified computation, verification governance, P = NP, canonicalization, SAT, transportability, reproducibility, P vs NP

Powered by OpenAIRE graph
Found an issue? Give us feedback