v0.1.0-rc1 — release-candidate build attestation

What this release is

This pre-release durably archives the evidence produced by the release-attestation GitHub Actions workflow, run 29714844283, which ran a full lake build plus every release-gate check against exactly the following commit:

7c15710a7b9068a2aa105fc7c11b432e7685b7b5

The tag v0.1.0-rc1 points directly at that commit.

Scope of the certification. A green result on every check in attestation.md certifies exactly the SHA above — not the branch HEAD at any later time. If main has moved since, this record says nothing about the new commits; a fresh release-attestation run against the new SHA would be needed to extend the certification.

Checks covered

• Full lake build (mathlib-cache-first)
• lake build LerayHopf.Experimental (opt-in module)
• scripts/check-no-sorry.sh
• scripts/check-no-axiom.sh
• scripts/check-theorem-names.sh
• scripts/check-axioms.sh
• scripts/check-release-cone.sh
• scripts/check-statement-cards.sh
• scripts/check-axioms-live.sh

All nine passed. See attestation.md for per-check status and guard-log checksums.

Assets

File	Contents
attestation.md	The workflow's summary table (attested SHA, toolchain, per-check results, guard-log checksums)
release-attestation-7c15710a7b9068a2aa105fc7c11b432e7685b7b5.zip	attestation.md plus all logs/*.log guard-check logs from the run
release-attestation-run-29714844283.log.gz	The complete raw workflow run log (includes the full lake build output, which is not captured in the per-check logs)
release-provenance.json	Machine-readable provenance record: repo, tag, attested SHA, workflow run URL/id, toolchain, and SHA-256 of every other asset
SHA256SUMS	Checksums for all of the above, mutually verifiable via sha256sum -c SHA256SUMS

Toolchain

• lean-toolchain: leanprover/lean4:v4.31.0-rc2
• lake-manifest.json sha256: e0e0f7bd665cf5d4c9a79daa535b2a591368de8e0832138b0f0e26ad3d391793

Refs #187.