https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4
.trig | .trig.txt | .jelly | .jelly.txt | .jsonld | .jsonld.txt | .nq | .nq.txt | .xml | .xml.txt
@prefix this: <https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4> .
@prefix sub: <https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/> .
@prefix schema: <http://schema.org/> .
@prefix np: <http://www.nanopub.org/nschema#> .
@prefix dct: <http://purl.org/dc/terms/> .
@prefix spdx: <http://spdx.org/rdf/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 orcid: <https://orcid.org/> .
@prefix iscc: <http://purl.org/iscc/terms/#> .
@prefix prov: <http://www.w3.org/ns/prov#> .
@prefix foaf: <http://xmlns.com/foaf/0.1/> .
sub:Head {
this: a np:Nanopublication;
np:hasAssertion sub:assertion;
np:hasProvenance sub:provenance;
np:hasPublicationInfo sub:pubinfo .
}
sub:assertion {
sub:agent-anthropic a schema:Organization, prov:Organization;
schema:name "Anthropic PBC";
schema:url <https://www.anthropic.com/> .
sub:agent-axton a schema:Person, prov:Person;
schema:identifier orcid:0000-0002-8042-4131;
schema:name "Myles Axton";
schema:sameAs orcid:0000-0002-8042-4131;
rdfs:comment "The GitHub account hosting the artifact is not cryptographically bound to the ORCID; see NP2 for that gap.";
foaf:account <https://github.com/johnmaxton> .
sub:agent-claude a schema:SoftwareApplication, prov:SoftwareAgent;
schema:name "Claude (Anthropic PBC)";
schema:publisher sub:agent-anthropic;
rdfs:comment "The specific model version is not recorded in the conversation export; see NP2." .
sub:artifact a schema:SoftwareSourceCode, prov:Entity;
dct:conformsTo sub:src-sst;
dct:references sub:person-euclid, sub:person-hilbert, sub:src-gupta, sub:src-pasch,
sub:src-tarski-givant;
dct:relation sub:dedication;
dct:tableOfContents sub:concordance;
dct:title "Tarski's Euclidean geometry in Lean 4 - Stages 0-4";
iscc:datahash "1e20eb61415a5383e8037259c33ad1bc4fe912516562a125c862e03648571b86d938";
iscc:filename "Tarski.lean";
iscc:iscc "ISCC:KAC67GWDV372567ANMUX3VYVTO7YIYHV2AILIDWJV3VWCQK2KOB6QAY";
iscc:metahash "1e20bde6645eb61ec39e972274a1bd94924c754662a55ed8a84999eca3bd6eacdfc4";
schema:codeRepository <https://github.com/johnmaxton/lean4-starter>;
schema:contentUrl <https://raw.githubusercontent.com/johnmaxton/lean4-starter/main/Tarski.lean>;
schema:description "A standalone synthetic development of Tarski's axiomatic Euclidean geometry following Schwabhaeuser-Szmielew-Tarski (SST) chapters 2, 3, 4 and 7, culminating in SST 7.13/7.15: point reflection is an isometry. Two primitives, eight axiom groups, no coordinates, no numbers. Contains 40 theorems and 5 definitions in namespace Synthetic.";
schema:encodingFormat "text/x-lean";
schema:fileSize "28435"^^xsd:integer;
schema:name "Tarski.lean";
schema:programmingLanguage "Lean 4";
schema:runtimePlatform "Lean 4 core; zero import statements; no Mathlib dependency";
schema:url <https://github.com/johnmaxton/lean4-starter/blob/main/Tarski.lean>;
spdx:checksum sub:checksum-gitblob, sub:checksum-sha256;
rdfs:comment "The ISCC (ISO 24138) above was generated with iscc-core over the exact 28435 bytes retrieved from the raw content URL on 2026-07-29; it binds this declaration to that byte sequence and to no other.";
prov:qualifiedAttribution sub:attr-axton, sub:attr-claude;
prov:wasDerivedFrom sub:src-geocoq, sub:src-sst .
sub:attr-axton a prov:Attribution;
dct:description "Framed the governing constraint (prove Pythagoras from inside Euclidean space with straightedge and compass only), selected each descent of the trajectory, directed the development to zero sorry, commissioned the provenance record, and published the artifact.";
prov:agent sub:agent-axton;
prov:hadRole <https://credit.niso.org/contributor-roles/conceptualization/>, <https://credit.niso.org/contributor-roles/investigation/>,
<https://credit.niso.org/contributor-roles/project-administration/>, <https://credit.niso.org/contributor-roles/supervision/> .
sub:attr-claude a prov:Attribution;
dct:description "Reconstructed the SST development from the published architecture into dependency-free core Lean 4, re-deriving proof details where recall failed - notably the l4_5 scaffold bookkeeping, the SST 3.7(2) mirror argument, and the three-stroke five-segment cascade that breaks the circularity in SST 7.13. Under prevailing scholarly norms a software agent is not an author; this attribution is an acknowledgement of contribution, and responsibility for correctness rests with the named human agent.";
prov:agent sub:agent-claude;
prov:hadRole <https://credit.niso.org/contributor-roles/formal-analysis/>, <https://credit.niso.org/contributor-roles/software/>,
<https://credit.niso.org/contributor-roles/writing-original-draft/> .
sub:checksum-gitblob a spdx:Checksum;
spdx:algorithm spdx:checksumAlgorithm_sha1;
spdx:checksumValue "04bafa6be95f6992566cde3cd4788d881e07f74c";
rdfs:comment "Git blob object identifier (SHA-1 over the 'blob <len>\\0' header plus content), for matching against the GitHub object store." .
sub:checksum-sha256 a spdx:Checksum;
spdx:algorithm spdx:checksumAlgorithm_sha256;
spdx:checksumValue "1372181e2284465648cf15fdd9b7a761ceef9288224feccfd71fb63a5417bfd1" .
sub:concordance a schema:Dataset;
dct:isPartOf sub:artifact;
schema:description "Each proved statement in the artifact, mapped to its printed SST theorem number and, where one exists, the corresponding GeoCoq lemma label. GeoCoq's lXX_YY labels denote SST Satz XX.YY, so the chapter digit of the label and of the SST reference agree by construction. Chapter titles are given as printed in the 1983 Springer edition.";
schema:name "Theorem-to-source concordance for Tarski.lean";
prov:wasDerivedFrom sub:src-sst .
sub:dedication a schema:Comment;
schema:about sub:artifact;
schema:mentions sub:person-richard-axton;
schema:name "Dedication";
schema:text "Myles Axton thanks his father, Richard Axton (1941-2021), for his introduction to Euclidean geometry and the lifelong inspiration to do more with less - straightedge and compass only." .
sub:map-betw_exchange2 a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 3.6(2), chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.betw_exchange2";
rdfs:seeAlso "GeoCoq label: between_exchange2";
prov:wasDerivedFrom sub:src-sst .
sub:map-betw_exchange_left a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 3.6, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.betw_exchange_left";
rdfs:seeAlso "GeoCoq label: between_exchange3";
prov:wasDerivedFrom sub:src-sst .
sub:map-betw_inner_trans a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 3.5, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.betw_inner_trans";
rdfs:seeAlso "GeoCoq label: between_inner_transitivity";
prov:wasDerivedFrom sub:src-sst .
sub:map-betw_left_trivial a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 3.3, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.betw_left_trivial";
prov:wasDerivedFrom sub:src-sst .
sub:map-betw_outer_trans a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 3.7, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.betw_outer_trans";
rdfs:seeAlso "GeoCoq label: outer_transitivity_between";
prov:wasDerivedFrom sub:src-sst .
sub:map-betw_outer_trans-prime a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 3.7(2), chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.betw_outer_trans'";
rdfs:seeAlso "GeoCoq label: outer_transitivity_between2";
prov:wasDerivedFrom sub:src-sst .
sub:map-betw_symm a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 3.2, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.betw_symm";
rdfs:seeAlso "GeoCoq label: between_symmetry";
prov:wasDerivedFrom sub:src-sst .
sub:map-betw_transfer a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 4.6, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.betw_transfer";
rdfs:seeAlso "GeoCoq label: l4_6";
prov:wasDerivedFrom sub:src-sst .
sub:map-betw_trivial a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 3.1, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.betw_trivial";
prov:wasDerivedFrom sub:src-sst .
sub:map-cong3_construction a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 4.5, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.cong3_construction";
rdfs:seeAlso "GeoCoq label: l4_5";
prov:wasDerivedFrom sub:src-sst .
sub:map-cong_add a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 2.11, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.cong_add";
rdfs:seeAlso "GeoCoq label: l2_11";
prov:wasDerivedFrom sub:src-sst .
sub:map-cong_left_comm a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 2.4, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.cong_left_comm";
prov:wasDerivedFrom sub:src-sst .
sub:map-cong_refl a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 2.1, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.cong_refl";
prov:wasDerivedFrom sub:src-sst .
sub:map-cong_right_comm a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 2.5, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.cong_right_comm";
prov:wasDerivedFrom sub:src-sst .
sub:map-cong_sub a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 4.3, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.cong_sub";
rdfs:seeAlso "GeoCoq label: l4_3";
prov:wasDerivedFrom sub:src-sst .
sub:map-cong_symm a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 2.2, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.cong_symm";
prov:wasDerivedFrom sub:src-sst .
sub:map-cong_trans a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 2.3, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.cong_trans";
prov:wasDerivedFrom sub:src-sst .
sub:map-cong_trivial a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 2.8, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.cong_trivial";
prov:wasDerivedFrom sub:src-sst .
sub:map-construction_uniqueness a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 2.12, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.construction_uniqueness";
rdfs:seeAlso "GeoCoq label: construction_uniqueness";
prov:wasDerivedFrom sub:src-sst .
sub:map-inner_five_segment a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 4.2, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.inner_five_segment";
rdfs:seeAlso "GeoCoq label: l4_2";
prov:wasDerivedFrom sub:src-sst .
sub:map-reflect_betw a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 7.15, chapter 7: Punktspiegelungen (pp. 49-56)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.reflect_betw";
rdfs:seeAlso "GeoCoq label: l7_15";
prov:wasDerivedFrom sub:src-sst .
sub:map-reflect_cong a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 7.13, chapter 7: Punktspiegelungen (pp. 49-56)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.reflect_cong";
rdfs:seeAlso "GeoCoq label: l7_13";
prov:wasDerivedFrom sub:src-sst .
sub:map-symmetric_point_exists a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 7.4, chapter 7: Punktspiegelungen (pp. 49-56)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.symmetric_point_exists";
rdfs:seeAlso "GeoCoq label: symmetric_point_construction";
prov:wasDerivedFrom sub:src-sst .
sub:map-symmetric_point_uniqueness a prov:Entity;
dct:bibliographicCitation "SST (1983), Satz 7.5, chapter 7: Punktspiegelungen (pp. 49-56)";
dct:isPartOf sub:artifact;
dct:isReferencedBy sub:concordance;
schema:name "Synthetic.symmetric_point_uniqueness";
rdfs:seeAlso "GeoCoq label: symmetric_point_uniqueness";
prov:wasDerivedFrom sub:src-sst .
sub:person-euclid a schema:Person, prov:Person;
schema:name "Euclid";
rdfs:comment "The axiomatic ideal the artifact rebuilds, and the straightedge-and-compass constraint that governs it." .
sub:person-gupta a schema:Person, prov:Person;
schema:name "Haragauri Narayan Gupta" .
sub:person-hilbert a schema:Person, prov:Person;
schema:name "David Hilbert";
rdfs:comment "The modern axiomatic programme and the segment arithmetic that is the eventual route from this development to Pythagoras." .
sub:person-mehta a schema:Person, prov:Person;
schema:name "Bhavik Mehta" .
sub:person-narboux a schema:Person, prov:Person;
schema:name "Julien Narboux" .
sub:person-pasch a schema:Person, prov:Person;
schema:name "Moritz Pasch" .
sub:person-richard-axton a schema:Person, prov:Person;
schema:birthDate "1941"^^xsd:gYear;
schema:deathDate "2021"^^xsd:gYear;
schema:name "Richard Axton" .
sub:person-schwabhaeuser a schema:Person, prov:Person;
schema:name "Wolfram Schwabhaeuser";
rdfs:comment "Wrote and completed Part I of SST for publication in 1983." .
sub:person-szmielew a schema:Person, prov:Person;
schema:name "Wanda Szmielew";
rdfs:comment "Part I of SST, the development the artifact follows lemma for lemma, grew from her Berkeley lectures; she died in 1976, before publication." .
sub:person-tarski a schema:Person, prov:Person;
schema:name "Alfred Tarski";
rdfs:comment "Designed the axiom system (Warsaw, 1926-27) and proved its completeness and decidability." .
sub:src-geocoq a schema:SoftwareSourceCode, prov:Entity;
dct:license <http://spdx.org/licenses/LGPL-3.0-only>;
schema:author sub:person-narboux;
schema:contributor "C. Gries", "G. Braun", "M. Beeson", "P. Boutry", "P. Schreck";
schema:name "GeoCoq";
schema:programmingLanguage "Coq";
schema:url <https://github.com/GeoCoq/GeoCoq>;
rdfs:comment "Origin of the lemma labels (l4_2, l4_5, l4_6, l7_13, l7_15) cited in the artifact's comments, and the first machine-checked ascent of the SST development at scale. GeoCoq's file names track SST chapters one-for-one; the artifact reconstructs that architecture and does not port GeoCoq proof scripts. No specific commit was consulted; see NP2." .
sub:src-geolean a schema:SoftwareSourceCode, prov:Entity;
schema:author sub:person-mehta;
schema:name "GeoLean (mathlib3 branch)";
schema:programmingLanguage "Lean 3";
schema:url <https://github.com/leanprover-community/mathlib>;
rdfs:comment "A port of a large portion of GeoCoq into a branch of mathlib3, described by its author as covering roughly 70 percent of the Tarski work in GeoCoq. Cited here as prior art establishing that Tarski.lean is not the first formalisation of Tarski's axioms in Lean. It is NOT an ancestor of this artifact: see NP2, which records that no derivation relation holds." .
sub:src-gupta a schema:Thesis, prov:Entity;
schema:author sub:person-gupta;
schema:datePublished "1965"^^xsd:gYear;
schema:name "Contributions to the axiomatic foundations of geometry";
rdfs:comment "Doctoral dissertation, University of California, Berkeley, supervised by Tarski. Source of axiom simplifications adopted in SST and of the continuity-free perpendicular construction that the artifact stops short of." .
sub:src-pasch a schema:Book, prov:Entity;
schema:author sub:person-pasch;
schema:datePublished "1882"^^xsd:gYear;
schema:name "Vorlesungen ueber neuere Geometrie";
rdfs:comment "Origin of the order axiom formalised in the artifact as inner_pasch." .
sub:src-sst a schema:Book, prov:Entity;
dct:bibliographicCitation "W. Schwabhaeuser, W. Szmielew, A. Tarski, Metamathematische Methoden in der Geometrie, Hochschultext, Springer, 1983. Part I, 'Ein axiomatischer Aufbau der euklidischen Geometrie', pp. 1-171.";
dct:identifier <https://doi.org/10.1007/978-3-642-69418-9>;
schema:author sub:person-schwabhaeuser, sub:person-szmielew, sub:person-tarski;
schema:datePublished "1983"^^xsd:gYear;
schema:isbn "978-3-540-12958-5";
schema:name "Metamathematische Methoden in der Geometrie";
schema:publisher "Springer-Verlag, Berlin Heidelberg";
rdfs:comment "The source of the 'SST n.m' theorem numbering used throughout the artifact. Part I rests in part on unpublished results of Tarski and Szmielew and on results of H. N. Gupta, per the authors' preface." .
sub:src-tarski-givant a schema:ScholarlyArticle, prov:Entity;
dct:bibliographicCitation "A. Tarski, S. Givant, Tarski's system of geometry, Bulletin of Symbolic Logic 5(2), 1999, pp. 175-214.";
schema:author sub:person-tarski;
schema:contributor "Steven Givant";
schema:datePublished "1999"^^xsd:gYear;
schema:name "Tarski's system of geometry" .
}
sub:provenance {
sub:activity-declaration a prov:Activity;
dct:description "Drafting of the credit ledger, its expression as nanopublications, an external review pass on 2026-07-21, and the correction of that review. The correction history is recorded in NP2.";
schema:name "Provenance declaration drafting and revision";
prov:endedAtTime "2026-07-29T00:00:00Z"^^xsd:dateTime;
prov:startedAtTime "2026-07-18T10:37:00Z"^^xsd:dateTime;
prov:used sub:artifact, sub:transcript;
prov:wasAssociatedWith sub:agent-axton, sub:agent-claude .
sub:activity-dialogue a prov:Activity;
dct:description "Thirty-six turns beginning from the Pythagorean theorem in Mathlib's inner product spaces, specialising to EuclideanSpace R (Fin n), then inverting the question to ask whether Pythagoras can be earned synthetically from within. The development proceeded in stages: congruence calculus, betweenness calculus, vocabulary, point reflection, the chapter-4 bridge, and finally SST 7.13. Two sorry placeholders were introduced and both were subsequently discharged.";
schema:name "Interactive formalization dialogue";
prov:endedAtTime "2026-07-19T07:51:20Z"^^xsd:dateTime;
prov:generated sub:artifact, sub:transcript;
prov:startedAtTime "2026-07-18T08:47:58Z"^^xsd:dateTime;
prov:used sub:src-geocoq, sub:src-sst;
prov:wasAssociatedWith sub:agent-axton, sub:agent-claude .
sub:artifact prov:wasGeneratedBy sub:activity-dialogue .
sub:assertion prov:wasAttributedTo sub:agent-axton, sub:agent-claude;
prov:wasDerivedFrom sub:transcript;
prov:wasGeneratedBy sub:activity-declaration .
sub:checksum-transcript a spdx:Checksum;
spdx:algorithm spdx:checksumAlgorithm_sha256;
spdx:checksumValue "213dbd5947f170c2e1480e894a20450442f4a6bde340df1492d6e6d86a7efd51" .
sub:transcript a schema:Dataset, prov:Entity;
dct:identifier "db0d830f-aa6a-432d-8675-0daf6066fb20";
schema:dateCreated "2026-07-21T08:51:48Z"^^xsd:dateTime;
schema:encodingFormat "application/json";
schema:fileSize "69228"^^xsd:integer;
schema:name "Conversation export: Pythagorean theorem in Lean4 inner product spaces";
spdx:checksum sub:checksum-transcript;
rdfs:comment "Not publicly resolvable at the time of this declaration; the checksum permits verification if and when it is deposited." .
}
sub:pubinfo {
this: dct:created "2026-07-29T15:00:47Z"^^xsd:dateTime;
dct:creator sub:agent-axton;
dct:description "Version 2. Supersedes the 2026-07-21 draft and its external review pass, both of which contained attribution and citation errors now corrected and itemised in NP2.";
dct:license <http://creativecommons.org/publicdomain/zero/1.0/>;
npx:hasNanopubType prov:Attribution;
npx:introduces sub:artifact;
rdfs:label "Tarski.lean: attribution, ancestry and source concordance (v2)";
prov:wasAttributedTo sub:agent-axton .
sub:sig npx:hasAlgorithm "RSA";
npx:hasPublicKey "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB";
npx:hasSignature "XF1tMKmlAQ7I6eWkMWOOZe1Cl/B95TfuRo8alV/gL2oGOD75egvyJRifS1bD9Z6mJgFgcvJZAZi0xY4OSWusz7JMBUkw3dgb9+sM3WvEvJVHp6As0Ba4kyJt35rNoMl3SbaPbhLsDAhaw68EfBLKzlvW40T52tJ/j8QpU4WXNQBpRDodB9ODPIY5nwqZvj+HV+g5jGruDc6vGunTVg3JofhbF6KUaoOT1T2H6nUnz7hiPMhBaACxNkgDpZZkTeaMmmZW/wVtJesLgjiNgXTZ7FAlLMp+xaGxQSRnjt5XL9OCJJBrsKKTiVBtgnTuNjHMz/jU8+ekU979SE+5zxrF+A==";
npx:hasSignatureTarget this:;
npx:signedBy orcid:0000-0002-8042-4131 .
}