https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE
.trig | .trig.txt | .jelly | .jelly.txt | .jsonld | .jsonld.txt | .nq | .nq.txt | .xml | .xml.txt
@prefix this: <https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE> .
@prefix sub: <https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE/> .
@prefix np: <http://www.nanopub.org/nschema#> .
@prefix dct: <http://purl.org/dc/terms/> .
@prefix d: <https://provenance.example/tarski-lean/> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix orcid: <https://orcid.org/> .
@prefix prov: <http://www.w3.org/ns/prov#> .
@prefix npx: <http://purl.org/nanopub/x/> .
sub:Head {
this: a np:Nanopublication;
np:hasAssertion sub:assertion;
np:hasProvenance sub:provenance;
np:hasPublicationInfo sub:pubinfo .
}
sub:assertion {
d:artifact-Tarski-lean a d:SourceCodeArtifact;
dct:identifier "https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/Tarski.lean";
rdfs:label "Tarski.lean";
d:atCommit "802b1d583032c44ea9affb2a61b0c8cda6c60b72";
d:axiomDependentDeclarationCount "9"^^xsd:integer;
d:axiomDependentDeclarationsUseAxioms "propext, Classical.choice, Quot.sound";
d:axiomFreeDeclarationCount "36"^^xsd:integer;
d:compilationResult "Build completed successfully (3 jobs); target Tarski built without error";
d:compilationStatus d:Compiled;
d:compilationTool "elan 4.2.3 / Lean (version 4.32.0, arm64-apple-darwin24.6.0, commit 8c9756b28d64dab099da31a4c09229a9e6a2ef35, Release) / lake build";
d:declarationCount "45"^^xsd:integer;
d:fileSizeBytes "29024"^^xsd:integer;
d:fromRepository <https://github.com/johnmaxton/lean4-starter>;
d:gitBlobSha1Hex "da7557b355045d2b0b16c5d5eca90a2db029e253";
d:gitBlobVerification "git hash-object on the fetched bytes reproduced GitHub's own stored blob SHA-1 exactly, independently confirming the fetched bytes match the repository's record for this path at this commit";
d:hasNoImportStatements "true"^^xsd:boolean;
d:independentCiConclusion "success";
d:independentCiConfirmation <https://github.com/johnmaxton/lean4-starter/actions/runs/31168537874>;
d:isccCombinedCode "ISCC:KYCO7GWDV372567AMDK5AEFUB3E24SRQZYC6ZHAET4";
d:isccComputedWith "iscc-core Python package v1.3.0 (ISO 24138 reference implementation)";
d:isccDataCode "ISCC:GAAWBVOQCC2A5SNO";
d:isccInstanceCode "ISCC:IAAUUMGOAXWJYBE7";
d:isccInstanceDatahash "1e204a30ce05ec9c049fb543feb1af45c4b9fa70452950b4ce36538c69598a7ca7b8";
d:isccMetaCode "ISCC:AAA67GWDV372567A";
d:lakeManifestExternalPackageCount "0"^^xsd:integer;
d:leanToolchain "leanprover/lean4:v4.32.0";
d:lineCount "663"^^xsd:integer;
d:sha256Hex "928b0c859d95f02ce5b8dcba197ec0ec01d67f22b6588742842de4fa2d41ceac";
d:sorryAxCount "0"^^xsd:integer .
d:decl-Col a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.Col";
d:sourceLine "273"^^xsd:integer .
d:decl-Cong3 a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.Cong3";
d:sourceLine "391"^^xsd:integer .
d:decl-Midpoint a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.Midpoint";
d:sourceLine "345"^^xsd:integer .
d:decl-Out a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.Out";
d:sourceLine "276"^^xsd:integer .
d:decl-SegLe a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.SegLe";
d:sourceLine "280"^^xsd:integer .
d:decl-betw_col a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.betw_col";
d:sourceLine "282"^^xsd:integer .
d:decl-betw_exchange2 a d:AuditedDeclaration;
d:axiomAuditResult "propext, Classical.choice, Quot.sound";
d:qualifiedName "Synthetic.betw_exchange2";
d:sourceLine "259"^^xsd:integer .
d:decl-betw_exchange_left a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.betw_exchange_left";
d:sourceLine "230"^^xsd:integer .
d:decl-betw_inner_trans a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.betw_inner_trans";
d:sourceLine "220"^^xsd:integer .
d:decl-betw_left_trivial a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.betw_left_trivial";
d:sourceLine "215"^^xsd:integer .
d:decl-betw_outer_trans a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.betw_outer_trans";
d:sourceLine "238"^^xsd:integer .
d:decl-betw_outer_trans-prime a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.betw_outer_trans'";
d:sourceLine "251"^^xsd:integer .
d:decl-betw_symm a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.betw_symm";
d:sourceLine "207"^^xsd:integer .
d:decl-betw_transfer a d:AuditedDeclaration;
d:axiomAuditResult "propext, Classical.choice, Quot.sound";
d:qualifiedName "Synthetic.betw_transfer";
d:sourceLine "494"^^xsd:integer .
d:decl-betw_trivial a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.betw_trivial";
d:sourceLine "198"^^xsd:integer .
d:decl-col_rotate a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.col_rotate";
d:sourceLine "286"^^xsd:integer .
d:decl-col_swap a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.col_swap";
d:sourceLine "296"^^xsd:integer .
d:decl-col_trivial_left a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.col_trivial_left";
d:sourceLine "304"^^xsd:integer .
d:decl-col_trivial_mid a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.col_trivial_mid";
d:sourceLine "310"^^xsd:integer .
d:decl-col_trivial_right a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.col_trivial_right";
d:sourceLine "307"^^xsd:integer .
d:decl-cong3_construction a d:AuditedDeclaration;
d:axiomAuditResult "propext, Classical.choice, Quot.sound";
d:qualifiedName "Synthetic.cong3_construction";
d:sourceLine "455"^^xsd:integer .
d:decl-cong_add a d:AuditedDeclaration;
d:axiomAuditResult "propext, Classical.choice, Quot.sound";
d:qualifiedName "Synthetic.cong_add";
d:sourceLine "162"^^xsd:integer .
d:decl-cong_comm a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.cong_comm";
d:sourceLine "143"^^xsd:integer .
d:decl-cong_left_comm a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.cong_left_comm";
d:sourceLine "135"^^xsd:integer .
d:decl-cong_refl a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.cong_refl";
d:sourceLine "122"^^xsd:integer .
d:decl-cong_reverse_identity a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.cong_reverse_identity";
d:sourceLine "156"^^xsd:integer .
d:decl-cong_right_comm a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.cong_right_comm";
d:sourceLine "139"^^xsd:integer .
d:decl-cong_sub a d:AuditedDeclaration;
d:axiomAuditResult "propext, Classical.choice, Quot.sound";
d:qualifiedName "Synthetic.cong_sub";
d:sourceLine "441"^^xsd:integer .
d:decl-cong_symm a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.cong_symm";
d:sourceLine "126"^^xsd:integer .
d:decl-cong_trans a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.cong_trans";
d:sourceLine "130"^^xsd:integer .
d:decl-cong_trivial a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.cong_trivial";
d:sourceLine "148"^^xsd:integer .
d:decl-construction_uniqueness a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.construction_uniqueness";
d:sourceLine "180"^^xsd:integer .
d:decl-inner_five_segment a d:AuditedDeclaration;
d:axiomAuditResult "propext, Classical.choice, Quot.sound";
d:qualifiedName "Synthetic.inner_five_segment";
d:sourceLine "403"^^xsd:integer .
d:decl-midpoint_refl a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.midpoint_refl";
d:sourceLine "347"^^xsd:integer .
d:decl-midpoint_symm a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.midpoint_symm";
d:sourceLine "350"^^xsd:integer .
d:decl-out_col a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.out_col";
d:sourceLine "322"^^xsd:integer .
d:decl-out_symm a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.out_symm";
d:sourceLine "316"^^xsd:integer .
d:decl-out_trivial a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.out_trivial";
d:sourceLine "313"^^xsd:integer .
d:decl-reflect_betw a d:AuditedDeclaration;
d:axiomAuditResult "propext, Classical.choice, Quot.sound";
d:qualifiedName "Synthetic.reflect_betw";
d:sourceLine "642"^^xsd:integer .
d:decl-reflect_cong a d:AuditedDeclaration;
d:axiomAuditResult "propext, Classical.choice, Quot.sound";
d:qualifiedName "Synthetic.reflect_cong";
d:sourceLine "541"^^xsd:integer .
d:decl-segle_nil a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.segle_nil";
d:sourceLine "331"^^xsd:integer .
d:decl-segle_of_cong a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.segle_of_cong";
d:sourceLine "334"^^xsd:integer .
d:decl-segle_refl a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.segle_refl";
d:sourceLine "327"^^xsd:integer .
d:decl-symmetric_point_exists a d:AuditedDeclaration;
d:axiomAuditResult "no axioms";
d:qualifiedName "Synthetic.symmetric_point_exists";
d:sourceLine "355"^^xsd:integer .
d:decl-symmetric_point_uniqueness a d:AuditedDeclaration;
d:axiomAuditResult "propext, Classical.choice, Quot.sound";
d:qualifiedName "Synthetic.symmetric_point_uniqueness";
d:sourceLine "362"^^xsd:integer .
}
sub:provenance {
d:activity-retrieve-execute a prov:Activity;
rdfs:label "Retrieve artifact, hash it, compute ISCC, install/run Lean toolchain, audit axioms";
prov:generated d:artifact-Tarski-lean;
prov:used <https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/Tarski.lean>;
prov:wasAssociatedWith d:agent-claude-sonnet-5 .
d:agent-claude-sonnet-5 a prov:SoftwareAgent;
rdfs:label "Claude Sonnet 5 (Anthropic), running as Claude Code" .
sub:assertion dct:description "Every statement in this assertion graph was produced by running a tool against the artifact's actual bytes in this session: curl (retrieval), git hash-object and shasum (hashing), python3 iscc-core v1.3.0 (ISCC), and elan/lean/lake 4.32.0 (compilation + '#print axioms' over every declaration extracted from the file by grep). None of it is recalled from training data.";
prov:wasDerivedFrom <https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/Tarski.lean>;
prov:wasGeneratedBy d:activity-retrieve-execute .
}
sub:pubinfo {
this: dct:created "2026-08-10T12:57:30Z"^^xsd:dateTime;
dct:creator orcid:0000-0002-8042-4131;
dct:license <https://creativecommons.org/licenses/by/4.0/>;
rdfs:label "Tarski.lean: retrieval, hashing, ISCC, compilation, axiom audit (machine-verified)";
d:verificationBucket d:MachineVerified .
sub:sig npx:hasAlgorithm "RSA";
npx:hasPublicKey "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB";
npx:hasSignature "lG+p0162FcytbbLIJ1p3p+xmYhYHqk9I88NdkxctC5vWiPYmse3t84cB/SgE6xv3fswpjlSKQSPGcOZy44eJzU4arQR+2qLTtxp8B/T+Pe0K1ktll+WQ0PW40NwwmokRC4xyqZBoQXFVj7YthCa8TcmLsRXhcsyBzVTQakjAZitFY4ZD+M7cyGHrnVF7By+pd7y3B5VQEealqE9oSljku3qCm+EHqP00p3HWgWf4QDvhSRV8BX8TnWBV0cwZ2LDWhFsBoWiwmwGUh5MR1qg10Fb8EWGJBABLF1w2X2zFBNjZDxpkM5YYZJ7Do/Hc8ryIOzxYjFSRPUFjghqdGtjGhQ==";
npx:hasSignatureTarget this:;
npx:signedBy orcid:0000-0002-8042-4131 .
}