@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 .
}