v0.2.0 — Persistence distances, representations, metric inputs, Reeb and Mapper

This release extends v0.1.0 with Lean-checked results merged to develop since that release: persistence distances and transport, finite-constructible real persistence modules, persistence representations, metric inputs, and bounded Reeb and Mapper theory. The certified finite F₂ persistence computation of v0.1.0 is unchanged.

Included results

• Persistent homology distances and transport. For finite positive birth–death pairs with unit occurrence masses and the maximum ground norm, powered partial-matching minima for real p ≥ 1 equal the optima over all feasible finite real boundary-reservoir plans; rooted optima agree, and both are attained. Rooted costs satisfy symmetry, the triangle inequality and separation by multiplicity. With N the sum of both finite-occurrence counts, d_p ≤ d_1 ≤ N^(1−1/p) d_p. Finite-part transport is bounded by N^(1/p) times a finite full bottleneck distance, giving face-value perturbation bounds for filters on the same finite complex without a fixed pairing. Common diagonal translation preserves these costs; nonnegative coordinate scaling by c multiplies powered costs by c^p and rooted costs by c. Finite boundary transport also permits arbitrary nonnegative real masses that split between labels, with attained optima for p ≥ 1; unit masses recover the occurrence-based costs. Total persistence over finite bars is translation-invariant, homogeneous under positive scaling, and bounded for finite Rips and Čech diagrams by explicit face-count bounds. Essential bars are excluded from these transport quantities but remain in the full diagrams.
• Finite-constructible real persistence modules. Over a field, finite-constructible real-indexed modules admit barcode realizations and a bottleneck–interleaving isometry, assuming finite-dimensional critical fibers, a zero left tail and isomorphic structure maps within left-closed, right-open strata. Different finite critical grids and a nonzero final tail are allowed; unequal essential multiplicities give infinite distance. The isometry applies to the sublevel homology modules of filters on the same finite complex. Pointwise finite-dimensional finite-chain modules have canonical mono/epi occurrence embeddings and induced partial matchings with quantitative endpoint and long-bar bounds. Positive scaling of real-indexed modules scales the extended interleaving distance by the same factor over every ring. Finite-line and rectangular matrix-sequence adapters give persistence modules over a ring, or a commutative ring; over a field their interval barcodes are independent of supplied bases.
• Persistence representations. Gaussian persistence images at fixed positive bandwidth and fixed disjoint measurable pixels, and weighted Gaussian kernel embeddings, are stable on finite diagram parts against the first-order matching cost under explicit weight assumptions, with explicit constants for the arctan weight. Rips and Čech diagrams have radius-scale and log-scale image and kernel consumers under the stated same-label, compatible-label and positivity hypotheses. At nonzero bandwidth, the Gaussian reproducing-kernel Hilbert space on the birth–death plane separates finite signed Borel measures and is uniformly dense in C₀(ℝ²); strictly positive measurable weights with finite weighted mass give injective embeddings of positive persistence measures, including infinite-mass Radon measures. These analytic constructions are abstract and do not make finite-pixel images characteristic.
• Metric inputs. Finite Rips and ambient Čech filtrations are constructed, with the Rips/Čech sandwich, same-label and distance-matrix perturbation stability, and the sup-norm, displacement and log-scale comparisons. For finite nonempty metric spaces, full Rips diagrams satisfy d_B ≤ 2 d_GH in every degree without equal-cardinality or common-label assumptions. Finite samples in a common ambient space have a twice-Hausdorff-error bound; two finite samples of a possibly infinite target are compared through their finite diagrams only, and Hausdorff-convergent samples of a fixed finite target have bottleneck-convergent diagrams. Exact diagrams and bottleneck values over ZMod 2 are computed for two points and the acute triangle.
• Reeb. In the finite real-graph category, geometric smoothing composes coherently, and geometric and cosheaf interleavings agree with equal extended distances. Smoothing enlarges along the parameter, interleavings are monotone, constructible smoothing lifts to constructible cosheaves, and smoothing an interleaving preserves its parameter with two-sided distance bounds. Height-range, top-component and interval-local obstructions give lower bounds, with exact fixture distances. Finite Reeb data have an incidence quiver and a simple incidence graph. The Reeb quotient of every constructible real space satisfies the smoothing absorption comparison; constructibility of the product thickening is established for graph input. Changing the level list of a fixed cylinder presentation gives a homeomorphism of realizations and a constructible perturbed height on the fixed carrier; the constructible interleaving distance is bounded by the sup distance of the two level lists, with the exact value |c| for vertical translation of a nonempty realization.
• Mapper. Graph-PL inputs have ordinary and MultiNerve Mapper constructions, a cover-dependent cell classification and finite Reeb incidence data under explicit cover and height assumptions. Member-adapted, height-separating, vertex-height-covering uniform covers with 0 < g and 2g ≤ r identify the MultiNerve Mapper data with the graph-PL finite Reeb data, and such covers exist below any prescribed radius. Closed level sets, level windows and covering refinements are compatible with this identification; the ordinary Mapper one-skeleton agrees with the incidence graph. The interval-components cosheaf of a vertex-height-covering input is constructible and agrees with the cosheaf of the finite Reeb data. The Reeb quotient of a finite graph-PL realization is identified with its finite graph realization. For a finite bounded interval cover of the attained height range, categorical Mapper reconstruction lies within the full width of the retained intervals of that quotient in geometric interleaving distance, and vanishing resolution gives convergence.

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.

Renames and module moves

Statements, hypotheses and proofs are unchanged by the following; only identifiers and module paths moved. No compatibility aliases are provided.

• Public names of the form actual* / Actual* are replaced by names for the represented mathematical objects, for example ActualLossDerivative → SublevelLossDerivative, actualBoundaryMatrix → faceBoundaryMatrix, actualHomologyEquivOriginal → prefixHomologyEquivMatrixHomology, actualPivotBarcode → facePivotBarcode. The complete old-to-new table is in PR #473. The digests docs/math/actual-ph-loss-*.md are now docs/math/sublevel-loss-derivatives.md and docs/math/sublevel-loss-hessians.md.
• TDA.Mapper.GraphPL.exists_mem_K_of_mem_Icc became TDA.Reeb.CriticalValues.exists_mem_K_of_mem_Icc (module TDA.Reeb.CriticalValues); the shared lemma TDA.Reeb.GraphPL.dartHeight_injective (module TDA.Reeb.GraphPLHeight) replaces private copies (#487).
• The generic label-face lemmas labelFace, labelFace_le, eq_labelFace_of_le, vertexCellsEquiv_labelFace and vertexCellsEquiv moved to TDA.Mapper.MultiNerveGraphPL (#486).
• New module TDA.Mapper.GraphPLRealizationTopology holds the barycentric-coordinate, Hausdorffness, edge/vertex equality, local path-connectedness, injectivity and compactness results for graph realizations, moved out of GraphPLConstructible and GraphPLReebQuotient (#489).
• New module TDA.Mapper.GraphPLDataRefinement holds the graph-PL data refinement maps (graphPLRefineHom, graphPLRefineIso, the level-vertex and span-edge equivalences, their transitivity lemmas, range_vertexHeightLevels_subset and graphPLRefineToOverIso), moved out of TDA.Mapper.GraphPLRefinement, which keeps the uniform Mapper comparison declarations and still imports everything it did before (#490).
• TDA.Persistence.Reduction.FilteredNormalForm is split into three stage modules: FilteredNormalForm.NormalMatrix (pivot pairing, normalMatrix, normalDifferential and its conjugation of the boundary), FilteredNormalForm.NormalHomology (alive coordinates, paired and essential intervals, normal cycles, boundaries, homology and rank formulas) and FilteredNormalForm.OriginalHomology (OriginalCycle, OriginalBoundary, cycleBasisEquiv, originalHomologyEquivAlive and the originalHomologyMap family). FilteredNormalForm itself is now an imports-only entry point, so existing imports and fully qualified names keep working (#491).
• Example fixtures only: the shared rank-example fixtures live in TDA.Persistence.RankExampleFixtures (#488).

Scope and provenance

The results do not establish all-Radon boundary-transport identification, general infinite or q-tame persistence, metric stability for diagrams of infinite point sets, executable arbitrary-field decomposition, an executable Mapper algorithm, or constructibility of the product thickening of a general constructible real space beyond graph input. Level-change stability of Reeb presentations fixes the presentation and the number of levels; arbitrary continuous perturbations are outside that API. Categorical Mapper is not identified with the ordinary Mapper simple graph, and neither Mapper construction claims a Nerve Lemma. The source register distinguishes directly verified source matches, checked finite specializations, library extensions and remaining review limits. The pre-release consolidated semantic and API review recorded on #390 covered representative exported paths and does not certify every declaration against external sources. The package's Apache-2.0 license does not replace source-specific rights analysis for third-party works.