← 研究文稿
研究文稿 / zero-rotatability-even-arm-spiders
等长偶数臂蜘蛛树的零可旋转性
对于每个偶数 k ≥ 2、n ≥ 2 和 m ≥ 0，S(k^n,1^m) 的每个命名顶点都能在某个优美标号中取值 0；每次选定顶点时使用单独的标号。
- 作者
- Beedbyte
- 发布日期
- 版本
- 1
- 源代码版本
4914435310380581d4d781cc1640465f27651100
本文证明了命名蜘蛛树 S(k^n,1^m) 的零可旋转性，其中长臂具有相同的偶数长度 k ≥ 2，长臂数量 n ≥ 2，中心还带有 m ≥ 0 个单位叶顶点。中心、每条长臂上的每个命名位置，以及每个实际存在的中心叶顶点，都能分别在某个优美标号中取值 0。
零可旋转性关注的是：能否在保持优美标号全部条件的同时，把零标号放在任意选定的顶点上。证明直接处理臂长为 2 和 4 的情形；其余偶数长度则通过平衡中点路径、显式有限证书和递归扩展的壳层构造来处理。这些构造涵盖所有允许的中心叶数量。
既有研究提供了相关的部分结果和构造工具。Rofa 证明了臂长不超过 3 的对称蜘蛛树的零可旋转性，并给出了更一般的有根对称树的边界层结果；Luiz、Campos 和 Richter 研究了路径以及带中心悬叶的路径。四边长臂的构造使用 Krop 的广义细分操作，以及 Shan–Zhong 对 Huang–Kotzig–Rosa 零值/指标识别构造的转述。Hicks–Ollis–Schmitt 的三段反转优美排列提供了臂长为 6 的路径序列和优美排列拼接构造。Ollis 的引理 5.5 给出端点可自由选择的二部优美排列，并将这一结果归于 Kotzig；定理 5.6 则给出插入构造。臂长为 4 和 6 的完整情形由已发表构造组合而成。
陈述与证据
GE2-ALL-EVEN-ZERO-ROTATABILITY 已提供证明
对于每个偶数整数 k ≥ 2、每个整数 n ≥ 2、每个整数 m ≥ 0，以及 S(k^n,1^m) 中每个实际存在的顶点 v，都存在一个将 v 标为 0 的优美标号。标号可以随选定顶点而变化。
- 形式化验证
- 已在声明范围内完成形式化验证
- 审查状态
- 内部核查
- 证据
- 形式化定理 GracefulBoundary.Integration2Closed.all_even_ge_2_actual 对应于冻结的 -d 手稿及完整、干净构建的 186 模块 Lean 源码包核查。手稿 SHA-256：916679d81fe8a4db7888cf6b4f0ff5a8e31af1660f319f8a4314d0e1ccb30790。源码包 QA 报告 SHA-256：a12575d294fec81ce6fd538d6cf27442a30a2070d0a6a33afd2a854f75b11bec。独立手稿 QA 报告针对冻结 -c 中逐字节相同的数学主体，确认了命题、范围、归属和静态 TeX 文本；SHA-256：7d2c82011f1c0c7dfe88e08c0f485724a7c18e5eba4384a7ef062d4dd48527a9。-d 作者报告记录了数学主体字节未变及其静态检查；SHA-256：65c05654f43427cf98530e567dd5667e69ddeeaa616ce8dc9c1a371b16d03f83。
- 范围
- 对每个偶数整数 k ≥ 2、n ≥ 2、m ≥ 0，以及 S(k^n,1^m) 中每个实际存在的命名顶点；每个选定顶点分别使用一个优美标号。
- 假设
- S(k^n,1^m) 表示有 n 条等长长臂（每臂 k 条边）及中心 m 个单位叶顶点的有限蜘蛛树。优美标号将顶点双射到 0 至 |E|，并将边差双射到 1 至 |E|。每个选定顶点分别处理。
- 工具链
- Lean 4.34.0；干净构建全部 186 个复制的源码模块，并启用 -DwarningAsError=true；定理 GracefulBoundary.Integration2Closed.all_even_ge_2_actual；源码包报告 SHA-256：a12575d294fec81ce6fd538d6cf27442a30a2070d0a6a33afd2a854f75b11bec。包级声明查询只允许 propext、Classical.choice 和 Quot.sound。这属于内部形式化验证，不是外部审查。
- 审查者
- 仅有项目内部 QA；没有记录外部审查或同行评审。
贡献与 AI 辅助
贡献
Jordi Gartner 通过 Beedbyte 发布这项工作。
AI 辅助
方法：AI 工具协助了本工作的构造与证明开发、编程、具体标号证书核查和来源检查。
参考资料
- Rafael I. Rofa, 0-rotatability of classes of rooted symmetric trees. Are rooted symmetric trees 0-rotatable? (arXiv:2312.16235v1).
- Luiz, Campos, and Richter, report IC-17-12 (Lemma 4 and Theorem 14).
- Krop, arXiv:1402.3994v1 (Theorem 2.4).
- Songling Shan and Yucheng Zhong, Graceful Labeling of Two Families of Spiders (arXiv:2605.14295v2).
- Hicks, Ollis, and Schmitt, author manuscript on graceful permutations and constructions.
- Ollis (2020), section 5 on graceful permutations, Lemmas 5.5 and Theorem 5.6.
- Beedbyte, all-even GE2 version folder at commit 4914435310380581d4d781cc1640465f27651100.
- Beedbyte, all-even GE2 source package at commit 4914435310380581d4d781cc1640465f27651100 (README.md).
- Beedbyte, all-even GE2 source package at commit 4914435310380581d4d781cc1640465f27651100 (manuscript.tex).
- Beedbyte, all-even GE2 source package at commit 4914435310380581d4d781cc1640465f27651100 (lean/README.md).
Beedbyte
评论
讨论版本 1
暂无评论。