For every n ≥ 2 and m ≥ 0, each actual vertex of S(23^n,1^m) can be assigned zero in a graceful labeling, with a separate labeling for each selected vertex.
Authors
Beedbyte
Published
Version
1
Source revision
b7546e3aac1a25e6a62c1a9eeb8794049ad093ed
This result proves zero-rotatability for S(23^n,1^m) for every n ≥ 2 and m ≥ 0. The center, every vertex at depths 1 through 23 on each of the n named arms, and every original center leaf when m > 0 can each receive label zero in a graceful labeling. The labeling may differ with the selected vertex; when m = 0, there are no center leaves.
Zero-rotatability asks whether a graceful labeling can place zero at any chosen vertex while retaining the required distinct vertex labels and edge differences. The construction combines explicit midpoint alpha-path certificates with the classical alpha-amalgamation transfer and an odd residual construction, covering every arm name, depth, center, and existing leaf.
Earlier work gives the complete path cases n = 2, m = 0 and n = 2, m = 1: the first is the path result of Rosa as restated by Luiz, Campos, and Richter; their Theorem 14 treats the path with one center leaf. Classical alpha-amalgamation supplies a construction tool used here. These results provide relevant prior cases and ingredients for the stated theorem.
For every integer n ≥ 2, every integer m ≥ 0, and every actual vertex v of S(23^n,1^m), there exists a graceful labeling f of that graph with f(v)=0. The labeling may depend on v.
Formal verification
Formally verified within the stated scope
Review status
Internal check
Evidence
The root-reviewed public fixed-k23 source package at commit b7546e3aac1a25e6a62c1a9eeb8794049ad093ed contains theorem GracefulBoundary.K23Full.all_vertices in source/K23Full.lean; the package README records the Lean 4.34.0 build and copied-source replay.
Scope
For every n ≥ 2 and m ≥ 0, every actual named vertex of the finite spider S(23^n,1^m): its center, each arm (Fin n) at each of the 23 depths, and each of its m original center leaves when present. For each selected vertex v, a possibly different graceful labeling f exists with f(v)=0. The graph has 23n+m edges; graceful vertex labels are 0..23n+m and edge weights are 1..23n+m.
Assumptions
S(23^n,1^m) is the finite spider with n arms of exactly 23 edges each and m original unit leaves attached to the center. A graceful labeling is a bijection from vertices to 0 through |E| and induces a bijection from edges to 1 through |E| by absolute endpoint differences. Every selected vertex is handled separately.
Toolchain
Lean 4.34.0; all 27 frozen package modules freshly compiled in order with -DwarningAsError=true; theorem GracefulBoundary.K23Full.all_vertices; copied-source replay compiled 27 fresh modules and audited 1,649 package-owned theorem closures against standard Lean axioms only. Internal formal project checks.
Reviewer
Internal project checks 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.
Beedbyte
Comments
Discussion of version 1
No comments yet.
Comments on this version are preserved here. Comment on the current version →