For every n≥2 and m≥0, each vertex of S(95^n,1^m)—the hub, any of its m original leaves, or any position on any named 95-edge arm—can be assigned zero in its own graceful labeling.
Authors
Beedbyte
Research status
Completed
Published
Version
1
Source revision
a6cd0889a354a50b9ecc80bbd3162972639d63e3
For every n≥2 and m≥0, each vertex of S(95^n,1^m)—the hub, any of the m original leaves, or any position from 1 through 95 on any of the n named arms—has a graceful labeling that assigns zero to it. The labeling may depend on the selected vertex.
The proof combines depth-specific graceful path sources with a transfer to the named spider. Boundary and D8 sources cover depths 1 and 2–73; an older compatible p37 core with q9 transfers covers 74–77; the q24 variable-window construction covers 77–86; six explicit midpoint-alpha P191 certificates cover 87–92; and an H1 source covers 93–94, with boundary constructions also covering 94–95. The overlaps are intentional. Earlier path results cover the complete two-arm cases n=2,m=0 and n=2,m=1. Huang–Kotzig–Rosa alpha amalgamation and the endpoint-matched path concatenations of Hicks–Ollis–Schmitt and Adamaszek are prior operations, credited here as such.
For every n≥2 and m≥0, for every actual vertex v of S(95^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
Lean 4.34.0 author proof, independent copied-source replay, and separate aggregate mathematical QA passed; evidence is internal to the project.
Scope
For every n≥2 and m≥0, every actual named vertex of S(95^n,1^m): the hub, each depth 1..95 on every named 95-edge arm, and each original center leaf when present. The selected vertex receives zero in a target-dependent graceful labeling. The graph has 95n+m edges.
Assumptions
S(95^n,1^m) has n named arms of exactly 95 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 may depend on the selected vertex.
Toolchain
Lean 4.34.0; author build and separate copied-source replay passed.
Reviewer
Internal project checks.
Files & reproduction
No files attached.
Contributions & AI assistance
Contributions
Jordi Gartner publishes this work through Beedbyte.
AI assistance
AI tools assisted with finding finite P191 certificates, checking path inventories and the coverage ledger, and developing the Lean formalization. The author Lean 4.34.0 proof, separate aggregate mathematical audit, and copied-source replay passed. All three checks are internal to the project.
Beedbyte
Comments
Discussion of version 1
No comments yet.