MathlibAnnex v0.1.0

Source and Project entry

• Source repository
• v0.1.0 release
• Mankiewicz Project import entry
• Mankiewicz Project Source Manifest

Release assets

• mathlib-annex-v0.1.0-source.zip
  File identity

  34368 bytes

  533abb85700813aef391de0a1a42f7c64ce9a11a6e7bbda65696076ec4a1ef12
• GITHUB_QUALIFICATION_RECEIPT.json
  File identity

  2235 bytes

  32b851e39c530cb0c918af0ad7015957232b8774b166e0eb7b917b4f044ce39a
• MATHLIBANNEX_PROJECT_SOURCE_MANIFESTS.json
  File identity

  7241 bytes

  e1cbf75abf56a0eb533b6ce7adaa3e4e21d4dd28ade5ddedffa9c218331cba3a
• SOURCE_RELEASE_MANIFEST.json
  File identity

  4051 bytes

  5b07a000efc34801f481196f87b33f6ebc5a3976f94ca2b4dbce1d14288dae56
• SHA256SUMS.txt
  File identity

  402 bytes

  8215b167cabafe55cf93699030d6df4c048f25039dad2de216fc12c9da1c489e

Qualification and trust boundary

The recorded source qualification passed the pinned build, root import, Project-entry import, cleanliness and compiled-axiom checks. All 88 audited declarations were within the allowlist: propext, Classical.choice and Quot.sound. This is not a line-by-line human proof audit.

Qualification receipt · Run 35029159302