[#P2502] Minimum spanning-tree dilation on the regular nonagon

Contents

Problem. Place nine vertices at the corners of a regular nonagon of circumradius one. For a spanning tree \(T\), let \(\delta(T)=\max_{u\ne v} d_T(u,v)/\|u-v\|\), where \(d_T\) is Euclidean path length in \(T\). Is the minimum of \(\delta(T)\) equal to \(2\sin(4\pi/9)/\sin(\pi/9)\), the dilation of a star centered at a polygon vertex?

Agent access

Work in ChatGPT

The agent reads this problem's research brief and asks you before it saves anything to TheoremDB.

Definitions and notation

1Context

For the star, the worst pair is the adjacent pair opposite its center. The exact dilation is \(2\sin(4\pi/9)/\sin(\pi/9)\), approximately \(5.758770483143634\).

2Definitions

Definition 1 (Every tree edge). Every tree edge is weighted by its Euclidean chord length.

Definition 2 (Trees). Trees are labeled by the nine fixed polygon vertices; rotations and reflections preserve dilation.

3What counts as a solution

Prove that every nonagon spanning tree has dilation at least \(2\sin(4\pi/9)/\sin(\pi/9)\) and exhibit equality, or exhibit a tree with strictly smaller dilation.

1Status

Saved packet · July 24, 2026

What counts as a solution

Submitted solution (The minimum nonagon tree dilation is 2+4 cos(pi/9)). Every spanning tree has dilation at least 2+4 cos(pi/9), and each vertex-centered star attains equality.^[1]

Verification

Number the vertices cyclically from 0 through 8, put \(\theta=\pi/9\), and write \(\ell_k=2\sin(k\theta)\) for a chord spanning \(k\) polygon steps. The star centered at vertex 0 has its largest detour between vertices 4 and 5. That path has length \(2\ell_4\), while the direct chord has length \(\ell_1\). Its dilation is therefore \[ S=\frac{2\sin(4\pi/9)}{\sin(\pi/9)}. \] The executable certificate compares every pair in this star and finds no larger ratio.

Let \(x=2\cos(\pi/9)\). The triple-angle identity gives \(x^3-3x-1=0\), and \(\sin(4\theta)/\sin\theta=x^3-2x=x+1\). Hence \[ S=2+2x=2+4\cos(\pi/9). \] Equivalently, \(S\) is the largest root of \(s^3-6s^2+8\). The certified interval is \[ 5.758770483142<S<5.758770483144. \]

Pruefer words enumerate the \(9^7=4{,}782{,}969\) labeled spanning trees exactly once. For each tree, the certificate finds a vertex pair whose path-to-chord ratio is at least \(S\). Every comparison is decided in the cubic field generated by \(x\), using integer polynomial arithmetic and a rational isolating interval. This proves the matching lower bound. There are 7,515 labeled minimizing trees. They include the nine vertex-centered stars, one for each choice of center.

1Packet records

Show recorded summaries

Record	Kind	Assessment
Every spanning tree has dilation at least 2+4 cos(pi/9), and each vertex-centered star attains equality.	Result	Evidence: Reproduced A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 1 Every spanning tree has dilation at least 2+4 cos(pi/9), and each vertex-centered star attains equality.^[1] Relevance to this problem For Minimum spanning-tree dilation on the regular nonagon, record nonagon-tree-claim-exact-minimum (“The minimum nonagon tree dilation is 2+4 cos(pi/9)”) records a bound, answer, status fact, or structural consequence. The record states: Every spanning tree has dilation at least 2+4 cos(pi/9), and each vertex-centered star attains equality. Evidence ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope. Record state established Scope all Euclidean spanning trees on the nine labeled vertices of a regular nonagon of circumradius one Sources Reference 1 Details Number the vertices cyclically from 0 through 8, put \(\theta=\pi/9\), and write \(\ell_k=2\sin(k\theta)\) for a chord spanning \(k\) polygon steps. The star centered at vertex 0 has its largest detour between vertices 4 and 5. That path has length \(2\ell_4\), while the direct chord has length \(\ell_1\). Its dilation is therefore \[ S=\frac{2\sin(4\pi/9)}{\sin(\pi/9)}. \] The executable certificate compares every pair in this star and finds no larger ratio. Let \(x=2\cos(\pi/9)\). The triple-angle identity gives \(x^3-3x-1=0\), and \(\sin(4\theta)/\sin\theta=x^3-2x=x+1\). Hence \[ S=2+2x=2+4\cos(\pi/9). \] Equivalently, \(S\) is the largest root of \(s^3-6s^2+8\). The certified interval is \[ 5.758770483142<S<5.758770483144. \] Pruefer words enumerate the \(9^7=4{,}782{,}969\) labeled spanning trees exactly once. For each tree, the certificate finds a vertex pair whose path-to-chord ratio is at least \(S\). Every comparison is decided in the cubic field generated by \(x\), using integer polynomial arithmetic and a rational isolating interval. This proves the matching lower bound. There are 7,515 labeled minimizing trees. They include the nine vertex-centered stars, one for each choice of center. Open full record →
The closest papers study minimum-dilation trees, star centers, and asymptotic bounds for equally spaced circle points.	Trace	Evidence: Supported Backed by a cited source or by evidence short of a proof.
attempt · Route 1 The closest papers study minimum-dilation trees, star centers, and asymptotic bounds for equally spaced circle points.^[1][3][4][2] Relevance to this problem For Minimum spanning-tree dilation on the regular nonagon, record nonagon-tree-attempt-literature-audit (“Literature gives general circle bounds but no exact nonagon value”) documents a concrete method, search boundary, or failed route. The record states: The closest papers study minimum-dilation trees, star centers, and asymptotic bounds for equally spaced circle points. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state completed Scope focused search for geometric-spanner results on minimum-dilation trees and equally spaced points on a circle through 2026-07-24 Sources Reference 1, Reference 3, Reference 4, Reference 2 What happened Cheong, Haverkort, and Lee prove that computing a minimum-dilation spanning tree is NP-hard for general planar point sets. Eppstein and Wortman give algorithms for evaluating a star and choosing its center, including the case where the center must be an input point. Aronov, de Berg, Cheong, Gudmundsson, Haverkort, Smid, and Vigneron use equally spaced circle points to obtain a linear lower bound for sparse geometric graphs. Buchin, Rehs, and Scheele revisit the same family. Their 2025 paper records the tree lower bound \(2n/\pi-1\) from Aronov and coauthors and proves a tree upper bound \[ \frac{2n}{\pi}+\frac{\pi}{2n}. \] These bounds frame the present value without specifying the optimum for nine points. Searches for the title terms together with `nonagon`, `regular 9-gon`, and `nine equally spaced points` found no paper stating the exact nine-point tree value. This is a focused prior-art check, so the originality of the exact value remains unverified. Related: Computation 1 Open full record →
Integer algebraic comparisons certify the lower bound for all 4,782,969 labeled trees and identify 7,515 minimizers.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1 Integer algebraic comparisons certify the lower bound for all 4,782,969 labeled trees and identify 7,515 minimizers. Relevance to this problem For Minimum spanning-tree dilation on the regular nonagon, record nonagon-tree-artifact-complete-pruefer-search (“Exact Pruefer search over all nonagon spanning trees”) supplies evidence or a replay used to check the packet. The record states: Integer algebraic comparisons certify the lower bound for all 4,782,969 labeled trees and identify 7,515 minimizers. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state available Scope every labeled spanning tree and every unordered vertex pair on a fixed regular nonagon Entry point `join source_lines with newline, compile with the stated command, and run` Runtime C++20 with the signed __int128 integer type supplied by GCC or Clang Details Set \(x=2\cos(\pi/9)\), so \(x^3-3x-1=0\) and \(1<x<2\). The cubic is strictly increasing for \(x>1\). Exact integer substitution at rational endpoints therefore isolates the relevant root in \[ \frac{1879385241571}{10^{12}}<x<\frac{1879385241572}{10^{12}}. \] Suppose a tree path uses \(c_k\) chords of class \(k\), and its endpoints are \(d\) polygon steps apart. Comparing its dilation with \(S=2\ell_4/\ell_1\) reduces to the sign of \[ Q=\ell_1\sum_{k=1}^4 c_k\ell_k-2\ell_4\ell_d. \] Define \(C_j(x)=2\cos(j\pi/9)\). The identity \(\ell_a\ell_b=C_{\|a-b\|}-C_{a+b}\), followed by reduction modulo \(x^3-3x-1\), writes \(Q=a+bx+cx^2\) with integer coefficients. Rational interval evaluation decides every nonzero sign. The program checks a superset of all possible path types, comprising 26,244 count-vector and endpoint-separation combinations. Fourteen reduce identically to zero, and none remain undecided. Each base-nine integer from 0 through \(9^7-1\) supplies one Pruefer word. The standard smallest-leaf decoder constructs its labeled tree. A depth-first traversal records the four chord counts on every path. All 4,782,969 trees contain a pair with ratio at least \(S\). Exactly 7,515 have no pair above \(S\). Nine of these have a degree-eight vertex, giving one centered star at every nonagon vertex. The FNV-1a digest serializes each minimizing Pruefer code as eight little-endian bytes. Related: Computation 1 Open full record →
No records match these filters.

Notes and companion material

Original intake status. SOLVED in the reviewed TheoremDB packet as of 2026-08-01. Every spanning tree has dilation at least 2+4 cos(pi/9), and each vertex-centered star attains equality.

There are \(9^7=4782969\) labeled trees before dihedral quotienting. A proof by enumeration should compare algebraic chord expressions or use certified intervals near ties.
The star is attractive because it minimizes hop count. Its long detours between adjacent vertices on the far side are the likely obstruction.
Fresh exact-title, parameter, source, and corpus searches were completed on 2026-08-01.

Recorded example 1. The vertex-centered star gives the exact upper bound \(\delta\le 2\sin(4\pi/9)/\sin(\pi/9)\).

Computational notes

Complete Prüfer-code enumeration used double-precision chord lengths for every labeled tree with \(3\le n\le8\). The smallest observed values were approximately 2, 2.414213562373095, 3.236067977499789, 3.732050807568878, 4.493959207434934, and 5.027339492125848. A vertex-centered star produced each observed value. The \(n=8\) sweep examined all 262144 trees; the floating-point comparisons still need interval certification.

How the 3 records connect

The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemMinimum spanning-tree dilation on the regular nonagon

All 2 recorded relations between these records and the problem

2See also

Exact ten-point Heilbronn number in the unit squarecomputational geometry
Rectilinear crossing number of K_28computational geometry
Minimum number of convex pentagons determined by seventeen pointscomputational geometry

Contribute to this problem

Cite this problem statement

Cite the original sources separately.

Plain text

“Minimum spanning-tree dilation on the regular nonagon.” TheoremDB. P2502. Problem statement; statement text SHA-256 91a915fbb812ec3437e8d3ef87f8d0e4663e33f2430a664f7b35e4f7be3dcbbc. https://theoremdb.org/statement/?ref=P2502

BibTeX

@misc{theoremdb-problem-91a915fbb812ec3437e8d3ef87f8d0e4663e33f2430a664f7b35e4f7be3dcbbc,
  title = {{Minimum spanning-tree dilation on the regular nonagon}},
  howpublished = {TheoremDB},
  note = {Problem statement; statement text SHA-256 91a915fbb812ec3437e8d3ef87f8d0e4663e33f2430a664f7b35e4f7be3dcbbc},
  url = {https://theoremdb.org/statement/?ref=P2502}
}

Plain text: Built Markdown snapshot

This problem includes 3 records joined by 2 typed links, sourced from doi.org^[1], current as of July 24, 2026.

1Lean verification

Lean formalization needed

A solution has been submitted and awaits independent review.

Open TheoremDB Researcher

Upload a Lean project archive

Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.

1References

Packet source. Buchin, Kevin, Rehs, Carolin, and Scheele, Torben, “Geometric Spanners of Bounded Tree-Width”. LIPIcs, Volume 332, SoCG 2025 (2025). DOI 10.4230/LIPIcs.SoCG.2025.26. Section 6.1, minimum-dilation trees for points in convex position. ↗proceedings article · primary source · checked 2026-08-01Source use: original summary.This is the primary or maintained source used to check the formulation, neighboring results, and current research boundary.Also cited at Buchin, Rehs, and Scheele, Geometric Spanners of Bounded Tree-Width, SoCG 2025, section 6.1; Aronov et al., Sparse Geometric Graphs with Small Dilation, Computational Geometry 40 (2008); Cheong, Haverkort, and Lee, Computing a Minimum-Dilation Spanning Tree is NP-hard, Computational Geometry 41 (2008); Eppstein and Wortman, Minimum Dilation Stars, Computational Geometry 37 (2007); checked 2026-07-24.Also cited at Independent exact certificate nonagon-tree-artifact-complete-pruefer-search, executed on 2026-07-24.For Minimum spanning-tree dilation on the regular nonagon, the reviewed source scope is Buchin, Rehs, and Scheele, Geometric Spanners of Bounded Tree-Width, SoCG 2025, section 6.1; Aronov et al., Sparse Geometric Graphs with Small Dilation, Computational Geometry 40 (2008); Cheong, Haverkort, and Lee, Computing a Minimum-Dilation Spanning Tree is NP-hard, Computational Geometry 41 (2008); Eppstein and Wortman, Minimum Dilation Stars, Computational Geometry 37 (2007); checked 2026-07-24. The packet makes no inference beyond that cited scope.Source named by the research packet.
David Eppstein and Kevin A. Wortman, “Minimum dilation stars,” Computational Geometry 37(1) (2007), 27-37. DOI 10.1016/j.comgeo.2006.05.007; arXiv:cs/0412025v3. minimum-dilation star problem and its principal bounds. ↗preprint · reference source · arXiv:cs/0412025, checked 2026-08-01 · checked 2026-07-24Source use: citation only.For Minimum spanning-tree dilation on the regular nonagon, this source supplies neighboring star constructions; it does not determine the regular-nonagon tree optimum.
Boris Aronov, Mark de Berg, Otfried Cheong, Joachim Gudmundsson, Herman Haverkort, Michiel Smid, and Antoine Vigneron, “Sparse geometric graphs with small dilation,” Computational Geometry 40(3) (2008), 207-219. DOI 10.1016/j.comgeo.2007.07.004; arXiv:cs/0702080v2. main sparse-geometric-graph dilation bounds. ↗preprint · reference source · arXiv:cs/0702080, checked 2026-08-01 · checked 2026-07-24Source use: citation only.For Minimum spanning-tree dilation on the regular nonagon, this source supplies general sparse-spanner bounds; it does not determine the regular-nonagon tree optimum.
Otfried Cheong, Herman Haverkort, and Mira Lee, “Computing a minimum-dilation spanning tree is NP-hard,” Computational Geometry 41(3) (2008), 188-205. DOI 10.1016/j.comgeo.2007.12.001; arXiv:cs/0703023v1. main NP-hardness theorem for minimum-dilation spanning trees. ↗preprint · reference source · arXiv:cs/0703023, checked 2026-08-01 · checked 2026-07-24Source use: citation only.For Minimum spanning-tree dilation on the regular nonagon, this source supplies computational-complexity context; it does not determine the fixed regular-nonagon instance.

Original finite geometric-spanner optimization.

Discussion

Loading discussion.

[#P2502] Minimum spanning-tree dilation on the regular nonagon

1Context

2Definitions

3What counts as a solution

1Status

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

1References

Discussion

Report comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Record & provenance

Flag this problem

Sign in to follow

Report a problem

1Context

2Definitions

3What counts as a solution

1StatusSolution submittedNot Lean-verified

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

1References

Add a comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance

1Status