. . . . "https://github.com/johnmaxton/lean4-starter/blob/802b1d583032c44ea9affb2a61b0c8cda6c60b72/Tarski.lean" . . "Tarski.lean" . "802b1d583032c44ea9affb2a61b0c8cda6c60b72" . "9"^^ . "propext, Classical.choice, Quot.sound" . "36"^^ . "Build completed successfully (3 jobs); target Tarski built without error" . . "elan 4.2.3 / Lean (version 4.32.0, arm64-apple-darwin24.6.0, commit 8c9756b28d64dab099da31a4c09229a9e6a2ef35, Release) / lake build" . "45"^^ . "29024"^^ . . "da7557b355045d2b0b16c5d5eca90a2db029e253" . "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" . "true"^^ . "success" . . "ISCC:KYCO7GWDV372567AMDK5AEFUB3E24SRQZYC6ZHAET4" . "iscc-core Python package v1.3.0 (ISO 24138 reference implementation)" . "ISCC:GAAWBVOQCC2A5SNO" . "ISCC:IAAUUMGOAXWJYBE7" . "1e204a30ce05ec9c049fb543feb1af45c4b9fa70452950b4ce36538c69598a7ca7b8" . "ISCC:AAA67GWDV372567A" . "0"^^ . "leanprover/lean4:v4.32.0" . "663"^^ . "928b0c859d95f02ce5b8dcba197ec0ec01d67f22b6588742842de4fa2d41ceac" . "0"^^ . . "no axioms" . "Synthetic.Col" . "273"^^ . . "no axioms" . "Synthetic.Cong3" . "391"^^ . . "no axioms" . "Synthetic.Midpoint" . "345"^^ . . "no axioms" . "Synthetic.Out" . "276"^^ . . "no axioms" . "Synthetic.SegLe" . "280"^^ . . "no axioms" . "Synthetic.betw_col" . "282"^^ . . "propext, Classical.choice, Quot.sound" . "Synthetic.betw_exchange2" . "259"^^ . . "no axioms" . "Synthetic.betw_exchange_left" . "230"^^ . . "no axioms" . "Synthetic.betw_inner_trans" . "220"^^ . . "no axioms" . "Synthetic.betw_left_trivial" . "215"^^ . . "no axioms" . "Synthetic.betw_outer_trans" . "238"^^ . . "no axioms" . "Synthetic.betw_outer_trans'" . "251"^^ . . "no axioms" . "Synthetic.betw_symm" . "207"^^ . . "propext, Classical.choice, Quot.sound" . "Synthetic.betw_transfer" . "494"^^ . . "no axioms" . "Synthetic.betw_trivial" . "198"^^ . . "no axioms" . "Synthetic.col_rotate" . "286"^^ . . "no axioms" . "Synthetic.col_swap" . "296"^^ . . "no axioms" . "Synthetic.col_trivial_left" . "304"^^ . . "no axioms" . "Synthetic.col_trivial_mid" . "310"^^ . . "no axioms" . "Synthetic.col_trivial_right" . "307"^^ . . "propext, Classical.choice, Quot.sound" . "Synthetic.cong3_construction" . "455"^^ . . "propext, Classical.choice, Quot.sound" . "Synthetic.cong_add" . "162"^^ . . "no axioms" . "Synthetic.cong_comm" . "143"^^ . . "no axioms" . "Synthetic.cong_left_comm" . "135"^^ . . "no axioms" . "Synthetic.cong_refl" . "122"^^ . . "no axioms" . "Synthetic.cong_reverse_identity" . "156"^^ . . "no axioms" . "Synthetic.cong_right_comm" . "139"^^ . . "propext, Classical.choice, Quot.sound" . "Synthetic.cong_sub" . "441"^^ . . "no axioms" . "Synthetic.cong_symm" . "126"^^ . . "no axioms" . "Synthetic.cong_trans" . "130"^^ . . "no axioms" . "Synthetic.cong_trivial" . "148"^^ . . "no axioms" . "Synthetic.construction_uniqueness" . "180"^^ . . "propext, Classical.choice, Quot.sound" . "Synthetic.inner_five_segment" . "403"^^ . . "no axioms" . "Synthetic.midpoint_refl" . "347"^^ . . "no axioms" . "Synthetic.midpoint_symm" . "350"^^ . . "no axioms" . "Synthetic.out_col" . "322"^^ . . "no axioms" . "Synthetic.out_symm" . "316"^^ . . "no axioms" . "Synthetic.out_trivial" . "313"^^ . . "propext, Classical.choice, Quot.sound" . "Synthetic.reflect_betw" . "642"^^ . . "propext, Classical.choice, Quot.sound" . "Synthetic.reflect_cong" . "541"^^ . . "no axioms" . "Synthetic.segle_nil" . "331"^^ . . "no axioms" . "Synthetic.segle_of_cong" . "334"^^ . . "no axioms" . "Synthetic.segle_refl" . "327"^^ . . "no axioms" . "Synthetic.symmetric_point_exists" . "355"^^ . . "propext, Classical.choice, Quot.sound" . "Synthetic.symmetric_point_uniqueness" . "362"^^ . . "Retrieve artifact, hash it, compute ISCC, install/run Lean toolchain, audit axioms" . . . . . "Claude Sonnet 5 (Anthropic), running as Claude Code" . "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." . . . "2026-08-10T12:57:30Z"^^ . . . "Tarski.lean: retrieval, hashing, ISCC, compilation, axiom audit (machine-verified)" . . "RSA" . "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB" . "lG+p0162FcytbbLIJ1p3p+xmYhYHqk9I88NdkxctC5vWiPYmse3t84cB/SgE6xv3fswpjlSKQSPGcOZy44eJzU4arQR+2qLTtxp8B/T+Pe0K1ktll+WQ0PW40NwwmokRC4xyqZBoQXFVj7YthCa8TcmLsRXhcsyBzVTQakjAZitFY4ZD+M7cyGHrnVF7By+pd7y3B5VQEealqE9oSljku3qCm+EHqP00p3HWgWf4QDvhSRV8BX8TnWBV0cwZ2LDWhFsBoWiwmwGUh5MR1qg10Fb8EWGJBABLF1w2X2zFBNjZDxpkM5YYZJ7Do/Hc8ryIOzxYjFSRPUFjghqdGtjGhQ==" . . .