Zero-rotatability for spiders with equal even-length arms
For every even k ≥ 2, n ≥ 2, and m ≥ 0, each named vertex of S(k^n,1^m) can receive zero in a graceful labeling, with a separate labeling for each chosen vertex.
Authors
Beedbyte
Published
Version
1
Source revision
4914435310380581d4d781cc1640465f27651100
This work proves zero-rotatability for the named spider S(k^n,1^m) whenever the long arms have the same even length k ≥ 2, there are n ≥ 2 long arms, and the center has m ≥ 0 unit leaves. The center, every named position on every long arm, and each existing center leaf can each be assigned zero in a graceful labeling.
Zero-rotatability asks whether the zero label can be placed at any selected vertex while preserving all graceful-labeling conditions. The proof handles lengths two and four directly, then treats the remaining even lengths through balanced midpoint paths, explicit finite certificates, and recursively extended shell constructions. The constructions cover every allowed number of center leaves.
Earlier work supplies relevant overlap and construction tools. Rofa proves zero-rotatability for symmetric spiders with leg length at most three and gives boundary-level results for broader rooted symmetric trees; Luiz, Campos, and Richter cover paths and paths with a central pendant. The four-edge-arm construction uses Krop's generalized subdivision operation and the Huang–Kotzig–Rosa zero/index identification as restated by Shan–Zhong. Hicks–Ollis–Schmitt's three-twizzler graceful permutations supply the length-six path words and graceful-permutation concatenations. Ollis's Lemma 5.5 gives bipartite graceful permutations with endpoint freedom, credited there to Kotzig, and Theorem 5.6 supplies an insertion construction. The complete length-four and length-six cases combine published constructions.
Statements & evidence
GE2-ALL-EVEN-ZERO-ROTATABILITYProof provided
For every even integer k ≥ 2, every integer n ≥ 2, every integer m ≥ 0, and every actual vertex v of S(k^n,1^m), there exists a graceful labeling assigning zero to v. The labeling may depend on the selected vertex.
Formal verification
Formally verified within the stated scope
Review status
Internal check
Evidence
Formal theorem GracefulBoundary.Integration2Closed.all_even_ge_2_actual is tied to frozen manuscript -d and the complete clean 186-module Lean source-package check. Manuscript: research-manuscripts/graceful-even-spiders-ge2-2026-10-10-d/manuscript.tex, SHA-256 916679d81fe8a4db7888cf6b4f0ff5a8e31af1660f319f8a4314d0e1ccb30790. Source-package QA report: research-audits/graceful-even-ge2-source-independent-qa-2026-10-10-a/report.md, SHA-256 a12575d294fec81ce6fd538d6cf27442a30a2070d0a6a33afd2a854f75b11bec. Independent manuscript QA report for the byte-identical mathematical body in frozen -c: research-audits/graceful-ge2-manuscript-independent-qa-2026-10-10-a/report.md, SHA-256 7d2c82011f1c0c7dfe88e08c0f485724a7c18e5eba4384a7ef062d4dd48527a9. The -d author report records unchanged mathematical-body bytes and its static checks; its SHA-256 is 65c05654f43427cf98530e567dd5667e69ddeeaa616ce8dc9c1a371b16d03f83.
Scope
For every even integer k ≥ 2, n ≥ 2, m ≥ 0, and each actual named vertex of S(k^n,1^m), with a separate graceful labeling for each selected vertex.
Assumptions
S(k^n,1^m) is the finite spider with n equal arms of k edges and m unit leaves at its center; graceful labelings use the standard bijection of vertices to 0 through |E| and edge differences to 1 through |E|. Each selected vertex is considered separately.
Toolchain
Lean 4.34.0; clean copied build of all 186 source modules with -DwarningAsError=true; theorem GracefulBoundary.Integration2Closed.all_even_ge_2_actual; source-package report SHA-256 a12575d294fec81ce6fd538d6cf27442a30a2070d0a6a33afd2a854f75b11bec. The package-wide declaration query allows only propext, Classical.choice, and Quot.sound. This is internal formal verification, not external review.
Reviewer
Internal project QA only; no external reviewer or peer review is recorded.
Files & reproduction
No files attached.
Contributions & AI assistance
Contributions
Jordi Gartner publishes this work through Beedbyte.
AI assistance
Methods: AI tools assisted with construction and proof development, coding, checking the explicit labeling certificates, and inspecting the cited sources.
Proves zero-rotatability for every named vertex of S(k^n,1^m) when k ≥ 2 is even, n ≥ 2, and m ≥ 0, using a separate graceful labeling for each selected vertex.
Cite this version
Beedbyte. Zero-rotatability for spiders with equal even-length arms. Beedbyte, v1, 2026-10-10.
Beedbyte
Comments
Discussion of version 1
No comments yet.