For k=23+24t, n≥2 and m≥0, every selected named long-arm vertex at depth 17+20t through 20+22t can be zero in its own graceful labeling for every integer t≥0. For t≥1, the same holds at the additional depth 21+22t.
Authors
Beedbyte
Published
Version
2
Source revision
9f92eeefaf8cc57a7d04446b20e66bd169848e3b
For every integer t≥0, let k=23+24t. For all n≥2 and m≥0, each selected named long-arm vertex of S(k^n,1^m) at a depth d with 17+20t≤d≤20+22t can be assigned zero in a graceful labeling. When t≥1, this also holds at depth d=21+22t. A separate labeling may be used for each chosen arm and depth.
The q24 B2 and B4 constructions give the existing interval. A terminal B1 adapter reverses a neighboring zero pair while preserving the midpoint alpha condition, adding the adjacent depth 21+22t for t≥1. The path labels transfer to the selected arm of the actual spider, and a residual construction completes the labeling on the other arms and the original center leaves. At t=0, the statement remains the previously established k=23 case.
Endpoint-matched alpha-path concatenation is established machinery: Hicks–Ollis–Schmitt use it in the proof of Lemma 4.5, and Adamaszek gives the reversed gluing in Lemma 1. Earlier path cases also cover n=2,m=0 and n=2,m=1, as reported by Luiz, Campos, and Richter.
Statements & evidence
Q24-VARIABLE-WINDOW-ACTUAL-SPIDERProof provided
For every integer t≥0, k=23+24t, n≥2 and m≥0, every selected named long-arm vertex of the actual spider S(k^n,1^m) at any integer depth d with 17+20t≤d≤20+22t has a graceful labeling assigning zero to that vertex. For t≥1, the same holds at d=21+22t. The labeling may depend on the selected arm and depth.
Formal verification
Formally verified within the stated scope
Review status
Internal check
Evidence
The terminal adapter extends the q24 interval by the additional depth 21+22t for every t≥1. The frozen author formalization and a separate copied-source replay were checked with Lean 4.34.0; the versioned source package will contain the theorem and reproducibility records.
Scope
For integer t≥0, k=23+24t, n≥2 and m≥0. The prior depths are all integers in [17+20t,20+22t]; for t≥1 the added depth is 21+22t. Each selected named long-arm vertex is treated separately and may have its own graceful labeling. No other depths or vertex classes are asserted.
Assumptions
S(k^n,1^m) is the finite spider with n named arms of k edges and m original unit leaves at the center. Graceful means a bijection from vertices to 0..|E| whose edge absolute differences biject to 1..|E|.
Toolchain
Lean 4.34.0; the terminal author source and separate copied-source replay each compiled 34 modules. Standard Lean kernel verification.
Reviewer
Formal and literature checks are internal project checks only; no external or peer review is claimed. Worldwide priority of the exact positional result remains unknown.
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 B2/B4 constructions and terminal adapter, checking finite label and edge-sum inventories, and building the Lean formalization. The theorem and a separate copied source were checked with Lean 4.34.0.
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. An extended zero-label interval for equal-arm spiders. Beedbyte, v2, 2026-10-10.
Beedbyte
Comments
Discussion of version 2
No comments yet.
Comments on this version are preserved here. Comment on the current version →