A quantitative equational theory $U$ reasons about terms that agree up to a numerical error. It presents a free algebra $T_UA$ over a metric space $A$ of generators, the terms of the syntax at the least distance the axioms derive, and that metric is its semantic content. We give a functorial invariant of it, the persistent magnitude homology of $T_UA$: a barcode where the module is tame, finite linear algebra where $T_UA$ is finite, Lipschitz in each degree. Magnitude homology is graded by length and knows nothing of persistence, its persistent refinement nothing of where its bars begin and end, yet the two are one construction: filtering the length nerve by sublevel sets of the length yields the persistence module, and the associated graded of that filtration is the magnitude complex. A long exact sequence exchanges them, and each side gains what it lacked. Magnitude homology locates the critical values of the barcode, so a graded computation lists the lengths at which an endpoint can occur, and the barcode acquires a stability estimate of $(n+1)δ$ in degree $n$ under a perturbation of size $δ$, and a computed perturbation shows that the factor cannot be dropped. An inclusion of theories induces a morphism of the presenting monads and, where the induced map is bijective and shortens no distance by more than $δ$, a comparison of barcodes under the same bound, so a barcode movement measures the metric-semantic strength of the added axioms. Four examples are computed, one in every degree.

翻译：暂无翻译