← 研究文稿
研究文稿 / zero-rotatability-23-edge-arm-spiders
23 边长臂蜘蛛树的零可旋转性
对于每个 n ≥ 2 和 m ≥ 0，S(23^n,1^m) 中每个实际存在的顶点都能在一个优美标号中取值 0；每个选定顶点分别使用一个标号。
- 作者
- Beedbyte
- 发布日期
- 版本
- 1
- 源代码版本
b7546e3aac1a25e6a62c1a9eeb8794049ad093ed
本结果证明，对于每个 n ≥ 2 和 m ≥ 0，S(23^n,1^m) 都具有零可旋转性。中心、n 条命名长臂上深度 1 至 23 的每个顶点，以及 m > 0 时每个实际存在的原始中心叶顶点，都可以分别在一个优美标号中取值 0。所用标号可以随选定顶点而不同；当 m = 0 时，不存在中心叶顶点。
零可旋转性研究的是：能否把零放在任意选定顶点，同时保持顶点标号互异及边差符合要求。构造结合了明确的中点 alpha 路径证书、经典 alpha 拼接方法和奇数余部构造，从而覆盖每条命名长臂、每个深度、中心以及每个实际存在的叶顶点。
既有研究完整覆盖了路径情形 n = 2、m = 0 和 n = 2、m = 1：前者是 Rosa 的路径结果，由 Luiz、Campos 和 Richter 转述；他们的定理 14 处理带一个中心叶的路径。经典 alpha 拼接则提供了本文使用的一项构造工具。这些工作为上述定理提供了相关的既有情形和构造依据。
陈述与证据
K23-ALL-NAMED-VERTEX-ZERO-ROTATABILITY 已提供证明
对于每个整数 n ≥ 2、每个整数 m ≥ 0，以及 S(23^n,1^m) 中每个实际存在的顶点 v，都存在该图的一个优美标号 f，使得 f(v)=0。标号可以随 v 而不同。
- 形式化验证
- 已在声明范围内完成形式化验证
- 审查状态
- 内部核查
- 证据
- Root 已核查的公开固定 k23 源码包（提交 b7546e3aac1a25e6a62c1a9eeb8794049ad093ed）在 source/K23Full.lean 中包含定理 GracefulBoundary.K23Full.all_vertices；软件包 README 记录了 Lean 4.34.0 构建和复制源码重放。
- 范围
- 对于每个 n ≥ 2 和 m ≥ 0，有限蜘蛛树 S(23^n,1^m) 中每个实际存在的命名顶点：中心、每条臂 (Fin n) 上 23 个深度的顶点，以及存在时的 m 个原始中心叶顶点。对每个选定顶点 v，都存在一个可能不同的优美标号 f，使 f(v)=0。该图有 23n+m 条边；顶点标号为 0..23n+m，边权为 1..23n+m。
- 假设
- S(23^n,1^m) 是有限蜘蛛树，每条长臂恰有 23 条边，中心连接 m 个原始单位叶顶点。优美标号将顶点双射到 0 至 |E|，并通过端点标号的绝对差将边双射到 1 至 |E|。每个选定顶点分别处理。
- 工具链
- Lean 4.34.0；按顺序全新编译全部 27 个冻结软件包模块，并启用 -DwarningAsError=true；定理 GracefulBoundary.K23Full.all_vertices；复制源码重放全新编译 27 个模块，并依据 Lean 标准公理核查了 1,649 个软件包内定理闭包。以上均为项目内部形式化检查。
- 审查者
- 仅有项目内部检查；没有记录外部审稿或同行评审。
贡献与 AI 辅助
贡献
Jordi Gartner 通过 Beedbyte 发布这项工作。
AI 辅助
方法：AI 工具协助了本工作的构造与证明开发、编程、核查明确的标号证书，并检查所引来源。
参考资料
- Beedbyte, fixed-k23/v1 source package and release notes (commit-pinned).
- Beedbyte, fixed-k23/v1 README (formal and replay status).
- Beedbyte, fixed-k23/v1 English research note.
- Beedbyte, fixed-k23/v1 German draft translation.
- Beedbyte, fixed-k23/v1 simplified Chinese draft translation.
- Beedbyte, fixed-k23/v1 formal theorem source K23Full.lean.
- Luiz, Campos, and Richter, technical report IC-17-12 (Rosa path result, Lemma 4; Theorem 14).
- Shan and Zhong, Graceful Labeling of Two Families of Spiders, Lemma 1 (classical alpha-amalgamation statement).
Beedbyte
评论
讨论版本 1
暂无评论。