https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/Head https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://www.nanopub.org/nschema#hasAssertion https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/assertion https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://www.nanopub.org/nschema#hasProvenance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/provenance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://www.nanopub.org/nschema#hasPublicationInfo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/pubinfo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.nanopub.org/nschema#Nanopublication https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/assertion https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-anthropic http://schema.org/name Anthropic PBC https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-anthropic http://schema.org/url https://www.anthropic.com/ https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-anthropic http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Organization https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-anthropic http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Organization https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton http://schema.org/identifier https://orcid.org/0000-0002-8042-4131 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton http://schema.org/name Myles Axton https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton http://schema.org/sameAs https://orcid.org/0000-0002-8042-4131 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton http://www.w3.org/2000/01/rdf-schema#comment The GitHub account hosting the artifact is not cryptographically bound to the ORCID; see NP2 for that gap. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton http://xmlns.com/foaf/0.1/account https://github.com/johnmaxton https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude http://schema.org/name Claude (Anthropic PBC) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude http://schema.org/publisher https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-anthropic https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/SoftwareApplication https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#SoftwareAgent https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude http://www.w3.org/2000/01/rdf-schema#comment The specific model version is not recorded in the conversation export; see NP2. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/dc/terms/conformsTo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/dc/terms/references https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-euclid https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/dc/terms/references https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-hilbert https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/dc/terms/references https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-gupta https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/dc/terms/references https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-pasch https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/dc/terms/references https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-tarski-givant https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/dc/terms/relation https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/dedication https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/dc/terms/tableOfContents https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/dc/terms/title Tarski's Euclidean geometry in Lean 4 - Stages 0-4 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/iscc/terms/#datahash 1e20eb61415a5383e8037259c33ad1bc4fe912516562a125c862e03648571b86d938 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/iscc/terms/#filename Tarski.lean https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/iscc/terms/#iscc ISCC:KAC67GWDV372567ANMUX3VYVTO7YIYHV2AILIDWJV3VWCQK2KOB6QAY https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://purl.org/iscc/terms/#metahash 1e20bde6645eb61ec39e972274a1bd94924c754662a55ed8a84999eca3bd6eacdfc4 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://schema.org/codeRepository https://github.com/johnmaxton/lean4-starter https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://schema.org/contentUrl https://raw.githubusercontent.com/johnmaxton/lean4-starter/main/Tarski.lean https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://schema.org/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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://schema.org/encodingFormat text/x-lean https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://schema.org/fileSize 28435 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://schema.org/name Tarski.lean https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://schema.org/programmingLanguage Lean 4 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://schema.org/runtimePlatform Lean 4 core; zero import statements; no Mathlib dependency https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://schema.org/url https://github.com/johnmaxton/lean4-starter/blob/main/Tarski.lean https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://spdx.org/rdf/terms#checksum https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-gitblob https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://spdx.org/rdf/terms#checksum https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-sha256 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/SoftwareSourceCode https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://www.w3.org/2000/01/rdf-schema#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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://www.w3.org/ns/prov#qualifiedAttribution https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-axton https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://www.w3.org/ns/prov#qualifiedAttribution https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-claude https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-axton http://purl.org/dc/terms/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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-axton http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Attribution https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-axton http://www.w3.org/ns/prov#agent https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-axton http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/conceptualization/ https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-axton http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/investigation/ https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-axton http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/project-administration/ https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-axton http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/supervision/ https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-claude http://purl.org/dc/terms/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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-claude http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Attribution https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-claude http://www.w3.org/ns/prov#agent https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-claude http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/formal-analysis/ https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-claude http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/software/ https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/attr-claude http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/writing-original-draft/ https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-gitblob http://spdx.org/rdf/terms#algorithm http://spdx.org/rdf/terms#checksumAlgorithm_sha1 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-gitblob http://spdx.org/rdf/terms#checksumValue 04bafa6be95f6992566cde3cd4788d881e07f74c https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-gitblob http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://spdx.org/rdf/terms#Checksum https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-gitblob http://www.w3.org/2000/01/rdf-schema#comment Git blob object identifier (SHA-1 over the 'blob <len>\0' header plus content), for matching against the GitHub object store. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-sha256 http://spdx.org/rdf/terms#algorithm http://spdx.org/rdf/terms#checksumAlgorithm_sha256 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-sha256 http://spdx.org/rdf/terms#checksumValue 1372181e2284465648cf15fdd9b7a761ceef9288224feccfd71fb63a5417bfd1 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-sha256 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://spdx.org/rdf/terms#Checksum https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance http://schema.org/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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance http://schema.org/name Theorem-to-source concordance for Tarski.lean https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Dataset https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/dedication http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/dedication http://schema.org/mentions https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-richard-axton https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/dedication http://schema.org/name Dedication https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/dedication http://schema.org/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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/dedication http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Comment https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange2 http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 3.6(2), chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange2 http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange2 http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange2 http://schema.org/name Synthetic.betw_exchange2 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange2 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange2 http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: between_exchange2 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange2 http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange_left http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 3.6, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange_left http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange_left http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange_left http://schema.org/name Synthetic.betw_exchange_left https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange_left http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange_left http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: between_exchange3 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_exchange_left http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_inner_trans http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 3.5, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_inner_trans http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_inner_trans http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_inner_trans http://schema.org/name Synthetic.betw_inner_trans https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_inner_trans http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_inner_trans http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: between_inner_transitivity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_inner_trans http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_left_trivial http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 3.3, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_left_trivial http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_left_trivial http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_left_trivial http://schema.org/name Synthetic.betw_left_trivial https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_left_trivial http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_left_trivial http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 3.7, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans http://schema.org/name Synthetic.betw_outer_trans https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: outer_transitivity_between https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans-prime http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 3.7(2), chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans-prime http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans-prime http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans-prime http://schema.org/name Synthetic.betw_outer_trans' https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans-prime http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans-prime http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: outer_transitivity_between2 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_outer_trans-prime http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_symm http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 3.2, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_symm http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_symm http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_symm http://schema.org/name Synthetic.betw_symm https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_symm http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_symm http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: between_symmetry https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_symm http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_transfer http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 4.6, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_transfer http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_transfer http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_transfer http://schema.org/name Synthetic.betw_transfer https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_transfer http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_transfer http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: l4_6 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_transfer http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_trivial http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 3.1, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_trivial http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_trivial http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_trivial http://schema.org/name Synthetic.betw_trivial https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_trivial http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-betw_trivial http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong3_construction http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 4.5, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong3_construction http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong3_construction http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong3_construction http://schema.org/name Synthetic.cong3_construction https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong3_construction http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong3_construction http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: l4_5 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong3_construction http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_add http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 2.11, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_add http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_add http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_add http://schema.org/name Synthetic.cong_add https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_add http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_add http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: l2_11 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_add http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_left_comm http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 2.4, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_left_comm http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_left_comm http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_left_comm http://schema.org/name Synthetic.cong_left_comm https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_left_comm http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_left_comm http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_refl http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 2.1, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_refl http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_refl http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_refl http://schema.org/name Synthetic.cong_refl https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_refl http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_refl http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_right_comm http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 2.5, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_right_comm http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_right_comm http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_right_comm http://schema.org/name Synthetic.cong_right_comm https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_right_comm http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_right_comm http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_sub http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 4.3, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_sub http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_sub http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_sub http://schema.org/name Synthetic.cong_sub https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_sub http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_sub http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: l4_3 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_sub http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_symm http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 2.2, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_symm http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_symm http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_symm http://schema.org/name Synthetic.cong_symm https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_symm http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_symm http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trans http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 2.3, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trans http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trans http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trans http://schema.org/name Synthetic.cong_trans https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trans http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trans http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trivial http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 2.8, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trivial http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trivial http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trivial http://schema.org/name Synthetic.cong_trivial https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trivial http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-cong_trivial http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-construction_uniqueness http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 2.12, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-construction_uniqueness http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-construction_uniqueness http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-construction_uniqueness http://schema.org/name Synthetic.construction_uniqueness https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-construction_uniqueness http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-construction_uniqueness http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: construction_uniqueness https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-construction_uniqueness http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-inner_five_segment http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 4.2, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-inner_five_segment http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-inner_five_segment http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-inner_five_segment http://schema.org/name Synthetic.inner_five_segment https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-inner_five_segment http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-inner_five_segment http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: l4_2 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-inner_five_segment http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_betw http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 7.15, chapter 7: Punktspiegelungen (pp. 49-56) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_betw http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_betw http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_betw http://schema.org/name Synthetic.reflect_betw https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_betw http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_betw http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: l7_15 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_betw http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_cong http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 7.13, chapter 7: Punktspiegelungen (pp. 49-56) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_cong http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_cong http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_cong http://schema.org/name Synthetic.reflect_cong https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_cong http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_cong http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: l7_13 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-reflect_cong http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_exists http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 7.4, chapter 7: Punktspiegelungen (pp. 49-56) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_exists http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_exists http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_exists http://schema.org/name Synthetic.symmetric_point_exists https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_exists http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_exists http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: symmetric_point_construction https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_exists http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_uniqueness http://purl.org/dc/terms/bibliographicCitation SST (1983), Satz 7.5, chapter 7: Punktspiegelungen (pp. 49-56) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_uniqueness http://purl.org/dc/terms/isPartOf https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_uniqueness http://purl.org/dc/terms/isReferencedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_uniqueness http://schema.org/name Synthetic.symmetric_point_uniqueness https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_uniqueness http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_uniqueness http://www.w3.org/2000/01/rdf-schema#seeAlso GeoCoq label: symmetric_point_uniqueness https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/map-symmetric_point_uniqueness http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-euclid http://schema.org/name Euclid https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-euclid http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-euclid http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-euclid http://www.w3.org/2000/01/rdf-schema#comment The axiomatic ideal the artifact rebuilds, and the straightedge-and-compass constraint that governs it. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-gupta http://schema.org/name Haragauri Narayan Gupta https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-gupta http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-gupta http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-hilbert http://schema.org/name David Hilbert https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-hilbert http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-hilbert http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-hilbert http://www.w3.org/2000/01/rdf-schema#comment The modern axiomatic programme and the segment arithmetic that is the eventual route from this development to Pythagoras. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-mehta http://schema.org/name Bhavik Mehta https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-mehta http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-mehta http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-narboux http://schema.org/name Julien Narboux https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-narboux http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-narboux http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-pasch http://schema.org/name Moritz Pasch https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-pasch http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-pasch http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-richard-axton http://schema.org/birthDate 1941 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-richard-axton http://schema.org/deathDate 2021 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-richard-axton http://schema.org/name Richard Axton https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-richard-axton http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/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/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-schwabhaeuser http://schema.org/name Wolfram Schwabhaeuser https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-schwabhaeuser http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-schwabhaeuser http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-schwabhaeuser http://www.w3.org/2000/01/rdf-schema#comment Wrote and completed Part I of SST for publication in 1983. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-szmielew http://schema.org/name Wanda Szmielew https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-szmielew http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-szmielew http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-szmielew http://www.w3.org/2000/01/rdf-schema#comment Part I of SST, the development the artifact follows lemma for lemma, grew from her Berkeley lectures; she died in 1976, before publication. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-tarski http://schema.org/name Alfred Tarski https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-tarski http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-tarski http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-tarski http://www.w3.org/2000/01/rdf-schema#comment Designed the axiom system (Warsaw, 1926-27) and proved its completeness and decidability. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://purl.org/dc/terms/license http://spdx.org/licenses/LGPL-3.0-only https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://schema.org/author https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-narboux https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://schema.org/contributor C. Gries https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://schema.org/contributor G. Braun https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://schema.org/contributor M. Beeson https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://schema.org/contributor P. Boutry https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://schema.org/contributor P. Schreck https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://schema.org/name GeoCoq https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://schema.org/programmingLanguage Coq https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://schema.org/url https://github.com/GeoCoq/GeoCoq https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/SoftwareSourceCode https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq http://www.w3.org/2000/01/rdf-schema#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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geolean http://schema.org/author https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-mehta https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geolean http://schema.org/name GeoLean (mathlib3 branch) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geolean http://schema.org/programmingLanguage Lean 3 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geolean http://schema.org/url https://github.com/leanprover-community/mathlib https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geolean http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/SoftwareSourceCode https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geolean http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geolean http://www.w3.org/2000/01/rdf-schema#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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-gupta http://schema.org/author https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-gupta https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-gupta http://schema.org/datePublished 1965 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-gupta http://schema.org/name Contributions to the axiomatic foundations of geometry https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-gupta http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Thesis https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-gupta http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-gupta http://www.w3.org/2000/01/rdf-schema#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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-pasch http://schema.org/author https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-pasch https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-pasch http://schema.org/datePublished 1882 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-pasch http://schema.org/name Vorlesungen ueber neuere Geometrie https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-pasch http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Book https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-pasch http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-pasch http://www.w3.org/2000/01/rdf-schema#comment Origin of the order axiom formalised in the artifact as inner_pasch. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://purl.org/dc/terms/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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://purl.org/dc/terms/identifier https://doi.org/10.1007/978-3-642-69418-9 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://schema.org/author https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-schwabhaeuser https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://schema.org/author https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-szmielew https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://schema.org/author https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-tarski https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://schema.org/datePublished 1983 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://schema.org/isbn 978-3-540-12958-5 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://schema.org/name Metamathematische Methoden in der Geometrie https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://schema.org/publisher Springer-Verlag, Berlin Heidelberg https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Book https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst http://www.w3.org/2000/01/rdf-schema#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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-tarski-givant http://purl.org/dc/terms/bibliographicCitation A. Tarski, S. Givant, Tarski's system of geometry, Bulletin of Symbolic Logic 5(2), 1999, pp. 175-214. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-tarski-givant http://schema.org/author https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/person-tarski https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-tarski-givant http://schema.org/contributor Steven Givant https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-tarski-givant http://schema.org/datePublished 1999 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-tarski-givant http://schema.org/name Tarski's system of geometry https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-tarski-givant http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/ScholarlyArticle https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-tarski-givant http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/provenance https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-declaration http://purl.org/dc/terms/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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-declaration http://schema.org/name Provenance declaration drafting and revision https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-declaration http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-declaration http://www.w3.org/ns/prov#endedAtTime 2026-07-29T00:00:00Z https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-declaration http://www.w3.org/ns/prov#startedAtTime 2026-07-18T10:37:00Z https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-declaration http://www.w3.org/ns/prov#used https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-declaration http://www.w3.org/ns/prov#used https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-declaration http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-declaration http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue http://purl.org/dc/terms/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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue http://schema.org/name Interactive formalization dialogue https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue http://www.w3.org/ns/prov#endedAtTime 2026-07-19T07:51:20Z https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue http://www.w3.org/ns/prov#generated https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue http://www.w3.org/ns/prov#generated https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue http://www.w3.org/ns/prov#startedAtTime 2026-07-18T08:47:58Z https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue http://www.w3.org/ns/prov#used https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue http://www.w3.org/ns/prov#used https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-sst https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact http://www.w3.org/ns/prov#wasGeneratedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-dialogue https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/assertion http://www.w3.org/ns/prov#wasAttributedTo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/assertion http://www.w3.org/ns/prov#wasAttributedTo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/assertion http://www.w3.org/ns/prov#wasDerivedFrom https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/assertion http://www.w3.org/ns/prov#wasGeneratedBy https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/activity-declaration https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-transcript http://spdx.org/rdf/terms#algorithm http://spdx.org/rdf/terms#checksumAlgorithm_sha256 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-transcript http://spdx.org/rdf/terms#checksumValue 213dbd5947f170c2e1480e894a20450442f4a6bde340df1492d6e6d86a7efd51 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-transcript http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://spdx.org/rdf/terms#Checksum https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript http://purl.org/dc/terms/identifier db0d830f-aa6a-432d-8675-0daf6066fb20 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript http://schema.org/dateCreated 2026-07-21T08:51:48Z https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript http://schema.org/encodingFormat application/json https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript http://schema.org/fileSize 69228 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript http://schema.org/name Conversation export: Pythagorean theorem in Lean4 inner product spaces https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript http://spdx.org/rdf/terms#checksum https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/checksum-transcript https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Dataset https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/transcript http://www.w3.org/2000/01/rdf-schema#comment Not publicly resolvable at the time of this declaration; the checksum permits verification if and when it is deposited. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/pubinfo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://purl.org/dc/terms/created 2026-07-29T15:00:47Z https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://purl.org/dc/terms/creator https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://purl.org/dc/terms/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. https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://purl.org/dc/terms/license http://creativecommons.org/publicdomain/zero/1.0/ https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://purl.org/nanopub/x/hasNanopubType http://www.w3.org/ns/prov#Attribution https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://purl.org/nanopub/x/introduces https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://www.w3.org/2000/01/rdf-schema#label Tarski.lean: attribution, ancestry and source concordance (v2) https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 http://www.w3.org/ns/prov#wasAttributedTo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/sig http://purl.org/nanopub/x/hasAlgorithm RSA https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/sig http://purl.org/nanopub/x/hasPublicKey MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/sig http://purl.org/nanopub/x/hasSignature XF1tMKmlAQ7I6eWkMWOOZe1Cl/B95TfuRo8alV/gL2oGOD75egvyJRifS1bD9Z6mJgFgcvJZAZi0xY4OSWusz7JMBUkw3dgb9+sM3WvEvJVHp6As0Ba4kyJt35rNoMl3SbaPbhLsDAhaw68EfBLKzlvW40T52tJ/j8QpU4WXNQBpRDodB9ODPIY5nwqZvj+HV+g5jGruDc6vGunTVg3JofhbF6KUaoOT1T2H6nUnz7hiPMhBaACxNkgDpZZkTeaMmmZW/wVtJesLgjiNgXTZ7FAlLMp+xaGxQSRnjt5XL9OCJJBrsKKTiVBtgnTuNjHMz/jU8+ekU979SE+5zxrF+A== https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/sig http://purl.org/nanopub/x/hasSignatureTarget https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/sig http://purl.org/nanopub/x/signedBy https://orcid.org/0000-0002-8042-4131