rows {
  options {
    physical_type: PHYSICAL_STREAM_TYPE_QUADS
    max_name_table_size: 128
    max_prefix_table_size: 16
    max_datatype_table_size: 16
    logical_type: LOGICAL_STREAM_TYPE_DATASETS
    version: 2
  }
}
rows {
  prefix {
    value: "https://w3id.org/np/"
  }
}
rows {
  name {
    value: "RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk"
  }
}
rows {
  namespace {
    name: "this"
    value {
      prefix_id: 1
    }
  }
}
rows {
  prefix {
    value: "https://w3id.org/np/RAPZy_zxYnL2Ly--AORi9mIRX2gMsxs6IockxFuBf0Kvk/"
  }
}
rows {
  name {
  }
}
rows {
  namespace {
    name: "sub"
    value {
      prefix_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.nanopub.org/nschema#"
  }
}
rows {
  namespace {
    name: "np"
    value {
      prefix_id: 3
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://purl.org/dc/terms/"
  }
}
rows {
  namespace {
    name: "dct"
    value {
      prefix_id: 4
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "https://provenance.example/tarski-lean/"
  }
}
rows {
  namespace {
    name: "d"
    value {
      prefix_id: 5
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/2001/XMLSchema#"
  }
}
rows {
  namespace {
    name: "xsd"
    value {
      prefix_id: 6
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/2000/01/rdf-schema#"
  }
}
rows {
  namespace {
    name: "rdfs"
    value {
      prefix_id: 7
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "https://orcid.org/"
  }
}
rows {
  namespace {
    name: "orcid"
    value {
      prefix_id: 8
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/ns/prov#"
  }
}
rows {
  namespace {
    name: "prov"
    value {
      prefix_id: 9
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://purl.org/nanopub/x/"
  }
}
rows {
  namespace {
    name: "npx"
    value {
      prefix_id: 10
      name_id: 2
    }
  }
}
rows {
  name {
    value: "hasAssertion"
  }
}
rows {
  name {
    value: "assertion"
  }
}
rows {
  name {
    value: "Head"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 1
      name_id: 1
    }
    p_iri {
      prefix_id: 3
      name_id: 3
    }
    o_iri {
      prefix_id: 2
    }
    g_iri {
    }
  }
}
rows {
  name {
    value: "hasProvenance"
  }
}
rows {
  name {
    value: "provenance"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  name {
    value: "hasPublicationInfo"
  }
}
rows {
  name {
    value: "pubinfo"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/1999/02/22-rdf-syntax-ns#"
  }
}
rows {
  name {
    value: "type"
  }
}
rows {
  name {
    value: "Nanopublication"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 11
    }
    o_iri {
      prefix_id: 3
    }
  }
}
rows {
  name {
    value: "artifact-Tarski-lean"
  }
}
rows {
  name {
    value: "license"
  }
}
rows {
  prefix {
    value: "http://www.apache.org/licenses/"
  }
}
rows {
  name {
    value: "LICENSE-2.0"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 5
    }
    p_iri {
      prefix_id: 4
    }
    o_iri {
      prefix_id: 12
    }
    g_iri {
      prefix_id: 2
      name_id: 4
    }
  }
}
rows {
  name {
    value: "authorIdentityBinding"
  }
}
rows {
  name {
    value: "0000-0002-8042-4131"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
      name_id: 15
    }
    o_iri {
      prefix_id: 8
    }
  }
}
rows {
  name {
    value: "commitAuthorEmail"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "myle54xton@gmail.com"
    }
  }
}
rows {
  name {
    value: "commitAuthorName"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Myles Axton"
    }
  }
}
rows {
  name {
    value: "commitDate"
  }
}
rows {
  datatype {
    value: "http://www.w3.org/2001/XMLSchema#dateTime"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "2026-08-07T10:03:56Z"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "commitMessage"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Add copyright and license information to Tarski.lean"
    }
  }
}
rows {
  name {
    value: "commitSha"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "802b1d583032c44ea9affb2a61b0c8cda6c60b72"
    }
  }
}
rows {
  name {
    value: "copyrightLineQuoted"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Copyright 2026 John Myles Axton orcid:0000-0002-8042-4131"
    }
  }
}
rows {
  name {
    value: "copyrightLineSourceLocation"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Tarski.lean, line 2 (top-of-file comment block)"
    }
  }
}
rows {
  name {
    value: "hasNamespace"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic (Lean namespace; declarations are qualified as Synthetic.<name>, e.g. Synthetic.cong_refl)"
    }
  }
}
rows {
  name {
    value: "licenseEvidence"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Two independent, mutually consistent sources: (1) the file\'s own header states \'Licensed under the Apache License, Version 2.0\'; (2) the GitHub repository API (api.github.com/repos/johnmaxton/lean4-starter) reports license.spdx_id = \'Apache-2.0\', backed by a LICENSE file at repo root matching the standard Apache 2.0 text."
    }
  }
}
rows {
  name {
    value: "priorCommitDate"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "2026-07-18T14:18:18Z"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "priorCommitMessage"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Add Tarski\'s synthetic Euclidean geometry (Stages 0-4)"
    }
  }
}
rows {
  name {
    value: "priorCommitSha"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "90018aec70b2bb8950c1045cac443731825d79ef"
    }
  }
}
rows {
  name {
    value: "cite-dependency-free"
  }
}
rows {
  name {
    value: "CheckedClaim"
  }
}
rows {
  quad {
    s_iri {
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 30
    }
  }
}
rows {
  name {
    value: "label"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
    }
    o_literal {
      lex: "File is dependency-free (compiles with core Lean 4 alone, no Mathlib)"
    }
  }
}
rows {
  name {
    value: "asClaimedByArtifact"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "This file is dependency-free: it compiles with core Lean 4 alone (`lean Tarski.lean`), no Mathlib required."
    }
  }
}
rows {
  name {
    value: "verificationMethod"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "grep for \'^import\' in Tarski.lean returned zero matches; lake-manifest.json at the pinned commit lists packages: [] (zero external dependencies); the successful build in NP-A used only this manifest."
    }
  }
}
rows {
  name {
    value: "verificationResult"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "CONFIRMED (this claim is machine-verifiable and is additionally recorded in NP-A\'s compilation evidence)."
    }
  }
}
rows {
  name {
    value: "cite-geocoq-authors"
  }
}
rows {
  name {
    value: "CheckedCitation"
  }
}
rows {
  quad {
    s_iri {
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 36
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
      name_id: 31
    }
    o_literal {
      lex: "GeoCoq project authorship"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "GeoCoq (J. Narboux, M. Beeson, P. Boutry, G. Braun, C. Gries, P. Schreck, et al.): the first machine-checked ascent."
    }
  }
}
rows {
  name {
    value: "verificationNote"
  }
}
rows {
  quad {
    p_iri {
      name_id: 37
    }
    o_literal {
      lex: "The repo\'s top-level AUTHORS file lists Beeson, Boutry, Braun, Gries, Kastenbaum, Narboux (omitting Schreck); the coq-geocoq-axioms.opam package metadata\'s authors field lists exactly Beeson, Braun, Boutry, Gries, Narboux, Schreck -- matching the artifact\'s six named credits verbatim. Both sources were checked; the opam file is the one that fully confirms the claim as written."
    }
  }
}
rows {
  name {
    value: "verifiedAgainst"
  }
}
rows {
  prefix {
    value: "https://raw.githubusercontent.com/GeoCoq/GeoCoq/master/"
  }
}
rows {
  name {
    value: "coq-geocoq-axioms.opam"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 13
    }
  }
}
rows {
  name {
    value: "cite-geocoq-l7_13"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 5
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 36
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
      name_id: 31
    }
    o_literal {
      lex: "GeoCoq lemma l7_13 corresponds to SST chapter 7 (midpoint / point reflection)"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "The capstone is SST 7.13 (GeoCoq l7_13): point reflection preserves congruence."
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 37
    }
    o_literal {
      lex: "GeoCoq\'s official documentation page confirms l7_13 is defined in the Ch07_midpoint module and concerns congruence preservation under point-reflection/midpoint symmetry, consistent with the artifact\'s claim that it corresponds to SST theorem 7.13. This is a spot-check of one specific chapter/lemma pairing, not a verification of every \'SST n.m\' tag in the file (see NP-D)."
    }
  }
}
rows {
  prefix {
    value: "https://geocoq.github.io/GeoCoq/html/"
  }
}
rows {
  name {
    value: "GeoCoq.Tarski_dev.Ch07_midpoint.html"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 14
      name_id: 41
    }
  }
}
rows {
  name {
    value: "cite-sst-1983"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 5
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 36
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
      name_id: 31
    }
    o_literal {
      lex: "Schwabh\303\244user, Szmielew, Tarski, \"Metamathematische Methoden in der Geometrie\", Springer-Verlag, Berlin, 1983"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "W. Schwabh\303\244user: completed and published SST (1983); the \"SST n.m\" tags cite all three authors."
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 37
    }
    o_literal {
      lex: "Title, three authors, publisher, and 1983 date confirmed via Springer Link and a Journal of Symbolic Logic review. Chapter-by-chapter content of the book was NOT opened or checked against the artifact\'s per-stage chapter tags (see NP-D, negative space) except for the single spot-check in d:cite-geocoq-l7_13 below."
    }
  }
}
rows {
  prefix {
    value: "https://link.springer.com/book/10.1007/"
  }
}
rows {
  name {
    value: "978-3-642-69418-9"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 15
      name_id: 43
    }
  }
}
rows {
  prefix {
    value: "https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/wolfram-schwabhauser-wanda-szmielew-and-alfred-tarski-ein-axiomatischer-aujbau-der-euklidischen-geometrie-metamathematische-methoden-in-der-geometrie-hochschultext-springerverlag-berlin-etc-1983-pp-1171-wolfram-schwabhauser-metamathematische-betrachtungen-metamathematische-methoden-in-der-geometrie-pp-173457/"
  }
}
rows {
  name {
    value: "47332AEED25CD5AB54C9A989C7D1718B"
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 16
    }
  }
}
rows {
  name {
    value: "cite-tarski-givant-1999"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 5
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 36
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
      name_id: 31
    }
    o_literal {
      lex: "Tarski & Givant, \"Tarski\'s System of Geometry\", Bulletin of Symbolic Logic, vol. 5, no. 2, pp. 175-214, 1999"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "A. Tarski (1926-27; Tarski & Givant, BSL 1999): the axiom system and the completeness/decidability metatheorems."
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 37
    }
    o_literal {
      lex: "Publication venue, volume, issue, and page range (175-214) confirmed as consistent across PhilPapers, Semantic Scholar, and Cambridge Core listings."
    }
  }
}
rows {
  prefix {
    id: 6
    value: "https://philpapers.org/rec/"
  }
}
rows {
  name {
    value: "TARTSO"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 6
      name_id: 46
    }
  }
}
rows {
  prefix {
    id: 9
    value: "https://www.semanticscholar.org/paper/Tarski\'s-System-of-Geometry-Tarski-Givant/"
  }
}
rows {
  name {
    value: "f9dc27b0f3f9436f0b194ecc6f558a74d346e0e6"
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 9
    }
  }
}
rows {
  name {
    value: "activity-ground"
  }
}
rows {
  prefix {
    value: "http://www.w3.org/ns/prov#"
  }
}
rows {
  name {
    value: "Activity"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 5
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 10
      name_id: 49
    }
    g_iri {
      prefix_id: 2
      name_id: 7
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
      name_id: 31
    }
    o_literal {
      lex: "Build theorem-to-source concordance; check external historical/authorship claims against citable sources"
    }
  }
}
rows {
  name {
    value: "wasAssociatedWith"
  }
}
rows {
  name {
    value: "agent-claude-sonnet-5"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 10
      name_id: 50
    }
    o_iri {
      prefix_id: 5
    }
  }
}
rows {
  name {
    value: "SoftwareAgent"
  }
}
rows {
  quad {
    s_iri {
      name_id: 51
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 10
      name_id: 52
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
      name_id: 31
    }
    o_literal {
      lex: "Claude Sonnet 5 (Anthropic), running as Claude Code"
    }
  }
}
rows {
  name {
    value: "description"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 4
    }
    p_iri {
      prefix_id: 4
      name_id: 53
    }
    o_literal {
      lex: "Each statement here was checked against a specific, cited, dereferenceable external document during this session (via HTTP fetch and web search), not recalled from training data. Where a claim\'s underlying content could not be checked in full (e.g. every \'SST n.m\' chapter tag), that limit is stated explicitly in d:verificationNote rather than extended by inference."
    }
  }
}
rows {
  name {
    value: "wasDerivedFrom"
  }
}
rows {
  prefix {
    id: 1
    value: "https://api.github.com/repos/johnmaxton/"
  }
}
rows {
  name {
    value: "lean4-starter"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 10
    }
    o_iri {
      prefix_id: 1
    }
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 14
      name_id: 41
    }
  }
}
rows {
  prefix {
    id: 3
    value: "https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/"
  }
}
rows {
  name {
    value: "Tarski.lean"
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 3
      name_id: 56
    }
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 15
      name_id: 43
    }
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 6
      name_id: 46
    }
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 13
      name_id: 39
    }
  }
}
rows {
  name {
    value: "wasGeneratedBy"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 10
      name_id: 57
    }
    o_iri {
      prefix_id: 5
      name_id: 48
    }
  }
}
rows {
  prefix {
    id: 12
    value: "https://w3id.org/np/"
  }
}
rows {
  name {
    value: "created"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 12
      name_id: 1
    }
    p_iri {
      prefix_id: 4
      name_id: 58
    }
    o_literal {
      lex: "2026-08-10T12:57:30Z"
      datatype: 1
    }
    g_iri {
      prefix_id: 2
      name_id: 9
    }
  }
}
rows {
  name {
    value: "creator"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 4
      name_id: 59
    }
    o_iri {
      prefix_id: 8
      name_id: 16
    }
  }
}
rows {
  prefix {
    id: 16
    value: "https://creativecommons.org/licenses/by/4.0/"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 4
      name_id: 13
    }
    o_iri {
      prefix_id: 16
      name_id: 2
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
      name_id: 31
    }
    o_literal {
      lex: "Tarski.lean: license, authorship, and historical-citation grounding (source-verified)"
    }
  }
}
rows {
  name {
    value: "verificationBucket"
  }
}
rows {
  name {
    value: "SourceVerified"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
      name_id: 60
    }
    o_iri {
    }
  }
}
rows {
  name {
    value: "sig"
  }
}
rows {
  prefix {
    id: 9
    value: "http://purl.org/nanopub/x/"
  }
}
rows {
  name {
    value: "hasAlgorithm"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
    }
    p_iri {
      prefix_id: 9
    }
    o_literal {
      lex: "RSA"
    }
  }
}
rows {
  name {
    value: "hasPublicKey"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB"
    }
  }
}
rows {
  name {
    value: "hasSignature"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "cQjcMTuBG6lzr3xucx4Xaq9ahrq64h700CRi9bgyn+2JmJ97tmSftMy9Vj4AjcbGrgECMLHwD9qdsZXzPThZLhtd5MIpGvcZ7ea9hVlPb2Qf5yYqmN99GKWjRFyL7zsRSlOsPLNxsCgP18aJhGbhEO+AkWrx7rJWHbYmS0ffiKZTT+Gu5G9z0HsrKrZUvlDTj/NVBhbr61Kjbi7gA5PuuWrbry7mSiLX+5RBBbx13uirDTGzsVMBtMqHSIocP8AS0VLjVaD2Ct+8Cb1NmxKyX1U5l7EuZkHJBgp/vFo4YG0/SWYJnDz7Ket4Fl/Bp/cABALsxfV/P0/MjxMj8WwtWQ=="
    }
  }
}
rows {
  name {
    value: "hasSignatureTarget"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 12
      name_id: 1
    }
  }
}
rows {
  name {
    value: "signedBy"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
      name_id: 67
    }
    o_iri {
      prefix_id: 8
      name_id: 16
    }
  }
}