For every n ≥ 2 and m ≥ 0, each actual vertex of S(47^n,1^m) can be the unique zero in a graceful labeling; a separate labeling may be used for each target.
Authors
Beedbyte
Published
Version
1
Source revision
28e8174b8b1ab5a82261c4160f3674b9120f7484
Let S(47^n,1^m) be the spider with n named arms of 47 edges each and m original unit leaves at the center. For every n ≥ 2, m ≥ 0, and every actual vertex v, there is a graceful labeling f with f(v)=0 and f(w)=0 exactly when w=v. This covers the center, every depth 1 through 47 on every named arm, and each original leaf when present. The labeling may depend on v. The result concerns the fixed arm length 47; it is not a theorem for all odd arm lengths.
The proof combines 95-vertex graceful path labelings with a prescribed midpoint and a zero or maximum at a specified distance, the classical alpha-amalgamation operation described by Shan and Zhong with a residual spider labeling, and separate constructions for the center, original leaves, and arm tips. A Lean 4.34.0 formalization and a separate copied-source replay check the theorem; these are internal project checks.
Earlier work covers the complete path case S(47^2,1^0)=P95 and the case with one center leaf, S(47^2,1^1), including every vertex. Bahls, Lake, and Wertheim give ordinary graceful labelings for equal-arm spiders with no center leaves, using a hub-zero construction for odd numbers of arms. These results are relevant overlaps but do not by themselves state the full all-n,m all-vertex theorem here. Historical priority remains unknown.
For every n ≥ 2, m ≥ 0, and every actual vertex v of S(47^n,1^m), there exists a graceful labeling f with f(v)=0 and, for every vertex w, f(w)=0 if and only if w=v.
For all n≥2,m≥0, every actual named vertex of S(47^n,1^m), including center, every depth 1..47 on each named arm and all original center leaves when present; the selected vertex is the unique zero in a possibly target-specific graceful labeling. The graph has 47n+m edges and the standard graceful label and weight ranges.
Assumptions
S(47^n,1^m) is the finite spider with n named arms of exactly 47 edges and m original unit leaves attached to the center. Graceful means a bijection of vertices to 0..|E| whose absolute edge differences biject to 1..|E|. The labeling can depend on the selected target vertex and has no other zero.
Toolchain
Lean 4.34.0; 42 modules freshly compiled with -DwarningAsError=true in author freeze and separate copied-source replay; principal theorem GracefulBoundary.K47Full.all_vertices_unique_zero; internal mathematical composition check. Standard Lean kernel verification.
Reviewer
Internal mathematical composition audit and separate copied-source Lean replay only; no external or peer review is claimed.
Files & reproduction
No files attached.
Contributions & AI assistance
Contributions
Jordi Gartner publishes this work through Beedbyte.
AI assistance
Methods: AI tools assisted with developing the construction, formalizing and checking the proof, and comparing earlier sources; the Lean 4.34.0 formalization verifies the stated theorem.
Beedbyte
Comments
Discussion of version 1
No comments yet.
Comments on this version are preserved here. Comment on the current version →