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