等长臂蜘蛛的零标号深度区间扩展

对于 k=23+24t、n≥2、m≥0 及每个整数 t≥0，实际蜘蛛图命名长臂上深度 17+20t 至 20+22t 的每个选定顶点都可在各自的优美标号中取值 0。当 t≥1 时，深度 21+22t 也有此性质；当 t≥2 时，深度 22+22t 也有此性质。因此，对 t≥5，q24/D8 前缀与 q48 深度合并后覆盖所有深度 1≤d≤22+22t。

对于每个整数 t≥0，令 k=23+24t。对于所有 n≥2、m≥0，实际蜘蛛图 S(k^n,1^m) 中命名长臂上任一选定实际顶点，若其深度 d 满足 17+20t≤d≤20+22t，则存在一种优美标号使该顶点取值为 0。当 t≥1 时，深度 d=21+22t 也成立；当 t≥2 时，深度 d=22+22t 也成立。每个所选臂和深度都可使用各自的标号。因此，对每个整数 t≥5，令 k=23+24t。对所有 n≥2、m≥0，在 S(k^n,1^m) 的每个指定具名长臂上，对每个物理深度 1≤d≤22+22t，都存在一种优美标号使该实际顶点的标号为零。不同目标顶点可以需要不同的标号。

q24 的 B2 和 B4 构造给出原有区间。末端 B1 适配构造反转一对相邻零，同时保持中点 alpha 条件；当 t≥1 时增加相邻深度 21+22t。当 t≥2 时，末端 q48 双翻转构造再增加下一深度 22+22t。该构造先进行 t−2 次保持原接口的 q24 步骤，再进行一次 q48 宏操作；其输出不满足旧的静态接口，因此不声称可以继续迭代。路径标号转移到实际蜘蛛图中选定的臂，余部构造补全其他臂和所有原有中心叶子的标号。当 t=0 时，区间结论仍是此前已证明的 k=23 情形。q48 主定理 GracefulBoundary.Q48Flip.selected_actual 位于按提交固定的 q48-two-flip/v1 源码包。

本文准确地将较早的优美路径排列操作归于Hicks–Ollis–Schmitt（引理 4.5 的证明）和Adamaszek（引理 1）。Shan–Zhong，引理 1作为经典 alpha 拼接的来源。上述引文不用于认定图层面剩余图转移的历史优先权；该转移已在源码包中证明。Luiz、Campos 和 Richter 报道的早期路径结果还涵盖 n=2,m=0 和 n=2,m=1。该精确位置结果的全球优先权仍为 UNKNOWN。

陈述与证据

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

对于每个整数 t≥0、k=23+24t、n≥2、m≥0，实际蜘蛛图 S(k^n,1^m) 中命名长臂上的每个选定实际顶点，只要其整数深度 d 满足 17+20t≤d≤20+22t，就存在一种优美标号把该顶点标为 0。当 t≥1 时，d=21+22t 也成立；当 t≥2 时，d=22+22t 也成立。标号可以随所选臂和深度而变化。因此，对每个整数 t≥5，令 k=23+24t。对所有 n≥2、m≥0，在 S(k^n,1^m) 的每个指定具名长臂上，对每个物理深度 1≤d≤22+22t，都存在一种优美标号使该实际顶点的标号为零。不同目标顶点可以需要不同的标号。

形式化验证: 已在声明范围内完成形式化验证
审查状态: 内部核查
证据: 此前已发布 v2 中的 q24 区间和末端 B1 扩展均予保留。对于 t≥2、d=22+22t 的 q48 新增结论，已在公开的 q48-two-flip/v1 源码包中形式化为 GracefulBoundary.Q48Flip.selected_actual（提交 e1b8e0035071cfb8b0c04cf6cce21806fd23e1c3；包索引 SHA-256 为 35381f87fc1490deebb0f0245337ab2178cdc377871975aa535ac07ea1831e77）。此外还有单独复制源码的 Lean 复核和内部数学检查。这些均为项目内部检查，不是外部评审。
范围: 整数 t≥0、k=23+24t、n≥2、m≥0。对每个 t≥0，包含 [17+20t,20+22t] 中所有整数深度；另有 t≥1 时的 d=21+22t，以及 t≥2 时的 d=22+22t。t≥5 时的推论：将延伸至 21+22t 的 q24/D8 前缀与 q48 深度合并，对于每条选定的命名长臂、n≥2、m≥0，可覆盖所有物理深度 1≤d≤22+22t，并可使用各自的标号。该合并不是 q48 包中另一个形式化定理。每个选定的命名长臂实际顶点分别处理，并可使用各自的优美标号。保留实际蜘蛛图及所有原有中心叶子；不声称其他顶点类别或深度。
假设: S(k^n,1^m) 是有限蜘蛛图，含 n 条各有 k 条边的命名臂，以及中心处 m 个原始单位叶顶点。优美标号指顶点到 0..|E| 的双射，且边上的绝对差值构成到 1..|E| 的双射。
工具链: Lean 4.34.0；q24 v2 包含其记录的复制源代码复核。q48 新增部分另行复制并复核了全部 36 个源模块，将警告视为错误；定理依赖闭包仅含标准公理，并通过了命名顶点正例和有效语义变异测试。
审查者: 形式化与文献核查均为项目内部核查；不声称经过外部评审或同行评审。该精确位置结果的全球优先权仍未知。

贡献与 AI 辅助

贡献

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

AI 辅助

方法：AI 工具协助开发 q24 B2/B4 构造、末端 B1 适配构造、q48 双翻转证书及证明与代码，检查有限标号和边权和清单，编写 Lean 代码并进行翻译。q24 v2 和 q48 源码包包含形式化与内部检查记录；这些不属于外部评审或同行评审。

版本历史

版本	发布日期	更新说明
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 的顶点。