Nanopublication

ID

https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0
Formats

Content

@prefix this: <https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0> .
@prefix sub: <https://w3id.org/np/RAFG2VXoLIbpCSbU5LxtYw1k6ehvliwj5NxDR15I3ZBh0/> .
@prefix np: <http://www.nanopub.org/nschema#> .
@prefix dct: <http://purl.org/dc/terms/> .
@prefix d: <https://provenance.example/tarski-lean/> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix orcid: <https://orcid.org/> .
@prefix prov: <http://www.w3.org/ns/prov#> .
@prefix npx: <http://purl.org/nanopub/x/> .

sub:Head {
  this: a np:Nanopublication;
    np:hasAssertion sub:assertion;
    np:hasProvenance sub:provenance;
    np:hasPublicationInfo sub:pubinfo .
}

sub:assertion {
  d:asserted-ai-coauthorship a d:UnverifiedSelfReportedClaim;
    d: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.";
    d:sourceLocation "Tarski.lean, lines 69-71 (top-of-file comment block)";
    d:subjectOfClaim d:artifact-Tarski-lean;
    d: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." .
  
  d:asserted-completeness-of-proof a d:UnverifiedSelfReportedClaim;
    d:quotedText "Every theorem is fully proved -- no `sorry` remains.";
    d:sourceLocation "Tarski.lean, line 44 (top-of-file comment block)";
    d:subjectOfClaim d:artifact-Tarski-lean;
    d: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." .
  
  d:asserted-full-chapter-mapping a d:UnverifiedSelfReportedClaim;
    d: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)";
    d:sourceLocation "Tarski.lean, lines 33-42 (top-of-file comment block, 'Contents' section)";
    d:subjectOfClaim d:artifact-Tarski-lean;
    d: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)." .
  
  d:asserted-originality a d:UnverifiedSelfReportedClaim;
    d:quotedText "This file reconstructs the architecture; it does not port GeoCoq code.";
    d:sourceLocation "Tarski.lean, lines 67-68 (top-of-file comment block)";
    d:subjectOfClaim d:artifact-Tarski-lean;
    d: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." .
}

sub:provenance {
  d:activity-separate a prov:Activity;
    rdfs:label "Sort artifact self-claims into verification buckets; isolate the unverifiable ones";
    prov:wasAssociatedWith d:agent-claude-sonnet-5 .
  
  d:agent-claude-sonnet-5 a prov:SoftwareAgent;
    rdfs:label "Claude Sonnet 5 (Anthropic), running as Claude Code" .
  
  sub:assertion dct: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.";
    prov:wasDerivedFrom <https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/Tarski.lean>;
    prov:wasGeneratedBy d:activity-separate .
}

sub:pubinfo {
  this: dct:created "2026-08-10T12:57:30Z"^^xsd:dateTime;
    dct:creator orcid:0000-0002-8042-4131;
    dct:license <https://creativecommons.org/licenses/by/4.0/>;
    rdfs:label "Tarski.lean: self-reported claims neither machine- nor source-verified (asserted bucket)";
    d:verificationBucket d:Asserted .
  
  sub:sig npx:hasAlgorithm "RSA";
    npx:hasPublicKey "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB";
    npx:hasSignature "fk58onT4AUkkd3epc0gQFvAKYQHAtJtQJa9tBHlnenndyyOyWlowJN/n6trKQmAfQGuUnD1Q7iaByRiShQPE3McWqaX0rq0xCI5iJ09jvLE0/yT8ZMPhNFi+ao9qABgGOK/Tc6h8ffCL5reF/v4vj7HYqoFi6x0VMjpTlGjpBYTzsm4fpxSjKYLYPbI/2GyPiIh+J/8wlFrHCqYh5PFpyC2PwwrCCinsafZFz+ZF55w0+cs1Wylti3wGnMk2GUeuq6yGlONwiHn+6Q/Poi4wCYwHtLa5tO7UWW+mJ1eDkRgat9fgjRDmP0Po0sLud6vg96iMZGJWTycUaYDonDM4yw==";
    npx:hasSignatureTarget this:;
    npx:signedBy orcid:0000-0002-8042-4131 .
}