v0.1.0 — First mathematical TDA library release

v0.1.0 — First mathematical TDA library release

This is the first release of the mathematical TDA library. The earlier v0.0.1 and v0.0.2 releases covered infrastructure only. This version publishes Lean-checked results and a certified finite F₂ persistence computation.

Included results

• Finite simplicial faces, signed chains, square-zero boundaries, simplicial homology, and inclusion and vertex-map interfaces. Chain-level results use the stated ring assumptions; finite-dimensional homology uses the stated field and finite-face assumptions.
• Finite-chain, pointwise finite-dimensional persistence modules over a field: interval decomposition and classification by structure-map ranks. The canonical interval multiset is separate from a noncanonical choice of summands and isomorphism.
• Actual simplicial sublevel diagrams, including repeated occurrences, half-open finite bars, omitted zero-length value bars, and essential bars with death ⊤. The reduction development identifies graded output with actual homology and natural structure maps.
• A finite real-filter bottleneck bound that permits pairing changes, plus local diagram regularity, derivatives, and Hessians under explicit ordered-lift and factorization hypotheses.
• Executable unaugmented F₂ persistence for finite integer-graded simplex lists. FiniteInput.run rejects invalid presentations; on valid input, outputDiagram_eq_dgm identifies its output with actual sublevel diagrams in every degree.
• Ordinary Mapper and coherent-cover-tower interfaces, plus Reeb/component-cosheaf, smoothing, and finite real-graph comparison results under their documented hypotheses.

Use import TDA.Persistence for persistent homology or another area import for a narrower development. import TDA.Library loads all six library areas. import TDA also loads standalone examples and acceptance fixtures. See the API guide for exact assumptions and module boundaries.

Lean is pinned to leanprover/lean4:v4.33.1; mathlib is pinned to 0df444a360eaa60ab8c11dca51a86af692955474. This is a 0.x API, with no cross-version compatibility promise.

Scope and provenance

The results do not establish general geometric or singular-homology comparison for tame functions, infinite/q-tame persistence, executable arbitrary-field decomposition, or global diagram smoothness across arbitrary pairing changes. The Mapper and Reeb interfaces are theoretical and do not claim unrestricted convergence or geometric interleaving equivalence. The five directions in #227 are future work.

The source register distinguishes directly verified source matches, narrower checked specializations, original library extensions, and remaining review limits. The package's Apache-2.0 license does not replace source-specific rights analysis for third-party works.