arxiv: 2605.03487 · v2 · submitted 2026-05-05 · 🧮 math.AT · math.CT

Recognition: 2 theorem links

· Lean Theorem

Weighted algebraic topology, II (Real valued metrics)

Marco Grandis

Authors on Pith no claims yet

Pith reviewed 2026-05-14 22:10 UTC · model grok-4.3

classification 🧮 math.AT math.CT

keywords real metricsenriched categoriesweighted algebraic topologypotential functionextended real linemonoidal closed categorydirected paths

0 comments

The pith

Linear real metrics derive from a potential function when defined via enrichment over the extended real line.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper extends Lawvere metric spaces to real metrics valued in the extended real line. The extended reals are treated as a symmetric monoidal closed category so that enriched categories over it assign measurements to paths or processes. These measurements represent profits and losses in any sense, such as energy or variables from other sciences. A central result shows that linear real metrics derive from a potential function. The work forms part of weighted algebraic topology, which enriches directed algebraic topology to handle measured paths.

Core claim

By viewing the extended real line as a symmetric monoidal closed category, real metrics arise as enriched categories that measure the profits and losses of processes. In particular, linear real metrics derive from a potential function.

What carries the argument

The symmetric monoidal closed category structure on the extended real line, which serves as the enrichment base for defining real metrics that quantify directed measurements of processes.

Load-bearing premise

The extended real line with its order and operations forms a symmetric monoidal closed category whose enrichment structure meaningfully captures profits and losses in processes.

What would settle it

A concrete linear real metric on a process that cannot be recovered as the difference of values from any potential function.

read the original abstract

Extending the `metric spaces' of Lawvere, we study `real metrics', with values in the extended real line. Formally, this ordered set is a symmetric monoidal closed category, and our structures are enriched categories on the latter. Concretely, the present goal is measuring `profits' and `losses' of a process, in any sense - possibly related to energy, or a variable in any science. In particular, linear real metrics derive from a potential function. This article is Part II in a series devoted to `weighted algebraic topology' - an enriched version of directed algebraic topology, where paths are measured. Part III will introduce a finer framework, more adequate to `quotient spaces' (as the spheres) and better related to topology.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Grandis extends Lawvere metrics to signed extended reals to track gains and losses in paths, deriving linear cases from potentials, but the monoidal closed structure on infinities needs explicit checks.

read the letter

Grandis extends Lawvere's non-negative metrics to real-valued ones over the extended reals, so that weights can be negative and capture losses as well as gains in directed processes. The concrete claim is that linear real metrics arise from a potential function, and the whole setup is presented as enriched categories over that ordered monoidal structure. This keeps the work inside the weighted algebraic topology series and gives a direct interpretation for energy-like variables or other scientific quantities. The paper does a straightforward job of stating the formal move and the intended applications without adding unrelated machinery. It stays consistent with the earlier parts of the series and with Lawvere's original enrichment idea. The main soft spot is the arithmetic on the extended reals. Addition and the internal hom (subtraction) are not total once both positive and negative infinities appear, and expressions like +∞ + (−∞) are left undefined in standard conventions. If the paper does not fix a specific rule that preserves associativity, the triangle inequality, and the closed monoidal universal property in every case, then the enrichment and the potential-function derivation rest on incomplete foundations. The abstract simply asserts the structure works, so the body needs to show the conventions explicitly. This is for readers already comfortable with enriched categories and directed topology who want to track signed weights on paths. A specialist in the area would get a clear next step in the series and could check the details on the monoidal axioms. It is not a broad new paradigm but a direct continuation, so it deserves a serious referee to verify the handling of infinities and the potential-function claim rather than a desk rejection.

Referee Report

1 major / 1 minor

Summary. The paper extends Lawvere's metric spaces to real metrics valued in the extended real line, treated formally as a symmetric monoidal closed category whose enriched categories capture directed paths with real-valued weights. The concrete goal is to measure profits and losses (e.g., energy or other process variables), with the specific claim that linear real metrics derive from a potential function. This is Part II of a series on weighted algebraic topology, with Part III promised for quotient spaces.

Significance. If the enrichment is rigorously constructed and the derivation of metrics from potentials is established without ad-hoc conventions, the framework would supply a categorical setting for real-weighted directed topology that could interface with optimization, physics, or process analysis. The explicit link to potential functions would be a concrete strength, distinguishing the work from purely abstract enrichment results.

major comments (1)

[Abstract and formal setup] Abstract and formal setup: the claim that linear real metrics derive from a potential function rests on the extended real line (with its order and operations) forming a symmetric monoidal closed category suitable for enrichment. The paper must supply an explicit, total convention for indeterminate expressions such as (+∞) + (−∞) that preserves the monoidal unit, associativity, and the universal property of the internal hom (presumably subtraction); without it the triangle inequality for enriched homs and the potential-function derivation become formally unsupported.

minor comments (1)

[Abstract] The abstract is dense; separating the categorical definition from the motivational examples (profits/losses, energy) would improve readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading and for identifying a point that requires greater explicitness in the formal setup. We address the major comment below and will revise the manuscript accordingly.

read point-by-point responses

Referee: [Abstract and formal setup] Abstract and formal setup: the claim that linear real metrics derive from a potential function rests on the extended real line (with its order and operations) forming a symmetric monoidal closed category suitable for enrichment. The paper must supply an explicit, total convention for indeterminate expressions such as (+∞) + (−∞) that preserves the monoidal unit, associativity, and the universal property of the internal hom (presumably subtraction); without it the triangle inequality for enriched homs and the potential-function derivation become formally unsupported.

Authors: We agree that the manuscript must supply an explicit convention for the indeterminate case (+∞) + (−∞). The current text assumes the usual arithmetic on the extended reals but does not state the convention explicitly. In the revision we will add a short subsection (new §2.2) that defines addition on ℝ ∪ {±∞} by the rule (+∞) + (−∞) := +∞ (and symmetrically for the opposite sign), verifies that this choice preserves the monoidal unit 0, associativity on all defined triples, and the closed structure whose internal hom is subtraction. With these definitions the enriched triangle inequality and the derivation of linear real metrics from potential functions become formally supported. revision: yes

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper extends Lawvere metric spaces by enriching over the extended real line as a symmetric monoidal closed category. The central claim that linear real metrics derive from a potential function is presented as following from this enrichment structure and the ordered monoid operations, without any quoted equations or steps that reduce by construction to fitted parameters, self-definitions, or load-bearing self-citations. The work references prior Lawvere structures and the author's series but treats them as independent input rather than circular justification. No specific reduction of a prediction to its input is exhibited in the provided claims or abstract.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on the standard axioms of enriched category theory and the monoidal closed structure of the extended reals; no free parameters or new invented entities are introduced in the abstract.

axioms (1)

domain assumption The extended real line forms a symmetric monoidal closed category under its order and operations.
Invoked to define the enrichment base for the real metrics.

pith-pipeline@v0.9.0 · 5414 in / 1090 out tokens · 36971 ms · 2026-05-14T22:10:49.876462+00:00 · methodology

Review history (3 revisions) →

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

linear real metrics derive from a potential function... ρ(x, y) = Φ(y)−Φ(x)
IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean absolute_floor_iff_bare_distinguishability unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

the extended real line... symmetric monoidal closed category... λ+ρ

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

20 extracted references · 20 canonical work pages · 1 internal anchor

[1]

Barr, *-Autonomous categories, Lecture Notes in Mathematics, Vol

M. Barr, *-Autonomous categories, Lecture Notes in Mathematics, Vol. 752, Springer, 1979

work page 1979
[2]

Bourbaki, Topologie g\'en\'erale, Ch

N. Bourbaki, Topologie g\'en\'erale, Ch. 10, Hermann, 1961

work page 1961
[3]

Christensen, G

J.D. Christensen, G. Sinnamon and E. Wu, The D-topology for diffeological spaces, Pacific. J. Math. 272 (2014), 87--110

work page 2014
[4]

Eilenberg and G.M

S. Eilenberg and G.M. Kelly, Closed categories, in Proc. Conf. Categorical Algebra, La Jolla 1965, Springer, 1966, pp. 421--562

work page 1965
[5]

Fajstrup, E

L. Fajstrup, E. Goubault, E. Haucourt, S. Mimram and M. Raussen, Directed algebraic topology and concurrency, Springer, 2016

work page 2016
[6]

Flagg, Quantales and continuity spaces, Algebra Universalis, 37 (1997), 257--276

R. Flagg, Quantales and continuity spaces, Algebra Universalis, 37 (1997), 257--276

work page 1997
[7]

Grandis, Directed homotopy theory, I

M. Grandis, Directed homotopy theory, I. The fundamental category, Cah. Topol. G\'eom. Diff\'er. Cat\'eg. 44 (2003), 281--316. Available at https://www.numdam.org/issues/CTGDC\_2003\_44\_4/

work page 2003
[8]

Grandis, Categories, norms and weights, J

M. Grandis, Categories, norms and weights, J. Homotopy Relat. Struct. 2 (2007), No. 9, 171--186

work page 2007
[9]

Grandis, The fundamental weighted category of a weighted space (From directed to weighted algebraic topology), Homology Homotopy Appl

M. Grandis, The fundamental weighted category of a weighted space (From directed to weighted algebraic topology), Homology Homotopy Appl. 9 (2007), 221--256. Available at https://intlpress.com/JDetail/1805807194991902721

work page arXiv 2007
[10]

Grandis, Directed Algebraic Topology, Models of non-reversible worlds, Cambridge Univ

M. Grandis, Directed Algebraic Topology, Models of non-reversible worlds, Cambridge Univ. Press, 2009. Available at https://www.researchgate.net/publication/267089582

work page arXiv 2009
[11]

Grandis, Weighted algebraic topology, II (Relative metrics), Preprint, arXiv, 2026

M. Grandis, Weighted algebraic topology, II (Relative metrics), Preprint, arXiv, 2026

work page 2026
[12]

Kelly, Bitopological spaces, Proc

J.C. Kelly, Bitopological spaces, Proc. London Math. Soc. 13 (1963), 71--89

work page 1963
[13]

Kelly, Basic concepts of enriched category theory, Cambridge University Press, 1982

G.M. Kelly, Basic concepts of enriched category theory, Cambridge University Press, 1982

work page 1982
[14]

Lawvere, Metric spaces, generalized logic and closed categories, Rend

F.W. Lawvere, Metric spaces, generalized logic and closed categories, Rend. Sem. Mat. Fis. Univ. Milano 43 (1974), 135--166. Republished in: Reprints Th. Appl. Categ. 1 (2002), 1--37. Available at http://www.tac.mta.ca/tac/reprints/articles/1/tr1.pdf

work page 1974
[15]

Lawvere, State Categories, Closed Categories, and the Existence Semi-Continuous Entropy Functions, IMA Preprint Series 84, University of Minnesota, 1984

F.W. Lawvere, State Categories, Closed Categories, and the Existence Semi-Continuous Entropy Functions, IMA Preprint Series 84, University of Minnesota, 1984

work page 1984
[16]

Mac Lane, Categories for the working mathematician, Springer, 1971

S. Mac Lane, Categories for the working mathematician, Springer, 1971

work page 1971
[17]

Mulvey, ``&", Rend

C.J. Mulvey, ``&", Rend. Circ. Mat. Palermo, Suppl. 12 (1986), 99--104

work page 1986
[18]

Rosenthal, Quantales and Their Applications, Longman Scientific & Technical, 1990

K. Rosenthal, Quantales and Their Applications, Longman Scientific & Technical, 1990

work page 1990
[19]

The Legendre-Fenchel transform from a category theoretic perspective

S. Willerton, The Legendre-Fenchel transform from a category theoretic perspective, arXiv 1501.03791v1, 2015

work page internal anchor Pith review Pith/arXiv arXiv 2015
[20]

Yetter, Quantales and (noncommutative) linear logic, J

D. Yetter, Quantales and (noncommutative) linear logic, J. Symb. Log. 55 (1990), 41--64

work page 1990