# Bounded-distortion <i>L</i><sub>1</sub> embeddings of planar and bounded-treewidth graphs

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Planar Graph Metrics Embed into $L_1$ with Constant Distortion](../../preprints/Planar-Graph-Metrics-Embed-into-L1-with-Constant-Distortion-September-23-2026/paper.pdf)
- [$L_1$ Embeddings of Graphs of Bounded Treewidth](../../preprints/L1-Embeddings-of-Graphs-of-Bounded-Treewidth-September-23-2026/paper.pdf)

## Scope

The planar case of the Gupta–Newman–Rabinovich–Sinclair embedding problem asks for a universal distortion bound in $L_1$. The formalized result gives one constant $C$ for every finite connected planar graph with arbitrary positive real edge lengths: its weighted shortest-path metric embeds into real $L_1$ with distortion at most $C$. The constant is independent of the number of vertices and the ratios between edge lengths; singleton graphs are included.

The formalized result gives a uniform $L_1$ embedding bound for each bounded-treewidth class. For every bag-size bound $k\ge2$, there is a constant $C(k)$ such that the weighted shortest-path metric of every nonempty finite connected graph with a tree decomposition of bag size at most $k$ embeds into finite-dimensional real $L_1$ with distortion at most $C(k)$. Edge lengths may be arbitrary positive real numbers, and the constant is independent of the graph and decomposition size.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Planar graph metrics in $L_1$ | [PlanarL1.lean](../ComparatorChallenges/PlanarL1.lean) |
| Bounded-treewidth graph metrics in $L_1$ | [BoundedTreewidthL1.lean](../ComparatorChallenges/BoundedTreewidthL1.lean) |