https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/Head https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 http://www.nanopub.org/nschema#hasAssertion https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/assertion https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 http://www.nanopub.org/nschema#hasProvenance https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/provenance https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 http://www.nanopub.org/nschema#hasPublicationInfo https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/pubinfo https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.nanopub.org/nschema#Nanopublication https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/assertion https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/agent-reviewer http://schema.org/name Google Gemini https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/agent-reviewer http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/SoftwareApplication https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/agent-reviewer http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#SoftwareAgent https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/agent-reviewer http://www.w3.org/2000/01/rdf-schema#comment Performed the 2026-07-21 review pass. Specific model version not recorded. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-concordance http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-concordance http://schema.org/datePublished 2026-07-29 https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-concordance http://schema.org/name Erratum: withdrawal of the substituted concordance https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-concordance http://schema.org/text An intermediate revision replaced the concordance with the mapping inner_five_segment = SST 2.13, cong_sub = SST 2.14, cong3_construction = SST 2.16, betw_transfer = SST 3.17. That mapping is unsupported and is withdrawn. GeoCoq's convention is that the label lX_Y denotes SST Satz X.Y, so l4_2, l4_3, l4_5 and l4_6 denote Saetze 4.2, 4.3, 4.5 and 4.6, which is what the artifact's own source comments state and what the original concordance recorded. The concordance in NP1 was regenerated directly from the artifact's source text on 2026-07-29. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-concordance http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-concordance http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-myers http://schema.org/about https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/prior-art-geolean https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-myers http://schema.org/datePublished 2026-07-29 https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-myers http://schema.org/name Erratum: misattribution of GeoLean to Joseph Myers https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-myers http://schema.org/text GeoLean is the work of Bhavik Mehta alone. An assistant turn on 2026-07-18 attributed it to Joseph Myers, conflating it with Myers' analytic EuclideanGeometry development in Mathlib, which is a different body of work using a different approach. The 2026-07-21 external review pass partially corrected this by adding Mehta but retained Myers, producing the compound misattribution 'GeoLean Project (J. Myers, B. Mehta)'. Both forms are wrong and are withdrawn. Corrected against the leanprover Zulip archive, thread 'tarski axiom geometry', in which Mehta refers to GeoLean in the first person and separately distinguishes it from Joseph's development. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-myers http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-myers http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-sst-chapter http://purl.org/dc/terms/source https://doi.org/10.1007/978-3-642-69418-9 https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-sst-chapter http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/concordance https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-sst-chapter http://schema.org/datePublished 2026-07-29 https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-sst-chapter http://schema.org/name Erratum: withdrawal of the claimed SST chapter mismapping https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-sst-chapter http://schema.org/text An intermediate revision of this record asserted that SST chapter 4 is devoted exclusively to the upper dimension axiom, that the congruence-betweenness bridge lemmas belong to chapters 2 and 3, and that GeoCoq's 'Ch04' designation is a repository artifact. All three assertions are false and are withdrawn. In the 1983 Springer edition, chapter 4 is 'Einfache Saetze ueber Kongruenz und Zwischenbeziehung', pp. 34-38, which is exactly the bridge material; chapter 7 is 'Punktspiegelungen', pp. 49-56, the point reflections that SST 7.13 belongs to; and upper dimension is an axiom introduced with the axiom system, not a chapter. GeoCoq's file naming tracks the printed chapter sequence faithfully. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-sst-chapter http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/erratum-sst-chapter http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-geocoq-commit http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geocoq https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-geocoq-commit http://schema.org/name Gap: no GeoCoq or SST edition is pinned https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-geocoq-commit http://schema.org/text The artifact cites GeoCoq lemma labels but no commit, tag or version of GeoCoq was consulted or can be pinned, because the labels were reconstructed from the software agent's training data rather than read from the repository. Likewise no page-level citation to a specific printing of SST was checked at drafting time. Chapter titles and pagination were verified against the publisher's record on 2026-07-29; individual Satz numbers were not verified against the printed page and rest on GeoCoq's labelling convention. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-geocoq-commit http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-identity-binding http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-identity-binding http://schema.org/name Gap: repository identity is not bound to the declared ORCID https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-identity-binding http://schema.org/text The artifact is hosted under a GitHub account whose ownership is not cryptographically or publicly linked to the ORCID declared in NP1. Until the declaration is signed with a key bound to that identity, the attribution rests on assertion alone. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-identity-binding http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-model-version http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-model-version http://schema.org/name Gap: the model version is not recorded https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-model-version http://schema.org/text The conversation export identifies the software agent only as 'Claude (Anthropic PBC)'. The specific model version that produced the proofs is not recoverable from the record, which limits reproducibility of the generation step. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-model-version http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-no-license http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-no-license http://schema.org/name Gap: the artifact carries no licence https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-no-license http://schema.org/text The hosting repository contains no LICENSE file and Tarski.lean carries no licence header, so the artifact is under default exclusive copyright and cannot lawfully be reused, redistributed or built upon by third parties. This blocks the citation and reuse that the rest of this record is designed to enable. A permissive licence, Apache-2.0 to match Lean and Mathlib, should be added before publication. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/gap-no-license http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/non-derivation-geolean http://purl.org/dc/terms/references https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geolean https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/non-derivation-geolean http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/non-derivation-geolean http://schema.org/name Negative claim: no derivation relation holds between GeoLean and this artifact https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/non-derivation-geolean http://schema.org/text GeoLean was not consulted during the development of Tarski.lean. It surfaced only afterwards, during a web search on 2026-07-18 undertaken to check the publication landscape. No identifier, tactic or proof structure in Tarski.lean is inherited from it. The naming that Tarski.lean does inherit comes from GeoCoq's lemma labels and from SST's theorem numbering, both of which predate GeoLean. Asserting a GeoLean-to-Tarski.lean derivation, as an intermediate draft of this record did, would misdescribe the artifact and misattribute its lineage. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/non-derivation-geolean http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/non-origination http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/non-origination http://schema.org/name The software agent did not originate the mathematics https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/non-origination http://schema.org/text No mathematics in Tarski.lean is new. Every proved statement carries a printed SST theorem number, enumerated in the concordance in NP1; the axiom system is Tarski's, the order axiom is Pasch's, the axiom simplifications are Gupta's, and the proof architecture is that of SST Part I as machine-checked at scale in GeoCoq. The software agent's contribution is translation, reconstruction and exposition into Lean 4, together with the re-derivation of proof details it could not recall. Novelty, if any, is confined to the Lean 4 rendering and to the particular route taken through SST 7.13. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/non-origination http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/prior-art-geolean http://purl.org/dc/terms/references https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/src-geolean https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/prior-art-geolean http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/prior-art-geolean http://schema.org/name Prior art: Tarski.lean is not the first Tarski formalisation in Lean https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/prior-art-geolean http://schema.org/text The GeoLean branch of mathlib3, by Bhavik Mehta, ports a large portion of GeoCoq into Lean 3 and predates this artifact. Any claim of priority for Tarski.lean must be narrowed accordingly: what is distinctive is that it is a dependency-free single file in Lean 4 core, not that it is first. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/prior-art-geolean http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/review-finding http://schema.org/about https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/agent-reviewer https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/review-finding http://schema.org/name Finding: both automated review passes introduced citation errors https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/review-finding http://schema.org/text Two language models in sequence produced confident, well-formed, incorrect citations in the layer of the record whose function is trustworthiness: the drafting agent misattributed GeoLean, and the reviewing agent added a fabricated chapter erratum and a fabricated concordance while only partly fixing the misattribution it was reviewing. This is recorded as an empirical result about the method, not merely as housekeeping. It implies that a provenance record produced or reviewed by a language model requires source-level human or programmatic verification before it can carry evidential weight, and that the review step itself needs its own provenance. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/review-finding http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/scope-limit http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/scope-limit http://schema.org/name Scope: the development stops well short of Pythagoras https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/scope-limit http://schema.org/text The artifact reaches SST 7.15. It does not define right angles, does not construct the dropped perpendicular without continuity (SST 8.18, after Gupta 1965), does not prove midpoint existence (SST 8.22), and contains no line reflections, angles, parallels or segment arithmetic. The Pythagorean theorem, which motivated the trajectory, is not proved and is many chapters away; reaching it requires the construction of an ordered field from the geometry. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/scope-limit http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/unclaimed-independent-verification http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/unclaimed-independent-verification http://schema.org/name Unclaimed: independent verification by a human agent https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/unclaimed-independent-verification http://schema.org/text Compilation has been performed and is asserted in NP3, but by a software agent in an ephemeral sandbox. No human agent has independently re-run the build, and no continuous integration exists in the hosting repository to make the result repeatable on every commit. The CRediT validation role is therefore claimed only in the weak sense recorded in NP3, and independent replication remains outstanding. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/unclaimed-independent-verification http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/unclaimed-peer-review http://schema.org/about https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/unclaimed-peer-review http://schema.org/name Unclaimed: peer review and archival deposit https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/unclaimed-peer-review http://schema.org/text The artifact has not been refereed, has no DOI, and has not been deposited in an archival repository. Compilation establishes that the proofs are accepted by the Lean kernel; it does not establish that the axioms as transcribed are a faithful rendering of Tarski's, that the definitions are the intended ones, or that the statements are the ones SST proves. Those are questions of adequacy, not of soundness, and only a human reader of both texts can settle them. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/unclaimed-peer-review http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://schema.org/Claim https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/provenance https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction http://purl.org/dc/terms/description Each disputed claim in the 2026-07-21 revision was checked against a primary or near-primary source: chapter titles and pagination against the publisher's table of contents for the 1983 edition, the GeoLean attribution against the leanprover community Zulip archive, and the concordance against the artifact's own source text, retrieved and re-hashed on the same date. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction http://schema.org/name Source-level verification and correction of the declaration record https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction http://www.w3.org/ns/prov#startedAtTime 2026-07-29T00:00:00Z https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction http://www.w3.org/ns/prov#used https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/evidence-springer https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction http://www.w3.org/ns/prov#used https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/evidence-zulip https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction http://www.w3.org/ns/prov#used https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/artifact https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-review http://purl.org/dc/terms/description Produced the revision superseded by this record. Its one substantive contribution, the GeoLean prior-art disclosure, is retained in corrected form; its three citation claims are withdrawn under the errata above. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-review http://schema.org/name External review pass https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-review http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-review http://www.w3.org/ns/prov#endedAtTime 2026-07-21T13:56:27Z https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-review http://www.w3.org/ns/prov#generated https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/superseded-v1 https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-review http://www.w3.org/ns/prov#wasAssociatedWith https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/agent-reviewer https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/assertion http://www.w3.org/ns/prov#wasAttributedTo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/assertion http://www.w3.org/ns/prov#wasAttributedTo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-claude https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/assertion http://www.w3.org/ns/prov#wasGeneratedBy https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/checksum-superseded http://spdx.org/rdf/terms#algorithm http://spdx.org/rdf/terms#checksumAlgorithm_sha256 https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/checksum-superseded http://spdx.org/rdf/terms#checksumValue 3ce67a1938db370e60e2ad6794f1a401119d0e27a999b64da8bc4e3a3a29ed80 https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/checksum-superseded http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://spdx.org/rdf/terms#Checksum https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/checksum-superseded http://www.w3.org/2000/01/rdf-schema#comment Computed over the file as received, which was RTF-encoded and did not parse as JSON-LD. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/evidence-springer http://schema.org/name Publisher table of contents, SST 1983 https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/evidence-springer http://schema.org/url https://link.springer.com/book/10.1007/978-3-642-69418-9 https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/evidence-springer http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/evidence-springer http://www.w3.org/ns/prov#wasUsedBy https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/evidence-zulip http://schema.org/name leanprover community Zulip archive, stream maths, topic 'tarski axiom geometry' https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/evidence-zulip http://schema.org/url https://leanprover-community.github.io/archive/stream/116395-maths/topic/tarski.20axiom.20geometry.html https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/evidence-zulip http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/evidence-zulip http://www.w3.org/ns/prov#wasUsedBy https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/superseded-v1 http://schema.org/name Tarski_negative-space.jsonld (2026-07-21 revision) https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/superseded-v1 http://spdx.org/rdf/terms#checksum https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/checksum-superseded https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/superseded-v1 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/superseded-v1 http://www.w3.org/ns/prov#wasInvalidatedBy https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/activity-correction https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/pubinfo https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 http://purl.org/dc/terms/created 2026-07-29T15:00:47Z https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 http://purl.org/dc/terms/creator https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 http://purl.org/dc/terms/description Version 2. Records what the artifact does not claim, what credit is unclaimed, what the record itself does not know, and the specific errors introduced into earlier versions of this record by both the drafting and the reviewing agent. https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 http://purl.org/dc/terms/license http://creativecommons.org/publicdomain/zero/1.0/ https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 http://purl.org/dc/terms/relation https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4 https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 http://www.w3.org/2000/01/rdf-schema#label Tarski.lean: negative space, limits and errata (v2) https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 http://www.w3.org/ns/prov#wasAttributedTo https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/agent-axton https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/sig http://purl.org/nanopub/x/hasAlgorithm RSA https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/sig http://purl.org/nanopub/x/hasPublicKey MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/sig http://purl.org/nanopub/x/hasSignature DL8h/iZKQhW3dBm19cQeemf5y6vkDI9RgWuIhmGg2Ai/mChCJhNVFULVKJkT3lUZnvRBb7wSWgn52foCpejyY+G4UKgT2+fOe6vgaWXPc0evxnq9U3AFhwVRSZA9Gi/obCoIStBhLmS/TgEA2ziAbVQ63q//vx4Tcv5h9zKJdBaeciGuMr/Y8JBrtXdd3ZNpCR+oiPOQ1VHZAuaPWeQ5sivh4MCtbVBm71e8L7Jc29ACZsFNeGkElqgRJMOnuLDyHZylLkgy+VI6WMkSfeu75C7pid18R9Dh7o6ZibyvHOMlcXBiGeKqdzFKydVwyb+re9YsPJrJ8zuGUxM8XvGIUw== https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/sig http://purl.org/nanopub/x/hasSignatureTarget https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0 https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/sig http://purl.org/nanopub/x/signedBy https://orcid.org/0000-0002-8042-4131