https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/Head https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://www.nanopub.org/nschema#hasAssertion https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/assertion https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://www.nanopub.org/nschema#hasProvenance https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/provenance https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://www.nanopub.org/nschema#hasPublicationInfo https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/pubinfo https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.nanopub.org/nschema#Nanopublication https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/assertion https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/attr-verification http://purl.org/dc/terms/description 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. https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/attr-verification http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Attribution https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/attr-verification http://www.w3.org/ns/prov#agent https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/attr-verification http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/validation/ https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/axiom-audit http://purl.org/dc/terms/description For each of the 44 declarations obtained by scanning the source for top-level theorem and def bindings, a '#print axioms Synthetic.<name>' 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. https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/axiom-audit http://schema.org/name Axiom dependency audit https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/axiom-audit http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0 http://purl.org/dc/terms/description 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. https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0 http://schema.org/name Compilation under an earlier toolchain https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0 http://schema.org/softwareVersion Lean 4.24.0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0 http://purl.org/dc/terms/description 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. https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0 http://schema.org/name Compilation under the pinned toolchain https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0 http://schema.org/softwareVersion Lean 4.32.0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/verification http://purl.org/dc/terms/date 2026-07-29 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/verification http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/verification http://schema.org/name Tarski.lean compiles under Lean 4 with no errors and no unproved statements https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/verification http://schema.org/result PASS https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/verification http://schema.org/text 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. https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/verification http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/verification http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/verification http://www.w3.org/ns/prov#qualifiedAttribution https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/attr-verification https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/verification http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/provenance https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/artifact-copy http://purl.org/dc/terms/date 2026-07-29 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/artifact-copy http://schema.org/contentUrl https://raw.githubusercontent.com/johnmaxton/lean4-starter/main/Tarski.lean https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/artifact-copy http://schema.org/name Retrieved copy of Tarski.lean https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/artifact-copy http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/artifact-copy http://www.w3.org/2000/01/rdf-schema#comment 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. https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/artifact-copy http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/assertion http://www.w3.org/ns/prov#wasAttributedTo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/assertion http://www.w3.org/ns/prov#wasGeneratedBy https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/axiom-audit https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/assertion http://www.w3.org/ns/prov#wasGeneratedBy https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/assertion http://www.w3.org/ns/prov#wasGeneratedBy https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/axiom-audit http://www.w3.org/ns/prov#used https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-32-0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/axiom-audit http://www.w3.org/ns/prov#used https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/axiom-audit http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0 http://www.w3.org/ns/prov#startedAtTime 2026-07-29T00:00:00Z https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0 http://www.w3.org/ns/prov#used https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-24-0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0 http://www.w3.org/ns/prov#used https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-24-0 http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0 http://www.w3.org/ns/prov#startedAtTime 2026-07-29T00:00:00Z https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0 http://www.w3.org/ns/prov#used https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-32-0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0 http://www.w3.org/ns/prov#used https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/run-4-32-0 http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-24-0 http://purl.org/dc/terms/identifier 797c613eb9b6d4ec95db23e3e00af9ac6657f24b https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-24-0 http://schema.org/name Lean 4.24.0 (x86_64-unknown-linux-gnu) https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-24-0 http://schema.org/softwareVersion 4.24.0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-24-0 http://schema.org/url https://github.com/leanprover/lean4/releases/tag/v4.24.0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-24-0 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/SoftwareApplication https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-24-0 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-32-0 http://purl.org/dc/terms/identifier 8c9756b28d64dab099da31a4c09229a9e6a2ef35 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-32-0 http://schema.org/name Lean 4.32.0 (x86_64-unknown-linux-gnu) https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-32-0 http://schema.org/softwareVersion 4.32.0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-32-0 http://schema.org/url https://github.com/leanprover/lean4/releases/tag/v4.32.0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-32-0 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/SoftwareApplication https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/toolchain-4-32-0 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/pubinfo https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://purl.org/dc/terms/created 2026-07-29T15:00:47Z https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://purl.org/dc/terms/creator https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://purl.org/dc/terms/license http://creativecommons.org/publicdomain/zero/1.0/ https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://purl.org/dc/terms/relation https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://purl.org/dc/terms/relation https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://purl.org/nanopub/x/hasNanopubType http://www.w3.org/ns/prov#Activity https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://www.w3.org/2000/01/rdf-schema#comment This record supersedes the statement in earlier drafts that verification-by-compilation was unclaimed; it does not supersede the requirement for independent replication. https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://www.w3.org/2000/01/rdf-schema#label Tarski.lean: compilation verification under Lean 4.32.0 and 4.24.0 https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU http://www.w3.org/ns/prov#wasAttributedTo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/sig http://purl.org/nanopub/x/hasAlgorithm RSA https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/sig http://purl.org/nanopub/x/hasPublicKey MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/sig http://purl.org/nanopub/x/hasSignature eMDXFadOqHjMhTZNn3myQj3YLd4Mbpzc0w42pkhUyP1mcVgjGszDbVPB8tGIX6/7/t8zjo5nuY2XF9cxAGK6V0Io/BVn2dmQs6vJfQkuLNPaaJ62t3eujVFQG8Vfx8/P3F+CdFOh1LBc6LTVI+GuTosqWBRvWycYw3KtLtAHu33mLJUMe3Gu4FHDZIlC7Yz3NweQG8jjLqxx+fKgz8YYk1X1mgQlN6PoJgKNicVHYeg95LcskuSL/Jrhx6tfWFXk0Pnkkk2Z3KySabFn6EWBwxaFO95I2N6Txj/ACpOi3qIAuGHTzqqPA8DKOL1l+aAp7LMWct/ZXOvNF6bJbTUDKw== https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/sig http://purl.org/nanopub/x/hasSignatureTarget https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/sig http://purl.org/nanopub/x/signedBy https://orcid.org/0000-0002-8042-4131