Following the paragraph preceding Section 1.1 of Albin, Clemens, Hoare, Poggi-Corradini, Sit, and Tymochko (2021): throughout, \(G = (V, E)\) denotes a finite, connected multigraph with vertex set \(V\) and edge set \(E\). Parallel edges are allowed; self-loops are not.

To formalize this, a multigraph on vertex type \(V\) and edge type \(E\) consists of a map \(\mathrm{endpoints} \colon E \to \operatorname {Sym}^2(V)\) assigning to each edge its (unordered) pair of endpoints. By making the edges a separate type (rather than a relation on \(V\) or a subset of unordered pairs of vertices), we implicilty allow parallel edges. They are simply distinct elements of \(E\) with the same image under \(\mathrm{endpoints}\). Finiteness, connectedness, and the absence of self-loops are not built into the type itself. Instead, they are added explicitly wherever a paper’s results need them, matching the “throughout this paper” statement.

Throughout, we write \(G = (V, E, \sigma )\) for a multigraph \(G = (V, E)\) together with an edge-weight function \(\sigma \in \mathbb R_{{\gt}0}^E\). However, \(\sigma \) is not part of the multigraph structure itself. We use the triple notation for modulus results, which is where the edge weights are relevant. . For the weight-agnostic combinatorial defintions and theorems (families of objects, densities, admissibility, the Fulkerson dual) we write the plain pair \(G = (V, E)\) instead, since none of those notions depend on \(\sigma \).

A set of edges \(T \subseteq E\) is a spanning tree of \(G\) if it touches every vertex of \(V\) and contains no cycle. In particular, this immediately rules out parallel edges, which would form a 2-cycle.

This is formalized in Multigraph.IsSpanningTree: \(T\) is acyclic (no loops, no parallel edges within \(T\), and the simple graph obtained by forgetting edge identities is acyclic) and that same simple graph is connected, i.e. touches and joins every vertex of \(V\).

Let \(G = (V, E)\) be a multigraph. A family of objects on \(G\) is a nonempty countable set \(\Gamma \subseteq \mathbb R_{\ge 0}^E\) (\(\eta \)-space). In practice, each each \(\gamma \in \Gamma \) is associated with graph-theoretic object (a spanning tree, path, cut, etc.) identified with its usage vector: \(\gamma (e)\) is the usage of edge \(e\) by \(\gamma \).

A family of objects \(\Gamma \) has no zero object if every \(\gamma \in \Gamma \) has \(\gamma (e) {\gt} 0\) for some edge \(e \in E\), i.e. \(\gamma \ne 0\). This rules out the trivial all-zero object, for which no density could ever be admissible.

A density is a point \(\rho \in \mathbb R_{\ge 0}^E\) that assigns a nonnegative cost \(\rho (e)\) to each edge \(e \in E\).

Let \(\rho \) be a density on \(G\). The length of an object \(\gamma \in \Gamma \) with respect to \(\rho \) is

Implementation note: the sum is implemented with finsum rather than Finset.sum over Finset.univ, so that it only requires Finite E, not a Fintype instance. See docs/common.md for details.

A density \(\rho \in \mathbb R_{\ge 0}^E\) is admissible for a family \(\Gamma \) if \(\ell _\rho (\gamma ) \ge 1\) for every \(\gamma \in \Gamma \). The admissible set of \(\Gamma \) is defined as

Let \(\Gamma \) be a finite family of objects on \(G = (V, E)\). The Fulkerson dual family of \(\Gamma \) is \(\widehat\Gamma := \operatorname {ext}(\operatorname {Adm}(\Gamma )) \subset \mathbb R_{\ge 0}^E\), the set of extreme points of \(\operatorname {Adm}(\Gamma )\).

Let \(1 \le p \le \infty \) and let \(G = (V, E, \sigma )\) be a multigraph. The energy of a density \(\rho \) is

Let \(G = (V, E, \sigma )\) be a multigraph. Fix \(1 \le p \le \infty \). The \(p\)-modulus of a family of objects \(\Gamma \) on \(G\) is

A density achieving this infimum is called extremal (or optimal).

A density \(\rho ^* \in \operatorname {Adm}(\Gamma )\) is extremal (or optimal) for \(\operatorname {Mod}_{p,\sigma }(\Gamma )\) if