Repository and Project source
- Source repository
- v0.2.0 release
- Mankiewicz Project entry · Project Source Manifest
Exact file identity
c1d5be872e56c41be3c37e503b64467a5fc6ea098dc13bb66a3e53dc7b55036c·0c2fed827acd2a631c8f0182da489cf6f2886a38b286dad8d92e63f440b77b00 - Sphere Rigidity Project entry · Project Source Manifest
Exact file identity
b2d65019159b56484a87ec139ce8ec9ebd8f7a51cfdf7eaf44a97d8c99a05f80·c4b77099d6b66b217ecd4c371ac81269f11a811986b6018154c6eeb477add1c6
Release assets
- mathlib-annex-v0.2.0-source.zip
File identity
208954 bytes
585c1a07ff8a125ab189405d6fa7432703e3c1622c8515fb39bd9894ee74dd74 - GITHUB_QUALIFICATION_RECEIPT.json
File identity
2341 bytes
4b0bd54faa09df6cc594e57348535fc80314e529d8e4af2597ab3e3546665609 - MATHLIBANNEX_PROJECT_SOURCE_MANIFESTS.json
File identity
35527 bytes
128d1fa10a8b286bfb3b70b091e60cee823be8bde7f26014704cbbeb868cca5a - SOURCE_RELEASE_MANIFEST.json
File identity
2818 bytes
8a8bc59f242d8479bfc7784fadf106821fafbf4b6af7ad77a415ffd3e663741c - SHA256SUMS.txt
File identity
402 bytes
5444ce0fbc10d161d540c028cedb736141044637ec81fb2532df47ef3294b55d
Qualification and trust boundary
The exact source qualification passed the pinned build, downstream imports, both Project-entry imports, repository cleanliness and compiled-axiom audit. The 2,016 audited declarations used only propext, Classical.choice and Quot.sound. This does not constitute a line-by-line human proof audit or verify the Brief Report against the Lean source.
Qualification receipt · Run 35086615666
Exact source identity
- Tag
v0.2.0- Commit
30963f26ac8ffa3dc3e9ec9de91fd0f9daf05305- Tree
b3378851a5287f5e3c8418f668e4d0ba52718739