https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/Head https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0 http://www.nanopub.org/nschema#hasAssertion https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/assertion https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0 http://www.nanopub.org/nschema#hasProvenance https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/provenance https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0 http://www.nanopub.org/nschema#hasPublicationInfo https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/pubinfo https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.nanopub.org/nschema#Nanopublication https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/assertion https://provenance.example/tarski-lean/asserted-ai-coauthorship http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/UnverifiedSelfReportedClaim https://provenance.example/tarski-lean/asserted-ai-coauthorship https://provenance.example/tarski-lean/quotedText Drafted with Claude (Anthropic), which reconstructed and in places re-derived the proofs; errors are the draft's, not the tradition's. Directed and pursued to zero `sorry`s by the user. https://provenance.example/tarski-lean/asserted-ai-coauthorship https://provenance.example/tarski-lean/sourceLocation Tarski.lean, lines 69-71 (top-of-file comment block) https://provenance.example/tarski-lean/asserted-ai-coauthorship https://provenance.example/tarski-lean/subjectOfClaim https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/asserted-ai-coauthorship https://provenance.example/tarski-lean/whyUnverified This describes a human/AI drafting process external to the artifact's bytes. No session transcript, chat log, or other independently-checkable record of that drafting process was available to this session; the claim's truth cannot be established from the file alone. https://provenance.example/tarski-lean/asserted-completeness-of-proof http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/UnverifiedSelfReportedClaim https://provenance.example/tarski-lean/asserted-completeness-of-proof https://provenance.example/tarski-lean/quotedText Every theorem is fully proved -- no `sorry` remains. https://provenance.example/tarski-lean/asserted-completeness-of-proof https://provenance.example/tarski-lean/sourceLocation Tarski.lean, line 44 (top-of-file comment block) https://provenance.example/tarski-lean/asserted-completeness-of-proof https://provenance.example/tarski-lean/subjectOfClaim https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/asserted-completeness-of-proof https://provenance.example/tarski-lean/whyUnverified This claim is listed here because it originates as a self-report in the artifact's own prose. It is, however, corroborated by machine evidence: NP-A's axiom audit found sorryAx in 0 of 45 declarations. Recorded in both places deliberately -- the self-report and the independent machine check are different epistemic categories even when they agree. https://provenance.example/tarski-lean/asserted-full-chapter-mapping http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/UnverifiedSelfReportedClaim https://provenance.example/tarski-lean/asserted-full-chapter-mapping https://provenance.example/tarski-lean/quotedText Stage 0 - the axioms (SST ch. 1); Stage 1 - congruence is an equivalence; uniqueness of segment construction (SST ch. 2); Stage 2 - betweenness behaves (SST ch. 3); Stage 3 - vocabulary: Col, Out, SegLe (SST ch. 4); Stage 4 - point reflection (SST ch. 7); Ch04 block - Cong3, the inner five-segment lemma, betweenness transfer (SST ch. 4) https://provenance.example/tarski-lean/asserted-full-chapter-mapping https://provenance.example/tarski-lean/sourceLocation Tarski.lean, lines 33-42 (top-of-file comment block, 'Contents' section) https://provenance.example/tarski-lean/asserted-full-chapter-mapping https://provenance.example/tarski-lean/subjectOfClaim https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/asserted-full-chapter-mapping https://provenance.example/tarski-lean/whyUnverified Only the Stage-4/SST-7.13/GeoCoq-l7_13 correspondence was independently spot-checked (see NP-B, d:cite-geocoq-l7_13). The 1983 Schwabhauser-Szmielew-Tarski book itself was not opened to confirm that chapters 2, 3, and 4 actually contain the material these tags claim; this session only confirmed the book exists, its authorship, and its publisher (see NP-B). https://provenance.example/tarski-lean/asserted-originality http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/UnverifiedSelfReportedClaim https://provenance.example/tarski-lean/asserted-originality https://provenance.example/tarski-lean/quotedText This file reconstructs the architecture; it does not port GeoCoq code. https://provenance.example/tarski-lean/asserted-originality https://provenance.example/tarski-lean/sourceLocation Tarski.lean, lines 67-68 (top-of-file comment block) https://provenance.example/tarski-lean/asserted-originality https://provenance.example/tarski-lean/subjectOfClaim https://provenance.example/tarski-lean/artifact-Tarski-lean https://provenance.example/tarski-lean/asserted-originality https://provenance.example/tarski-lean/whyUnverified Verifying non-copying would require a line-by-line diff of this file's proof terms against GeoCoq's actual Coq source (a ~130,000-line library in a different proof language). That comparison was not performed in this session; the claim is recorded as the author's assertion only. https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/provenance https://provenance.example/tarski-lean/activity-separate http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://provenance.example/tarski-lean/activity-separate http://www.w3.org/2000/01/rdf-schema#label Sort artifact self-claims into verification buckets; isolate the unverifiable ones https://provenance.example/tarski-lean/activity-separate http://www.w3.org/ns/prov#wasAssociatedWith https://provenance.example/tarski-lean/agent-claude-sonnet-5 https://provenance.example/tarski-lean/agent-claude-sonnet-5 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#SoftwareAgent https://provenance.example/tarski-lean/agent-claude-sonnet-5 http://www.w3.org/2000/01/rdf-schema#label Claude Sonnet 5 (Anthropic), running as Claude Code https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/assertion http://purl.org/dc/terms/description Every d:quotedText value here is a literal quotation from the artifact's own comment text (retrieved and hashed in NP-A), reproduced verbatim so its accuracy as a quotation can be checked by re-reading the artifact. This nanopublication asserts only that the artifact contains these statements, and explains why this session could not establish whether the statements themselves are true. It does not assert that the quoted claims are true. https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/assertion http://www.w3.org/ns/prov#wasDerivedFrom https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/Tarski.lean https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/assertion http://www.w3.org/ns/prov#wasGeneratedBy https://provenance.example/tarski-lean/activity-separate https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/pubinfo https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0 http://purl.org/dc/terms/created 2026-08-10T12:57:30Z https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0 http://purl.org/dc/terms/creator https://orcid.org/0000-0002-8042-4131 https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0 http://purl.org/dc/terms/license https://creativecommons.org/licenses/by/4.0/ https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0 http://www.w3.org/2000/01/rdf-schema#label Tarski.lean: self-reported claims neither machine- nor source-verified (asserted bucket) https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0 https://provenance.example/tarski-lean/verificationBucket https://provenance.example/tarski-lean/Asserted https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/sig http://purl.org/nanopub/x/hasAlgorithm RSA https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/sig http://purl.org/nanopub/x/hasPublicKey MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/sig http://purl.org/nanopub/x/hasSignature fk58onT4AUkkd3epc0gQFvAKYQHAtJtQJa9tBHlnenndyyOyWlowJN/n6trKQmAfQGuUnD1Q7iaByRiShQPE3McWqaX0rq0xCI5iJ09jvLE0/yT8ZMPhNFi+ao9qABgGOK/Tc6h8ffCL5reF/v4vj7HYqoFi6x0VMjpTlGjpBYTzsm4fpxSjKYLYPbI/2GyPiIh+J/8wlFrHCqYh5PFpyC2PwwrCCinsafZFz+ZF55w0+cs1Wylti3wGnMk2GUeuq6yGlONwiHn+6Q/Poi4wCYwHtLa5tO7UWW+mJ1eDkRgat9fgjRDmP0Po0sLud6vg96iMZGJWTycUaYDonDM4yw== https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/sig http://purl.org/nanopub/x/hasSignatureTarget https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0 https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/sig http://purl.org/nanopub/x/signedBy https://orcid.org/0000-0002-8042-4131