# P101162: Gracefulness of diameter-six trees

- ID: `P101162`
- Reference: `gtc-problem-diameter-six`
- Page: https://theoremdb.org/statements/P101162
- Record maturity: Retired source record

## Problem

Determine whether every tree of diameter six has a graceful labeling.

## Status

The mathematical status has not passed editorial review.

## Work

### Other known results

- **Computation 1** (reproduced): All 13,188 trees on at most 15 vertices are graceful, by exact search, with every labeling checked independently of the search that found it.
- **Computation 2** (reproduced): The spider with three legs of length two admits a graceful labeling but no alpha-labeling, and it is the smallest tree that does not.
- **Computation 3** (reproduced): Counted exhaustively: n=7: 1, n=8: 2, n=9: 5, n=10: 11, n=11: 22, n=12: 44, n=13: 82, n=14: 147, n=15: 254. The count grows by about 1.8 per vertex, while the share of all trees peaks at 10.6% at n=9 and falls to 3.3% at n=15.
- **Computation 4** (reproduced): Search nodes per size: n=10: 8,264, n=11: 28,462, n=12: 97,710, n=13: 587,455, n=14: 2,503,495, n=15: 16,305,531. Cost grows by a factor of 4.6 per vertex while the tree count grows by 2.4.
- **Computation 5** (reproduced): A two-by-two ablation through n=13. Taking the largest free edge label first costs 120 times more search when removed. Sibling ordering pays only when that heuristic is absent.
- **Proposition 1** (supported): A graceful labeling of a tree with \(m\) edges gives a cyclic decomposition of \(K_{2m+1}\) into \(2m+1\) copies of that tree. [2](#reference-2)
- **Proposition 2** (supported): Rosa's zig-zag labeling gives a graceful labeling, in fact an alpha-labeling, for every caterpillar. [2](#reference-2)
- **Proposition 3** (supported): The diameter ladder is settled through five, by Hrncar and Haviar for the diameter-five case. [2](#reference-2)
- **Proposition 4** (supported): Published computation verifies that every tree with at most 35 vertices is graceful; the conjecture for trees with at least 36 vertices remains open. [1](#reference-1)

### Prior approaches

- **Route 1** (incomplete method): Alpha-labelings compose, so an induction that keeps one would close the conjecture. It cannot: alpha-labelings fail to exist from seven vertices up, and the count of exceptions keeps growing.
- **Route 2** (blocked): A finite sweep cannot settle a statement about all trees, and the cost data shows this implementation cannot even reach the published bound.

### Open directions

- **Question 1** (supported): Determine whether every lobster has a graceful labeling. [2](#reference-2)
- **Question 2** (supported): Characterize exactly which finite trees admit no alpha-labeling. [2](#reference-2)
- **Question 3** (reproduced): Let \(a_n\) be the proportion of unlabeled \(n\)-vertex trees with no alpha-labeling. Determine whether \(a_n\to0\).
- **Route 3** (conjectured): Settle the diameter-six families that Superdock's construction leaves open, using the diameter-five proof as the base case. [3](#reference-3)
- **Route 4** (conjectured): Adapt the zig-zag spine labeling to trees whose vertices lie within distance two of a path. [2](#reference-2)

### Formalizations

- **Formalization 1** (reported): A proposed Lean definition of gracefulness for a finite simple graph, specialized to trees by the edge count. [3](#reference-3)
- **Formalization 2** (reported): The conjecture as a Lean proposition over finite trees, using the drafted gracefulness predicate. [3](#reference-3)

### Runnable artifacts

- **Artifact 1** (reproduced): A dependency-free Python program that enumerates all trees up to a given size and searches for graceful and alpha-labelings, with both search heuristics switchable for comparison.
- **Artifact 2** (reproduced): Centroid decomposition enumerates every tree on n vertices exactly once, matching the known counts through n=15.
- **Artifact 3** (reproduced): Edge lists and counts for every tree through n=15 that admits no alpha-labeling, with diameter and caterpillar flags.
- **Artifact 4** (reproduced): Trees, backtracking nodes, and wall-clock seconds per size for the recorded sweep.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `gtc-problem-diameter-six`, 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

2 declarations, with 1 open proof obligation.

### graceful_tree_conjecture

- State: 1 open proof obligation
- Role: target declaration
- Depends on: `IsGraceful`

```lean
theorem graceful_tree_conjecture {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (h : G.IsTree) :
    ∃ l : V → ℕ, IsGraceful G l := by
  sorry
```

### IsGraceful

- State: source contains no sorry; verification pending
- Role: dependency depth 1

```lean
def IsGraceful {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (l : V → ℕ) : Prop :=
  Function.Injective l ∧
  (∀ v, l v ≤ G.edgeFinset.card) ∧
  (G.edgeFinset.image (fun e => Sym2.lift ⟨fun a b => max (l a) (l b) - min (l a) (l b), by intros; simp [max_comm, min_comm]⟩ e))
    = Finset.Icc 1 G.edgeFinset.card
```

## References

Reference review is pending for 1 entry. Each affected row names the fields still awaiting review.

1. <a id="reference-1"></a>Wenjie Fang, “A Computational Approach to the Graceful Tree Conjecture”. arXiv:1003.3045 (2010). Fang, arXiv:1003.3045, abstract https://arxiv.org/abs/1003.3045
   - preprint; primary source; arXiv:1003.3045v2; checked 2026-08-01
   - Source use: original_summary
   - For Graceful tree conjecture: Published computation verifies that every tree with at most 35 vertices is graceful; the conjecture for trees with at least 36 vertices remains open.
2. <a id="reference-2"></a>Joseph A. Gallian, “A Dynamic Survey of Graph Labeling,” Electronic Journal of Combinatorics, Dynamic Survey DS6, checked 2026-08-01. Gallian, Dynamic Survey of Graph Labeling, Hrncar and Haviar 2001 https://www.combinatorics.org/ojs/index.php/eljc/article/view/DS6
   - Also cited at Gallian, Dynamic Survey of Graph Labeling, introduction
   - Also cited at Gallian, Dynamic Survey of Graph Labeling, Rosa 1967
   - Also cited at Gallian, Dynamic Survey of Graph Labeling, trees section
   - Also cited at Gallian, Dynamic Survey of Graph Labeling, alpha-labelings
   - Also cited at Gallian, Dynamic Survey of Graph Labeling, lobsters
   - journal_article; secondary source; checked 2026-08-01
   - Source use: original_summary
   - For Graceful tree conjecture: The diameter ladder is settled through five, by Hrncar and Haviar for the diameter-five case.
3. <a id="reference-3"></a>Superdock, arXiv:1403.1564 https://arxiv.org/abs/1403.1564
   - Also cited at draft for this project
   - preprint; reference source; checked 2026-07-24
   - Reference review pending: publication-style citation, source version.
   - Source use: citation_only
   - Source named by the research packet.