Steiner ratio

AbbreviationThe Euclidean plane of the Steiner ratio problem#✓fully proved

The space \(\mathbb{R}^2\) with the Euclidean distance, in which the point sets of the Steiner ratio problem lie.

abbrev Plane := EuclideanSpace ℝ (Fin 2)

Used by 8

Used byLength of an edge · Minimum spanning tree length · Lengths of spanning trees · Steiner minimal tree length · The Steiner length is at most the minimum spanning tree length · The Steiner ratio of the Euclidean plane · Lengths of Steiner trees · Total length of a graph on points of the plane

DefinitionLength of an edge#✓fully proved

For points \(x\) and \(y\) of the Euclidean plane, the length of the unordered pair \(\{x, y\}\) is the Euclidean distance between \(x\) and \(y\).

noncomputable def edgeLength (e : Sym2 Plane) : ℝ :=
  Sym2.lift (⟨fun x y : Plane => dist x y, fun x y : Plane => dist_comm x y⟩ :
    { f : Plane → Plane → ℝ // ∀ a b, f a b = f b a }) e

Uses 1 · Used by 2

Statement usesThe Euclidean plane of the Steiner ratio problem

Used byThe Steiner length is at most the minimum spanning tree length · Total length of a graph on points of the plane

DefinitionTotal length of a graph on points of the plane#✓fully proved

For a finite set \(V\) of points in the Euclidean plane and a simple graph \(G\) with vertex set \(V\), the total length of \(G\) is the sum, over all edges \(\{x, y\}\) of \(G\), of the Euclidean distance between \(x\) and \(y\).

noncomputable def totalLength {V : Finset Plane} (G : SimpleGraph V) : ℝ := by
  classical
  exact ∑ e ∈ G.edgeFinset, edgeLength (Sym2.map Subtype.val e)

Uses 2 · Used by 3

Statement usesThe Euclidean plane of the Steiner ratio problem · Length of an edge

Used byLengths of spanning trees · The Steiner length is at most the minimum spanning tree length · Lengths of Steiner trees

DefinitionLengths of spanning trees#✓fully proved

For a finite set \(V\) of points in the Euclidean plane, this is the set of real numbers \(\ell\) such that some tree with vertex set \(V\) has total length \(\ell\), the total length being the sum of the Euclidean lengths of its edges.

def spanningTreeLengths (V : Finset Plane) : Set ℝ :=
  { l | ∃ G : SimpleGraph V, G.IsTree ∧ totalLength G = l }

Uses 2 · Used by 2

Statement usesThe Euclidean plane of the Steiner ratio problem · Total length of a graph on points of the plane

Used byMinimum spanning tree length · The Steiner length is at most the minimum spanning tree length

DefinitionLengths of Steiner trees#✓fully proved

For a finite set \(V\) of points in the Euclidean plane, this is the set of real numbers \(\ell\) such that, for some finite set \(W\) of points of the plane containing \(V\), some tree with vertex set \(W\) has total length \(\ell\). The points of \(W\) outside \(V\) are the Steiner points.

def steinerTreeLengths (V : Finset Plane) : Set ℝ :=
  { l | ∃ W : Finset Plane, V ⊆ W ∧
      ∃ G : SimpleGraph W, G.IsTree ∧ totalLength G = l }

Uses 2 · Used by 2

Statement usesThe Euclidean plane of the Steiner ratio problem · Total length of a graph on points of the plane

Used bySteiner minimal tree length · The Steiner length is at most the minimum spanning tree length

DefinitionMinimum spanning tree length#✓fully proved

For a finite set \(V\) of points in the Euclidean plane, the minimum spanning tree length of \(V\) is the infimum of the total lengths of the trees with vertex set \(V\). For nonempty \(V\) this set of lengths is finite and nonempty, so the infimum is a minimum; for empty \(V\) the value is \(0\) by convention.

noncomputable def mstLength (V : Finset Plane) : ℝ :=
  sInf (spanningTreeLengths V)

Uses 2 · Used by 2

Statement usesThe Euclidean plane of the Steiner ratio problem · Lengths of spanning trees

Used byThe Steiner length is at most the minimum spanning tree length · The Steiner ratio of the Euclidean plane

DefinitionSteiner minimal tree length#✓fully proved

For a finite set \(V\) of points in the Euclidean plane, the Steiner length of \(V\) is the infimum of the total lengths of the trees whose vertex set is a finite set of points of the plane containing \(V\). This set of lengths is nonempty and bounded below by \(0\), so the infimum exists.

noncomputable def steinerLength (V : Finset Plane) : ℝ :=
  sInf (steinerTreeLengths V)

Uses 2 · Used by 2

Statement usesThe Euclidean plane of the Steiner ratio problem · Lengths of Steiner trees

Used byThe Steiner length is at most the minimum spanning tree length · The Steiner ratio of the Euclidean plane

TheoremThe Steiner length is at most the minimum spanning tree length#✓fully proved

For every nonempty finite set \(V\) of points in the Euclidean plane, the Steiner minimal tree length of \(V\) is at most the minimum spanning tree length of \(V\): allowing Steiner points never increases the optimal length.

theorem steinerLength_le_mstLength {V : Finset Plane} (hV : V.Nonempty) :
    steinerLength V ≤ mstLength V

Uses 7

Statement usesThe Euclidean plane of the Steiner ratio problem · Minimum spanning tree length · Steiner minimal tree length

Proof usesLength of an edge · Lengths of spanning trees · Lengths of Steiner trees · Total length of a graph on points of the plane

DefinitionThe Steiner ratio of the Euclidean plane#✓fully proved

The Steiner ratio constant is the infimum, over all finite sets \(V\) of at least two points in the Euclidean plane \(\mathbb{R}^2\), of the ratio of the Steiner minimal tree length of \(V\) to the minimum spanning tree length of \(V\).

noncomputable def steinerRatioConstant : ℝ :=
  sInf { r | ∃ V : Finset Plane, 2 ≤ V.card ∧
    r = steinerLength V / mstLength V }

Uses 3 · Used by 3

Statement usesThe Euclidean plane of the Steiner ratio problem · Minimum spanning tree length · Steiner minimal tree length

Used byChung–Graham lower bound for the Steiner ratio · Gilbert–Pollak conjecture · Gilbert–Pollak upper bound for the Steiner ratio

DefinitionGilbert–Pollak conjecture#✓fully proved

The Steiner ratio of the Euclidean plane, that is, the infimum of the ratio of the Steiner minimal tree length to the minimum spanning tree length over all finite sets of at least two points in the plane, equals \(\sqrt{3}/2\).

The vertices of an equilateral triangle have ratio exactly \(\sqrt{3}/2\), so the conjecture says that no finite set of at least two points in the plane has a smaller ratio.

def GilbertPollakConjecture : Prop :=
  steinerRatioConstant = Real.sqrt 3 / 2

Uses 1

Statement usesThe Steiner ratio of the Euclidean plane

TheoremGilbert–Pollak upper bound for the Steiner ratio#●ready to prove

The Steiner ratio constant, the infimum over finite sets \(V\) of at least two points in the Euclidean plane of the length of a Steiner minimal tree for \(V\) divided by the length of a minimum spanning tree of \(V\), is at most \(\sqrt{3}/2\).

theorem_wanted gilbertPollakUpperBound_wanted :
    steinerRatioConstant ≤ Real.sqrt 3 / 2

Sources

• Gilbert and Pollak, Steiner minimal trees (1968): the equilateral triangle gives the upper bound √3 / 2.

Uses 1

Statement usesThe Steiner ratio of the Euclidean plane

TheoremChung–Graham lower bound for the Steiner ratio#●ready to prove

The Steiner ratio constant, the infimum over finite sets \(V\) of at least two points in the Euclidean plane of the length of a Steiner minimal tree for \(V\) divided by the length of a minimum spanning tree of \(V\), is at least \(0.824\).

theorem_wanted chungGrahamLowerBound_wanted :
    (824 / 1000 : ℝ) ≤ steinerRatioConstant

Sources

• Chung and Graham (1985), via the catalogue's best unconditional published lower bound 0.824 before the conditional 2026 computer-assisted rows.

Uses 1

Statement usesThe Steiner ratio of the Euclidean plane

10 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.