[ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/Head", "@graph": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU", "http://www.nanopub.org/nschema#hasAssertion": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/assertion" } ], "http://www.nanopub.org/nschema#hasProvenance": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/provenance" } ], "http://www.nanopub.org/nschema#hasPublicationInfo": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/pubinfo" } ], "@type": [ "http://www.nanopub.org/nschema#Nanopublication" ] } ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/provenance", "@graph": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/artifact-copy", "http://purl.org/dc/terms/date": [ { "@value": "2026-07-29", "@type": "http://www.w3.org/2001/XMLSchema#date" } ], "http://schema.org/contentUrl": [ { "@id": "https://raw.githubusercontent.com/johnmaxton/lean4-starter/main/Tarski.lean" } ], "http://schema.org/name": [ { "@value": "Retrieved copy of Tarski.lean" } ], "@type": [ "http://www.w3.org/ns/prov#Entity" ], "http://www.w3.org/2000/01/rdf-schema#comment": [ { "@value": "Retrieved from the main branch; no commit was pinned at retrieval time, so re-verification requires re-checking the ISCC and SHA-256 recorded in NP1 before trusting this result against a later state of the branch." } ], "http://www.w3.org/ns/prov#wasDerivedFrom": [ { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact" } ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/assertion", "http://www.w3.org/ns/prov#wasAttributedTo": [ { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude" } ], "http://www.w3.org/ns/prov#wasGeneratedBy": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/axiom-audit" }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0" }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0" } ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/axiom-audit", "http://www.w3.org/ns/prov#used": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-32-0" }, { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact" } ], "http://www.w3.org/ns/prov#wasAssociatedWith": [ { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude" } ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0", "http://www.w3.org/ns/prov#startedAtTime": [ { "@value": "2026-07-29T00:00:00Z", "@type": "http://www.w3.org/2001/XMLSchema#dateTime" } ], "http://www.w3.org/ns/prov#used": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-24-0" }, { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact" } ], "http://www.w3.org/ns/prov#wasAssociatedWith": [ { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude" } ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0", "http://www.w3.org/ns/prov#startedAtTime": [ { "@value": "2026-07-29T00:00:00Z", "@type": "http://www.w3.org/2001/XMLSchema#dateTime" } ], "http://www.w3.org/ns/prov#used": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-32-0" }, { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact" } ], "http://www.w3.org/ns/prov#wasAssociatedWith": [ { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude" } ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-32-0", "http://purl.org/dc/terms/identifier": [ { "@value": "8c9756b28d64dab099da31a4c09229a9e6a2ef35" } ], "http://schema.org/name": [ { "@value": "Lean 4.32.0 (x86_64-unknown-linux-gnu)" } ], "http://schema.org/softwareVersion": [ { "@value": "4.32.0" } ], "http://schema.org/url": [ { "@id": "https://github.com/leanprover/lean4/releases/tag/v4.32.0" } ], "@type": [ "http://schema.org/SoftwareApplication", "http://www.w3.org/ns/prov#Entity" ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-24-0", "http://purl.org/dc/terms/identifier": [ { "@value": "797c613eb9b6d4ec95db23e3e00af9ac6657f24b" } ], "http://schema.org/name": [ { "@value": "Lean 4.24.0 (x86_64-unknown-linux-gnu)" } ], "http://schema.org/softwareVersion": [ { "@value": "4.24.0" } ], "http://schema.org/url": [ { "@id": "https://github.com/leanprover/lean4/releases/tag/v4.24.0" } ], "@type": [ "http://schema.org/SoftwareApplication", "http://www.w3.org/ns/prov#Entity" ] } ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/pubinfo", "@graph": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU", "http://purl.org/dc/terms/created": [ { "@value": "2026-07-29T15:00:47Z", "@type": "http://www.w3.org/2001/XMLSchema#dateTime" } ], "http://purl.org/dc/terms/creator": [ { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton" } ], "http://purl.org/dc/terms/license": [ { "@id": "http://creativecommons.org/publicdomain/zero/1.0/" } ], "http://purl.org/dc/terms/relation": [ { "@id": "https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0" }, { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4" } ], "http://purl.org/nanopub/x/hasNanopubType": [ { "@id": "http://www.w3.org/ns/prov#Activity" } ], "http://www.w3.org/2000/01/rdf-schema#comment": [ { "@value": "This record supersedes the statement in earlier drafts that verification-by-compilation was unclaimed; it does not supersede the requirement for independent replication." } ], "http://www.w3.org/2000/01/rdf-schema#label": [ { "@value": "Tarski.lean: compilation verification under Lean 4.32.0 and 4.24.0" } ], "http://www.w3.org/ns/prov#wasAttributedTo": [ { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude" } ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/sig", "http://purl.org/nanopub/x/hasAlgorithm": [ { "@value": "RSA" } ], "http://purl.org/nanopub/x/hasPublicKey": [ { "@value": "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB" } ], "http://purl.org/nanopub/x/hasSignature": [ { "@value": "eMDXFadOqHjMhTZNn3myQj3YLd4Mbpzc0w42pkhUyP1mcVgjGszDbVPB8tGIX6/7/t8zjo5nuY2XF9cxAGK6V0Io/BVn2dmQs6vJfQkuLNPaaJ62t3eujVFQG8Vfx8/P3F+CdFOh1LBc6LTVI+GuTosqWBRvWycYw3KtLtAHu33mLJUMe3Gu4FHDZIlC7Yz3NweQG8jjLqxx+fKgz8YYk1X1mgQlN6PoJgKNicVHYeg95LcskuSL/Jrhx6tfWFXk0Pnkkk2Z3KySabFn6EWBwxaFO95I2N6Txj/ACpOi3qIAuGHTzqqPA8DKOL1l+aAp7LMWct/ZXOvNF6bJbTUDKw==" } ], "http://purl.org/nanopub/x/hasSignatureTarget": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU" } ], "http://purl.org/nanopub/x/signedBy": [ { "@id": "https://orcid.org/0000-0002-8042-4131" } ] } ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/assertion", "@graph": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/attr-verification", "http://purl.org/dc/terms/description": [ { "@value": "The validation role is claimed here by a software agent executing in an ephemeral sandbox, on behalf of and at the direction of the human agent named in NP1. This is a weaker claim than independent human replication or continuous integration, both of which remain outstanding; see the unclaimed-credit assertions in NP2." } ], "@type": [ "http://www.w3.org/ns/prov#Attribution" ], "http://www.w3.org/ns/prov#agent": [ { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude" } ], "http://www.w3.org/ns/prov#hadRole": [ { "@id": "https://credit.niso.org/contributor-roles/validation/" } ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/axiom-audit", "http://purl.org/dc/terms/description": [ { "@value": "For each of the 44 declarations obtained by scanning the source for top-level theorem and def bindings, a '#print axioms Synthetic.' command was appended to a copy of the file and elaborated under Lean 4.32.0. All 44 reported; sorryAx occurred zero times in the output." } ], "http://schema.org/name": [ { "@value": "Axiom dependency audit" } ], "@type": [ "http://www.w3.org/ns/prov#Activity" ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0", "http://purl.org/dc/terms/description": [ { "@value": "lean Tarski.lean; exit status 0; stdout and stderr empty. Toolchain commit 797c613eb9b6d4ec95db23e3e00af9ac6657f24b, x86_64-unknown-linux-gnu, Release build. Establishes that the result is not an artifact of a single compiler version." } ], "http://schema.org/name": [ { "@value": "Compilation under an earlier toolchain" } ], "http://schema.org/softwareVersion": [ { "@value": "Lean 4.24.0" } ], "@type": [ "http://www.w3.org/ns/prov#Activity" ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0", "http://purl.org/dc/terms/description": [ { "@value": "lean Tarski.lean; exit status 0; stdout and stderr empty. Toolchain leanprover/lean4:v4.32.0, commit 8c9756b28d64dab099da31a4c09229a9e6a2ef35, x86_64-unknown-linux-gnu, Release build. This is the version pinned by the lean-toolchain file of the hosting repository." } ], "http://schema.org/name": [ { "@value": "Compilation under the pinned toolchain" } ], "http://schema.org/softwareVersion": [ { "@value": "Lean 4.32.0" } ], "@type": [ "http://www.w3.org/ns/prov#Activity" ] }, { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/verification", "http://purl.org/dc/terms/date": [ { "@value": "2026-07-29", "@type": "http://www.w3.org/2001/XMLSchema#date" } ], "http://schema.org/about": [ { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact" } ], "http://schema.org/name": [ { "@value": "Tarski.lean compiles under Lean 4 with no errors and no unproved statements" } ], "http://schema.org/result": [ { "@value": "PASS" } ], "http://schema.org/text": [ { "@value": "The byte sequence identified by ISCC:KAC67GWDV372567ANMUX3VYVTO7YIYHV2AILIDWJV3VWCQK2KOB6QAY and SHA-256 1372181e2284465648cf15fdd9b7a761ceef9288224feccfd71fb63a5417bfd1 was submitted to the Lean 4 elaborator and kernel. The compiler exited with status 0 and emitted no diagnostics of any severity. An axiom audit over all 44 declarations in namespace Synthetic returned no dependency on sorryAx: 43 declarations depend only on the three standard Lean axioms propext, Classical.choice and Quot.sound, and Synthetic.construction_uniqueness depends on no axioms at all. The claim of zero sorry in the artifact's header comment is therefore confirmed, on two independent toolchain versions." } ], "@type": [ "http://schema.org/Claim", "http://www.w3.org/ns/prov#Entity" ], "http://www.w3.org/ns/prov#qualifiedAttribution": [ { "@id": "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/attr-verification" } ], "http://www.w3.org/ns/prov#wasDerivedFrom": [ { "@id": "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact" } ] } ] } ]