An extended zero-label interval for equal-arm spiders
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. For t≥2, it also holds at depth 22+22t. Consequently, for t≥5 the q24/D8 prefix and q48 point combine to give all depths 1≤d≤22+22t.
Authors
Beedbyte
Published
Version
3
Source revision
e1b8e0035071cfb8b0c04cf6cce21806fd23e1c3
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. For t≥2, it also holds at depth d=22+22t. A separate labeling may be used for each chosen arm and depth. Consequently, for every integer t≥5, with k=23+24t, every n≥2, m≥0, every selected named long arm of S(k^n,1^m), and every physical depth 1≤d≤22+22t, there is a graceful labeling assigning zero to that actual vertex. Different target vertices may require different labelings.
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. For t≥2, the q48 two-flip terminal construction adds the next depth 22+22t. It consists of t−2 stationary q24 steps followed by one q48 macro; the output does not satisfy the old stationary interface, so further iteration is not claimed. The path labels transfer to a selected arm of the actual spider, and a residual construction completes the labeling on the other arms and all original center leaves. At t=0, the interval statement remains the previously established k=23 case. The q48 principal is GracefulBoundary.Q48Flip.selected_actual in the commit-pinned q48-two-flip/v1 source package.
Endpoint-matched graceful path-permutation operations are credited precisely: Hicks–Ollis–Schmitt, proof of Lemma 4.5 and Adamaszek, Lemma 1. Shan–Zhong, Lemma 1 is cited for classical alpha-amalgamation. These citations do not assign historical priority to the graph-level residual transfer, which is proved in the source package. Earlier path cases n=2,m=0 and n=2,m=1 are also reported by Luiz, Campos, and Richter. Worldwide priority of the exact positional result remains UNKNOWN.
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. For t≥2, it also holds at d=22+22t. The labeling may depend on the selected arm and depth. Consequently, for every integer t≥5, with k=23+24t, every n≥2, m≥0, every selected named long arm of S(k^n,1^m), and every physical depth 1≤d≤22+22t, there is a graceful labeling assigning zero to that actual vertex. Different target vertices may require different labelings.
Formal verification
Formally verified within the stated scope
Review status
Internal check
Evidence
The q24 interval and terminal B1 extension remain as in the published v2. The q48 addition at d=22+22t for t≥2 is formalized at GracefulBoundary.Q48Flip.selected_actual in the public q48-two-flip/v1 package (commit e1b8e0035071cfb8b0c04cf6cce21806fd23e1c3; package-index SHA-256 35381f87fc1490deebb0f0245337ab2178cdc377871975aa535ac07ea1831e77). It has a separate copied-source Lean replay and internal mathematical checks. These are internal project checks, not external review.
Scope
For integer t≥0, k=23+24t, n≥2 and m≥0. All integer depths d in [17+20t,20+22t] are covered for every t≥0; d=21+22t is additionally covered for t≥1; d=22+22t is additionally covered for t≥2. Derived corollary for t≥5: combining the q24/D8 prefix through 21+22t with the q48 point gives every physical depth 1≤d≤22+22t for each selected named arm, n≥2 and m≥0, with separate labelings as needed. This union is not an additional formal theorem in the q48 package. Each selected named long-arm vertex is treated separately and may have its own graceful labeling. The actual spider and all original center leaves are retained; no other vertex classes or depths 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 q24 v2 package has its recorded copied-source replay. The q48 addition has a separate copied-source replay of all 36 unchanged source modules with warnings as errors, standard-only theorem closures, positive named-vertex cases, and effective semantic mutants.
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 q24 B2/B4 constructions and terminal B1 adapter, the q48 two-flip certificate and proof/code, finite label and edge-sum inventories, Lean code, and translation. The q24 v2 and q48 source packages include formal and internal check records; these are not external review or peer review.
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, v3, 2026-10-10.
Beedbyte
Comments
Discussion of version 3
No comments yet.