← 研究文稿
研究文稿 / prescribed-zero-positions-rooted-graceful-graft
有根优美标号图所接两条臂上的指定零标号 对任意具有常规优美标号的有限图 H，选取标号为 0 的根，并接上两条分别命名、各有 K=23+24t 条边的臂，其中 t≥1。对每条新臂，分别存在常规优美标号，使深度 20+22t 或 21+22t 处取值为 0。
作者 Beedbyte
研究状态 已完成
发布日期 2026-10-10
版本 1
源代码版本 a8125ba821be4b89867d379501a81ebf95445cf2
陈述与证据 文件与复现 贡献与 AI 辅助 版本历史 评论
设 H 为任意有限带索引图，含 Q 条边并具有常规优美标号 g：其顶点标号是 0,…,Q 中互不相同的元素，边差恰为 1,…,Q。选取一个实际存在且 g(r)=0 的根顶点 r。在 r 处接上两条分别命名、各含 K=23+24t 条边的路径，将每条路径的起点与 r 识别，并保留 H 的全部顶点和边。对每条新臂，以及分别对从 r 起算的深度 d₀=20+22t 和 d₁=21+22t，所得拼接图都存在一种常规优美标号，使选定顶点取值为 0。这是四个分别成立的存在命题；标号可以随臂和深度而变化。H 不要求是树、连通、具有 α 标号，或顶点标号填满整个区间。若 g 未覆盖 0,…,Q 中的全部值，输出仍是常规优美标号，但不一定使用其整个顶点标号范围中的每个值。结论不指定 H 中旧顶点、新臂端点或其他深度处为零。
构造使用一条具有 α 标号、长 2K 条边的路径，其中点位于 α 边界。指定位置承载所需的零和最大值；将路径反向即可处理另一条臂。拼接时将路径上的高标号整体加 Q，并将 H 的标号整体加 K−1，因此路径边权位于 Q+1,…,Q+2K，余图边权位于 1,…,Q。对整个标号取补可把目标处的最大值变成零，同时保持边差不变。α/优美标号合并和高标号区间平移是已有操作；Barrientos（2022）描述了这一操作层面的重合。已核查的比较尚不能确定早期文献是否已包含这四个指定位置的结论。
作者的 Lean 4.34.0 证明、单独的数学核查和独立复制源码 Lean 重放均已作为项目内部核查通过；它们不是外部同行评审。全球优先权尚不明确。
陈述与证据
Q24-ROOTED-RESIDUAL-FOUR-PRESCRIBED-ZERO-TARGETS 已提供证明 对每个 t≥1，令 K=23+24t、d₀=20+22t、d₁=21+22t。对任意有限带索引图 H（含 Q 条边）及其常规优美标号 g:V(H)→{0,…,Q}，再取任意实际顶点 r 使 g(r)=0；在 r 处接上两条分别命名、各含 K 条边的路径并保留 H，得到 X。对每一侧 s∈{左,右} 和每个深度 d∈{d₀,d₁}，X 都存在常规优美标号 f，使 f(v(s,d))=0。每个“侧别—深度”组合都是分别成立的存在命题；四个标号可以彼此不同。
形式化验证 已在声明范围内完成形式化验证
审查状态 内部核查
证据 作者 Lean 证明、单独数学核查和复制源码 Lean 重放均已通过；这些属于项目内部核查。
范围 对每个 t≥1，令 K=23+24t，深度 d₀=20+22t、d₁=21+22t。对任意含 Q 条边、具有常规优美标号 g:V(H)→{0,…,Q} 的有限带索引图 H，选取实际顶点 r 使 g(r)=0，并在 r 处接上两条分别命名、各含 K 条边的路径，同时保留 H。对两侧及每个指定深度，拼接图都存在常规优美标号使该顶点取值为零。四种选择分别成立，标号可以不同。
假设 常规优美标号是将顶点单射到 0..|E|，且边差恰为 1..|E|；不要求顶点标号覆盖整个区间。H 为有限带索引图，选定的实际根顶点 r 标号为零。两条新臂是不同的 K 边路径，H 的所有旧顶点和边均保留。
工具链 Lean 4.34.0；作者证明和独立复制源码重放均已通过。
审查者 项目内部核查；不声称经过外部评审或同行评审。
贡献与 AI 辅助
贡献 Jordi Gartner 通过 Beedbyte 发布这项工作。
AI 辅助 AI 工具协助了证明开发及 Lean/核查代码、对早期拼接文献的针对性比较，以及翻译草稿。
Beedbyte
评论
讨论版本 1
暂无评论。