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: "RAXut_tYBIBaf53frjHN9ttCnUj4zq8JhXllSz7MyKpME"
  }
}
rows {
  namespace {
    name: "this"
    value {
      prefix_id: 1
    }
  }
}
rows {
  prefix {
    value: "https://w3id.org/np/RAXut_tYBIBaf53frjHN9ttCnUj4zq8JhXllSz7MyKpME/"
  }
}
rows {
  name {
  }
}
rows {
  namespace {
    name: "sub"
    value {
      prefix_id: 2
    }
  }
}
rows {
  prefix {
    value: "https://schema.org/"
  }
}
rows {
  namespace {
    name: "schema"
    value {
      prefix_id: 3
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.nanopub.org/nschema#"
  }
}
rows {
  namespace {
    name: "np"
    value {
      prefix_id: 4
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://purl.org/dc/terms/"
  }
}
rows {
  namespace {
    name: "dct"
    value {
      prefix_id: 5
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "https://w3id.org/np/o/ntemplate/"
  }
}
rows {
  namespace {
    name: "nt"
    value {
      prefix_id: 6
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/2001/XMLSchema#"
  }
}
rows {
  namespace {
    name: "xsd"
    value {
      prefix_id: 7
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/2000/01/rdf-schema#"
  }
}
rows {
  namespace {
    name: "rdfs"
    value {
      prefix_id: 8
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "https://orcid.org/"
  }
}
rows {
  namespace {
    name: "orcid"
    value {
      prefix_id: 9
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://purl.org/iscc/terms/"
  }
}
rows {
  namespace {
    name: "iscc"
    value {
      prefix_id: 10
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://purl.org/faia/terms/"
  }
}
rows {
  namespace {
    name: "faia"
    value {
      prefix_id: 11
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "https://credit.niso.org/contributor-roles/"
  }
}
rows {
  namespace {
    name: "credit"
    value {
      prefix_id: 12
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/ns/prov#"
  }
}
rows {
  namespace {
    name: "prov"
    value {
      prefix_id: 13
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://purl.org/nanopub/x/"
  }
}
rows {
  namespace {
    name: "npx"
    value {
      prefix_id: 14
      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: 4
      name_id: 3
    }
    o_iri {
      prefix_id: 2
    }
    g_iri {
    }
  }
}
rows {
  name {
    value: "hasProvenance"
  }
}
rows {
  name {
    value: "provenance"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 4
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  name {
    value: "hasPublicationInfo"
  }
}
rows {
  name {
    value: "pubinfo"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 4
    }
    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: 15
    }
    o_iri {
      prefix_id: 4
    }
  }
}
rows {
  name {
    value: "agent-claude"
  }
}
rows {
  name {
    value: "description"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
    }
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "Drafted all Lean code and documentation; reconstructed and in places re-derived the proofs (see sub:faia). In a follow-up session, diagnosed and fixed the sole compile error and verified compilation under two toolchains (see sub:activity-verify). Not an author under prevailing scholarly norms; correctly credited by acknowledgment. All errors in the draft are attributable here, not to the mathematical tradition."
    }
    g_iri {
      prefix_id: 2
      name_id: 4
    }
  }
}
rows {
  name {
    value: "SoftwareAgent"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 14
    }
  }
}
rows {
  name {
    value: "hadRole"
  }
}
rows {
  name {
    value: "software"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 12
    }
  }
}
rows {
  name {
    value: "validation"
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  name {
    value: "writing-original-draft"
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  name {
    value: "name"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
    }
    o_literal {
      lex: "Claude (Anthropic)"
    }
  }
}
rows {
  name {
    value: "agent-euclid"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "The axiomatic ideal the artifact rebuilds; the original tower (Elements, Book I), including target propositions I.47\342\200\223I.48 (Pythagoras and converse) and Definition I.10, echoed in the planned `Per` (SST ch. 8)."
    }
  }
}
rows {
  name {
    value: "Person"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 21
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 15
    }
    o_literal {
      lex: "Intellectual ancestor"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Euclid of Alexandria (fl. c. 300 BCE)"
    }
  }
}
rows {
  name {
    value: "agent-geocoq"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 22
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "First machine-checked ascent of the SST development (Coq, from Narboux 2006 onward). The artifact reconstructs the GeoCoq architecture and navigated by its lemma map (l4_2 \342\206\222 inner_five_segment, l4_3 \342\206\222 cong_sub, l4_5 \342\206\222 cong3_construction, l4_6 \342\206\222 betw_transfer, l7_13 \342\206\222 reflect_cong, l7_15 \342\206\222 reflect_betw) but ports no GeoCoq code."
    }
  }
}
rows {
  name {
    value: "Organization"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 23
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 15
    }
    o_literal {
      lex: "Formal ancestor"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "GeoCoq project (J. Narboux, M. Beeson, P. Boutry, G. Braun, C. Gries, P. Schreck, et al.)"
    }
  }
}
rows {
  name {
    value: "url"
  }
}
rows {
  prefix {
    value: "https://github.com/GeoCoq/"
  }
}
rows {
  name {
    value: "GeoCoq"
  }
}
rows {
  quad {
    p_iri {
      name_id: 24
    }
    o_iri {
      prefix_id: 16
    }
  }
}
rows {
  name {
    value: "agent-gupta"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "PhD dissertation, UC Berkeley 1965, under Tarski: axiom independence and simplification (several axioms are as lean as A1\342\200\223A8 because of him), and the perpendicular and midpoint constructions without any continuity axiom \342\200\224 SST 8.18 and 8.22, the declared next stage of this artifact, not yet contained in it."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 21
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 15
    }
    o_literal {
      lex: "Axiom simplifier; author of the continuity-free constructions ahead"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Haragauri Narayan Gupta (1925\342\200\2232016)"
    }
  }
}
rows {
  name {
    value: "agent-hilbert"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 27
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "Grundlagen der Geometrie (1899): the modern axiomatic program, and the segment arithmetic (Streckenrechnung, cf. SST ch. 14\342\200\22315) that is the declared future route from this artifact to Pythagoras."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 21
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 15
    }
    o_literal {
      lex: "Program architect"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "David Hilbert (1862\342\200\2231943)"
    }
  }
}
rows {
  name {
    value: "agent-pasch"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 28
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "Discovered that order is an assumption, not a triviality (Vorlesungen \303\274ber neuere Geometrie, 1882). Namesake of axiom A7 (`inner_pasch`), on which the whole of Stage 2 rests: SST 3.1 (betw_trivial, indirectly), 3.2 (betw_symm), 3.5 (betw_inner_trans)."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 21
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 15
    }
    o_literal {
      lex: "Axiom source"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Moritz Pasch (1843\342\200\2231930)"
    }
  }
}
rows {
  name {
    value: "agent-schwabhaeuser"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 29
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "Completed and published the treatise: Schwabh\303\244user, Szmielew, Tarski, \'Metamathematische Methoden in der Geometrie\', Springer 1983. Every \'SST n.m\' tag in the artifact cites all three authors through his numbering."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 21
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 15
    }
    o_literal {
      lex: "Systematizer and publisher"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Wolfram Schwabh\303\244user (1931\342\200\2231985)"
    }
  }
}
rows {
  name {
    value: "agent-szmielew"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 30
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "Part I of SST grew from her lectures; the artifact follows her development lemma-for-lemma: SST 2.1\342\200\2232.5, 2.8, 2.11, 2.12 (congruence calculus, segment addition, construction uniqueness); 3.1\342\200\2233.3, 3.5, 3.6(1), 3.6(2), 3.7(1), 3.7(2) (betweenness calculus); 4.2, 4.3, 4.5, 4.6 (congruence\342\200\223betweenness bridge); 7.4, 7.5, 7.13, 7.15 (point reflection and its isometry). She died before publication; her share of the credit is frequently understated."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 21
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 15
    }
    o_literal {
      lex: "Development author (followed lemma-for-lemma)"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Wanda Szmielew (1918\342\200\2231976)"
    }
  }
}
rows {
  name {
    value: "agent-tarski"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 31
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "The axiom system formalized as the `Tarski` typeclass, axioms A1\342\200\223A8 (cong_pseudo_refl, cong_inner_trans, cong_identity, segment_construction, five_segment, betw_identity, inner_pasch, lower_dim), developed 1926\342\200\22327; completeness and decidability of elementary geometry, guaranteeing the synthetic development agrees with EuclideanSpace \342\204\235 (Fin n) on all first-order sentences. Survey citation: Tarski & Givant, \'Tarski\'s System of Geometry\', Bulletin of Symbolic Logic 5(2), 1999."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 21
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 15
    }
    o_literal {
      lex: "Axiom-system author; metatheorist"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Alfred Tarski (1901\342\200\2231983)"
    }
  }
}
rows {
  name {
    value: "agent-user"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 32
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "Set the organizing question and metaphor (being \'trapped\' in EuclideanSpace \342\204\235 (Fin n) with only straightedge and compass), chose each descent (perpendiculars \342\206\222 compiling file \342\206\222 SST ch. 4 block \342\206\222 SST 7.13), and supplied the persistence that drove the artifact to zero `sorry`s. Directed the follow-up session that found a working Lean toolchain, compiled the artifact, and requested the fix for the sole compile error. Holds the director\'s and verifier\'s credit."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 21
    }
  }
}
rows {
  name {
    value: "conceptualization"
  }
}
rows {
  quad {
    p_iri {
      name_id: 15
    }
    o_iri {
      prefix_id: 12
      name_id: 33
    }
  }
}
rows {
  name {
    value: "supervision"
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  quad {
    o_iri {
      name_id: 17
    }
  }
}
rows {
  name {
    value: "identifier"
  }
}
rows {
  name {
    value: "0000-0002-8042-4131"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 35
    }
    o_iri {
      prefix_id: 9
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Myles Axton"
    }
  }
}
rows {
  name {
    value: "sameAs"
  }
}
rows {
  quad {
    p_iri {
      name_id: 37
    }
    o_iri {
      prefix_id: 9
      name_id: 36
    }
  }
}
rows {
  name {
    value: "artifact"
  }
}
rows {
  name {
    value: "contributor"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 38
    }
    p_iri {
      prefix_id: 5
    }
    o_iri {
      prefix_id: 2
      name_id: 12
    }
  }
}
rows {
  quad {
    o_iri {
      name_id: 20
    }
  }
}
rows {
  quad {
    o_iri {
      name_id: 22
    }
  }
}
rows {
  quad {
    o_iri {
      name_id: 26
    }
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  name {
    value: "relation"
  }
}
rows {
  name {
    value: "dedication"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
      name_id: 40
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  name {
    value: "tableOfContents"
  }
}
rows {
  name {
    value: "sst-map"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  name {
    value: "declaration"
  }
}
rows {
  name {
    value: "faia"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 11
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  name {
    value: "iscc"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 10
    }
    o_literal {
      lex: "ISCC:PENDING \342\200\224 see sub:isccNote"
    }
  }
}
rows {
  name {
    value: "Entity"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 47
    }
  }
}
rows {
  name {
    value: "SoftwareSourceCode"
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 3
    }
  }
}
rows {
  name {
    value: "codeRepository"
  }
}
rows {
  prefix {
    id: 6
    value: "https://github.com/johnmaxton/lean4-starter/blob/90018aec70b2bb8950c1045cac443731825d79ef/"
  }
}
rows {
  name {
    value: "Tarski.lean"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 6
    }
  }
}
rows {
  name {
    value: "contentSize"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
    }
    o_literal {
      lex: "28435 bytes (648 lines)"
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 13
    }
    o_literal {
      lex: "A synthetic development of Tarski\'s Euclidean geometry following Schwabh\303\244user\342\200\223Szmielew\342\200\223Tarski (SST) chapters 2\342\200\2237: eleven axioms over two primitives (betweenness, segment congruence), developed through SST 7.13/7.15 (point reflection is an isometry). Zero `sorry`s. Compiles cleanly (`lean Tarski.lean` and `lake build`, exit 0) under both leanprover/lean4-nightly:nightly-2023-05-16 and leanprover/lean4:v4.32.0, confirming the dependency-free (core-Lean-4-only) claim across toolchain versions."
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 19
    }
    o_literal {
      lex: "Tarski.lean"
    }
  }
}
rows {
  name {
    value: "programmingLanguage"
  }
}
rows {
  quad {
    p_iri {
      name_id: 52
    }
    o_literal {
      lex: "Lean 4 (core language only; no Mathlib dependency)"
    }
  }
}
rows {
  name {
    value: "sha256"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "1372181e2284465648cf15fdd9b7a761ceef9288224feccfd71fb63a5417bfd1"
    }
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 41
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "Myles Axton thanks his father, Richard Axton (1941\342\200\2232021), for his introduction to Euclidean geometry and the inspiration to do more with less (straight edge and compass only)."
    }
  }
}
rows {
  name {
    value: "Comment"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 3
      name_id: 54
    }
  }
}
rows {
  name {
    value: "about"
  }
}
rows {
  name {
    value: "person-richard-axton"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Dedication"
    }
  }
}
rows {
  name {
    value: "aiContribution"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 45
    }
    p_iri {
      prefix_id: 11
      name_id: 57
    }
    o_literal {
      lex: "Reconstruction of the SST/GeoCoq proof architecture from model memory; independent re-derivation where memory was insufficient (the SST 4.5 scaffold bookkeeping; SST 3.7(2) via mirror application of 3.7(1); the five-segment slot assignments in SST 7.13); translation into dependency-free core Lean 4; expository docstrings. In the follow-up session: diagnosed and fixed one compile error (the `example` at the end of Stage 5 used Mathlib\'s `\342\210\203!` unique-existence notation, unavailable in core Lean 4; rewritten as its explicit unfolding), then verified compilation."
    }
  }
}
rows {
  name {
    value: "aiSystem"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Claude (Anthropic), Claude Fable 5, chat interface, sandboxed (no network, no Lean toolchain), for the original drafting session; Claude (Anthropic), Claude Sonnet 5, Claude Code CLI, with network and a working Lean 4 toolchain, for the subsequent compilation and fix session."
    }
  }
}
rows {
  name {
    value: "humanOversight"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Every construction and proof step was chosen or approved turn-by-turn in dialogue; the human set direction, scope, and the requirement of resolving all `sorry`s. The human also directed the follow-up build/fix/compile session and reviewed its result before this declaration was finalized."
    }
  }
}
rows {
  name {
    value: "knownLimitations"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "The artifact now compiles cleanly under two independent Lean 4 toolchains (see schema:description); this discharges the compilation-verification limitation noted in the original sandbox draft. Remaining limitations: the mathematical content has not been cross-checked against an independent formalization (e.g. GeoCoq itself) beyond the lemma-map correspondence in sub:sst-map, and no ISCC or trusted timestamp has yet been minted (see sub:isccNote, sub:timestampNote)."
    }
  }
}
rows {
  name {
    value: "mode"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "AI-drafted, human-directed"
    }
  }
}
rows {
  name {
    value: "originalityStatement"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "No new mathematics. Every theorem in the artifact is prior art carrying an SST number (see sub:sst-map). The creative contributions of the AI-human collaboration are formalization engineering and exposition only."
    }
  }
}
rows {
  name {
    value: "AIUsageDeclaration"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 11
      name_id: 63
    }
  }
}
rows {
  name {
    value: "isccNote"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "ISO 24138 ISCC generation (Meta-, Content-, Data-, Instance-Code units) requires the iscc-core reference implementation, unavailable when this declaration was drafted. The declaration is therefore provisionally bound by the SHA-256 digest recorded in sub:artifact, computed over the compiled, current version of Tarski.lean. Upon finalization: (1) run `iscc-core` over the frozen file to mint the ISCC and replace the PENDING value; (2) obtain an RFC 3161 trusted timestamp or ledger anchor for this document; (3) sign the nanopublication with the declarant\'s key (this step is completed as of publication of this nanopub)."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 3
      name_id: 54
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 19
    }
    o_literal {
      lex: "ISCC binding status"
    }
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 56
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "Introduced Myles Axton to Euclidean geometry. The artifact\'s governing constraint \342\200\224 do more with less, straight edge and compass only \342\200\224 is his inspiration, and it is the same austerity that runs from Euclid\'s instruments through Tarski\'s two primitives to Gupta\'s removal of the continuity axiom."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 21
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 15
    }
    o_literal {
      lex: "Dedicatee; first teacher"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Richard Axton (1941\342\200\2232021)"
    }
  }
}
rows {
  name {
    value: "Dataset"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 43
    }
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 3
      name_id: 65
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 13
    }
    o_literal {
      lex: "Lean name = SST number [= GeoCoq name where applicable]: cong_refl = 2.1; cong_symm = 2.2; cong_trans = 2.3; cong_left_comm = 2.4; cong_right_comm = 2.5; cong_trivial = 2.8; cong_add = 2.11 [l2_11]; construction_uniqueness = 2.12; betw_trivial = 3.1; betw_symm = 3.2; betw_left_trivial = 3.3; betw_inner_trans = 3.5; betw_exchange_left = 3.6(1); betw_exchange2 = 3.6(2) [between_exchange2]; betw_outer_trans = 3.7(1); betw_outer_trans\' = 3.7(2); Cong3 = Def. 4.1 [Cong_3]; inner_five_segment = 4.2 [l4_2]; cong_sub = 4.3 [l4_3]; cong3_construction = 4.5 [l4_5]; betw_transfer = 4.6 [l4_6]; symmetric_point_exists = 7.4; symmetric_point_uniqueness = 7.5; reflect_cong = 7.13 [l7_13]; reflect_betw = 7.15 [l7_15]. Axioms A1\342\200\223A8 = Tarski. Declared future work: Per = Euclid Def. I.10 / SST ch. 8; perpendiculars and midpoints = 8.18, 8.22 (Gupta); target theorem = Pythagoras, Euclid I.47\342\200\223I.48, via segment arithmetic, SST ch. 14\342\200\22315 (Hilbert)."
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 19
    }
    o_literal {
      lex: "Theorem-to-source concordance"
    }
  }
}
rows {
  name {
    value: "timestampNote"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 66
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "All timestamps herein are the system clock of the drafting/verification sessions (self-asserted), not trusted timestamps. They are honest but not tamper-evident."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 3
      name_id: 54
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 19
    }
    o_literal {
      lex: "Timestamp status"
    }
  }
}
rows {
  name {
    value: "activity"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 67
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "A single sandboxed chat session beginning from the Pythagorean theorem in Mathlib\'s inner product spaces (norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero) and EuclideanSpace \342\204\235 (Fin n), pivoting to the synthetic question, and building the Lean 4 artifact over successive turns. Sources were drawn from model memory of SST and GeoCoq; no network access and no Lean toolchain were available, so all proofs were verified by hand-tracing (and, for SST 7.13, by an additional coordinate check) rather than by compilation."
    }
    g_iri {
      prefix_id: 2
      name_id: 7
    }
  }
}
rows {
  name {
    value: "Activity"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 68
    }
  }
}
rows {
  name {
    value: "startedAtTime"
  }
}
rows {
  datatype {
    value: "http://www.w3.org/2001/XMLSchema#date"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "2026-07-18"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "used"
  }
}
rows {
  name {
    value: "src-geocoq"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  name {
    value: "src-sst"
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  name {
    value: "wasAssociatedWith"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 13
    }
    o_iri {
      prefix_id: 2
      name_id: 12
    }
  }
}
rows {
  quad {
    o_iri {
      name_id: 32
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Interactive formalization dialogue"
    }
  }
}
rows {
  name {
    value: "activity-verify"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 74
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "A follow-up session with a working environment (network access, elan/Lean toolchains). Compiled `lean Tarski.lean` standalone and, separately, built it as a `lake` library target in two projects (pythagoras4, using leanprover/lean4-nightly:nightly-2023-05-16; and lean4-starter, using leanprover/lean4:v4.32.0). Found and fixed one error: the closing `example` used Mathlib\'s `\342\210\203!` notation, unavailable in core Lean 4, rewritten as its explicit unfolding. Both toolchains now build the file with zero errors and zero `sorry`s."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 68
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "2026-07-18"
      datatype: 1
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 2
      name_id: 38
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 13
      name_id: 73
    }
    o_iri {
      prefix_id: 2
      name_id: 12
    }
  }
}
rows {
  quad {
    o_iri {
      name_id: 32
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Build, fix, and compilation verification"
    }
  }
}
rows {
  name {
    value: "wasGeneratedBy"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 4
    }
    p_iri {
      prefix_id: 13
      name_id: 75
    }
    o_iri {
      prefix_id: 2
      name_id: 67
    }
  }
}
rows {
  name {
    value: "wasInfluencedBy"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 13
      name_id: 76
    }
    o_iri {
      prefix_id: 2
      name_id: 74
    }
  }
}
rows {
  quad {
    s_iri {
      name_id: 71
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "Used from model memory as the formalization map; no code consulted or ported in-session."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 47
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "GeoCoq repository and papers (Narboux et al., 2006\342\200\223)"
    }
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 72
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "Used from model memory as the architectural source; not consulted directly in-session."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 15
      name_id: 10
    }
    o_iri {
      prefix_id: 13
      name_id: 47
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Schwabh\303\244user, Szmielew, Tarski \342\200\224 Metamathematische Methoden in der Geometrie (Springer, 1983)"
    }
  }
}
rows {
  name {
    value: "created"
  }
}
rows {
  datatype {
    value: "http://www.w3.org/2001/XMLSchema#dateTime"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 1
      name_id: 1
    }
    p_iri {
      prefix_id: 5
      name_id: 77
    }
    o_literal {
      lex: "2026-07-18T14:45:07Z"
      datatype: 2
    }
    g_iri {
      prefix_id: 2
      name_id: 9
    }
  }
}
rows {
  name {
    value: "creator"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
      name_id: 78
    }
    o_iri {
      prefix_id: 9
      name_id: 36
    }
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 2
      name_id: 12
    }
  }
}
rows {
  quad {
    o_iri {
      name_id: 32
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "Provenance and credit declaration for Tarski.lean, a dependency-free Lean 4 formalization of Tarski\'s synthetic Euclidean geometry (SST chapters 2\342\200\2237, Stages 0\342\200\2234). Records intellectual lineage (Euclid through Gupta and GeoCoq), the AI-human authorship split, and a dedication."
    }
  }
}
rows {
  name {
    value: "license"
  }
}
rows {
  prefix {
    value: "https://creativecommons.org/licenses/by/4.0/"
  }
}
rows {
  quad {
    p_iri {
      name_id: 79
    }
    o_iri {
      prefix_id: 7
      name_id: 2
    }
  }
}
rows {
  name {
    value: "label"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 8
      name_id: 80
    }
    o_literal {
      lex: "Tarski.lean provenance and credit declaration"
    }
  }
}
rows {
  name {
    value: "generatedAtTime"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 13
    }
    o_literal {
      lex: "2026-07-18T14:45:07Z"
      datatype: 2
    }
  }
}
rows {
  prefix {
    id: 14
    value: "https://w3id.org/np/o/ntemplate/"
  }
}
rows {
  name {
    value: "wasCreatedFromProvenanceTemplate"
  }
}
rows {
  prefix {
    id: 4
    value: "http://purl.org/np/"
  }
}
rows {
  name {
    value: "RANwQa4ICWS5SOjw7gp99nBpXBasapwtZF1fIM3H2gYTM"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 14
    }
    o_iri {
      prefix_id: 4
    }
  }
}
rows {
  name {
    value: "wasCreatedFromPubinfoTemplate"
  }
}
rows {
  name {
    value: "RAA2MfqdBCzmz9yVWjKLXNbyfBNcwsMmOqcNUxkk1maIM"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 14
    }
    o_iri {
      prefix_id: 4
    }
  }
}
rows {
  name {
    value: "RAjpBMlw3owYhJUBo3DtsuDlXsNAJ8cnGeWAutDVjuAuI"
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  name {
    value: "wasCreatedFromTemplate"
  }
}
rows {
  name {
    value: "RAFu2BNmgHrjOTJ8SKRnKaRp-VP8AOOb7xX88ob0DZRsU"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 14
    }
    o_iri {
      prefix_id: 4
    }
  }
}
rows {
  name {
    value: "sig"
  }
}
rows {
  prefix {
    id: 16
    value: "http://purl.org/nanopub/x/"
  }
}
rows {
  name {
    value: "hasAlgorithm"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
    }
    p_iri {
      prefix_id: 16
    }
    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: "HQszDCt6s9WnRQy3Gsojrxc0m7Y7VrB2U13XPcPr6+f9sc6uY5Kjh27MU8OYBgm3zLc4gTeb3eLHtOnRYN0obiWqa2PiJldJoxANTi3irtphF4Z405s8K5Q6DmhqgVzd/Hj/APHScMZ/9A+CykC4v4YLMILQs81VDdrDfdbOrLRSpMv8pt/7/fiLF002Az5x1osg9814jn4cE3w5vLt5z26OLmXFo1bUsDahJVSnEBmr/RjKk3KxFA2WUlHv3ESLbUz1yIMSwyK4FVV0RR1LJr5Rw4ZjhUoXlOsDmObM3vn7N3c4Gp6gIIgTlELaYUJ0uue6sqaC/Ij+uH+7Qn7QKQ=="
    }
  }
}
rows {
  name {
    value: "hasSignatureTarget"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 1
      name_id: 1
    }
  }
}
rows {
  name {
    value: "signedBy"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 16
      name_id: 94
    }
    o_iri {
      prefix_id: 9
      name_id: 36
    }
  }
}