[
    {
        "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE/pubinfo",
        "@graph": [
            {
                "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE",
                "http://purl.org/dc/terms/created": [
                    {
                        "@value": "2026-08-10T12:57:30Z",
                        "@type": "http://www.w3.org/2001/XMLSchema#dateTime"
                    }
                ],
                "http://purl.org/dc/terms/creator": [
                    {
                        "@id": "https://orcid.org/0000-0002-8042-4131"
                    }
                ],
                "http://purl.org/dc/terms/license": [
                    {
                        "@id": "https://creativecommons.org/licenses/by/4.0/"
                    }
                ],
                "http://www.w3.org/2000/01/rdf-schema#label": [
                    {
                        "@value": "Tarski.lean: retrieval, hashing, ISCC, compilation, axiom audit (machine-verified)"
                    }
                ],
                "https://provenance.example/tarski-lean/verificationBucket": [
                    {
                        "@id": "https://provenance.example/tarski-lean/MachineVerified"
                    }
                ]
            },
            {
                "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE/sig",
                "http://purl.org/nanopub/x/hasAlgorithm": [
                    {
                        "@value": "RSA"
                    }
                ],
                "http://purl.org/nanopub/x/hasPublicKey": [
                    {
                        "@value": "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB"
                    }
                ],
                "http://purl.org/nanopub/x/hasSignature": [
                    {
                        "@value": "lG+p0162FcytbbLIJ1p3p+xmYhYHqk9I88NdkxctC5vWiPYmse3t84cB/SgE6xv3fswpjlSKQSPGcOZy44eJzU4arQR+2qLTtxp8B/T+Pe0K1ktll+WQ0PW40NwwmokRC4xyqZBoQXFVj7YthCa8TcmLsRXhcsyBzVTQakjAZitFY4ZD+M7cyGHrnVF7By+pd7y3B5VQEealqE9oSljku3qCm+EHqP00p3HWgWf4QDvhSRV8BX8TnWBV0cwZ2LDWhFsBoWiwmwGUh5MR1qg10Fb8EWGJBABLF1w2X2zFBNjZDxpkM5YYZJ7Do/Hc8ryIOzxYjFSRPUFjghqdGtjGhQ=="
                    }
                ],
                "http://purl.org/nanopub/x/hasSignatureTarget": [
                    {
                        "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE"
                    }
                ],
                "http://purl.org/nanopub/x/signedBy": [
                    {
                        "@id": "https://orcid.org/0000-0002-8042-4131"
                    }
                ]
            }
        ]
    },
    {
        "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE/provenance",
        "@graph": [
            {
                "@id": "https://provenance.example/tarski-lean/activity-retrieve-execute",
                "@type": [
                    "http://www.w3.org/ns/prov#Activity"
                ],
                "http://www.w3.org/2000/01/rdf-schema#label": [
                    {
                        "@value": "Retrieve artifact, hash it, compute ISCC, install/run Lean toolchain, audit axioms"
                    }
                ],
                "http://www.w3.org/ns/prov#generated": [
                    {
                        "@id": "https://provenance.example/tarski-lean/artifact-Tarski-lean"
                    }
                ],
                "http://www.w3.org/ns/prov#used": [
                    {
                        "@id": "https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/Tarski.lean"
                    }
                ],
                "http://www.w3.org/ns/prov#wasAssociatedWith": [
                    {
                        "@id": "https://provenance.example/tarski-lean/agent-claude-sonnet-5"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/agent-claude-sonnet-5",
                "@type": [
                    "http://www.w3.org/ns/prov#SoftwareAgent"
                ],
                "http://www.w3.org/2000/01/rdf-schema#label": [
                    {
                        "@value": "Claude Sonnet 5 (Anthropic), running as Claude Code"
                    }
                ]
            },
            {
                "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE/assertion",
                "http://purl.org/dc/terms/description": [
                    {
                        "@value": "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."
                    }
                ],
                "http://www.w3.org/ns/prov#wasDerivedFrom": [
                    {
                        "@id": "https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/Tarski.lean"
                    }
                ],
                "http://www.w3.org/ns/prov#wasGeneratedBy": [
                    {
                        "@id": "https://provenance.example/tarski-lean/activity-retrieve-execute"
                    }
                ]
            }
        ]
    },
    {
        "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE/Head",
        "@graph": [
            {
                "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE",
                "http://www.nanopub.org/nschema#hasAssertion": [
                    {
                        "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE/assertion"
                    }
                ],
                "http://www.nanopub.org/nschema#hasProvenance": [
                    {
                        "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE/provenance"
                    }
                ],
                "http://www.nanopub.org/nschema#hasPublicationInfo": [
                    {
                        "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE/pubinfo"
                    }
                ],
                "@type": [
                    "http://www.nanopub.org/nschema#Nanopublication"
                ]
            }
        ]
    },
    {
        "@id": "https://w3id.org/np/RAoWjlznRlDcT5f71Uy1kkyzDToUKUChfm-PYNex3bUvE/assertion",
        "@graph": [
            {
                "@id": "https://provenance.example/tarski-lean/artifact-Tarski-lean",
                "http://purl.org/dc/terms/identifier": [
                    {
                        "@value": "https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/Tarski.lean"
                    }
                ],
                "@type": [
                    "https://provenance.example/tarski-lean/SourceCodeArtifact"
                ],
                "http://www.w3.org/2000/01/rdf-schema#label": [
                    {
                        "@value": "Tarski.lean"
                    }
                ],
                "https://provenance.example/tarski-lean/atCommit": [
                    {
                        "@value": "802b1d583032c44ea9affb2a61b0c8cda6c60b72"
                    }
                ],
                "https://provenance.example/tarski-lean/axiomDependentDeclarationCount": [
                    {
                        "@value": "9",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ],
                "https://provenance.example/tarski-lean/axiomDependentDeclarationsUseAxioms": [
                    {
                        "@value": "propext, Classical.choice, Quot.sound"
                    }
                ],
                "https://provenance.example/tarski-lean/axiomFreeDeclarationCount": [
                    {
                        "@value": "36",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ],
                "https://provenance.example/tarski-lean/compilationResult": [
                    {
                        "@value": "Build completed successfully (3 jobs); target Tarski built without error"
                    }
                ],
                "https://provenance.example/tarski-lean/compilationStatus": [
                    {
                        "@id": "https://provenance.example/tarski-lean/Compiled"
                    }
                ],
                "https://provenance.example/tarski-lean/compilationTool": [
                    {
                        "@value": "elan 4.2.3 / Lean (version 4.32.0, arm64-apple-darwin24.6.0, commit 8c9756b28d64dab099da31a4c09229a9e6a2ef35, Release) / lake build"
                    }
                ],
                "https://provenance.example/tarski-lean/declarationCount": [
                    {
                        "@value": "45",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ],
                "https://provenance.example/tarski-lean/fileSizeBytes": [
                    {
                        "@value": "29024",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ],
                "https://provenance.example/tarski-lean/fromRepository": [
                    {
                        "@id": "https://github.com/johnmaxton/lean4-starter"
                    }
                ],
                "https://provenance.example/tarski-lean/gitBlobSha1Hex": [
                    {
                        "@value": "da7557b355045d2b0b16c5d5eca90a2db029e253"
                    }
                ],
                "https://provenance.example/tarski-lean/gitBlobVerification": [
                    {
                        "@value": "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"
                    }
                ],
                "https://provenance.example/tarski-lean/hasNoImportStatements": [
                    {
                        "@value": "true",
                        "@type": "http://www.w3.org/2001/XMLSchema#boolean"
                    }
                ],
                "https://provenance.example/tarski-lean/independentCiConclusion": [
                    {
                        "@value": "success"
                    }
                ],
                "https://provenance.example/tarski-lean/independentCiConfirmation": [
                    {
                        "@id": "https://github.com/johnmaxton/lean4-starter/actions/runs/31168537874"
                    }
                ],
                "https://provenance.example/tarski-lean/isccCombinedCode": [
                    {
                        "@value": "ISCC:KYCO7GWDV372567AMDK5AEFUB3E24SRQZYC6ZHAET4"
                    }
                ],
                "https://provenance.example/tarski-lean/isccComputedWith": [
                    {
                        "@value": "iscc-core Python package v1.3.0 (ISO 24138 reference implementation)"
                    }
                ],
                "https://provenance.example/tarski-lean/isccDataCode": [
                    {
                        "@value": "ISCC:GAAWBVOQCC2A5SNO"
                    }
                ],
                "https://provenance.example/tarski-lean/isccInstanceCode": [
                    {
                        "@value": "ISCC:IAAUUMGOAXWJYBE7"
                    }
                ],
                "https://provenance.example/tarski-lean/isccInstanceDatahash": [
                    {
                        "@value": "1e204a30ce05ec9c049fb543feb1af45c4b9fa70452950b4ce36538c69598a7ca7b8"
                    }
                ],
                "https://provenance.example/tarski-lean/isccMetaCode": [
                    {
                        "@value": "ISCC:AAA67GWDV372567A"
                    }
                ],
                "https://provenance.example/tarski-lean/lakeManifestExternalPackageCount": [
                    {
                        "@value": "0",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ],
                "https://provenance.example/tarski-lean/leanToolchain": [
                    {
                        "@value": "leanprover/lean4:v4.32.0"
                    }
                ],
                "https://provenance.example/tarski-lean/lineCount": [
                    {
                        "@value": "663",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ],
                "https://provenance.example/tarski-lean/sha256Hex": [
                    {
                        "@value": "928b0c859d95f02ce5b8dcba197ec0ec01d67f22b6588742842de4fa2d41ceac"
                    }
                ],
                "https://provenance.example/tarski-lean/sorryAxCount": [
                    {
                        "@value": "0",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-Col",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.Col"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "273",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-Cong3",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.Cong3"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "391",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-Midpoint",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.Midpoint"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "345",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-Out",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.Out"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "276",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-SegLe",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.SegLe"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "280",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-betw_col",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.betw_col"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "282",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-betw_exchange2",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "propext, Classical.choice, Quot.sound"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.betw_exchange2"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "259",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-betw_exchange_left",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.betw_exchange_left"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "230",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-betw_inner_trans",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.betw_inner_trans"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "220",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-betw_left_trivial",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.betw_left_trivial"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "215",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-betw_outer_trans",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.betw_outer_trans"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "238",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-betw_outer_trans-prime",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.betw_outer_trans'"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "251",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-betw_symm",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.betw_symm"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "207",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-betw_transfer",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "propext, Classical.choice, Quot.sound"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.betw_transfer"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "494",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-betw_trivial",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.betw_trivial"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "198",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-col_rotate",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.col_rotate"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "286",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-col_swap",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.col_swap"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "296",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-col_trivial_left",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.col_trivial_left"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "304",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-col_trivial_mid",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.col_trivial_mid"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "310",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-col_trivial_right",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.col_trivial_right"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "307",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-cong3_construction",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "propext, Classical.choice, Quot.sound"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.cong3_construction"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "455",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-cong_add",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "propext, Classical.choice, Quot.sound"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.cong_add"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "162",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-cong_comm",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.cong_comm"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "143",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-cong_left_comm",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.cong_left_comm"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "135",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-cong_refl",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.cong_refl"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "122",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-cong_reverse_identity",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.cong_reverse_identity"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "156",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-cong_right_comm",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.cong_right_comm"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "139",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-cong_sub",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "propext, Classical.choice, Quot.sound"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.cong_sub"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "441",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-cong_symm",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.cong_symm"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "126",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-cong_trans",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.cong_trans"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "130",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-cong_trivial",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.cong_trivial"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "148",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-construction_uniqueness",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.construction_uniqueness"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "180",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-inner_five_segment",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "propext, Classical.choice, Quot.sound"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.inner_five_segment"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "403",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-midpoint_refl",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.midpoint_refl"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "347",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-midpoint_symm",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.midpoint_symm"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "350",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-out_col",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.out_col"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "322",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-out_symm",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.out_symm"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "316",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-out_trivial",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.out_trivial"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "313",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-reflect_betw",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "propext, Classical.choice, Quot.sound"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.reflect_betw"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "642",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-reflect_cong",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "propext, Classical.choice, Quot.sound"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.reflect_cong"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "541",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-segle_nil",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.segle_nil"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "331",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-segle_of_cong",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.segle_of_cong"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "334",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-segle_refl",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.segle_refl"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "327",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-symmetric_point_exists",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "no axioms"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.symmetric_point_exists"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "355",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            },
            {
                "@id": "https://provenance.example/tarski-lean/decl-symmetric_point_uniqueness",
                "@type": [
                    "https://provenance.example/tarski-lean/AuditedDeclaration"
                ],
                "https://provenance.example/tarski-lean/axiomAuditResult": [
                    {
                        "@value": "propext, Classical.choice, Quot.sound"
                    }
                ],
                "https://provenance.example/tarski-lean/qualifiedName": [
                    {
                        "@value": "Synthetic.symmetric_point_uniqueness"
                    }
                ],
                "https://provenance.example/tarski-lean/sourceLine": [
                    {
                        "@value": "362",
                        "@type": "http://www.w3.org/2001/XMLSchema#integer"
                    }
                ]
            }
        ]
    }
]