https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/Head https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk http://www.nanopub.org/nschema#hasAssertion https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/assertion https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk http://www.nanopub.org/nschema#hasProvenance https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/provenance https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk http://www.nanopub.org/nschema#hasPublicationInfo https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/pubinfo https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.nanopub.org/nschema#Nanopublication https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/assertion https://provenance.example/tarski-lean/artifact-Tarski-lean http://purl.org/dc/terms/license http://www.apache.org/licenses/LICENSE-2.0 https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/authorIdentityBinding https://orcid.org/0000-0002-8042-4131 https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/commitAuthorEmail myle54xton@gmail.com https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/commitAuthorName Myles Axton https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/commitDate 2026-08-07T10:03:56Z https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/commitMessage Add copyright and license information to Tarski.lean https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/commitSha 802b1d583032c44ea9affb2a61b0c8cda6c60b72 https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/copyrightLineQuoted Copyright 2026 John Myles Axton orcid:0000-0002-8042-4131 https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/copyrightLineSourceLocation Tarski.lean, line 2 (top-of-file comment block) https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/hasNamespace Synthetic (Lean namespace; declarations are qualified as Synthetic.<name>, e.g. Synthetic.cong_refl) https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/licenseEvidence Two independent, mutually consistent sources: (1) the file's own header states 'Licensed under the Apache License, Version 2.0'; (2) the GitHub repository API (api.github.com/repos/johnmaxton/lean4-starter) reports license.spdx_id = 'Apache-2.0', backed by a LICENSE file at repo root matching the standard Apache 2.0 text. https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/priorCommitDate 2026-07-18T14:18:18Z https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/priorCommitMessage Add Tarski's synthetic Euclidean geometry (Stages 0-4) https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/priorCommitSha 90018aec70b2bb8950c1045cac443731825d79ef https://provenance.example/tarski-lean/cite-dependency-free http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/CheckedClaim https://provenance.example/tarski-lean/cite-dependency-free http://www.w3.org/2000/01/rdf-schema#label File is dependency-free (compiles with core Lean 4 alone, no Mathlib) https://provenance.example/tarski-lean/cite-dependency-free https://provenance.example/tarski-lean/asClaimedByArtifact This file is dependency-free: it compiles with core Lean 4 alone (`lean Tarski.lean`), no Mathlib required. https://provenance.example/tarski-lean/cite-dependency-free https://provenance.example/tarski-lean/verificationMethod grep for '^import' in Tarski.lean returned zero matches; lake-manifest.json at the pinned commit lists packages: [] (zero external dependencies); the successful build in NP-A used only this manifest. https://provenance.example/tarski-lean/cite-dependency-free https://provenance.example/tarski-lean/verificationResult CONFIRMED (this claim is machine-verifiable and is additionally recorded in NP-A's compilation evidence). https://provenance.example/tarski-lean/cite-geocoq-authors http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/CheckedCitation https://provenance.example/tarski-lean/cite-geocoq-authors http://www.w3.org/2000/01/rdf-schema#label GeoCoq project authorship https://provenance.example/tarski-lean/cite-geocoq-authors https://provenance.example/tarski-lean/asClaimedByArtifact GeoCoq (J. Narboux, M. Beeson, P. Boutry, G. Braun, C. Gries, P. Schreck, et al.): the first machine-checked ascent. https://provenance.example/tarski-lean/cite-geocoq-authors https://provenance.example/tarski-lean/verificationNote The repo's top-level AUTHORS file lists Beeson, Boutry, Braun, Gries, Kastenbaum, Narboux (omitting Schreck); the coq-geocoq-axioms.opam package metadata's authors field lists exactly Beeson, Braun, Boutry, Gries, Narboux, Schreck -- matching the artifact's six named credits verbatim. Both sources were checked; the opam file is the one that fully confirms the claim as written. https://provenance.example/tarski-lean/cite-geocoq-authors https://provenance.example/tarski-lean/verifiedAgainst https://raw.githubusercontent.com/GeoCoq/GeoCoq/master/coq-geocoq-axioms.opam https://provenance.example/tarski-lean/cite-geocoq-l7_13 http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/CheckedCitation https://provenance.example/tarski-lean/cite-geocoq-l7_13 http://www.w3.org/2000/01/rdf-schema#label GeoCoq lemma l7_13 corresponds to SST chapter 7 (midpoint / point reflection) https://provenance.example/tarski-lean/cite-geocoq-l7_13 https://provenance.example/tarski-lean/asClaimedByArtifact The capstone is SST 7.13 (GeoCoq l7_13): point reflection preserves congruence. https://provenance.example/tarski-lean/cite-geocoq-l7_13 https://provenance.example/tarski-lean/verificationNote GeoCoq's official documentation page confirms l7_13 is defined in the Ch07_midpoint module and concerns congruence preservation under point-reflection/midpoint symmetry, consistent with the artifact's claim that it corresponds to SST theorem 7.13. This is a spot-check of one specific chapter/lemma pairing, not a verification of every 'SST n.m' tag in the file (see NP-D). https://provenance.example/tarski-lean/cite-geocoq-l7_13 https://provenance.example/tarski-lean/verifiedAgainst https://geocoq.github.io/GeoCoq/html/GeoCoq.Tarski_dev.Ch07_midpoint.html https://provenance.example/tarski-lean/cite-sst-1983 http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/CheckedCitation https://provenance.example/tarski-lean/cite-sst-1983 http://www.w3.org/2000/01/rdf-schema#label Schwabhäuser, Szmielew, Tarski, "Metamathematische Methoden in der Geometrie", Springer-Verlag, Berlin, 1983 https://provenance.example/tarski-lean/cite-sst-1983 https://provenance.example/tarski-lean/asClaimedByArtifact W. Schwabhäuser: completed and published SST (1983); the "SST n.m" tags cite all three authors. https://provenance.example/tarski-lean/cite-sst-1983 https://provenance.example/tarski-lean/verificationNote Title, three authors, publisher, and 1983 date confirmed via Springer Link and a Journal of Symbolic Logic review. Chapter-by-chapter content of the book was NOT opened or checked against the artifact's per-stage chapter tags (see NP-D, negative space) except for the single spot-check in d:cite-geocoq-l7_13 below. https://provenance.example/tarski-lean/cite-sst-1983 https://provenance.example/tarski-lean/verifiedAgainst https://link.springer.com/book/10.1007/978-3-642-69418-9 https://provenance.example/tarski-lean/cite-sst-1983 https://provenance.example/tarski-lean/verifiedAgainst https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/wolfram-schwabhauser-wanda-szmielew-and-alfred-tarski-ein-axiomatischer-aujbau-der-euklidischen-geometrie-metamathematische-methoden-in-der-geometrie-hochschultext-springerverlag-berlin-etc-1983-pp-1171-wolfram-schwabhauser-metamathematische-betrachtungen-metamathematische-methoden-in-der-geometrie-pp-173457/47332AEED25CD5AB54C9A989C7D1718B https://provenance.example/tarski-lean/cite-tarski-givant-1999 http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/CheckedCitation https://provenance.example/tarski-lean/cite-tarski-givant-1999 http://www.w3.org/2000/01/rdf-schema#label Tarski & Givant, "Tarski's System of Geometry", Bulletin of Symbolic Logic, vol. 5, no. 2, pp. 175-214, 1999 https://provenance.example/tarski-lean/cite-tarski-givant-1999 https://provenance.example/tarski-lean/asClaimedByArtifact A. Tarski (1926-27; Tarski & Givant, BSL 1999): the axiom system and the completeness/decidability metatheorems. https://provenance.example/tarski-lean/cite-tarski-givant-1999 https://provenance.example/tarski-lean/verificationNote Publication venue, volume, issue, and page range (175-214) confirmed as consistent across PhilPapers, Semantic Scholar, and Cambridge Core listings. https://provenance.example/tarski-lean/cite-tarski-givant-1999 https://provenance.example/tarski-lean/verifiedAgainst https://philpapers.org/rec/TARTSO https://provenance.example/tarski-lean/cite-tarski-givant-1999 https://provenance.example/tarski-lean/verifiedAgainst https://www.semanticscholar.org/paper/Tarski's-System-of-Geometry-Tarski-Givant/f9dc27b0f3f9436f0b194ecc6f558a74d346e0e6 https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/provenance https://provenance.example/tarski-lean/activity-ground http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://provenance.example/tarski-lean/activity-ground http://www.w3.org/2000/01/rdf-schema#label Build theorem-to-source concordance; check external historical/authorship claims against citable sources https://provenance.example/tarski-lean/activity-ground http://www.w3.org/ns/prov#wasAssociatedWith https://provenance.example/tarski-lean/agent-claude-sonnet-5 https://provenance.example/tarski-lean/agent-claude-sonnet-5 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#SoftwareAgent https://provenance.example/tarski-lean/agent-claude-sonnet-5 http://www.w3.org/2000/01/rdf-schema#label Claude Sonnet 5 (Anthropic), running as Claude Code https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/assertion http://purl.org/dc/terms/description Each statement here was checked against a specific, cited, dereferenceable external document during this session (via HTTP fetch and web search), not recalled from training data. Where a claim's underlying content could not be checked in full (e.g. every 'SST n.m' chapter tag), that limit is stated explicitly in d:verificationNote rather than extended by inference. https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/assertion http://www.w3.org/ns/prov#wasDerivedFrom https://api.github.com/repos/johnmaxton/lean4-starter https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/assertion http://www.w3.org/ns/prov#wasDerivedFrom https://geocoq.github.io/GeoCoq/html/GeoCoq.Tarski_dev.Ch07_midpoint.html https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/assertion http://www.w3.org/ns/prov#wasDerivedFrom https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/Tarski.lean https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/assertion http://www.w3.org/ns/prov#wasDerivedFrom https://link.springer.com/book/10.1007/978-3-642-69418-9 https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/assertion http://www.w3.org/ns/prov#wasDerivedFrom https://philpapers.org/rec/TARTSO https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/assertion http://www.w3.org/ns/prov#wasDerivedFrom https://raw.githubusercontent.com/GeoCoq/GeoCoq/master/coq-geocoq-axioms.opam https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/assertion http://www.w3.org/ns/prov#wasGeneratedBy https://provenance.example/tarski-lean/activity-ground https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/pubinfo https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk http://purl.org/dc/terms/created 2026-08-10T12:57:30Z https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk http://purl.org/dc/terms/creator https://orcid.org/0000-0002-8042-4131 https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk http://purl.org/dc/terms/license https://creativecommons.org/licenses/by/4.0/ https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk http://www.w3.org/2000/01/rdf-schema#label Tarski.lean: license, authorship, and historical-citation grounding (source-verified) https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk https://provenance.example/tarski-lean/verificationBucket https://provenance.example/tarski-lean/SourceVerified https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/sig http://purl.org/nanopub/x/hasAlgorithm RSA https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/sig http://purl.org/nanopub/x/hasPublicKey MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/sig http://purl.org/nanopub/x/hasSignature cQjcMTuBG6lzr3xucx4Xaq9ahrq64h700CRi9bgyn+2JmJ97tmSftMy9Vj4AjcbGrgECMLHwD9qdsZXzPThZLhtd5MIpGvcZ7ea9hVlPb2Qf5yYqmN99GKWjRFyL7zsRSlOsPLNxsCgP18aJhGbhEO+AkWrx7rJWHbYmS0ffiKZTT+Gu5G9z0HsrKrZUvlDTj/NVBhbr61Kjbi7gA5PuuWrbry7mSiLX+5RBBbx13uirDTGzsVMBtMqHSIocP8AS0VLjVaD2Ct+8Cb1NmxKyX1U5l7EuZkHJBgp/vFo4YG0/SWYJnDz7Ket4Fl/Bp/cABALsxfV/P0/MjxMj8WwtWQ== https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/sig http://purl.org/nanopub/x/hasSignatureTarget https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/sig http://purl.org/nanopub/x/signedBy https://orcid.org/0000-0002-8042-4131