[amluto]

My issues with the definition of L are mostly about the order in which things are written.

L(t, epsilon)_e breaks down the range of L onto its component values indexed by edge, but this only really makes sense when you know that t and epsilon are. They are sort of defined in the middle of a sentence in the proof of 2.1, which IMO is asking a lot of the reader, and this sort of sloppiness is a way that errors can hide in a proof. (Not that I see an error here. But a formalization in Lean or whatever would not get away with this.)

And, in the same definition of L, for some reason the e=uv part comes at the end only after u and v are used.

What would be wrong with stating, in the definition, what sorts of objects t and epsilon are and with omitting e entirely in favor of just calling the edge uv everywhere?