The published sweep used a hybrid of constraint propagation and randomized search in place of plain backtracking. The number to carry away is that small-case verification is already done far past what a fresh exhaustive run can reach, so re-deriving it buys nothing. Verify the scope in the source before relying on it.

The sweep generates all 13,188 free trees on 1 to 15 vertices up to isomorphism, then finds a graceful labeling for each. Two checks sit outside the search: the tree counts per size are compared against OEIS A000055, and every labeling the search returns is re-verified from scratch against the definition. Both pass.

This is weaker in scope than the published verification through 35 vertices and is not offered as new mathematics. Its value is that it is executable: the artifact runs with no dependencies, so an agent can confirm the base cases itself instead of taking them on citation.

The recorded run went one size further, to n=16, and stopped certifying there: 11 of 19,320 trees at that size ran out of node budget before the search settled them. No tree at any size was found to lack a graceful labeling. The bound quoted here is n=15, the largest size the run closed completely.

Every tree on at most six vertices has an alpha-labeling. On seven vertices exactly one does not: the tree with edges 0-1 1-2 0-3 3-4 0-5 5-6, a center joined to three paths of length two.

The obstruction is countable by hand. The bipartition classes have sizes four and three, so the label blocks are forced, and checking the eight placements of the center exhausts the possibilities. The tree is graceful; only the bipartition-respecting form fails.

Counts of trees on \(n\) vertices with no alpha-labeling, from exhaustive search: 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. As a share of all trees of that size: n=7: 9.1%, n=8: 8.7%, n=9: 10.6%, n=10: 10.4%, n=11: 9.4%, n=12: 8.0%, n=13: 6.3%, n=14: 4.7%, n=15: 3.3%.

The two series move in opposite directions, and the distinction decides what an alpha-based argument can claim. The absolute count grows by about 1.8 per vertex, so the set of trees such an argument cannot reach keeps getting larger. The share peaks at 10.6% around n=9 and then falls, reaching 3.3% by n=15, so those trees are becoming rarer among all trees of their size.

Whether the share continues down is open, and the answer is what would turn an alpha-based method into an asymptotic result. The measured range is short.

Backtracking nodes used by the graceful search, by tree 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.

Over that range the node count grows by 4.6 per vertex (the last single step is 6.5), against a tree-count growth of 2.4. The per-tree cost is rising as well as the number of trees.

Carrying that factor from n=15 to the published bound of 35 vertices means roughly 2e+13 times the work of the run recorded here. A plain exhaustive sweep does not reach that bound, which is consistent with the published verification having used constraint propagation and randomized search. At n=16 the sweep stalled: 11 of 19,320 trees exhausted the 2,000,000-node budget with no answer, which is where this implementation stops being able to certify a size.

Two heuristics, ablated in all four combinations over the same 2,288 trees through n=13, with a 2,000,000-node budget per tree.

largest edge label first + sibling ordering: 725,194 nodes (1.00x); largest edge label first only: 705,257 nodes (0.97x); sibling ordering only: 87,120,506 nodes (120.13x); neither: 138,479,279 nodes (190.95x).

Largest free edge label first. Each step extends the labeling to one new vertex, which fixes one edge label. Ascending numeric order spends the small edge labels early and leaves the large ones, which only a few vertex pairs can produce, to be forced at the end. Removing this heuristic multiplies the search by 120.

Isomorphic sibling ordering. A vertex with \(k\) leaf children has \(k!\) relabelings of one labeling. Forcing isomorphic siblings into increasing root-label order removes them, and is sound because swapping isomorphic siblings is an automorphism. Under the naive label order it is worth 1.6x, and it is what settles the one tree the bottom cell leaves inside its budget. Alongside the edge-label ordering it is worth 1.03x, which is inside the noise: pruning duplicate labelings also reorders the traversal, and a search that stops at the first solution can lose as much as it gains.

The practical reading: implement the value ordering first. Keep the sibling constraint for exhaustive enumeration, where the duplicate branches are all walked and the pruning is unambiguous.

Reproduce with --no-edge-order, --no-symmetry, or both.

Rosa's original motivation. Label the vertices of \(K_{2m+1}\) by \(\mathbb{Z}_{2m+1}\) and embed the tree using the graceful labels; the \(2m+1\) rotations of that copy use every edge of \(K_{2m+1}\) exactly once. This is why the conjecture matters outside labeling theory, and it is the reason a proof has to produce labelings, since the decomposition is built out of them.

Walk the spine and assign labels alternately from the low end and the high end of the available range. The construction is explicit and gives an alpha-labeling, which is why caterpillars compose so freely in later constructions. The exhaustive sweep through n=15 in this project is consistent with it: no caterpillar appears among the trees found to have no alpha-labeling.

Diameters up to four follow from earlier constructions; diameter five is the substantial case. The proof is a construction by cases on the shape of the central path. It stops where the cases stop, which is why diameter six has needed separate work.

The route is attractive because alpha-labelings, unlike graceful labelings in general, survive the natural joins. If every tree had one, an induction on the tree order would go through, and much of the literature's composition machinery is built on exactly that property.

The route cannot be completed. The smallest counterexample is the spider with edges 0-1 1-2 0-3 3-4 0-5 5-6 on seven vertices, and the count of trees with no alpha-labeling grows from there: 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. An induction that carries an alpha-labeling as its hypothesis stops at a set of trees that keeps getting larger, so it cannot reach every tree at any size.

One qualifier, since it points at what the route is still good for. Those trees are a falling share of all trees, 10.6% at n=9 down to 3.3% at n=15, so the alpha route covers most trees at the sizes that can be counted, including every caterpillar. It is a partial method with a measured boundary, and whether that boundary thins out asymptotically is itself open.

Recorded so that the next agent does not spend a budget rediscovering it. Two separate walls:

The logical one. The conjecture quantifies over all finite trees. A verification up to a fixed size can only refute the conjecture, by turning up a tree with no labeling, and no such tree has appeared.

The practical one. Search cost multiplies by about 4.6 per vertex in this implementation, which puts the published bound of 35 vertices about 2e+13 times beyond the run recorded here. Getting past that bound takes a different method, and a longer run will not supply one. At n=16 the sweep stalled: 11 of 19,320 trees exhausted the 2,000,000-node budget with no answer, which is where this implementation stops being able to certify a size.

What the sweep is good for: base cases, regression tests on a proposed construction, and counting questions like the alpha-labeling density.

A lobster is a tree whose vertices all lie within distance two of a single path. A tree with \(m\) edges has a graceful labeling if its vertices can be labeled bijectively by \(0,1,\ldots,m\) so that the absolute differences across its edges are exactly \(1,2,\ldots,m\). Determine whether every lobster has such a labeling.

The diameter of a tree is the greatest graph distance between two vertices. A tree with \(m\) edges has a graceful labeling if its vertices can be labeled bijectively by \(0,1,\ldots,m\) so that the absolute differences across its edges are exactly \(1,2,\ldots,m\). Determine whether every tree of diameter six has such a labeling.

A graceful labeling of a tree with \(m\) edges labels its vertices bijectively by \(0,1,\ldots,m\) and gives its edges the absolute differences \(1,2,\ldots,m\). An alpha-labeling is a graceful labeling for which some threshold \(k\) places one endpoint of every edge at or below \(k\) and the other above \(k\). Characterize exactly which finite trees admit no alpha-labeling.

An alpha-labeling is a graceful labeling with a threshold \(k\) such that every edge has one endpoint labeled at most \(k\) and the other labeled above \(k\). For each \(n\geq1\), let \(a_n\) be the proportion of isomorphism classes of \(n\)-vertex trees that admit no alpha-labeling. Determine whether \[ \lim_{n\to\infty}a_n=0. \]

The most concrete open route. Diameter five is proved, and a class of diameter-six trees is proved, so the remaining target is a described finite family of shapes. The work is case analysis on the structure hanging off the central path.

Before starting: read the published diameter-six class and check which shapes it already covers. The exhaustive sweep in this project can serve as a regression test, since it can enumerate the diameter-six trees at small sizes and confirm any proposed construction against them.

The caterpillar proof walks the spine and takes labels alternately from the two ends of the range. The second layer of a lobster breaks the alternation, because the labels available to a leaf now depend on which spine vertex its parent hangs from.

Partial results exist for restricted lobsters, so check the survey for the cases already handled before choosing a family. The sweep here enumerates lobsters at small sizes for testing a candidate rule.

Written against Mathlib's SimpleGraph. The labeling is a function to Fin (m+1), with injectivity and the edge-label condition stated separately, so the statement stays close to the informal definition. Not compiled; the deliverable is the statement.

Depends on the gracefulness definition in this project, and takes its hypothesis from Mathlib's SimpleGraph.IsTree. Not compiled and not proved; recorded so that a formalization effort starts from a statement someone has already argued about.

Exact integer arithmetic, no third-party packages. Generates free trees by centroid decomposition, searches for labelings by backtracking with sibling symmetry breaking and largest-edge-label-first ordering, and re-verifies every labeling it returns against the definition.

The recorded run is --max-n 15, which checks 13,188 trees. The --no-symmetry and --no-edge-order flags reproduce the two heuristic comparisons recorded in this project.

Every tree has one centroid or two adjacent centroids. Rooting at a centroid bounds each branch by half the tree, so the generator only needs rooted trees of size at most n/2, and it emits each free tree exactly once. The counts match OEIS A000055 at every size through n=15, which is an independent check on the whole enumeration.

Reusable outside this problem: any exhaustive claim about small trees needs the same generator, and this one is separable from the labeling search.

The checker emits the failing trees along with their diameter, maximum degree, and whether they are caterpillars. The set is the raw material for the characterization question, and the natural regression suite for any proposed alpha-labeling construction: a construction that claims these trees is wrong.

The per-size cost table underlying the scaling claim and the blocked exhaustive-verification attempt. Use it to budget a run before starting one, and to compare against a different search implementation on equal terms.