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

你正在阅读一个固定版本。阅读当前版本

对于 k=23+24t、n≥2、m≥0 及每个整数 t≥0，命名长臂上深度 17+20t 至 20+22t 的每个选定顶点都可在各自的优美标号中取值 0。当 t≥1 时，深度 21+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 也有此性质。每个选定臂和深度都可以使用各自的标号。

q24 的 B2 和 B4 构造给出了原有区间。末端 B1 适配构造反转一对相邻零，同时保持中点 alpha 条件；当 t≥1 时，这增加了相邻深度 21+22t。路径标号转移到实际蜘蛛图中所选定的臂，余部构造则补全其他臂和原有中心叶顶点的标号。t=0 时仍是此前已证明的 k=23 情形。

端点匹配的 alpha 路径拼接是已有方法：Hicks–Ollis–Schmitt 在引理 4.5 的证明中使用该方法，Adamaszek 在引理 1 中给出反向拼接。Luiz、Campos 和 Richter 报道的早期路径结果还涵盖 n=2,m=0 和 n=2,m=1。

陈述与证据

对于每个整数 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≥1 将 q24 区间扩展到新增深度 21+22t。冻结的作者形式化证明及单独的复制源代码复核均已用 Lean 4.34.0 检查；版本化源代码包将包含该定理和复现记录。
范围: 整数 t≥0、k=23+24t、n≥2、m≥0。原有深度为 [17+20t,20+22t] 中的所有整数；当 t≥1 时增加深度 21+22t。每个选定的命名长臂实际顶点分别处理，并可使用各自的优美标号。不声称其他深度或顶点类别。
假设: S(k^n,1^m) 是有限蜘蛛图，含 n 条各有 k 条边的命名臂，以及中心处 m 个原始单位叶顶点。优美标号指顶点到 0..|E| 的双射，且边上的绝对差值构成到 1..|E| 的双射。
工具链: Lean 4.34.0；末端作者源代码和单独的复制源代码复核均编译了 34 个模块。采用标准 Lean 内核验证。
审查者: 形式化与文献核查均为项目内部核查；不声称经过外部评审或同行评审。该精确位置结果的全球优先权仍未知。

无附件。

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

方法：AI 工具协助开发 B2/B4 构造及末端适配构造、检查有限的标号与边权和清单，并构建 Lean 形式化证明。该定理及单独复制的源代码已用 Lean 4.34.0 检查。

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

Beedbyte. 等长臂蜘蛛的零标号深度区间扩展. Beedbyte, v2, 2026-10-10.

SHA-256 — 版本

9a5b0000576cd9a7c4754fe8efc6da9b38715ccbe891385e5c1d8c18b3a53b44

讨论版本 2

暂无评论。

此版本的评论保留在这里。在当前版本下评论 →