K215 generic framework: machine-checked Theorem 2/3 and G2 for theories extending PA or ZFC (Metamath Zero)

K215 generic framework: machine-checked Theorem 2/3 and G2 for theories extending PA or ZFC (Metamath Zero) Two Metamath Zero (MM0) proof binaries of the K215 generic framework, each with the specification it is checked against. The source is in the public repository https://github.com/elliotglazer/k215-pa, directory generic/ (https://github.com/elliotglazer/k215-pa/tree/main/generic). This record is a supplement to the K215 record https://doi.org/10.5281/zenodo.23872595 ("K215: machine-checked PA and HA proofs (Metamath Zero)"), which it cross-references; it is a separate record, not a new version of that one. Theories extending PA (and PA itself): g2pa_inst-linked.mmb.zst (from g2pa_inst-linked.mmb), checked against g2pa_inst-linked.mm0 (gen7 job 00000-C-084-gen7-g2pa_inst, hand module gen7/g2pa_inst). Set theories extending ZFC: g2sf_spec-linked.mmb.zst (from g2sf_spec-linked.mmb), checked against g2sf_spec-linked.mm0 (gen7 job 00000-C-092-gen7-g2sf_spec, hand module gen7/g2sf_spec). Naming: G2_* are the second incompleteness theorem, BB_*_thm2 / BB_*_thm3 (and the _P forms, for an arbitrary provability predicate P with the derivability conditions) the K215 Theorems 2 and 3, each for every theory satisfying the stated hypotheses (hR, hZ, hM, hT1, hB, ...); the hypotheses are part of each statement. Trust base: the classical Peano foundation peano.mm0 (26 axioms). Each linked.mm0 declares exactly those 26 axioms and no others; the link job checked that the binary uses exactly these axioms (axioms.py: "mmb 26, spec 26, peano.mm0 26; spec axioms not in peano.mm0: 0"). Every other symbol in the statements below is a def whose body is in the same linked.mm0, and mm0-c checks every definition body and every axiom against the binary, so the statements mean exactly what the file says. What is proved: theories extending PA (and PA itself) Exact text from g2pa_inst-linked.mm0: G2_generic_pa theorem G2_generic_pa (R: nat) (hR: $ thIsSigma1Rec R $): $ ~paThInconsistent R -> ~paThProvable (paThAxSet R) (paThCon R) $; BB_generic_pa_thm2 theorem BB_generic_pa_thm2 (R m n M: nat) {b: nat} (hR: $ thIsSigma1Rec R $) (hM: $ tmValid m M $) (hmn: $ m <= n $) (hT1: $ tmHalts m M <-> paThInconsistent R $) (hB: $ bb215ProvabilityInternalBridge (paThPr R) (tmHaltsPA m M) $): $ ~paThInconsistent R <-> A. b ~paThProvable (paThAxSet R) (bbSentencePA n b) $; BB_generic_pa_thm3 theorem BB_generic_pa_thm3 (R m n M: nat) {b: nat} (hR: $ thIsSigma1Rec R $) (hM: $ tmValid m M $) (hmn: $ m <= n $) (hT1: $ tmHalts m M <-> paThInconsistent R $) (hB: $ bb215ProvabilityInternalBridge (paThPr R) (tmHaltsPA m M) $): $ (~paThInconsistent R <-> ~tmHalts m M) /\ (~tmHalts m M <-> A. b ~paThProvable (paThAxSet R) (bbSentencePA n b)) $; G2_pa theorem G2_pa: $ ~paProvable 0 paFormulaFalse -> ~paProvable 0 (paThCon paFormulaFalse) $; BB_pa_thm2 theorem BB_pa_thm2 (m n M: nat) {b: nat} (hM: $ tmValid m M $) (hmn: $ m <= n $) (hT1: $ tmHalts m M <-> paProvable 0 paFormulaFalse $) (hB: $ bb215ProvabilityInternalBridge (paThPr paFormulaFalse) (tmHaltsPA m M) $): $ ~paProvable 0 paFormulaFalse <-> A. b ~paProvable 0 (bbSentencePA n b) $; BB_pa_thm3 theorem BB_pa_thm3 (m n M: nat) {b: nat} (hM: $ tmValid m M $) (hmn: $ m <= n $) (hT1: $ tmHalts m M <-> paProvable 0 paFormulaFalse $) (hB: $ bb215ProvabilityInternalBridge (paThPr paFormulaFalse) (tmHaltsPA m M) $): $ (~paProvable 0 paFormulaFalse <-> ~tmHalts m M) /\ (~tmHalts m M <-> A. b ~paProvable 0 (bbSentencePA n b)) $; What is proved: set theories extending ZFC Exact text from g2sf_spec-linked.mm0: G2_generic_set theorem G2_generic_set (R: nat) (hR: $ thIsSigma1Rec R $) (hZ: $ thExtendsZFC R $): $ ~sfThInconsistent R -> ~sfThProvable R (paFormulaSource (sfThCon R)) $; BB_generic_set_thm2 theorem BB_generic_set_thm2 (R m n M: nat) {b: nat} (hR: $ thIsSigma1Rec R $) (hZ: $ thExtendsZFC R $) (hM: $ tmValid m M $) (hmn: $ m <= n $) (hT1: $ tmHalts m M <-> sfThInconsistent R $) (hB: $ bb215ProvabilityInternalBridge (sfThPr R) (tmHaltsPA m M) $): $ ~sfThInconsistent R <-> A. b ~sfThProvable R (bbSentenceSource n b) $; BB_generic_set_thm3 theorem BB_generic_set_thm3 (R m n M: nat) {b: nat} (hR: $ thIsSigma1Rec R $) (hZ: $ thExtendsZFC R $) (hM: $ tmValid m M $) (hmn: $ m <= n $) (hT1: $ tmHalts m M <-> sfThInconsistent R $) (hB: $ bb215ProvabilityInternalBridge (sfThPr R) (tmHaltsPA m M) $): $ (~sfThInconsistent R <-> ~tmHalts m M) /\ (~tmHalts m M <-> A. b ~sfThProvable R (bbSentenceSource n b)) $; BB_generic_set_thm2_P theorem BB_generic_set_thm2_P (A: set) (P G m n M: nat) {a b c: nat} (hA: $ zfcAxioms C_ A $) (hP: $ paFormulaBound 1 P $) (h1: $ A. c bb215ProvabilityD1T A bb215G2ASrc P c $) (h2: $ A. a A. b bb215ProvabilityD2 P a b $) (h3: $ A. a bb215ProvabilityD3 P a $) (hG: $ bb215ProvabilityFixedPoint P G $) (hM: $ tmValid m M $) (hmn: $ m <= n $) (hT1: $ tmHalts m M <-> sfTheoryProvable A sfBot $) (hB: $ bb215ProvabilityInternalBridge P (tmHaltsPA m M) $): $ ~sfTheoryProvable A sfBot <-> A. b ~sfTheoryProvable A (bbSentenceSource n b) $; BB_generic_set_thm3_P theorem BB_generic_set_thm3_P (A: set) (P G m n M: nat) {a b c: nat} (hA: $ zfcAxioms C_ A $) (hP: $ paFormulaBound 1 P $) (h1: $ A. c bb215ProvabilityD1T A bb215G2ASrc P c $) (h2: $ A. a A. b bb215ProvabilityD2 P a b $) (h3: $ A. a bb215ProvabilityD3 P a $) (hG: $ bb215ProvabilityFixedPoint P G $) (hM: $ tmValid m M $) (hmn: $ m <= n $) (hT1: $ tmHalts m M <-> sfTheoryProvable A sfBot $) (hB: $ bb215ProvabilityInternalBridge P (tmHaltsPA m M) $): $ (~sfTheoryProvable A sfBot <-> ~tmHalts m M) /\ (~tmHalts m M <-> A. b ~sfTheoryProvable A (bbSentenceSource n b)) $; 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 g2pa_inst-linked.mmb.zst and zstd -d g2sf_spec-linked.mmb.zst (zstd 1.4 or later; each file is one zstd frame with a content checksum). Build the checker used by the link jobs, the capacity2 build: upstream mm0-c (https://github.com/digama0/mm0 at commit 0d414c0bfdaaeb7fea571895127abc1fa5a3d956, directory mm0-c/) plus mm0-c-capacity.patch (sha256 1ab54bfaa54a14e2eed982255e9daf2653d396abc16955b20cd53f0eada9d48e), which only makes the term/theorem tries heap-allocated and file sizes 64-bit (all overflow checks stay). BUILD.md and PINNED.md give the build; the pinned Windows binary has sha256 BBA77622E7540E3F68EB1CC0C202C1CFCDAA2C5BED01754EB0B86D143E4F6371 (recorded under tools in each *-gen7.json). Theories extending PA (and PA itself): mm0-c g2pa_inst-linked.mmb < g2pa_inst-linked.mm0 must exit 0 (on the proof host: 2.0 s). Set theories extending ZFC: mm0-c g2sf_spec-linked.mmb < g2sf_spec-linked.mm0 must exit 0 (on the proof host: 4.0 s). Controls (optional): replacing the conclusion of the last theorem of either spec by F. must make mm0-c fail; both receipts record that it did (false_control_rc nonzero). Files Besides README.md, MANIFEST.json and SHA256SUMS: | file | bytes | sha256 | | --- | --- | --- | | `g2pa_inst-linked.mmb.zst` | 74510857 | `50bce360ed6a9116dbae9e90031800a7389237be3fbfab7d5d43d5083ff5b191` | | `g2sf_spec-linked.mmb.zst` | 155904052 | `4a8d67608724c3c5528cca1d8dd6e035c2c277549533f2e83ca2d62c23d5d6b9` | | `g2pa_inst-linked.mm0` | 691298 | `c3d21d95de9c4964dfcfb2dd06a97046d494d4f9612d6bfe5b34362fe3fdd82b` | | `g2pa_inst-gen7.json` | 8506 | `21c30739223d58feca36cc9441de850fd515aea9416e781e547575ffa48f7a83` | | `g2sf_spec-linked.mm0` | 627355 | `4ccab9bbf85f513eb83fa1ee11ebcf31c596df2e4bcad7e97401c9b7d80ca401` | | `g2sf_spec-gen7.json` | 9780 | `a509d153b1e8c30c776065204092c7a19daa3fa96ea39ab8fed5c614a95621d1` | | `mm0-c-capacity.patch` | 2206 | `1ab54bfaa54a14e2eed982255e9daf2653d396abc16955b20cd53f0eada9d48e` | | `BUILD.md` | 6806 | `3f5879fe31ab5eb2aa253ffc9bf3aa5aa77f9b2a4251e61c08c8808f74f88b35` | | `PINNED.md` | 938 | `fe1d29f547625dc2132de6050d2d3dfa720bb7fa7a91186f17416776f3147901` | Provenance g2pa_inst-linked.mmb: job 00000-C-084-gen7-g2pa_inst (host-release ab686036f8c05dbe21804e14fb478048fb1e5aad, k215-pa-mm0 snapshot 06e8c65e2ecfe0006b19db3ec207153467f9ecca, mm0-pa-ha 66c119af172faee8414ff49aaaefb0d265251111, finished 2026-11-02T03:04:05.1782745Z); linked.mm0 from the gen7 work dir. g2sf_spec-linked.mmb: job 00000-C-092-gen7-g2sf_spec (host-release ab686036f8c05dbe21804e14fb478048fb1e5aad, k215-pa-mm0 snapshot 06e8c65e2ecfe0006b19db3ec207153467f9ecca, mm0-pa-ha 66c119af172faee8414ff49aaaefb0d265251111, finished 2026-11-02T04:58:16.3145846Z); linked.mm0 from the gen7 work dir. *-gen7.json are the link jobs' own receipts (steps, return codes, sha256 and sizes, tools).