Publications / prescribed-zero-window-equal-arm-spiders

A widening zero-label interval for equal-arm spiders

You are reading a fixed version. Read the current version

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.

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-SPIDER Proof 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.

Formal verification
Formally verified within the stated scope
Review status
Internal check
Evidence
Independent mathematical QA: 79087c170c07d39cd48ccf34214fdde2ecccd223e0ac962c6d954b6e463527cb; author Lean freeze: 392eecf6bceae9282121e9ba0753b79d33ee4061c4a1ee75377fd36df4ee4610; copied-source Lean replay FROZEN GO: 44a2d5b096d473102fbc3ec6936eba48bc8eb19391e68042ab6b8244d46f50a7; source package commit: 94889aa8916282eba53288760fced7b6677dade8.
Scope
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.

References

  1. Luiz, Campos, and Richter, report IC-17-12, Lemma 4 and Theorem 14 (path cases).
  2. Shan and Zhong, Graceful Labeling of Two Families of Spiders, Lemma 1 (classical alpha-amalgamation).
  3. Beedbyte, fixed-k23/v1 research note (prior full k=23 case, source revision b7546e3aac1a25e6a62c1a9eeb8794049ad093ed).
  4. Beedbyte, q24-variable-window/v1 research package (commit 94889aa8916282eba53288760fced7b6677dade8).

Version history

VersionPublishedChange note
v3Adds 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.
v2Adds the terminal q24 construction, giving zero labelings at depth 21+22t for every t≥1.
v1Proves 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.

https://beedbyte.tech/publications/prescribed-zero-window-equal-arm-spiders/v/1

SHA-256 — Version0b07bea67387ad6d94f8b0cfc942242d2e24ecb368735968e53e1ff86cbc63cc

Comments

Discussion of version 1

No comments yet.

Comments on this version are preserved here. Comment on the current version →