← 研究文稿
研究文稿 / even-arm-rooted-graceful-zero-depths
有根优美标号图所接两条偶数长度臂上的指定零标号深度
对每个偶数 K≥20,取任意有限图 H 及其给定的常规优美标号,在选定且标号为零的根处接上两条各含 K 条边的臂。对任一新臂及每个深度 2≤d≤D8(K),分别存在一种常规优美标号,使该顶点取零。所保证的深度区间随 K 无界增长。
- 作者
- Beedbyte
- 研究状态
- 已完成
- 发布日期
- 版本
- 1
- 源代码版本
af9cdee7824d14780870898ade045fe5edf6d47d
设 H 含 Q 条边,且已给定常规优美标号 g:顶点标号是 0,…,Q 中互不相同的元素,每个边差 1,…,Q 恰好出现一次。选取实际存在的根顶点 r,使 g(r)=0。对每个偶数 K≥20,在 r 处接上两条不同的新路径,每条含 K 条边,并保留 H 的全部顶点和边。对每条分别命名的臂,以及从 r 起算的每个实际深度 2≤d≤D8(K),所得图都存在常规优美标号,使目标顶点取零。标号可以随臂和深度而变化;并不要求这些目标在同一个标号中同时取零。H 无须是树、连通或具有 α 标号,g 也无须使用 0,…,Q 中的每个值。
对偶数 K,界为:
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.
其中 a 和 s 是由 p=61+11a+s 确定的非负商与余数。所保证的初始深度区间无界增长。定理给出充分区间,不声称 D8 最优。
证明提供同一条含 2K 条边的 α 标号路径,其 α 分界值为 K,中点标号为 K,目标标号为 0 或 2K。将该路径反向可处理另一条臂。在已有拼接操作中,H 的标号变为 K+g(v),路径高标号加 Q,低标号保持不变。旧边差仍为 1,…,Q;新边差为 Q+1,…,Q+2K。若目标承载最大值,则对整个拼接图的标号相对于 Q+2K 取补,将该目标变为零。
α/优美标号拼接归功于 Huang、Kotzig 和 Rosa(1982);Panpa、Imnang 和 Wasuanankul(2025)的定理 2.5,以及 Shan–Zhong(2026)的引理 1,明确给出了适用于任意图的形式及区间平移。Barrientos(2022)第 2 节也描述了这一操作。本次比较尚未取得 1982 年原文全文以及 Cattell(2007)完整的路径刻画。Barrientos–Minion(2019)已在 α 路径上使用零标号与分界标号这一对指定位置。Bell 等(2021)的定理 7 排除了偶数 K 时固定中点标号旁的相邻零标号。这一路径障碍并不证明任意拼接图在深度 1 处无法取零。早期结果是否已蕴含精确的中点与目标同时约束以及本 D8 区间,仍未确定;不主张全球优先权。
Lean 声明 GracefulBoundary.EvenRootedPrefix.all_even_prefix 已用 Lean 4.34.0 检查通过。单独进行的项目内部数学核查,以及从 79 个复制的源码模块进行的另一项内部重放均已通过。重放使用新编译的对象,并核查定理依赖仅使用标准公理 propext、Classical.choice 和 Quot.sound。这些检查依赖 Lean 内核及工具链,也依赖对图编码的正确数学解释。它们不构成外部同行评审。完整源码包为修订 af9cdee7824d14780870898ade045fe5edf6d47d 中的 all-even-rooted-prefix/v1;其来源记录保存了归档证据的哈希。
结论要求已给定的标号在所选根处取零。不覆盖奇数 K、K<20、深度 1、臂端点、超过 D8(K) 的深度或 H 中任意旧顶点;不声称完全零可旋转性、顶点标号满射,也不声称所列区间以外不存在相应标号。
陈述与证据
all-even-rooted-residual-d8 已提供证明
对每个偶数 K≥20,取任意有限图 H 及其给定的常规优美标号,在选定且标号为零的根处接上两条各含 K 条边的臂。对任一新臂及每个深度 2≤d≤D8(K),分别存在一种常规优美标号,使该顶点取零。所保证的深度区间随 K 无界增长。
- 形式化验证
- 已在声明范围内完成形式化验证
- 审查状态
- 内部核查
- 证据
- GracefulBoundary.EvenRootedPrefix.all_even_prefix 的作者 Lean 证明、单独内部数学核查及单独复制源码 Lean 重放均已通过。重放以新对象重建全部 79 个所需模块。源码:all-even-rooted-prefix/v1,修订 af9cdee7824d14780870898ade045fe5edf6d47d,source/EvenRootedPrefix.lean 的 SHA-256 为 09333b91d704b791f412232bd361ed0ed0bbf82e4ffdb6f460ae2d8fc734b9a0。归档重放报告的 SHA-256 为 7827a349c6b4308452bcf5161300203ff444ec85910bbba1f01d377b208820ad;其摘要记录在所引用的公开 provenance.json 中。
- 范围
- 结论要求已给定的标号在所选根处取零。不覆盖奇数 K、K<20、深度 1、臂端点、超过 D8(K) 的深度或 H 中任意旧顶点;不声称完全零可旋转性、顶点标号满射,也不声称所列区间以外不存在相应标号。
- 假设
- K 为偶数且 K≥20;2≤d≤D8(K)。H 含 Q 条边,并已给定到 0..Q 的顶点单射标号 g,每个边差 1..Q 恰好出现一次。选定的实际根满足 g(r)=0。在该处接上两条不同的 K 边臂,保留整个 H。不要求 H 为树、连通、具有 α 标号或顶点标号满射。
- 工具链
- Lean 4.34.0;信任范围包括内核/工具链、标准公理及忠实的图编码。
- 审查者
- 仅有项目内部核查;不声称经过外部评审或同行评审。全球优先权仍未确定。
贡献与 AI 辅助
贡献
Jordi Gartner 通过 Beedbyte 发布这项工作。
AI 辅助
AI 工具协助了已记录的证明开发与 Lean/核查代码、单独开展的内部数学核查及复制源码检查、原始文献比较,以及这些翻译草稿。
参考资料
- All-even rooted-prefix source package
- German source-package reader note (draft translation)
- Simplified Chinese source-package reader note (draft translation)
- Principal Lean theorem
- Reproduction driver
- Source and archived-evidence provenance
- Package checksums
- Source and query checksums
- Panpa, Imnang and Wasuanankul (2025), Graceful Labeling of Spider Graphs With at Most Five Legs, Theorem 2.5
- Shan–Zhong (2026), Lemma 1 (version 2)
- Barrientos (2022), On the generation of alpha graphs, Section 2
- Barrientos–Minion (2019), Series-Parallel Operations with Alpha-Graphs, Section 2.2
- Bell et al. (2021), Graceful Wind Chimes, Theorem 7
- Cattell (2007), Graceful labellings of paths (complete text not inspected)
评论
讨论版本 1
暂无评论。