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: "RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE"
  }
}
rows {
  namespace {
    name: "this"
    value {
      prefix_id: 1
    }
  }
}
rows {
  prefix {
    value: "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE/"
  }
}
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: "identifier"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 5
    }
    p_iri {
      prefix_id: 4
    }
    o_literal {
      lex: "https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/Tarski.lean"
    }
    g_iri {
      prefix_id: 2
      name_id: 4
    }
  }
}
rows {
  name {
    value: "SourceCodeArtifact"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 14
    }
  }
}
rows {
  name {
    value: "label"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
    }
    o_literal {
      lex: "Tarski.lean"
    }
  }
}
rows {
  name {
    value: "atCommit"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "802b1d583032c44ea9affb2a61b0c8cda6c60b72"
    }
  }
}
rows {
  name {
    value: "axiomDependentDeclarationCount"
  }
}
rows {
  datatype {
    value: "http://www.w3.org/2001/XMLSchema#integer"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "9"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "axiomDependentDeclarationsUseAxioms"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "propext, Classical.choice, Quot.sound"
    }
  }
}
rows {
  name {
    value: "axiomFreeDeclarationCount"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "36"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "compilationResult"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Build completed successfully (3 jobs); target Tarski built without error"
    }
  }
}
rows {
  name {
    value: "compilationStatus"
  }
}
rows {
  name {
    value: "Compiled"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
    }
  }
}
rows {
  name {
    value: "compilationTool"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "elan 4.2.3 / Lean (version 4.32.0, arm64-apple-darwin24.6.0, commit 8c9756b28d64dab099da31a4c09229a9e6a2ef35, Release) / lake build"
    }
  }
}
rows {
  name {
    value: "declarationCount"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "45"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "fileSizeBytes"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "29024"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "fromRepository"
  }
}
rows {
  prefix {
    value: "https://github.com/johnmaxton/"
  }
}
rows {
  name {
    value: "lean4-starter"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 12
    }
  }
}
rows {
  name {
    value: "gitBlobSha1Hex"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "da7557b355045d2b0b16c5d5eca90a2db029e253"
    }
  }
}
rows {
  name {
    value: "gitBlobVerification"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "git hash-object on the fetched bytes reproduced GitHub\'s own stored blob SHA-1 exactly, independently confirming the fetched bytes match the repository\'s record for this path at this commit"
    }
  }
}
rows {
  name {
    value: "hasNoImportStatements"
  }
}
rows {
  datatype {
    value: "http://www.w3.org/2001/XMLSchema#boolean"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "true"
      datatype: 2
    }
  }
}
rows {
  name {
    value: "independentCiConclusion"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "success"
    }
  }
}
rows {
  name {
    value: "independentCiConfirmation"
  }
}
rows {
  prefix {
    value: "https://github.com/johnmaxton/lean4-starter/actions/runs/"
  }
}
rows {
  name {
    value: "31168537874"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 13
    }
  }
}
rows {
  name {
    value: "isccCombinedCode"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "ISCC:KYCO7GWDV372567AMDK5AEFUB3E24SRQZYC6ZHAET4"
    }
  }
}
rows {
  name {
    value: "isccComputedWith"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "iscc-core Python package v1.3.0 (ISO 24138 reference implementation)"
    }
  }
}
rows {
  name {
    value: "isccDataCode"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "ISCC:GAAWBVOQCC2A5SNO"
    }
  }
}
rows {
  name {
    value: "isccInstanceCode"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "ISCC:IAAUUMGOAXWJYBE7"
    }
  }
}
rows {
  name {
    value: "isccInstanceDatahash"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "1e204a30ce05ec9c049fb543feb1af45c4b9fa70452950b4ce36538c69598a7ca7b8"
    }
  }
}
rows {
  name {
    value: "isccMetaCode"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "ISCC:AAA67GWDV372567A"
    }
  }
}
rows {
  name {
    value: "lakeManifestExternalPackageCount"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "0"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "leanToolchain"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "leanprover/lean4:v4.32.0"
    }
  }
}
rows {
  name {
    value: "lineCount"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "663"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "sha256Hex"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "928b0c859d95f02ce5b8dcba197ec0ec01d67f22b6588742842de4fa2d41ceac"
    }
  }
}
rows {
  name {
    value: "sorryAxCount"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "0"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-Col"
  }
}
rows {
  name {
    value: "AuditedDeclaration"
  }
}
rows {
  quad {
    s_iri {
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  name {
    value: "axiomAuditResult"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  name {
    value: "qualifiedName"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.Col"
    }
  }
}
rows {
  name {
    value: "sourceLine"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "273"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-Cong3"
  }
}
rows {
  quad {
    s_iri {
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.Cong3"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "391"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-Midpoint"
  }
}
rows {
  quad {
    s_iri {
      name_id: 51
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.Midpoint"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "345"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-Out"
  }
}
rows {
  quad {
    s_iri {
      name_id: 52
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.Out"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "276"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-SegLe"
  }
}
rows {
  quad {
    s_iri {
      name_id: 53
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.SegLe"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "280"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-betw_col"
  }
}
rows {
  quad {
    s_iri {
      name_id: 54
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.betw_col"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "282"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-betw_exchange2"
  }
}
rows {
  quad {
    s_iri {
      name_id: 55
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "propext, Classical.choice, Quot.sound"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.betw_exchange2"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "259"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-betw_exchange_left"
  }
}
rows {
  quad {
    s_iri {
      name_id: 56
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.betw_exchange_left"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "230"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-betw_inner_trans"
  }
}
rows {
  quad {
    s_iri {
      name_id: 57
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.betw_inner_trans"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "220"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-betw_left_trivial"
  }
}
rows {
  quad {
    s_iri {
      name_id: 58
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.betw_left_trivial"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "215"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-betw_outer_trans"
  }
}
rows {
  quad {
    s_iri {
      name_id: 59
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.betw_outer_trans"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "238"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-betw_outer_trans-prime"
  }
}
rows {
  quad {
    s_iri {
      name_id: 60
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.betw_outer_trans\'"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "251"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-betw_symm"
  }
}
rows {
  quad {
    s_iri {
      name_id: 61
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.betw_symm"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "207"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-betw_transfer"
  }
}
rows {
  quad {
    s_iri {
      name_id: 62
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "propext, Classical.choice, Quot.sound"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.betw_transfer"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "494"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-betw_trivial"
  }
}
rows {
  quad {
    s_iri {
      name_id: 63
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.betw_trivial"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "198"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-col_rotate"
  }
}
rows {
  quad {
    s_iri {
      name_id: 64
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.col_rotate"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "286"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-col_swap"
  }
}
rows {
  quad {
    s_iri {
      name_id: 65
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.col_swap"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "296"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-col_trivial_left"
  }
}
rows {
  quad {
    s_iri {
      name_id: 66
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.col_trivial_left"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "304"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-col_trivial_mid"
  }
}
rows {
  quad {
    s_iri {
      name_id: 67
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.col_trivial_mid"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "310"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-col_trivial_right"
  }
}
rows {
  quad {
    s_iri {
      name_id: 68
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.col_trivial_right"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "307"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-cong3_construction"
  }
}
rows {
  quad {
    s_iri {
      name_id: 69
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "propext, Classical.choice, Quot.sound"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.cong3_construction"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "455"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-cong_add"
  }
}
rows {
  quad {
    s_iri {
      name_id: 70
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "propext, Classical.choice, Quot.sound"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.cong_add"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "162"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-cong_comm"
  }
}
rows {
  quad {
    s_iri {
      name_id: 71
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.cong_comm"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "143"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-cong_left_comm"
  }
}
rows {
  quad {
    s_iri {
      name_id: 72
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.cong_left_comm"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "135"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-cong_refl"
  }
}
rows {
  quad {
    s_iri {
      name_id: 73
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.cong_refl"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "122"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-cong_reverse_identity"
  }
}
rows {
  quad {
    s_iri {
      name_id: 74
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.cong_reverse_identity"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "156"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-cong_right_comm"
  }
}
rows {
  quad {
    s_iri {
      name_id: 75
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.cong_right_comm"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "139"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-cong_sub"
  }
}
rows {
  quad {
    s_iri {
      name_id: 76
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "propext, Classical.choice, Quot.sound"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.cong_sub"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "441"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-cong_symm"
  }
}
rows {
  quad {
    s_iri {
      name_id: 77
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.cong_symm"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "126"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-cong_trans"
  }
}
rows {
  quad {
    s_iri {
      name_id: 78
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.cong_trans"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "130"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-cong_trivial"
  }
}
rows {
  quad {
    s_iri {
      name_id: 79
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.cong_trivial"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "148"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-construction_uniqueness"
  }
}
rows {
  quad {
    s_iri {
      name_id: 80
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.construction_uniqueness"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "180"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-inner_five_segment"
  }
}
rows {
  quad {
    s_iri {
      name_id: 81
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "propext, Classical.choice, Quot.sound"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.inner_five_segment"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "403"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-midpoint_refl"
  }
}
rows {
  quad {
    s_iri {
      name_id: 82
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.midpoint_refl"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "347"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-midpoint_symm"
  }
}
rows {
  quad {
    s_iri {
      name_id: 83
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.midpoint_symm"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "350"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-out_col"
  }
}
rows {
  quad {
    s_iri {
      name_id: 84
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.out_col"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "322"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-out_symm"
  }
}
rows {
  quad {
    s_iri {
      name_id: 85
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.out_symm"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "316"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-out_trivial"
  }
}
rows {
  quad {
    s_iri {
      name_id: 86
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.out_trivial"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "313"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-reflect_betw"
  }
}
rows {
  quad {
    s_iri {
      name_id: 87
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "propext, Classical.choice, Quot.sound"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.reflect_betw"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "642"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-reflect_cong"
  }
}
rows {
  quad {
    s_iri {
      name_id: 88
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "propext, Classical.choice, Quot.sound"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.reflect_cong"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "541"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-segle_nil"
  }
}
rows {
  quad {
    s_iri {
      name_id: 89
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.segle_nil"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "331"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-segle_of_cong"
  }
}
rows {
  quad {
    s_iri {
      name_id: 90
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.segle_of_cong"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "334"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-segle_refl"
  }
}
rows {
  quad {
    s_iri {
      name_id: 91
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.segle_refl"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "327"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-symmetric_point_exists"
  }
}
rows {
  quad {
    s_iri {
      name_id: 92
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "no axioms"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.symmetric_point_exists"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "355"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "decl-symmetric_point_uniqueness"
  }
}
rows {
  quad {
    s_iri {
      name_id: 93
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 5
      name_id: 46
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "propext, Classical.choice, Quot.sound"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Synthetic.symmetric_point_uniqueness"
    }
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "362"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "activity-retrieve-execute"
  }
}
rows {
  name {
    value: "Activity"
  }
}
rows {
  quad {
    s_iri {
      name_id: 94
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 9
      name_id: 95
    }
    g_iri {
      prefix_id: 2
      name_id: 7
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
      name_id: 15
    }
    o_literal {
      lex: "Retrieve artifact, hash it, compute ISCC, install/run Lean toolchain, audit axioms"
    }
  }
}
rows {
  name {
    value: "generated"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
      name_id: 96
    }
    o_iri {
      prefix_id: 5
      name_id: 12
    }
  }
}
rows {
  name {
    value: "used"
  }
}
rows {
  prefix {
    value: "https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/"
  }
}
rows {
  name {
    value: "Tarski.lean"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
      name_id: 97
    }
    o_iri {
      prefix_id: 14
    }
  }
}
rows {
  name {
    value: "wasAssociatedWith"
  }
}
rows {
  name {
    value: "agent-claude-sonnet-5"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
    }
    o_iri {
      prefix_id: 5
    }
  }
}
rows {
  name {
    value: "SoftwareAgent"
  }
}
rows {
  quad {
    s_iri {
      name_id: 100
    }
    p_iri {
      prefix_id: 11
      name_id: 10
    }
    o_iri {
      prefix_id: 9
      name_id: 101
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
      name_id: 15
    }
    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: 102
    }
    o_literal {
      lex: "Every statement in this assertion graph was produced by running a tool against the artifact\'s actual bytes in this session: curl (retrieval), git hash-object and shasum (hashing), python3 iscc-core v1.3.0 (ISCC), and elan/lean/lake 4.32.0 (compilation + \'#print axioms\' over every declaration extracted from the file by grep). None of it is recalled from training data."
    }
  }
}
rows {
  name {
    value: "wasDerivedFrom"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
    }
    o_iri {
      prefix_id: 14
      name_id: 98
    }
  }
}
rows {
  name {
    value: "wasGeneratedBy"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 9
      name_id: 104
    }
    o_iri {
      prefix_id: 5
      name_id: 94
    }
  }
}
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: 4
      name_id: 105
    }
    o_literal {
      lex: "2026-08-10T12:57:30Z"
      datatype: 3
    }
    g_iri {
      prefix_id: 2
      name_id: 9
    }
  }
}
rows {
  name {
    value: "creator"
  }
}
rows {
  name {
    value: "0000-0002-8042-4131"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 4
      name_id: 106
    }
    o_iri {
      prefix_id: 8
    }
  }
}
rows {
  name {
    value: "license"
  }
}
rows {
  prefix {
    value: "https://creativecommons.org/licenses/by/4.0/"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 4
    }
    o_iri {
      prefix_id: 15
      name_id: 2
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
      name_id: 15
    }
    o_literal {
      lex: "Tarski.lean: retrieval, hashing, ISCC, compilation, axiom audit (machine-verified)"
    }
  }
}
rows {
  name {
    value: "verificationBucket"
  }
}
rows {
  name {
    value: "MachineVerified"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
      name_id: 109
    }
    o_iri {
    }
  }
}
rows {
  name {
    value: "sig"
  }
}
rows {
  name {
    value: "hasAlgorithm"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
    }
    p_iri {
      prefix_id: 10
    }
    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: "lG+p0162FcytbbLIJ1p3p+xmYhYHqk9I88NdkxctC5vWiPYmse3t84cB/SgE6xv3fswpjlSKQSPGcOZy44eJzU4arQR+2qLTtxp8B/T+Pe0K1ktll+WQ0PW40NwwmokRC4xyqZBoQXFVj7YthCa8TcmLsRXhcsyBzVTQakjAZitFY4ZD+M7cyGHrnVF7By+pd7y3B5VQEealqE9oSljku3qCm+EHqP00p3HWgWf4QDvhSRV8BX8TnWBV0cwZ2LDWhFsBoWiwmwGUh5MR1qg10Fb8EWGJBABLF1w2X2zFBNjZDxpkM5YYZJ7Do/Hc8ryIOzxYjFSRPUFjghqdGtjGhQ=="
    }
  }
}
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: 10
      name_id: 116
    }
    o_iri {
      prefix_id: 8
      name_id: 107
    }
  }
}