https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/Head https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://www.nanopub.org/nschema#hasAssertion https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/assertion https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://www.nanopub.org/nschema#hasProvenance https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/provenance https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://www.nanopub.org/nschema#hasPublicationInfo https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/pubinfo https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.nanopub.org/nschema#Nanopublication https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/assertion https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-claude http://purl.org/dc/terms/description Drafted all Lean code and documentation; reconstructed and in places re-derived the proofs (see sub:faia). In a follow-up session, diagnosed and fixed the sole compile error and verified compilation under two toolchains (see sub:activity-verify). In a later session, generated the file's ISCC-CODE (see sub:activity-iscc). Not an author under prevailing scholarly norms; correctly credited by acknowledgment. All errors in the draft are attributable here, not to the mathematical tradition. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-claude http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#SoftwareAgent https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-claude http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/software https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-claude http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/validation https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-claude http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/writing-original-draft https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-claude https://schema.org/name Claude (Anthropic) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-euclid http://purl.org/dc/terms/description The axiomatic ideal the artifact rebuilds; the original tower (Elements, Book I), including target propositions I.47–I.48 (Pythagoras and converse) and Definition I.10, echoed in the planned `Per` (SST ch. 8). https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-euclid http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-euclid http://www.w3.org/ns/prov#hadRole Intellectual ancestor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-euclid https://schema.org/name Euclid of Alexandria (fl. c. 300 BCE) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-geocoq http://purl.org/dc/terms/description First machine-checked ascent of the SST development (Coq, from Narboux 2006 onward). The artifact reconstructs the GeoCoq architecture and navigated by its lemma map (l4_2 → inner_five_segment, l4_3 → cong_sub, l4_5 → cong3_construction, l4_6 → betw_transfer, l7_13 → reflect_cong, l7_15 → reflect_betw) but ports no GeoCoq code. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-geocoq http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Organization https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-geocoq http://www.w3.org/ns/prov#hadRole Formal ancestor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-geocoq https://schema.org/name GeoCoq project (J. Narboux, M. Beeson, P. Boutry, G. Braun, C. Gries, P. Schreck, et al.) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-geocoq https://schema.org/url https://github.com/GeoCoq/GeoCoq https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-gupta http://purl.org/dc/terms/description PhD dissertation, UC Berkeley 1965, under Tarski: axiom independence and simplification (several axioms are as lean as A1–A8 because of him), and the perpendicular and midpoint constructions without any continuity axiom — SST 8.18 and 8.22, the declared next stage of this artifact, not yet contained in it. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-gupta http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-gupta http://www.w3.org/ns/prov#hadRole Axiom simplifier; author of the continuity-free constructions ahead https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-gupta https://schema.org/name Haragauri Narayan Gupta (1925–2016) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-hilbert http://purl.org/dc/terms/description Grundlagen der Geometrie (1899): the modern axiomatic program, and the segment arithmetic (Streckenrechnung, cf. SST ch. 14–15) that is the declared future route from this artifact to Pythagoras. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-hilbert http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-hilbert http://www.w3.org/ns/prov#hadRole Program architect https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-hilbert https://schema.org/name David Hilbert (1862–1943) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-pasch http://purl.org/dc/terms/description Discovered that order is an assumption, not a triviality (Vorlesungen über neuere Geometrie, 1882). Namesake of axiom A7 (`inner_pasch`), on which the whole of Stage 2 rests: SST 3.1 (betw_trivial, indirectly), 3.2 (betw_symm), 3.5 (betw_inner_trans). https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-pasch http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-pasch http://www.w3.org/ns/prov#hadRole Axiom source https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-pasch https://schema.org/name Moritz Pasch (1843–1930) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-schwabhaeuser http://purl.org/dc/terms/description Completed and published the treatise: Schwabhäuser, Szmielew, Tarski, 'Metamathematische Methoden in der Geometrie', Springer 1983. Every 'SST n.m' tag in the artifact cites all three authors through his numbering. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-schwabhaeuser http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-schwabhaeuser http://www.w3.org/ns/prov#hadRole Systematizer and publisher https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-schwabhaeuser https://schema.org/name Wolfram Schwabhäuser (1931–1985) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-szmielew http://purl.org/dc/terms/description Part I of SST grew from her lectures; the artifact follows her development lemma-for-lemma: SST 2.1–2.5, 2.8, 2.11, 2.12 (congruence calculus, segment addition, construction uniqueness); 3.1–3.3, 3.5, 3.6(1), 3.6(2), 3.7(1), 3.7(2) (betweenness calculus); 4.2, 4.3, 4.5, 4.6 (congruence–betweenness bridge); 7.4, 7.5, 7.13, 7.15 (point reflection and its isometry). She died before publication; her share of the credit is frequently understated. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-szmielew http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-szmielew http://www.w3.org/ns/prov#hadRole Development author (followed lemma-for-lemma) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-szmielew https://schema.org/name Wanda Szmielew (1918–1976) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-tarski http://purl.org/dc/terms/description The axiom system formalized as the `Tarski` typeclass, axioms A1–A8 (cong_pseudo_refl, cong_inner_trans, cong_identity, segment_construction, five_segment, betw_identity, inner_pasch, lower_dim), developed 1926–27; completeness and decidability of elementary geometry, guaranteeing the synthetic development agrees with EuclideanSpace ℝ (Fin n) on all first-order sentences. Survey citation: Tarski & Givant, 'Tarski's System of Geometry', Bulletin of Symbolic Logic 5(2), 1999. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-tarski http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-tarski http://www.w3.org/ns/prov#hadRole Axiom-system author; metatheorist https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-tarski https://schema.org/name Alfred Tarski (1901–1983) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user http://purl.org/dc/terms/description Set the organizing question and metaphor (being 'trapped' in EuclideanSpace ℝ (Fin n) with only straightedge and compass), chose each descent (perpendiculars → compiling file → SST ch. 4 block → SST 7.13), and supplied the persistence that drove the artifact to zero `sorry`s. Directed the follow-up session that found a working Lean toolchain, compiled the artifact, and requested the fix for the sole compile error, and later directed the ISCC-CODE generation session. Holds the director's and verifier's credit. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/conceptualization https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/supervision https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/validation https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user https://schema.org/identifier https://orcid.org/0000-0002-8042-4131 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user https://schema.org/name Myles Axton https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user https://schema.org/sameAs https://orcid.org/0000-0002-8042-4131 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/contributor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-claude https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/contributor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-euclid https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/contributor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-geocoq https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/contributor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-gupta https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/contributor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-hilbert https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/contributor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-pasch https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/contributor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-schwabhaeuser https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/contributor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-szmielew https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/contributor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-tarski https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/contributor https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/relation https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/dedication https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/dc/terms/tableOfContents https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/sst-map https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/faia/terms/declaration https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/faia https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/iscc/terms/datahash 1e20eb61415a5383e8037259c33ad1bc4fe912516562a125c862e03648571b86d938 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/iscc/terms/generator iscc-sdk - v0.9.4 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/iscc/terms/iscc ISCC:KAC67GWDV372567ANMUX3VYVTO7YIYHV2AILIDWJV3VWCQK2KOB6QAY https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://purl.org/iscc/terms/metahash 1e20bde6645eb61ec39e972274a1bd94924c754662a55ed8a84999eca3bd6eacdfc4 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://schema.org/SoftwareSourceCode https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact https://schema.org/codeRepository https://github.com/johnmaxton/lean4-starter/blob/90018aec70b2bb8950c1045cac443731825d79ef/Tarski.lean https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact https://schema.org/contentSize 28435 bytes (648 lines) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact https://schema.org/description A synthetic development of Tarski's Euclidean geometry following Schwabhäuser–Szmielew–Tarski (SST) chapters 2–7: eleven axioms over two primitives (betweenness, segment congruence), developed through SST 7.13/7.15 (point reflection is an isometry). Zero `sorry`s. Compiles cleanly (`lean Tarski.lean` and `lake build`, exit 0) under both leanprover/lean4-nightly:nightly-2023-05-16 and leanprover/lean4:v4.32.0, confirming the dependency-free (core-Lean-4-only) claim across toolchain versions. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact https://schema.org/encodingFormat text/plain https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact https://schema.org/name Tarski.lean https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact https://schema.org/programmingLanguage Lean 4 (core language only; no Mathlib dependency) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact https://schema.org/sha256 1372181e2284465648cf15fdd9b7a761ceef9288224feccfd71fb63a5417bfd1 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/dedication http://purl.org/dc/terms/description Myles Axton thanks his father, Richard Axton (1941–2021), for his introduction to Euclidean geometry and the inspiration to do more with less (straight edge and compass only). https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/dedication http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://schema.org/Comment https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/dedication https://schema.org/about https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/person-richard-axton https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/dedication https://schema.org/name Dedication https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/faia http://purl.org/faia/terms/aiContribution Reconstruction of the SST/GeoCoq proof architecture from model memory; independent re-derivation where memory was insufficient (the SST 4.5 scaffold bookkeeping; SST 3.7(2) via mirror application of 3.7(1); the five-segment slot assignments in SST 7.13); translation into dependency-free core Lean 4; expository docstrings. In the follow-up session: diagnosed and fixed one compile error (the `example` at the end of Stage 5 used Mathlib's `∃!` unique-existence notation, unavailable in core Lean 4; rewritten as its explicit unfolding), then verified compilation. In a later session: generated the file's ISCC-CODE (see sub:isccNote, sub:activity-iscc). https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/faia http://purl.org/faia/terms/aiSystem Claude (Anthropic), Claude Fable 5, chat interface, sandboxed (no network, no Lean toolchain), for the original drafting session; Claude (Anthropic), Claude Sonnet 5, Claude Code CLI, with network and a working Lean 4 toolchain, for the subsequent compilation and fix session and for the ISCC-CODE generation session. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/faia http://purl.org/faia/terms/humanOversight Every construction and proof step was chosen or approved turn-by-turn in dialogue; the human set direction, scope, and the requirement of resolving all `sorry`s. The human also directed the follow-up build/fix/compile session and reviewed its result before this declaration was finalized, and directed the ISCC-CODE generation reported here. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/faia http://purl.org/faia/terms/knownLimitations The artifact now compiles cleanly under two independent Lean 4 toolchains (see schema:description); this discharges the compilation-verification limitation noted in the original sandbox draft. An ISCC-CODE has now been minted (see sub:isccNote); remaining limitations: the mathematical content has not been cross-checked against an independent formalization (e.g. GeoCoq itself) beyond the lemma-map correspondence in sub:sst-map, and no trusted timestamp or ledger anchor has yet been obtained (see sub:timestampNote). https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/faia http://purl.org/faia/terms/mode AI-drafted, human-directed https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/faia http://purl.org/faia/terms/originalityStatement No new mathematics. Every theorem in the artifact is prior art carrying an SST number (see sub:sst-map). The creative contributions of the AI-human collaboration are formalization engineering and exposition only. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/faia http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/faia/terms/AIUsageDeclaration https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/faia https://schema.org/url https://www.faia.io/statement?f=aac&ac=cocreation%2Ccontribution%2Cenhancement%2Crefinement&sys=Claude%2C++Claude+Code&ver=5%2C+4.8&note=AI+helped+assemble+provenance+nanopublications+under+my+close+supervision.+I+am+responsible+for+editing%2C+signing+and+publishing+the+nanopublications+and+the+entire+project https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/isccNote http://purl.org/dc/terms/description ISO 24138 ISCC generation (Meta-, Content-, Data-, Instance-Code units) has now been completed using iscc-sdk v0.9.4, which wraps the iscc-core reference implementation (see sub:activity-iscc), superseding the earlier PENDING value. The .lean extension is not in iscc-sdk's recognized extension map, so content-based auto-detection (UTF-8 decodability, low control-character ratio) was used to process the file as text/plain, yielding a genuine text Content-Code rather than a raw-bytes-only fallback. The resulting ISCC-CODE, datahash, and metahash are recorded on sub:artifact. A trusted timestamp or ledger anchor for this document is still outstanding (see sub:timestampNote). https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/isccNote http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://schema.org/Comment https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/isccNote https://schema.org/name ISCC binding status https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/person-richard-axton http://purl.org/dc/terms/description Introduced Myles Axton to Euclidean geometry. The artifact's governing constraint — do more with less, straight edge and compass only — is his inspiration, and it is the same austerity that runs from Euclid's instruments through Tarski's two primitives to Gupta's removal of the continuity axiom. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/person-richard-axton http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/person-richard-axton http://www.w3.org/ns/prov#hadRole Dedicatee; first teacher https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/person-richard-axton https://schema.org/name Richard Axton (1941–2021) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/sst-map http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://schema.org/Dataset https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/sst-map https://schema.org/description Lean name = SST number [= GeoCoq name where applicable]: cong_refl = 2.1; cong_symm = 2.2; cong_trans = 2.3; cong_left_comm = 2.4; cong_right_comm = 2.5; cong_trivial = 2.8; cong_add = 2.11 [l2_11]; construction_uniqueness = 2.12; betw_trivial = 3.1; betw_symm = 3.2; betw_left_trivial = 3.3; betw_inner_trans = 3.5; betw_exchange_left = 3.6(1); betw_exchange2 = 3.6(2) [between_exchange2]; betw_outer_trans = 3.7(1); betw_outer_trans' = 3.7(2); Cong3 = Def. 4.1 [Cong_3]; inner_five_segment = 4.2 [l4_2]; cong_sub = 4.3 [l4_3]; cong3_construction = 4.5 [l4_5]; betw_transfer = 4.6 [l4_6]; symmetric_point_exists = 7.4; symmetric_point_uniqueness = 7.5; reflect_cong = 7.13 [l7_13]; reflect_betw = 7.15 [l7_15]. Axioms A1–A8 = Tarski. Declared future work: Per = Euclid Def. I.10 / SST ch. 8; perpendiculars and midpoints = 8.18, 8.22 (Gupta); target theorem = Pythagoras, Euclid I.47–I.48, via segment arithmetic, SST ch. 14–15 (Hilbert). https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/sst-map https://schema.org/name Theorem-to-source concordance https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/timestampNote http://purl.org/dc/terms/description All timestamps herein are the system clock of the drafting/verification/ISCC-generation sessions (self-asserted), not trusted timestamps. They are honest but not tamper-evident. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/timestampNote http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://schema.org/Comment https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/timestampNote https://schema.org/name Timestamp status https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/provenance https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity http://purl.org/dc/terms/description A single sandboxed chat session beginning from the Pythagorean theorem in Mathlib's inner product spaces (norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero) and EuclideanSpace ℝ (Fin n), pivoting to the synthetic question, and building the Lean 4 artifact over successive turns. Sources were drawn from model memory of SST and GeoCoq; no network access and no Lean toolchain were available, so all proofs were verified by hand-tracing (and, for SST 7.13, by an additional coordinate check) rather than by compilation. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity http://www.w3.org/ns/prov#endedAtTime 2026-07-19 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity http://www.w3.org/ns/prov#startedAtTime 2026-07-18 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity http://www.w3.org/ns/prov#used https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity http://www.w3.org/ns/prov#used https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-geocoq https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity http://www.w3.org/ns/prov#used https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-sst https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-claude https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity https://schema.org/name Interactive formalization dialogue https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-iscc http://purl.org/dc/terms/description Generated the ISCC-CODE (ISO 24138) for Tarski.lean using iscc-sdk v0.9.4 via a standalone content-identification workflow (iscc-workflow/generate_iscc.py). Fetched the commit-pinned GitHub blob (johnmaxton/lean4-starter @ 90018aec70b2bb8950c1045cac443731825d79ef) and confirmed it is byte-identical (same SHA-256) to the local working copy before generating the code. Because the .lean extension is unrecognized by iscc-sdk's mediatype map, content-based text auto-detection (added to the workflow for this case) was used to process the file as text/plain rather than a raw-bytes fallback. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-iscc http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-iscc http://www.w3.org/ns/prov#startedAtTime 2026-07-21 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-iscc http://www.w3.org/ns/prov#used https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-iscc http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-claude https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-iscc http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-iscc https://schema.org/name ISCC-CODE generation https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-verify http://purl.org/dc/terms/description A follow-up session with a working environment (network access, elan/Lean toolchains). Compiled `lean Tarski.lean` standalone and, separately, built it as a `lake` library target in two projects (pythagoras4, using leanprover/lean4-nightly:nightly-2023-05-16; and lean4-starter, using leanprover/lean4:v4.32.0). Found and fixed one error: the closing `example` used Mathlib's `∃!` notation, unavailable in core Lean 4, rewritten as its explicit unfolding. Both toolchains now build the file with zero errors and zero `sorry`s. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-verify http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-verify http://www.w3.org/ns/prov#startedAtTime 2026-07-18 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-verify http://www.w3.org/ns/prov#used https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/artifact https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-verify http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-claude https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-verify http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-verify https://schema.org/name Build, fix, and compilation verification https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/assertion http://www.w3.org/ns/prov#wasGeneratedBy https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/assertion http://www.w3.org/ns/prov#wasInfluencedBy https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-iscc https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/assertion http://www.w3.org/ns/prov#wasInfluencedBy https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/activity-verify https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation http://purl.org/dc/terms/description Full transcript export (36 messages, participants 'Claude (Anthropic PBC)' and the human ORCID holder, per the export's own metadata) of the sandboxed formalization dialogue recorded as sub:activity; the source-of-record for this nanopublication's account of that session, ISCC-identified for tamper-evident reference. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation http://purl.org/iscc/terms/datahash 1e20ba75fff4f8f4c444367ab1a8b2a6dc174d8594a5e0a608629c783c3672ed9d13 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation http://purl.org/iscc/terms/generator iscc-sdk - v0.9.4 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation http://purl.org/iscc/terms/iscc ISCC:KACVLHAC56XUUSQOQMH3UGAUADDVMRS5VJT3THHCNW5HL77U7D2MIRA https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation http://purl.org/iscc/terms/metahash 1e203058b6a3e88931d06f05aaf71f1baef07909f330d8d6fa48952fa3a8184e823f https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://schema.org/CreativeWork https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation https://schema.org/dateCreated 2026-07-18T08:47:56Z https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation https://schema.org/dateModified 2026-07-19T07:51:20Z https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation https://schema.org/encodingFormat application/json https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-conversation https://schema.org/name Pythagorean theorem in Lean4 inner product spaces https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-geocoq http://purl.org/dc/terms/description Used from model memory as the formalization map; no code consulted or ported in-session. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-geocoq http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-geocoq https://schema.org/name GeoCoq repository and papers (Narboux et al., 2006–) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-sst http://purl.org/dc/terms/description Used from model memory as the architectural source; not consulted directly in-session. https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-sst http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/src-sst https://schema.org/name Schwabhäuser, Szmielew, Tarski — Metamathematische Methoden in der Geometrie (Springer, 1983) https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/pubinfo https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://purl.org/dc/terms/created 2026-07-21T13:56:27Z https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://purl.org/dc/terms/creator https://orcid.org/0000-0002-8042-4131 https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://purl.org/dc/terms/creator https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-claude https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://purl.org/dc/terms/creator https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/agent-user https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://purl.org/dc/terms/description Provenance and credit declaration for Tarski.lean, a dependency-free Lean 4 formalization of Tarski's synthetic Euclidean geometry (SST chapters 2–7, Stages 0–4). Records intellectual lineage (Euclid through Gupta and GeoCoq), the AI-human authorship split, a dedication, and the file's ISCC-CODE (ISO 24138). https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://purl.org/dc/terms/license https://creativecommons.org/licenses/by/4.0/ https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://purl.org/nanopub/x/supersedes https://w3id.org/np/RAXut_tYBIBaf53frjHN9ttCnUj4zq8JhXllSz7MyKpME https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://www.w3.org/2000/01/rdf-schema#label Tarski.lean provenance and credit declaration https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc http://www.w3.org/ns/prov#generatedAtTime 2026-07-21T13:56:27Z https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc https://w3id.org/np/o/ntemplate/wasCreatedFromProvenanceTemplate http://purl.org/np/RANwQa4ICWS5SOjw7gp99nBpXBasapwtZF1fIM3H2gYTM https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc https://w3id.org/np/o/ntemplate/wasCreatedFromPubinfoTemplate http://purl.org/np/RAA2MfqdBCzmz9yVWjKLXNbyfBNcwsMmOqcNUxkk1maIM https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc https://w3id.org/np/o/ntemplate/wasCreatedFromPubinfoTemplate http://purl.org/np/RAjpBMlw3owYhJUBo3DtsuDlXsNAJ8cnGeWAutDVjuAuI https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc https://w3id.org/np/o/ntemplate/wasCreatedFromTemplate http://purl.org/np/RAFu2BNmgHrjOTJ8SKRnKaRp-VP8AOOb7xX88ob0DZRsU https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/sig http://purl.org/nanopub/x/hasAlgorithm RSA https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/sig http://purl.org/nanopub/x/hasPublicKey MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/sig http://purl.org/nanopub/x/hasSignature Kwuop+7Coxlh3k+ENGFxX4Z4XTgLHpiEuqoQt1WVAunYvWomO5zeCfO/7mwSa1Y7nFxy0PZBdLYFIg/UmGAesX3ADWutrseRnSC07/LL7f7jRGVD+bs+NhpZ4sWyuKl48NXWhtK6onf86uV1+6b8FTCFGWmphPq0ikhk5lvNZj6+5/TYCtAgq0rMhqM4MiVA1GrOIFDZVNzS1CBIP7WCpGHD7Pozv+1RJ4fmo48ENliqhMZB6Ekah/PA/U817eWoH6CUx4QtX/f++30w3UMkcbCv59JLZBXiAOLf/bWh2CL+7JqNxZvZLRGTSoTdmnFKmzXPYqsty7IiWcJxWnxZGQ== https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/sig http://purl.org/nanopub/x/hasSignatureTarget https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc/sig http://purl.org/nanopub/x/signedBy https://orcid.org/0000-0002-8042-4131