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