研究文稿 / rooted-graceful-119-edge-arms

两条根接 119 边臂各内部深度的分别零标号

给定有限图及其在选定根处取零的 graceful 标号,在该根处添加两条各含 119 条边的新臂。任一新臂深度 1–118 的每个内部顶点都可在各自的标号中取零。源码还证明了 K=30·4^r−1、r≥1 时八个指定的近端点深度。

设 H 为任意有限图,具有 Q 条边、指定根顶点 o,以及给定的通常 graceful 标号 g。顶点标号是 0,…,Q 中互不相同的值,边的绝对差值恰为 1,…,Q,且 g(o)=0。保留 H 的所有顶点和边,在 o 处添加两条分别命名、各含 119 条边的臂,并将 o 与一条 238 边路径的索引 119 顶点识别。对于任一新臂及每个深度 d=1,…,118,整个拼接图都存在一种通常 graceful 标号,使所选顶点取零。每个目标使用各自的标号;顶点标号位于 0,…,Q+238,边的绝对差值恰为 1,…,Q+238。

给定的根处零标号是前提。H 不必连通、无环、为树、具有 alpha 标号或为顶点满射标号;Q=0 也允许。定理不指定公共根、深度 119 的任一新端点或 H 的旧顶点取零,也不提供一个具有多个零目标的标号。

源码还证明了一个单独的近端点族。对每个整数 r≥1,令 K=30·4^r−1。在相同的给定零根 graceful 图 H 前提下,任一新建 K 边臂的每个深度 K−8,…,K−1 都有各自的整个拼接图通常 graceful 标号,边标号范围为 2K+Q。这八个深度来自四对源码定理。这不证明 r>1 时的全部内部深度,也不证明每一种奇数臂长。

固定 K119 证明将保留的 1–114 定理与覆盖 115–116 和 117–118 的终端种子证明组合。经认证的 alpha 路径通过已有的 alpha/graceful 顶点合并接入;若所选路径顶点具有最大标号,则对整个图的标号取补。该合并的较早来源包括 Huang–Kotzig–Rosa 的结果,见 Panpa、Imnang 和 Wasuanankul(2025,定理 2.5)及 Shan–Zhong(2026,引理 1)的表述。端点匹配的路径串接也是已有操作,见 Adamaszek(引理 1)及 Hicks–Ollis–Schmitt(引理 4.5 的证明)。

两次应用 Shan–Zhong(定理 2)已可得到任意 H 情形下任一臂深度 1 和 2 的结果;Luiz–Campos–Richter(2017,定理 14)覆盖带一个中心叶顶点的路径。这些操作和特例均归于前人工作。较早结果是否蕴含完整 K119 范围 1–118 仍未解决,包括 Cattell(2007)的完整 alpha/路径构造。完整的深度 1–118 结论此前是否已有,尚不清楚。

陈述与证据

K119-ROOTED-GRACEFUL-INTERIOR-ZERO 已提供证明

对每个具有 Q 条边的有限图 H、指定根 o,以及满足 g(o)=0 的给定通常 graceful 标号 g,在 o 处添加两条命名的 119 边臂。对任一新臂的每个深度 d=1,…,118,整个拼接图都存在其各自的通常 graceful 标号,使所选顶点取零,边标号范围为 Q+238。标号可随臂和深度变化。

形式化验证
已在声明范围内完成形式化验证
审查状态
内部核查
证据
K119Through118.expanded 证明了准确的图命题。单独的项目内部 Lean 4.34.0 复制源码重放重新编译了全部 68 个源码模块,并核查定理及其声明的边界。这属于内部项目核查,并非外部评审。
范围
保留 H 的全部旧顶点和边。每个新臂内部深度 1..118 的零标号分别指定。不涵盖深度 119 的端点、公共根、H 的旧目标顶点或同时出现多个零标号。顶点标号单射到 0..Q+238;不声称输出为满射。
假设
H 为有限图;g 为给定的到 0..Q 的单射,边的绝对差值恰为 1..Q,且 g(o)=0。允许 Q=0。H 不必连通、无环、为树、具有 alpha 标号或为顶点满射标号。
工具链
Lean 4.34.0;从源码重新编译并将警告视为错误。内核、编译器、标准库及编码的图定义仍构成形式化信任边界。
审查者
单独的项目内部核查;不声称有外部评审。

K30-POWER4-ROOTED-NEAR-TIP-EIGHT-DEPTHS 已提供证明

对每个整数 r≥1,令 K=30·4^r−1。给定任意具有 Q 条边的有限图 H 及其通常 graceful 零根标号,在该根处添加两条命名的 K 边臂。任一臂每个深度 K−8,…,K−1 都有各自的整个拼接图通常 graceful 标号,使该目标取零,边标号范围为 2K+Q。

形式化验证
已在声明范围内完成形式化验证
审查状态
内部核查
证据
源码闭包包含 TerminalNormalized、TerminalSeed56、TerminalSeed34 和 TerminalSeed12 的 rooted_both 定理对。编译后的定理声明给出这八个深度;单独的复制源码内部重放核查保留的闭包及新的全 r 主定理。
范围
该族只声称八个深度 K−8..K−1。这不证明 r>1 时的全部内部深度,也不证明每个奇数 K。保留旧图 H;不涵盖根、端点、H 的旧目标或同时出现多个零标号。
假设
r≥1 且 K=30·4^r−1;H 为有限图,具有给定的通常 graceful 标号 g,单射到 0..Q,边差值为 1..Q,且 g(o)=0。对 H 不要求连通、为树、alpha 标号或顶点满射。
工具链
Lean 4.34.0;源码闭包和准确的定理声明保留在版本化材料包中。
审查者
单独的项目内部核查;不声称有外部评审。

文件与复现

无附件。

贡献与 AI 辅助

贡献

Jordi Gartner 通过 Beedbyte 发布这项工作。

AI 辅助

AI 工具协助了已记录的 Lean 实现、复现与核查脚本,以及德文和简体中文翻译草稿。

参考资料

  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

版本历史

版本发布日期更新说明
v1新增 K119 的每个内部深度 1–118 的零标号构造,以及 K=30·4^r−1(r≥1)时八个近端点深度的构造。

引用此版本

Beedbyte. 两条根接 119 边臂各内部深度的分别零标号. Beedbyte, v1, 2026-10-10.

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

SHA-256 — 版本e06f57f93117ae6e1eb71dbb25e39cc8e9451228cee68dfdfbf51989e1b932e6

评论

讨论版本 1

暂无评论。

发表评论

你的显示名称和评论会保存以供审核。通过审核的评论会公开显示;被拒绝的评论仍保留在非公开的审核记录中。请勿填写私人信息。