we-solve (beta)

Math-2643 · mathematics · Geometry

Uniform L1 distortion of planar graph metrics

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Is there one finite C such that every finite connected planar graph with arbitrary positive real edge lengths has a map f into a real $L^{1}$ space and a scale $s>0$ satisfying $s\cdot d(x,y)\leq \Vert f(x)-f(y)\Vert _{1}\leq C\cdot s\cdot d(x,y)$ for all vertices, where d is weighted shortest-path distance?

Short English statement

Is there one finite C such that every finite connected planar graph with arbitrary positive real edge lengths has a map f into a real $L^{1}$ space and a scale $s>0$ satisfying $s\cdot d(x,y)\leq \Vert f(x)-f(y)\Vert _{1}\leq C\cdot s\cdot d(x,y)$ for all vertices, where d is weighted shortest-path distance?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2643-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2643

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 089; 2026-09-23).

Uniform L1 distortion of planar graph metrics

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 089; 2026-09-23), the asserted result is that arbitrary positive edge lengths on finite planar graphs admit a common constant-distortion embedding into real $L_1$.

Mathematical statement of the claimed result

Manuscript 1.
Assign arbitrary positive real lengths to the edges of any finite planar graph that is connected. The claim supplies a real $L^1$ embedding and one constant $C<\infty$, common to all these graphs, satisfying \[ d_G(x,y)\le\|f(x)-f(y)\|_1\le C d_G(x,y)\quad(x,y\in V(G)). \] No dependence on vertex count, particular planar embedding or edge-length ratios occurs in $C$.

Outline of the argument

For manuscript 1 (family 089; 2026-09-23), measurable labels define cut distances whose upper comparison holds deterministically. Random chart changes, portals, and component ancestry supply a lower separation probability, and packing control permits the cut families to be assembled at all scales.

Formal verification

For manuscript 1 (family 089; 2026-09-23), OpenAI lists Lean statements for this assertion: arbitrary positive edge lengths on finite planar graphs admit a common constant-distortion embedding into real $L_1$.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

The linked family Comparator checks are BoundedTreewidthL1.lean, PlanarL1.lean.

Their named declarations include OAI.BoundedTreewidthL1.main_theorem, OAI.PlanarL1.planar_graph_metrics_embed_L1.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →