Prescribed zero depths on two even-length arms of a rooted graceful graph

Let H have Q edges and a supplied conventional graceful labeling g: its vertex labels are distinct elements of 0,…,Q, and its edge differences are exactly 1,…,Q, each once. Choose an actual root r with g(r)=0. For every even K≥20, attach two distinct new K-edge paths at r, preserving all vertices and edges of H. For either named arm and every physical depth 2≤d≤D8(K) measured from r, the resulting graph has a conventional graceful labeling assigning zero to that target. The labeling may depend on the arm and depth; the targets need not be zero in one common labeling. H need not be a tree, connected, or alpha-labeled, and g need not use every value in 0,…,Q.

For even K, the bound is: 20≤K≤34: D8(K)=11; 36≤K≤52: D8(K)=27; 54≤K≤124: D8(K)=25+16 floor((K−35)/18); K≥126: p=(K−4)/2=61+11a+s, 0≤s≤10, D8(K)=107+20a+2s. Here a and s are the nonnegative quotient and remainder specified by p=61+11a+s. The guaranteed prefix is unbounded. The theorem supplies a sufficient interval, without asserting that D8 is optimal.

The proof supplies a single alpha-labeled path with 2K edges, alpha cut K, midpoint label K, and target label either 0 or 2K. Reversing this path handles the opposite arm. In the established graft, H's labels become K+g(v), the high path labels increase by Q, and the low path labels stay fixed. Old edge differences remain 1,…,Q; new differences are Q+1,…,Q+2K. When the target carries the maximum, complementing the entire graft in Q+2K makes it zero.

The alpha/graceful graft is credited to Huang, Kotzig and Rosa (1982); its arbitrary-graph formulation and interval shifts are explicit in Panpa, Imnang and Wasuanankul (2025), Theorem 2.5, and Shan–Zhong (2026), Lemma 1. Barrientos (2022), Section 2, also describes this operation. The original 1982 full text and Cattell's complete 2007 path characterization remain access gaps in this comparison. Barrientos–Minion (2019) already use paired zero/boundary anchors on alpha paths. Bell et al. (2021), Theorem 7, rules out an adjacent zero beside the fixed midpoint label for even K. That path obstruction does not establish impossibility at depth 1 in an arbitrary graft. Whether earlier results imply the exact simultaneous midpoint/target certificate family and this D8 interval remains unresolved; no worldwide priority claim is made.

The Lean declaration GracefulBoundary.EvenRootedPrefix.all_even_prefix was checked with Lean 4.34.0. A separate internal mathematical check and a separate internal replay from 79 copied source modules passed. The replay used fresh compiled objects and audited theorem dependencies against the standard axioms propext, Classical.choice and Quot.sound. These checks rely on the Lean kernel/toolchain and the faithful interpretation of the encoded graph. They do not constitute external peer review. The complete source package is all-even-rooted-prefix/v1 at revision af9cdee7824d14780870898ade045fe5edf6d47d; its provenance records the archived evidence hashes.

The conclusion requires the supplied root-zero labeling. It does not cover odd K, K<20, depth 1, tips, depths above D8(K), or arbitrary old vertices of H. It does not assert full zero-rotatability, vertex-label surjectivity, or nonexistence outside the stated interval.