K215: machine-checked PA and HA proofs (Metamath Zero)

K215: machine-checked PA and HA proofs (Metamath Zero) Two Metamath Zero (MM0) proof binaries for the K215 project, each with the specification it is checked against: HA: b6-out.mmb.zst (from b6-out.mmb), checked against b6-out.mm0. The specification is the intuitionistic foundation hpeano.mm0 (Heyting arithmetic, verbatim), the bounded (bd*) definitions, and the 7 Pi2 theorems below. Produced by the Route B translator (mm0-pa-ha b6) from the PA proof, then checked by mm0-c. PA: b4b_final.mmb.zst (from b4b_final.mmb), checked against b4b_final-joined.mm0, the joined specification of module b4b_final over the classical Peano foundation peano.mm0 (26 axioms; the check also confirms the binary uses no other axiom). What is proved in HA Exact text from b6-out.mm0 (each --| line is the spec's own comment): sigma1: K215 Theorem 1, halting -> inconsistency, as a Pi2 sentence. theorem K215_sigma1 {h w: nat}: $ A. h (bdK215Halt h -> E. w bdZfcBot w) $; sigma2: K215 Theorem 1, inconsistency -> halting, as a Pi2 sentence. theorem K215_sigma2 {h w: nat}: $ A. w (bdZfcBot w -> E. h bdK215Halt h) $; Theorem 2, (->): a ZFC proof of some value sentence gives a ZFC proof of falsity. theorem K215_thm2_pi2a {u w: nat}: $ A. u (bdBB215Prf u -> E. w bdZfcBot w) $; Theorem 2, (<-): a ZFC proof of falsity gives a ZFC proof of some value sentence. theorem K215_thm2_pi2b {w u: nat}: $ A. w (bdZfcBot w -> E. u bdBB215Prf u) $; Theorem 3, second conjunct (->): a halting run gives a ZFC proof of some value sentence. theorem K215_thm3_pi2a {h u: nat}: $ A. h (bdK215Halt h -> E. u bdBB215Prf u) $; Theorem 3, second conjunct (<-): a ZFC proof of some value sentence gives a halting run. theorem K215_thm3_pi2b {u h: nat}: $ A. u (bdBB215Prf u -> E. h bdK215Halt h) $; G2: a ZFC proof of Con(ZFC) gives a ZFC proof of falsity. theorem K215_G2_pi2 {u w: nat}: $ A. u (bdZfcConPrf u -> E. w bdZfcBot w) $; The meaning of bdK215Halt, bdZfcBot, bdBB215Prf and bdZfcConPrf is fixed by their defs in the same file (bounded arithmetic formulas: a halting run of the 215-state machine K215, a ZFC proof of falsity, a ZFC proof of a sentence BB(215) = b, a ZFC proof of Con(ZFC)). mm0-c checks every definition body and every axiom against the binary, so the statements mean exactly what the file says. What is proved in PA The PA specification b4b_final-joined.mm0 states (among its other public theorems) the checked theorems of the PA report: Theorem 2, (->): a ZFC proof of some value sentence gives a ZFC proof of falsity. theorem K215_thm2_pi2a {u w: nat}: $ A. u (bdBB215Prf u -> E. w bdZfcBot w) $; Theorem 3, second conjunct (->): a halting run gives a ZFC proof of some value sentence. theorem K215_thm3_pi2a {h u: nat}: $ A. h (bdK215Halt h -> E. u bdBB215Prf u) $; Theorem 3, second conjunct (<-): a ZFC proof of some value sentence gives a halting run. theorem K215_thm3_pi2b {u h: nat}: $ A. u (bdBB215Prf u -> E. h bdK215Halt h) $; G2: a ZFC proof of Con(ZFC) gives a ZFC proof of falsity. theorem K215_G2_pi2 {u w: nat}: $ A. u (bdZfcConPrf u -> E. w bdZfcBot w) $; How to verify Download every file of this record and check the hashes: sha256sum -c --ignore-missing SHA256SUMS (it lists the files as uploaded and also the decompressed .mmb files, which step 2 creates; run it again after step 2). MANIFEST.json has the same data with sizes. Decompress: zstd -d b6-out.mmb.zst and zstd -d b4b_final.mmb.zst and zstd -d b4b_final-joined.mm0.zst (zstd 1.4 or later; each file is one zstd frame with a content checksum). Build the checker. Stock mm0-c cannot hold these proofs (its fixed-size term/theorem tries and its 256-entry hypothesis and unification stacks overflow). The capacity3 build is upstream mm0-c plus two small patches that only enlarge tables and stacks (all overflow checks stay): upstream: https://github.com/digama0/mm0 at commit 0d414c0bfdaaeb7fea571895127abc1fa5a3d956, directory mm0-c/ (the seven .c files; their sha256 are in BUILD.md); apply mm0-c-capacity.patch (sha256 1ab54bfaa54a14e2eed982255e9daf2653d396abc16955b20cd53f0eada9d48e): heap-allocated tries and 64-bit file sizes; apply mm0-c-capacity3.patch (sha256 5858170062cc60c9b3f94ce9a8fa35fff85d92dfa9a4a1df4603e863e3ea2e6e): HYP_STACK_SIZE and UNIFY_STACK_SIZE 256 -> 4096; build in mm0-c/ (upstream builds with gcc main.c -O2 -o mm0-c; the project itself only built and ran the Windows binary). The pinned Windows build used w64devkit 2.10.0 (https://github.com/skeeto/w64devkit/releases/download/v2.10.0/w64devkit-x64-2.10.0.7z.exe, sha256 18d0a4c71a166f8401ab6305781bec5882b40b5e06ba9807c61cb5f3b3c6325e), a wrapper k215_build.c = #include <io.h> / #define eof mm0c_eof / #include "main.c" (MinGW's io.h declares eof()), and gcc k215_build.c -O2 -Wall -DWIN32 -Wl,--no-insert-timestamp -o mm0-c.exe, twice, with identical output; that binary has sha256 FAAE03337E4ED3C318538ACBDBB495D00B080EFAA690B8F0423009BBD8FC5A08 (BUILD.md, section capacity3; ha-report.json records it under tools). HA: mm0-c b6-out.mmb < b6-out.mm0 must exit 0. On the proof host this took 81 s and 17.80 GB peak memory (18.46 GB binary). PA: mm0-c b4b_final.mmb < b4b_final-joined.mm0 must exit 0. On the proof host this took 50 s and 12.05 GB peak memory (9.70 GB binary); it was run with the capacity2 build (first patch only, sha256 BBA77622E7540E3F68EB1CC0C202C1CFCDAA2C5BED01754EB0B86D143E4F6371), and capacity3 accepts it as well since it only enlarges two stacks. Controls (optional): replacing the conclusion of K215_G2_pi2 by F. in either spec must make mm0-c fail; both reports record that it did. Files Besides README.md, MANIFEST.json and SHA256SUMS: | file | bytes | sha256 | | --- | --- | --- | | `b6-out.mmb.zst` | 2848780293 | `c0a84a2a4d00669a382f0ef9872d65ed1cf484bf39afb0f6dc8c1fcdb396ba8c` | | `b4b_final.mmb.zst` | 1729855852 | `a16d0d9b62ab7803bfe162e8022115fbf053ffea6cf36951bb8d5e80bf8c2d9d` | | `b4b_final-joined.mm0.zst` | 16372947 | `8cc0566c33d877b8a438ae9c591799e0141018343bafa6f7a22f0ff5b2c341b6` | | `b6-out.mm0` | 976658 | `29b8a7c405c180afd21cd04ed40295a11975c45346ceb87a609590cf97176e26` | | `ha-report.json` | 9071 | `f389e484cf83da8c17eada720735a0129139a20a4e5edb237e109949a76b7db8` | | `pa-report.json` | 813492 | `b842c2ab7cf59ae07ef8394895cf1c056c2fa5586356c00a249281770d6a0038` | | `mm0-c-capacity.patch` | 2206 | `1ab54bfaa54a14e2eed982255e9daf2653d396abc16955b20cd53f0eada9d48e` | | `mm0-c-capacity3.patch` | 354 | `5858170062cc60c9b3f94ce9a8fa35fff85d92dfa9a4a1df4603e863e3ea2e6e` | | `BUILD.md` | 6806 | `3f5879fe31ab5eb2aa253ffc9bf3aa5aa77f9b2a4251e61c08c8808f74f88b35` | | `PINNED.md` | 938 | `fe1d29f547625dc2132de6050d2d3dfa720bb7fa7a91186f17416776f3147901` | Provenance HA run: job 00000-C-065-translate-b4b_final (host-release 48ac28ee474e0a127850f8c0fbf2dc6b3421b117, mm0-pa-ha c00de0d1fbd0f3976a9b0495cdeaa3d15ae2a39a, b6 sha256 7f6f7cd6408d21428385baa5aa1855f2328792656c651a4ee020e566c121f394). PA run: job 00000-C-059-link-check-b4b_final (k215-pa-mm0 snapshot 074f0dbc1c0b3640ceb634f3f71409bd1b1a7ebf, host-release fcf58fd3c80433653e3a936a41b55cb35b533577). PA spec source on the host: link-check work dir (joined spec). ha-report.json and pa-report.json are the runs' own reports (inputs, pins, timings, controls).