For every n ≥ 2 and m ≥ 0, each actual vertex of S(71^n,1^m) can be the unique zero in a graceful labeling; a separate labeling may be used for each target.
Authors
Beedbyte
Published
Version
1
Source revision
f085233be2db924ab96fc82579a231c8e45b6992
Let S(71^n,1^m) be the spider with n named arms of 71 edges each and m original unit leaves attached to the center. For every n ≥ 2, m ≥ 0, and every actual vertex v, there is a graceful labeling f with f(v)=0 and f(w)=0 exactly when w=v. This covers the center, every depth 1 through 71 on each named arm, and every original leaf when present. The labeling may depend on v; the result is for the fixed arm length 71.
The construction combines explicit 143-vertex path labelings with a prescribed midpoint and a zero or maximum at the needed distance, a residual spider labeling joined at the hub, and separate constructions for the hub, original leaves, and arm tips. The theorem has a Lean 4.34.0 proof.
Luiz, Campos, and Richter’s path results cover the complete cases n=2 with m=0 and m=1. For m=0, Rofa also covers the hub and depths 1, 70, and 71. Earlier work supplies ordinary graceful labelings and alpha-amalgamation tools used in the construction. These prior results and methods are acknowledged; worldwide priority for the complete fixed-k71 statement remains unknown. This is not an all-odd-length theorem.
For every n ≥ 2, m ≥ 0, and every actual vertex v of S(71^n,1^m), there exists a graceful labeling f with f(v)=0 and, for every vertex w, f(w)=0 if and only if w=v.
Formal verification
Formally verified within the stated scope
Review status
Internal check
Evidence
Lean 4.34.0 proof, separately replayed from copied source; mathematical and literature checks are internal project evidence.
Scope
For all n≥2,m≥0, every actual named vertex of S(71^n,1^m), including the hub, every depth 1..71 on each named arm, and each original center leaf when present; the selected vertex is the unique zero in a possibly target-specific graceful labeling. The graph has 71n+m edges and the standard graceful label and weight ranges.
Assumptions
S(71^n,1^m) is the finite spider with n named arms of exactly 71 edges and m original unit leaves attached to the hub. Graceful means a bijection of vertices to 0..|E| whose absolute edge differences biject to 1..|E|. The labeling can depend on the selected target vertex and has no other zero.
Toolchain
Lean 4.34.0; separate copied-source replay checked 45 modules, 2,048 theorem closures, and 503 named target instances. Standard Lean kernel verification; the principal theorem uses only propext, Classical.choice, and Quot.sound.
Reviewer
Internal mathematical and copied-source Lean checks only; no external or peer review.
Files & reproduction
No files attached.
Contributions & AI assistance
Contributions
Jordi Gartner publishes this work through Beedbyte.
AI assistance
Methods: AI tools assisted with construction development, Lean formalization and checking, and comparison of earlier sources.
Beedbyte
Comments
Discussion of version 1
No comments yet.