Publications / rooted-graceful-119-edge-arms

Separate zero placements at every interior depth of two rooted 119-edge arms

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.

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-ZERO Proof 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.

K30-POWER4-ROOTED-NEAR-TIP-EIGHT-DEPTHS Proof provided

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.

References

  1. K119 source package and theorem scope
  2. German source presentation (translation draft)
  3. Simplified Chinese source presentation (translation draft)
  4. Fixed K119 full-interior Lean theorem
  5. Near-tip depths K−8 and K−7
  6. Near-tip depths K−6 and K−5
  7. Near-tip depths K−4 and K−3
  8. Near-tip depths K−2 and K−1
  9. Separate internal copied-source Lean replay
  10. Internal primary-literature priority comparison
  11. Exact Lean source checksums
  12. Panpa, Imnang and Wasuanankul (2025), Theorem 2.5
  13. Shan and Zhong (2026), Lemma 1 and Theorem 2
  14. Luiz, Campos and Richter (2017), Theorem 14
  15. Cattell (2007), Graceful labellings of paths
  16. Adamaszek, Lemma 1
  17. Hicks, Ollis and Schmitt, proof of Lemma 4.5

Version history

VersionPublishedChange note
v1Adds zero placements at every K119 interior depth 1–118 and at eight near-tip depths for K=30·4^r−1 (r≥1).

Cite this version

Beedbyte. Separate zero placements at every interior depth of two rooted 119-edge arms. Beedbyte, v1, 2026-10-10.

https://beedbyte.tech/publications/rooted-graceful-119-edge-arms/v/1

SHA-256 — Versione06f57f93117ae6e1eb71dbb25e39cc8e9451228cee68dfdfbf51989e1b932e6

Comments

Discussion of version 1

No comments yet.

Leave a comment

Your display name and comment are saved for review. Approved comments appear publicly; rejected comments remain in the private moderation record. Please leave out private information.