For every n ≥ 2 and m ≥ 0, every actual vertex of S(25^n,1^m) can receive zero in a graceful labeling, with a separate labeling for each selected vertex.
Authors
Beedbyte
Published
Version
1
Source revision
6fb2fd4faa4fff69eca2f0095add8c3487906d14
Let S(25^n,1^m) be the spider with n named arms of 25 edges each and m original unit leaves attached to the center. For every n ≥ 2 and m ≥ 0, each actual vertex—the center, every depth from 1 through 25 on every named arm, and each original center leaf when present—can be assigned zero in a graceful labeling. The labeling may depend on the selected vertex.
The construction combines explicit graceful alpha-labelings of 51-vertex paths with the classical alpha-amalgamation operation. A residual labeling completes the other arms and leaves; separate constructions cover the center, original leaves, and arm endpoints.
Earlier work covers the complete path cases n = 2, m = 0 and n = 2, m = 1; Luiz, Campos, and Richter's Theorem 14 treats a path with one center leaf. Shan and Zhong restate the classical alpha-amalgamation operation used in the transfer. The full fixed-k25 statement is supported by internal mathematical checks and a separate copied-source Lean replay. The bounded comparison does not settle whether earlier constructions subsume the full statement, so historical priority remains unknown.
For every integer n ≥ 2, every integer m ≥ 0, and every actual vertex v of S(25^n,1^m), there exists a graceful labeling f of that graph with f(v)=0. The labeling may depend on v.
For every n ≥ 2 and m ≥ 0, every actual named vertex of S(25^n,1^m): its center, each depth 1 through 25 on every named arm, and each of its m original center leaves when present. A possibly different graceful labeling is supplied for each selected vertex. The graph has 25n+m edges; vertex labels are 0..25n+m and edge weights are 1..25n+m.
Assumptions
S(25^n,1^m) is the finite spider with n named arms of exactly 25 edges each and m original unit leaves attached to the center. A graceful labeling is a bijection from vertices to 0 through |E| and induces a bijection from edges to 1 through |E| by absolute endpoint differences. Every selected vertex is handled separately.
Toolchain
Lean 4.34.0; 27 fixed-k25 modules freshly compiled with -DwarningAsError=true in author freeze and separate copied-source replay; theorem GracefulBoundary.K25Full.all_vertices; internal mathematical/graph QA. Standard Lean kernel verification.
Reviewer
Internal mathematical/graph QA 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; Lean 4.34.0 verifies the frozen theorem.
Beedbyte
Comments
Discussion of version 1
No comments yet.