23 边长臂蜘蛛树的零可旋转性

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 个软件包内定理闭包。以上均为项目内部形式化检查。

审查者

仅有项目内部检查；没有记录外部审稿或同行评审。