Skip to content

v0.0.1 — Initial scaffold

Choose a tag to compare

View all tags
@t-uda t-uda released this 07 Oct 09:21
· 109 commits to main since this release
v0.0.1
6fdfabe
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Initial development scaffold for the continuing TDA library. This release contains infrastructure only, with no TDA proofs or algorithms.

The Lean library is named TDA. Reviewed integration work targets develop; stable promotions target main and receive version tags. The continuing agent dot owns roadmap and queue decisions. Mathlib is pinned; TauCeti remains a candidate foundation.

Validation: independent review and PR CI passed; the merged main revision passed the full stable gate, live axiom audit and public theorem coverage. The single smoke theorem uses exactly propext, Classical.choice and Quot.sound.

Assets 2
Loading