# P2502: Minimum spanning-tree dilation on the regular nonagon

- ID: `P2502`
- Reference: `regular-nonagon-tree-dilation`
- Page: https://theoremdb.org/statements/P2502
- Record maturity: Reviewed problem with recorded work

## 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?

### Remarks

- **Remark.** Every tree edge is weighted by its Euclidean chord length.
- **Remark.** Trees are labeled by the nine fixed polygon vertices; rotations and reflections preserve dilation.

### What 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.

## The answer

Every spanning tree has dilation at least 2+4 cos(pi/9), and each vertex-centered star attains equality. [4](#reference-4)

**Review status:** Reproduced.

**Lean verification:** not Lean-verified.

### 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.

## Work

### Proof and evidence for the resolution

**Computation 1 (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.

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.

### Background and intake notes

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\).

- Original intake status: Status not established. No literature search was performed. Dilation of geometric spanning trees is an established subject.
- 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.

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

### Prior approaches

- **Route 1** (supported): The closest papers study minimum-dilation trees, star centers, and asymptotic bounds for equally spaced circle points. [4](#reference-4) [2](#reference-2) [3](#reference-3) [1](#reference-1)

### Runnable artifacts

- **Artifact 1** (reproduced): Integer algebraic comparisons certify the lower bound for all 4,782,969 labeled trees and identify 7,515 minimizers.

### 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.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `regular-nonagon-tree-dilation`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## Lean verification

An informal proof is recorded. A Lean formalization still needs to be attached.

[Prepare and check a Lean proof with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20regular-nonagon-tree-dilation%0A%0AExact%20title%3A%20Minimum%20spanning-tree%20dilation%20on%20the%20regular%20nonagon%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Fregular-nonagon-tree-dilation%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.).

## References

1. <a id="reference-1"></a>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 https://arxiv.org/abs/cs/0412025
   - preprint; reference source; arXiv:cs/0412025, checked 2026-08-01; checked 2026-07-24
   - Source 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.
2. <a id="reference-2"></a>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 https://arxiv.org/abs/cs/0702080
   - preprint; reference source; arXiv:cs/0702080, checked 2026-08-01; checked 2026-07-24
   - Source 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.
3. <a id="reference-3"></a>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 https://arxiv.org/abs/cs/0703023
   - preprint; reference source; arXiv:cs/0703023, checked 2026-08-01; checked 2026-07-24
   - Source 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.
4. <a id="reference-4"></a>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. 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 https://doi.org/10.4230/LIPIcs.SoCG.2025.26
   - Also cited at Independent exact certificate nonagon-tree-artifact-complete-pruefer-search, executed on 2026-07-24
   - scholarly_publication; reference source; checked 2026-08-01
   - Source use: citation_only
   - 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.