Given a finite graph with a supplied graceful labeling that assigns zero to a chosen root, attach two new 119-edge arms there. Every interior depth 1–118 on either arm can receive zero in its own labeling. The source also proves eight specified near-tip depths for K=30·4^r−1, r≥1.
Authors
Beedbyte
Published
Version
1
Source revision
2861f5ff90990462308728d0958dab2ee1e8b103
Let H be any finite graph with Q edges, a specified root o, and a supplied conventional graceful labeling g. Its vertex labels are distinct values in 0,…,Q, its edge absolute differences are exactly 1,…,Q, and g(o)=0. Retain every vertex and edge of H and attach two separately named 119-edge arms at o, identifying o with index 119 of a 238-edge path. For each depth d=1,…,118 on either new arm, the entire graft has a conventional graceful labeling assigning zero to that selected vertex. Each target has its own labeling; the vertex labels lie in 0,…,Q+238 and the edge differences are exactly 1,…,Q+238.
The supplied root-zero labeling is a premise. H need not be connected, acyclic, a tree, alpha-labeled or onto-labeled; Q=0 is allowed. The theorem does not prescribe zero at the shared root, either new tip at depth 119, or old vertices of H, and does not give one labeling with several zero targets.
The source also proves a separate near-tip family. For every integer r≥1, set K=30·4^r−1. With the same supplied root-zero H premise, each depth K−8,…,K−1 on either newly attached K-edge arm has its own conventional graceful labeling of the entire graft, with edge span 2K+Q. These eight depths arise from four source theorem pairs. This does not establish all interior depths for r>1 or every odd arm length.
The fixed K119 proof combines the retained 1–114 theorem with terminal-seed proofs for 115–116 and 117–118. Certified alpha paths are attached using established alpha/graceful vertex amalgamation, with label complementation when the selected path vertex carries the maximum. Earlier sources for this graft include Huang–Kotzig–Rosa, as stated in Panpa, Imnang and Wasuanankul (2025, Theorem 2.5) and Shan–Zhong (2026, Lemma 1). The endpoint-matched path concatenation is also an older operation, appearing in Adamaszek (Lemma 1) and the proof of Hicks–Ollis–Schmitt (Lemma 4.5).
Two applications of Shan–Zhong (Theorem 2) already give the arbitrary-H depth-1 and depth-2 cases on either arm; Luiz–Campos–Richter (2017, Theorem 14) covers a path with one central leaf. These operations and subcases are credited as prior work. Whether older results imply the complete K119 range 1–118 remains unresolved, including the full Cattell (2007) alpha/path construction. Whether the complete depth-1–118 statement was already known is unknown.
Statements & evidence
K119-ROOTED-GRACEFUL-INTERIOR-ZEROProof provided
For every finite graph H with Q edges, specified root o, and supplied conventional graceful labeling g with g(o)=0, attach two named 119-edge arms at o. For every depth d=1,…,118 on either new arm, the entire graft has its own conventional graceful labeling giving that selected vertex zero, with edge span Q+238. The labeling may depend on the arm and depth.
Formal verification
Formally verified within the stated scope
Review status
Internal check
Evidence
K119Through118.expanded proves the exact graph statement. A separate internal copied-source Lean 4.34.0 replay rebuilt all 68 source modules and checked the theorem and its stated limits. This is internal project checking, not external review.
Scope
All old H vertices and edges are retained. Zero is prescribed separately at each new-arm interior depth 1..118. Neither tip at depth 119, the shared root, old H targets, nor simultaneous zeros are covered. Vertex labels are injective into 0..Q+238; output surjectivity is not asserted.
Assumptions
H is finite; g is supplied, injective into 0..Q, with edge absolute differences exactly 1..Q and g(o)=0. Q=0 is allowed. H need not be connected, acyclic, a tree, alpha-labeled or onto-labeled.
Toolchain
Lean 4.34.0; fresh source compilation with warnings as errors. The kernel, compiler, standard library and encoded graph definitions remain the formal trust boundary.
Reviewer
Separate internal project checks; no external review claimed.
For every integer r≥1, let K=30·4^r−1. Given any finite graph H with Q edges and supplied conventional graceful root-zero labeling, attach two named K-edge arms at that root. Each depth K−8,…,K−1 on either arm has its own conventional graceful labeling of the entire graft giving that target zero, with edge span 2K+Q.
Formal verification
Formally verified within the stated scope
Review status
Internal check
Evidence
The source closure includes TerminalNormalized, TerminalSeed56, TerminalSeed34 and TerminalSeed12 rooted_both theorem pairs. Their compiled theorem statements supply the eight depths; the separate internal copied-source replay checks the retained closure and the new all-r principals.
Scope
Only the eight depths K−8..K−1 are asserted for this family. This does not establish all interior depths for r>1 or every odd K. The old H graph is retained; root, tips, old H targets and simultaneous zeros are not covered.
Assumptions
r≥1 and K=30·4^r−1; H finite with supplied conventional graceful labeling g injective into 0..Q, edge differences 1..Q, and g(o)=0. No connectedness, tree, alpha or onto assumption on H.
Toolchain
Lean 4.34.0; source closure and exact theorem heads are retained in the versioned package.
Reviewer
Separate internal project checks; no external review claimed.
Files & reproduction
No files attached.
Contributions & AI assistance
Contributions
Jordi Gartner publishes this work through Beedbyte.
AI assistance
AI tools assisted the documented Lean implementation, reproduction and check scripts, and draft translations into German and simplified Chinese.
Comments
Discussion of version 1
No comments yet.
Comments on this version are preserved here. Comment on the current version →