← 研究文稿
研究文稿 / rooted-graceful-119-edge-arms
两条根接 119 边臂各内部深度的分别零标号
你正在阅读一个固定版本。 阅读当前版本
给定有限图及其在选定根处取零的 graceful 标号,在该根处添加两条各含 119 条边的新臂。任一新臂深度 1–118 的每个内部顶点都可在各自的标号中取零。源码还证明了 K=30·4^r−1、r≥1 时八个指定的近端点深度。
- 作者
- Beedbyte
- 发布日期
- 版本
- 1
- 源代码版本
2861f5ff90990462308728d0958dab2ee1e8b103
设 H 为任意有限图,具有 Q 条边、指定根顶点 o,以及给定的通常 graceful 标号 g。顶点标号是 0,…,Q 中互不相同的值,边的绝对差值恰为 1,…,Q,且 g(o)=0。保留 H 的所有顶点和边,在 o 处添加两条分别命名、各含 119 条边的臂,并将 o 与一条 238 边路径的索引 119 顶点识别。对于任一新臂及每个深度 d=1,…,118,整个拼接图都存在一种通常 graceful 标号,使所选顶点取零。每个目标使用各自的标号;顶点标号位于 0,…,Q+238,边的绝对差值恰为 1,…,Q+238。
给定的根处零标号是前提。H 不必连通、无环、为树、具有 alpha 标号或为顶点满射标号;Q=0 也允许。定理不指定公共根、深度 119 的任一新端点或 H 的旧顶点取零,也不提供一个具有多个零目标的标号。
源码还证明了一个单独的近端点族。对每个整数 r≥1,令 K=30·4^r−1。在相同的给定零根 graceful 图 H 前提下,任一新建 K 边臂的每个深度 K−8,…,K−1 都有各自的整个拼接图通常 graceful 标号,边标号范围为 2K+Q。这八个深度来自四对源码定理。这不证明 r>1 时的全部内部深度,也不证明每一种奇数臂长。
固定 K119 证明将保留的 1–114 定理与覆盖 115–116 和 117–118 的终端种子证明组合。经认证的 alpha 路径通过已有的 alpha/graceful 顶点合并接入;若所选路径顶点具有最大标号,则对整个图的标号取补。该合并的较早来源包括 Huang–Kotzig–Rosa 的结果,见 Panpa、Imnang 和 Wasuanankul(2025,定理 2.5)及 Shan–Zhong(2026,引理 1)的表述。端点匹配的路径串接也是已有操作,见 Adamaszek(引理 1)及 Hicks–Ollis–Schmitt(引理 4.5 的证明)。
两次应用 Shan–Zhong(定理 2)已可得到任意 H 情形下任一臂深度 1 和 2 的结果;Luiz–Campos–Richter(2017,定理 14)覆盖带一个中心叶顶点的路径。这些操作和特例均归于前人工作。较早结果是否蕴含完整 K119 范围 1–118 仍未解决,包括 Cattell(2007)的完整 alpha/路径构造。完整的深度 1–118 结论此前是否已有,尚不清楚。
陈述与证据
K119-ROOTED-GRACEFUL-INTERIOR-ZERO 已提供证明
对每个具有 Q 条边的有限图 H、指定根 o,以及满足 g(o)=0 的给定通常 graceful 标号 g,在 o 处添加两条命名的 119 边臂。对任一新臂的每个深度 d=1,…,118,整个拼接图都存在其各自的通常 graceful 标号,使所选顶点取零,边标号范围为 Q+238。标号可随臂和深度变化。
- 形式化验证
- 已在声明范围内完成形式化验证
- 审查状态
- 内部核查
- 证据
- K119Through118.expanded 证明了准确的图命题。单独的项目内部 Lean 4.34.0 复制源码重放重新编译了全部 68 个源码模块,并核查定理及其声明的边界。这属于内部项目核查,并非外部评审。
- 范围
- 保留 H 的全部旧顶点和边。每个新臂内部深度 1..118 的零标号分别指定。不涵盖深度 119 的端点、公共根、H 的旧目标顶点或同时出现多个零标号。顶点标号单射到 0..Q+238;不声称输出为满射。
- 假设
- H 为有限图;g 为给定的到 0..Q 的单射,边的绝对差值恰为 1..Q,且 g(o)=0。允许 Q=0。H 不必连通、无环、为树、具有 alpha 标号或为顶点满射标号。
- 工具链
- Lean 4.34.0;从源码重新编译并将警告视为错误。内核、编译器、标准库及编码的图定义仍构成形式化信任边界。
- 审查者
- 单独的项目内部核查;不声称有外部评审。
K30-POWER4-ROOTED-NEAR-TIP-EIGHT-DEPTHS 已提供证明
对每个整数 r≥1,令 K=30·4^r−1。给定任意具有 Q 条边的有限图 H 及其通常 graceful 零根标号,在该根处添加两条命名的 K 边臂。任一臂每个深度 K−8,…,K−1 都有各自的整个拼接图通常 graceful 标号,使该目标取零,边标号范围为 2K+Q。
- 形式化验证
- 已在声明范围内完成形式化验证
- 审查状态
- 内部核查
- 证据
- 源码闭包包含 TerminalNormalized、TerminalSeed56、TerminalSeed34 和 TerminalSeed12 的 rooted_both 定理对。编译后的定理声明给出这八个深度;单独的复制源码内部重放核查保留的闭包及新的全 r 主定理。
- 范围
- 该族只声称八个深度 K−8..K−1。这不证明 r>1 时的全部内部深度,也不证明每个奇数 K。保留旧图 H;不涵盖根、端点、H 的旧目标或同时出现多个零标号。
- 假设
- r≥1 且 K=30·4^r−1;H 为有限图,具有给定的通常 graceful 标号 g,单射到 0..Q,边差值为 1..Q,且 g(o)=0。对 H 不要求连通、为树、alpha 标号或顶点满射。
- 工具链
- Lean 4.34.0;源码闭包和准确的定理声明保留在版本化材料包中。
- 审查者
- 单独的项目内部核查;不声称有外部评审。
贡献与 AI 辅助
贡献
Jordi Gartner 通过 Beedbyte 发布这项工作。
AI 辅助
AI 工具协助了已记录的 Lean 实现、复现与核查脚本,以及德文和简体中文翻译草稿。
评论
讨论版本 1
暂无评论。
此版本的评论保留在这里。 在当前版本下评论 →