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: "RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU"
  }
}
rows {
  namespace {
    name: "this"
    value {
      prefix_id: 1
    }
  }
}
rows {
  prefix {
    value: "https://w3id.org/np/RA74EndCdPO3d2g0ziTCnZmwsq2PsX-2UBl0ssY3d2OWU/"
  }
}
rows {
  name {
  }
}
rows {
  namespace {
    name: "sub"
    value {
      prefix_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://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: "http://purl.org/nanopub/x/"
  }
}
rows {
  namespace {
    name: "npx"
    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: "http://www.w3.org/ns/prov#"
  }
}
rows {
  namespace {
    name: "prov"
    value {
      prefix_id: 9
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/"
  }
}
rows {
  namespace {
    name: "np1"
    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: 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: 11
    }
    o_iri {
      prefix_id: 4
    }
  }
}
rows {
  name {
    value: "attr-verification"
  }
}
rows {
  name {
    value: "description"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
    }
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "The validation role is claimed here by a software agent executing in an ephemeral sandbox, on behalf of and at the direction of the human agent named in NP1. This is a weaker claim than independent human replication or continuous integration, both of which remain outstanding; see the unclaimed-credit assertions in NP2."
    }
    g_iri {
      prefix_id: 2
      name_id: 4
    }
  }
}
rows {
  name {
    value: "Attribution"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 9
      name_id: 14
    }
  }
}
rows {
  name {
    value: "agent"
  }
}
rows {
  name {
    value: "agent-claude"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 10
    }
  }
}
rows {
  name {
    value: "hadRole"
  }
}
rows {
  prefix {
    value: "https://credit.niso.org/contributor-roles/validation/"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
    }
    o_iri {
      prefix_id: 12
      name_id: 2
    }
  }
}
rows {
  name {
    value: "axiom-audit"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 18
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "For each of the 44 declarations obtained by scanning the source for top-level theorem and def bindings, a \'#print axioms Synthetic.<name>\' command was appended to a copy of the file and elaborated under Lean 4.32.0. All 44 reported; sorryAx occurred zero times in the output."
    }
  }
}
rows {
  name {
    value: "name"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Axiom dependency audit"
    }
  }
}
rows {
  name {
    value: "Activity"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 9
      name_id: 20
    }
  }
}
rows {
  name {
    value: "run-4-24-0"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "lean Tarski.lean; exit status 0; stdout and stderr empty. Toolchain commit 797c613eb9b6d4ec95db23e3e00af9ac6657f24b, x86_64-unknown-linux-gnu, Release build. Establishes that the result is not an artifact of a single compiler version."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Compilation under an earlier toolchain"
    }
  }
}
rows {
  name {
    value: "softwareVersion"
  }
}
rows {
  quad {
    p_iri {
      name_id: 22
    }
    o_literal {
      lex: "Lean 4.24.0"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 9
      name_id: 20
    }
  }
}
rows {
  name {
    value: "run-4-32-0"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 23
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "lean Tarski.lean; exit status 0; stdout and stderr empty. Toolchain leanprover/lean4:v4.32.0, commit 8c9756b28d64dab099da31a4c09229a9e6a2ef35, x86_64-unknown-linux-gnu, Release build. This is the version pinned by the lean-toolchain file of the hosting repository."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Compilation under the pinned toolchain"
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 22
    }
    o_literal {
      lex: "Lean 4.32.0"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 9
      name_id: 20
    }
  }
}
rows {
  name {
    value: "verification"
  }
}
rows {
  name {
    value: "date"
  }
}
rows {
  datatype {
    value: "http://www.w3.org/2001/XMLSchema#date"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 24
    }
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "2026-07-29"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "about"
  }
}
rows {
  name {
    value: "artifact"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
    }
    o_iri {
      prefix_id: 10
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Tarski.lean compiles under Lean 4 with no errors and no unproved statements"
    }
  }
}
rows {
  name {
    value: "result"
  }
}
rows {
  quad {
    p_iri {
      name_id: 28
    }
    o_literal {
      lex: "PASS"
    }
  }
}
rows {
  name {
    value: "text"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "The byte sequence identified by ISCC:KAC67GWDV372567ANMUX3VYVTO7YIYHV2AILIDWJV3VWCQK2KOB6QAY and SHA-256 1372181e2284465648cf15fdd9b7a761ceef9288224feccfd71fb63a5417bfd1 was submitted to the Lean 4 elaborator and kernel. The compiler exited with status 0 and emitted no diagnostics of any severity. An axiom audit over all 44 declarations in namespace Synthetic returned no dependency on sorryAx: 43 declarations depend only on the three standard Lean axioms propext, Classical.choice and Quot.sound, and Synthetic.construction_uniqueness depends on no axioms at all. The claim of zero sorry in the artifact\'s header comment is therefore confirmed, on two independent toolchain versions."
    }
  }
}
rows {
  name {
    value: "Claim"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 3
      name_id: 30
    }
  }
}
rows {
  name {
    value: "Entity"
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 9
    }
  }
}
rows {
  name {
    value: "qualifiedAttribution"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 2
      name_id: 12
    }
  }
}
rows {
  name {
    value: "wasDerivedFrom"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
      name_id: 33
    }
    o_iri {
      prefix_id: 10
      name_id: 27
    }
  }
}
rows {
  name {
    value: "artifact-copy"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 34
    }
    p_iri {
      prefix_id: 5
      name_id: 25
    }
    o_literal {
      lex: "2026-07-29"
      datatype: 1
    }
    g_iri {
      prefix_id: 2
      name_id: 7
    }
  }
}
rows {
  name {
    value: "contentUrl"
  }
}
rows {
  prefix {
    value: "https://raw.githubusercontent.com/johnmaxton/lean4-starter/main/"
  }
}
rows {
  name {
    value: "Tarski.lean"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 35
    }
    o_iri {
      prefix_id: 13
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Retrieved copy of Tarski.lean"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 9
      name_id: 31
    }
  }
}
rows {
  name {
    value: "comment"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 8
      name_id: 37
    }
    o_literal {
      lex: "Retrieved from the main branch; no commit was pinned at retrieval time, so re-verification requires re-checking the ISCC and SHA-256 recorded in NP1 before trusting this result against a later state of the branch."
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
      name_id: 33
    }
    o_iri {
      prefix_id: 10
      name_id: 27
    }
  }
}
rows {
  name {
    value: "wasAttributedTo"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 4
    }
    p_iri {
      prefix_id: 9
      name_id: 38
    }
    o_iri {
      prefix_id: 10
      name_id: 16
    }
  }
}
rows {
  name {
    value: "wasGeneratedBy"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
      name_id: 39
    }
    o_iri {
      prefix_id: 2
      name_id: 18
    }
  }
}
rows {
  quad {
    o_iri {
      name_id: 21
    }
  }
}
rows {
  quad {
    o_iri {
      name_id: 23
    }
  }
}
rows {
  name {
    value: "used"
  }
}
rows {
  name {
    value: "toolchain-4-32-0"
  }
}
rows {
  quad {
    s_iri {
      name_id: 18
    }
    p_iri {
      prefix_id: 9
      name_id: 40
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 10
      name_id: 27
    }
  }
}
rows {
  name {
    value: "wasAssociatedWith"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
      name_id: 42
    }
    o_iri {
      prefix_id: 10
      name_id: 16
    }
  }
}
rows {
  name {
    value: "startedAtTime"
  }
}
rows {
  datatype {
    value: "http://www.w3.org/2001/XMLSchema#dateTime"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 21
    }
    p_iri {
      prefix_id: 9
      name_id: 43
    }
    o_literal {
      lex: "2026-07-29T00:00:00Z"
      datatype: 2
    }
  }
}
rows {
  name {
    value: "toolchain-4-24-0"
  }
}
rows {
  quad {
    p_iri {
      name_id: 40
    }
    o_iri {
      prefix_id: 2
      name_id: 44
    }
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 10
      name_id: 27
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
      name_id: 42
    }
    o_iri {
      prefix_id: 10
      name_id: 16
    }
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 23
    }
    p_iri {
      prefix_id: 9
      name_id: 43
    }
    o_literal {
      lex: "2026-07-29T00:00:00Z"
      datatype: 2
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 40
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 10
      name_id: 27
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
      name_id: 42
    }
    o_iri {
      prefix_id: 10
      name_id: 16
    }
  }
}
rows {
  name {
    value: "identifier"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 44
    }
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "797c613eb9b6d4ec95db23e3e00af9ac6657f24b"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Lean 4.24.0 (x86_64-unknown-linux-gnu)"
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 22
    }
    o_literal {
      lex: "4.24.0"
    }
  }
}
rows {
  name {
    value: "url"
  }
}
rows {
  prefix {
    value: "https://github.com/leanprover/lean4/releases/tag/"
  }
}
rows {
  name {
    value: "v4.24.0"
  }
}
rows {
  quad {
    p_iri {
      name_id: 46
    }
    o_iri {
      prefix_id: 14
    }
  }
}
rows {
  name {
    value: "SoftwareApplication"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 3
      name_id: 48
    }
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 9
      name_id: 31
    }
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 41
    }
    p_iri {
      prefix_id: 5
      name_id: 45
    }
    o_literal {
      lex: "8c9756b28d64dab099da31a4c09229a9e6a2ef35"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
      name_id: 19
    }
    o_literal {
      lex: "Lean 4.32.0 (x86_64-unknown-linux-gnu)"
    }
  }
}
rows {
  quad {
    p_iri {
      name_id: 22
    }
    o_literal {
      lex: "4.32.0"
    }
  }
}
rows {
  name {
    value: "v4.32.0"
  }
}
rows {
  quad {
    p_iri {
      name_id: 46
    }
    o_iri {
      prefix_id: 14
      name_id: 49
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 3
      name_id: 48
    }
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 9
      name_id: 31
    }
  }
}
rows {
  name {
    value: "created"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 1
      name_id: 1
    }
    p_iri {
      prefix_id: 5
      name_id: 50
    }
    o_literal {
      lex: "2026-07-29T15:00:47Z"
      datatype: 2
    }
    g_iri {
      prefix_id: 2
      name_id: 9
    }
  }
}
rows {
  name {
    value: "creator"
  }
}
rows {
  name {
    value: "agent-axton"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
      name_id: 51
    }
    o_iri {
      prefix_id: 10
    }
  }
}
rows {
  name {
    value: "license"
  }
}
rows {
  prefix {
    value: "http://creativecommons.org/publicdomain/zero/1.0/"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_iri {
      prefix_id: 15
      name_id: 2
    }
  }
}
rows {
  name {
    value: "relation"
  }
}
rows {
  name {
    value: "RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
      name_id: 54
    }
    o_iri {
      prefix_id: 1
    }
  }
}
rows {
  name {
    value: "RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4"
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  name {
    value: "hasNanopubType"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 6
    }
    o_iri {
      prefix_id: 9
      name_id: 20
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 8
      name_id: 37
    }
    o_literal {
      lex: "This record supersedes the statement in earlier drafts that verification-by-compilation was unclaimed; it does not supersede the requirement for independent replication."
    }
  }
}
rows {
  name {
    value: "label"
  }
}
rows {
  quad {
    p_iri {
      name_id: 58
    }
    o_literal {
      lex: "Tarski.lean: compilation verification under Lean 4.32.0 and 4.24.0"
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
      name_id: 38
    }
    o_iri {
      prefix_id: 10
      name_id: 16
    }
  }
}
rows {
  name {
    value: "sig"
  }
}
rows {
  name {
    value: "hasAlgorithm"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 59
    }
    p_iri {
      prefix_id: 6
    }
    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: "eMDXFadOqHjMhTZNn3myQj3YLd4Mbpzc0w42pkhUyP1mcVgjGszDbVPB8tGIX6/7/t8zjo5nuY2XF9cxAGK6V0Io/BVn2dmQs6vJfQkuLNPaaJ62t3eujVFQG8Vfx8/P3F+CdFOh1LBc6LTVI+GuTosqWBRvWycYw3KtLtAHu33mLJUMe3Gu4FHDZIlC7Yz3NweQG8jjLqxx+fKgz8YYk1X1mgQlN6PoJgKNicVHYeg95LcskuSL/Jrhx6tfWFXk0Pnkkk2Z3KySabFn6EWBwxaFO95I2N6Txj/ACpOi3qIAuGHTzqqPA8DKOL1l+aAp7LMWct/ZXOvNF6bJbTUDKw=="
    }
  }
}
rows {
  name {
    value: "hasSignatureTarget"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 1
      name_id: 1
    }
  }
}
rows {
  name {
    value: "signedBy"
  }
}
rows {
  prefix {
    value: "https://orcid.org/"
  }
}
rows {
  name {
    value: "0000-0002-8042-4131"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 6
      name_id: 64
    }
    o_iri {
      prefix_id: 16
    }
  }
}