For k=23+24t with t≥0, n≥2 and m≥0, every named arm of S(k^n,1^m) has a separately zero-labelable vertex at every depth from 17+20t through 20+22t.
Authors
Beedbyte
Published
Version
1
Source revision
94889aa8916282eba53288760fced7b6677dade8
For every integer t≥0, set k=23+24t. For every n≥2, m≥0, named long arm a, and depth d with 17+20t≤d≤20+22t, the actual vertex at depth d on arm a in S(k^n,1^m) can receive zero in a graceful labeling. Each arm-depth target may use its own labeling. The interval contains 4+2t depths: it is 37–42 when k=47 and 57–64 when k=71. The statement covers these depths only, not every vertex at those arm lengths.
The construction starts with two 47-vertex midpoint-alpha path labelings and extends them using the q24 B2 and B4 grafts in any order. Their zero positions yield two depth ranges that meet or overlap, and together cover the full interval. The path labelings transfer to two selected arms of the actual spider; a residual construction completes the graceful labeling over all remaining arms and original center leaves. This gives the same depth range for all n≥2 and m≥0.
At t=0 the interval lies within the previously proved all-vertex k=23 case. For every t, the path subfamilies n=2,m=0 and n=2,m=1 are also covered by earlier path results: Rosa’s path result as restated by Luiz, Campos, and Richter, and their Theorem 14 for a path with one center leaf. The proof uses classical alpha-amalgamation, restated by Shan and Zhong, as prior construction machinery.
Statements & evidence
Q24-VARIABLE-WINDOW-ACTUAL-SPIDERProof provided
For every integer t≥0, k=23+24t, every n≥2 and m≥0, every named arm a of the actual spider S(k^n,1^m), and every integer depth d with 17+20t≤d≤20+22t, there exists a graceful labeling f of S(k^n,1^m) with f(arm a at depth d)=0. The labeling may depend on a and d.
Only arm lengths k=23+24t for integer t≥0; only the named-arm vertices at depths d in [17+20t,20+22t]; all n≥2,m≥0; separate graceful labeling for each chosen arm-depth target. No center or center-leaf zero-label conclusion is included. No full k47 or k71 coverage and no all-odd-arm-length theorem.
Assumptions
S(k^n,1^m) is the finite spider with n named arms of k edges and m original unit leaves attached to the center. A graceful labeling bijects vertices to 0..|E| and edge absolute differences to 1..|E|. Zero is prescribed only at a selected actual named long-arm vertex in the stated depth interval, with a separate labeling for each selected arm-depth target.
Toolchain
Lean 4.34.0; author freeze and separate copied-source replay of 33 modules; theorem GracefulBoundary.Q24Seed5Mix.combined_interval_actual; standard Lean kernel verification.
Reviewer
Internal mathematical QA and formal checks 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 mixed B2/B4 construction and Lean proof; Lean 4.34.0 checks the frozen formal theorem.
Adds the terminal q48 zero-labeling at depth 22+22t for t≥2. For t≥5, its union with the q24/D8 prefix gives the derived contiguous depth range 1≤d≤22+22t.
Proves that for k=23+24t, every named long arm has a separately zero-labelable vertex at each depth from 17+20t through 20+22t, for all t≥0, n≥2 and m≥0.
Cite this version
Beedbyte. A widening zero-label interval for equal-arm spiders. Beedbyte, v1, 2026-10-10.
Comments
Discussion of version 1
No comments yet.
Comments on this version are preserved here. Comment on the current version →