等臂蜘蛛树中逐渐扩大的零标号深度区间

当 k=23+24t、整数 t≥0、n≥2 且 m≥0 时，S(k^n,1^m) 的每条命名长臂上，在深度 17+20t 至 20+22t 的每个顶点都可分别在一个优美标号中取值 0。

对每个整数 t≥0，令 k=23+24t。对于每个 n≥2、m≥0、每条命名长臂 a，以及满足 17+20t≤d≤20+22t 的每个深度 d，S(k^n,1^m) 中臂 a 上深度 d 的实际顶点都可以在一个优美标号中取值 0。每个臂-深度目标可以使用各自的标号。该区间包含 4+2t 个深度：k=47 时为 37–42，k=71 时为 57–64。命题仅覆盖这些深度，不涵盖这些臂长下的所有顶点。

构造从两个 47 个顶点的中点 alpha 路径优美标号开始，再以任意顺序使用 q24 的 B2 和 B4 拼接。两种起始零位置给出两个相接或重叠的深度区间，合起来覆盖完整区间。路径标号转移到实际蜘蛛树中选定的两条长臂；余部构造补全其余长臂和原有中心叶顶点上的优美标号。因此，对所有 n≥2 和 m≥0 都得到同一深度范围。

当 t=0 时，该区间包含在此前已证明的 k=23 全顶点情形中。对于每个 t，路径子族 n=2,m=0 和 n=2,m=1 也已由早期路径结果覆盖：Rosa 的路径结果（由 Luiz、Campos 和 Richter 转述），以及他们关于中心附有一个叶顶点的路径的定理 14。证明使用了经典 alpha 拼接方法（Shan 和 Zhong 对其作了转述），将其作为已有构造工具。

陈述与证据

Q24-VARIABLE-WINDOW-ACTUAL-SPIDER 已提供证明

对于每个整数 t≥0、k=23+24t、每个 n≥2 和 m≥0、实际蜘蛛树 S(k^n,1^m) 的每条命名长臂 a，以及每个满足 17+20t≤d≤20+22t 的整数深度 d，都存在一个优美标号 f，使臂 a 上深度 d 的实际顶点取值为 0。标号可以随 a 和 d 而不同。

形式化验证: 已在声明范围内完成形式化验证
审查状态: 内部核查
证据: Independent mathematical QA: 79087c170c07d39cd48ccf34214fdde2ecccd223e0ac962c6d954b6e463527cb; author Lean freeze: 392eecf6bceae9282121e9ba0753b79d33ee4061c4a1ee75377fd36df4ee4610; copied-source Lean replay FROZEN GO: 44a2d5b096d473102fbc3ec6936eba48bc8eb19391e68042ab6b8244d46f50a7; source package commit: 94889aa8916282eba53288760fced7b6677dade8.
范围: Only arm lengths k=23+24t for integer t≥0; only the named-arm vertices at depths d in [17+20t,20+22t]; all n≥2,m≥0; separate graceful labeling for each chosen arm-depth target. No center or center-leaf zero-label conclusion is included. No full k47 or k71 coverage and no all-odd-arm-length theorem.
假设: S(k^n,1^m) is the finite spider with n named arms of k edges and m original unit leaves attached to the center. A graceful labeling bijects vertices to 0..|E| and edge absolute differences to 1..|E|. Zero is prescribed only at a selected actual named long-arm vertex in the stated depth interval, with a separate labeling for each selected arm-depth target.
工具链: Lean 4.34.0; author freeze and separate copied-source replay of 33 modules; theorem GracefulBoundary.Q24Seed5Mix.combined_interval_actual; standard Lean kernel verification.
审查者: Internal mathematical QA and formal checks only; no external or peer review is claimed.

版本历史

版本	发布日期	更新说明
v3	2026-10-10	新增 t≥2 时深度 22+22t 处的末端 q48 零标号。对于 t≥5，该结论与 q24/D8 前缀合并，得到推论连续深度范围 1≤d≤22+22t。
v2	2026-10-10	新增 q24 末端构造，对每个 t≥1 给出深度 21+22t 处的零标号。
v1	2026-10-10	证明：当 k=23+24t、整数 t≥0、n≥2、m≥0 时，每条命名长臂在 17+20t 至 20+22t 的每个深度都有一个可单独标为 0 的顶点。

等臂蜘蛛树中逐渐扩大的零标号深度区间

陈述与证据

Q24-VARIABLE-WINDOW-ACTUAL-SPIDER 已提供证明

文件与复现

贡献与 AI 辅助

贡献

AI 辅助

参考资料

版本历史

引用此版本

评论