Mode A
Current file integrity
Compare the eighty-eight-page PDF, TeX source, status, and inventory against the exact release ledger. This identifies current bytes; it is not external validation of a theorem.
Check the published files or reproduce the formal build.
A quick browser check confirms that a report file matches its published hash. A full technical reproduction rebuilds Lean and regenerates the inventory and report. Neither shortcut turns missing mathematics into a proof.
Mode B
Compiled Lean reproduction
Build PNP, export the declaration inventory, verify its reviewed SHA-256 and theorem pins, then regenerate the publication status and report.
Browser check
Check the bundled report digest in your browser.
The console first loads the current release seal, then fetches the bundled canonical PDF, checks its byte count, and computes SHA-256 with the browser Web Crypto API. It checks file identity, not theorem correctness.
Mode A · file integrity
Canonical report file check
idle
- seal
downloads/release-seal.json - target
canonical_proof_report.pdf - ready
press Run check to load the seal, fetch the file, and compare
Expected SHA-256
loaded from release seal
Computed SHA-256
not run
Awaiting browser check.
This checks the current inventory-derived PDF against the published digest. It does not validate P = NP or discharge any current formal blocker.
Historical release identifiers
Sealed revision and artefact bundle.
These identifiers locate the historical report record. They do not override the current formal-reconstruction status or establish theorem correctness.
| Object | Identifier |
|---|---|
| Source/checker tag | final-pnp-proof-report-hardened-7072f8d |
| Source/checker commit | 7072f8d0bda6d44d240f9bb3fad624fd357e1278 |
| Sealed artefact tag | final-pnp-proof-report-artifacts-hardened-7072f8d-sealed |
| Artefact bundle | proof-artifacts/final-pnp-proof-report-hardened-7072f8d/ |
| Manifest | proof-artifacts/final-pnp-proof-report-hardened-7072f8d/release-seal.json |
| Checksum ledger | proof-artifacts/final-pnp-proof-report-hardened-7072f8d/SHA256SUMS |
| Bundled site manifest | downloads/release-seal.json |
| Bundled site checksum ledger | downloads/SHA256SUMS |
| Current public source | 63f38f39881dd8293e139b1687bf09688acb8e5d |
Commands
Current inventory and report flow.
Run from a clean checkout of the current Lean source repository.
git clone https://github.com/aisknab/pnp.git pnp-review cd pnp-review git checkout 63f38f39881dd8293e139b1687bf09688acb8e5d npm ci lake build PNP npm run pnp:verify -- --no-write npm run formal:inventory:check npm run formal:publication:check npm run report:check
Historical 57-page manuscript
What the legacy assertion checker reported.
Tag final-pnp-proof-report-hardened-7072f8d, commit 7072f8d0bda6d44d240f9bb3fad624fd357e1278, provenance archive/legacy-v0/ARCHIVE.json. Historical only.
Assertion-bearing report record
The historical record contains the string P = NP. Acceptance verifies record predicates, not the truth of that mathematical statement.
Historical linkage acceptance
The package, replay, certificate, audit, and gate records passed their implemented JavaScript predicates. This is not formal proof of their asserted propositions.
Canonical-byte discipline
Canonical-byte comparisons support historical artefact identity and drift detection. They do not provide theorem evidence.
Review checklist
Baseline checks for independent review.
Rebuild the reports
Run validation, compact report generation, and full report generation in a clean environment.
Inspect no-hidden-minimization
Confirm executable occurrences of hidden minimization symbols are rejected after macro and alias expansion.
Audit the mode firewall
Verify quotient equalities are not consumed as constructive full-mode replacements.
Check the final framework match
Confirm Package O and Package G use the same NAND syntax, output convention, charge convention, minimum-size notion, and slack definition.
Public source
Inspect the Lean repository directly.
The source, inventory generator, publication map, gate, and report generator are public. Use the review channel for findings or reproduction support.