← 研究文稿
研究文稿 / rule-30-checkerboard-completion
Rule 30:不同初始行,相同的左侧演化
你正在阅读一个固定版本。 阅读当前版本
位置 0 的单个 1 与从 0 向右无限延伸的 1010… 图案产生相同的中央序列,其余单元初始均为 0。中央左侧每个位置的演化也相同。
- 作者
- Beedbyte
- 发布日期
- 版本
- 4
- 源代码版本
85d7d83c06f692f3fa7d19af42b6c988e0f58ca0
我比较两条初始行:一条只有位置 0 为 1,另一条在 0、2、4、6、…… 处为 1。其余单元都为 0。
两条初始行在无限多个位置上不同,但中央单元在每个时刻的值都相同。中央左侧所有位置的完整演化也相同。
中央
单个种子: …000 | 1 | 000000…
右半射线: …000 | 1 | 010101…
Rule 30 的更新规则是 下一状态 = 左 XOR (中 OR 右)。用 F^t(u)(n) 表示从初始行 u 出发,经过 t 次更新后位置 n 的值。行在所有整数位置上都有定义,位置编号向右增大。
上面的两条初始行满足:
F^t(单个种子)(n) = F^t(右半射线)(n)
对所有 t ≥ 0 和所有 n ≤ 0 成立。
一般结论
设 u 是任意二进制行,最右侧的占用单元位于 R≥1,也就是 u(R)=1,且所有 n>R 都有 u(n)=0。左侧不受限制。
那么存在一条行 v,从某个正位置起向右按 1、0、1、0、…… 交替排列,并且:
F^t(v)(n) = F^t(u)(n)
对所有 t ≥ 0 和所有 n ≤ 0 成立。
这里的交替尾部指初始行中的空间排列,并不表示某个固定单元的值随时间交替。
单种子例子中的 R=0,所以它不是一般结论的直接特例。它来自下面的第一种构造:R−1=-1 处的值为 0,而该构造保留所有 n≤R 位置的完整演化。
如何构造新行
分两种情况。
R−1 处的值为 0。 保留原行截至 R 的部分,在 R+2、R+4、R+6、…… 添加占用单元。所有 n≤R 位置的演化保持不变。
R−1 处的值为 1。 将最右占用单元从 R 移到 R+1,其他位置不变。所有 n≤R−1 位置的值在全部 t≥0 时刻都相同。新右边缘的 R 和 R+1 两处为 01,因此可以在 R+1 应用第一种构造。
由于 R≥1,两种情况都保留所有 n≤0 位置的演化。
为什么差异一直留在右侧
证明使用两个局部恒等式。记 E=R+t,即原行向右移动的边缘。
当 u(R−1)=0 时,先只在 R+2 添加一个单元。两种演化的差异位置恰好为:
t 为偶数:{E+2}
t 为奇数:{E, E+1, E+2}
这些位置都在 R 右侧,因为奇数情况最早发生在 t=1。在移动边缘附近代入局部更新规则,即可用归纳法证明这一恒等式。在关键的一步,两种演化的局部三单元邻域中,中间输入都为 1。因此该处的 中 OR 右 项不依赖右输入。
新出现的最右占用单元左邻仍为 0,因此可以在右侧相隔两个位置处继续添加单元。每次有限添加都保留同一个左侧区域。
无限尾部的结论来自有限依赖性。对于任意固定的时间 t 和位置 n,输出只依赖初始区间 [n−t,n+t]。足够长的有限补全在该区间内与无限补全一致,所以它们在该时空点的值相同。这对任意 t 和 n≤R 都成立。
第二种情况下,将最外侧占用单元右移一格后,差异位置为:
t 为偶数:{E, E+1}
t 为奇数:{E+1}
同样的局部归纳证明这些差异始终严格位于 R−1 右侧。再接上第一种补全,就得到一般结论。
仍未解决的问题
补全后的初始行右侧有无限多个 1。因此,这个构造既没有为任意指定的中央序列给出有限初始行,也没有判定单种子中央列最终是否周期性。
相关工作研究过侧向重建、对角线结构和时间轨迹限制,例如 Wolfram 的重建说明、Rowland 的局部结构论文和 Kopra 的轨迹结果。我尚未确定这个具体构造是否已在早期文献中出现。
来源与检查
本笔记使用源提交 85d7d83c06f692f3fa7d19af42b6c988e0f58ca0。一般的 R≥1 命题是 Phase20ExplicitCompletion.lean 中的 Rule30.full_checkerboard_completion_exists。R=0 的单种子例子在 Phase17InfiniteFiber.lean 中有单独的形式化证明:Rule30.infiniteEvenRow_same_left_trace 和 Rule30.infiniteEvenRow_same_center。
为检查本笔记,在新建目录中使用 Lean 4.34.0 重新构建了检查所涉及的全部十个 Lean 模块,构建通过。一名 AI 审查者还重新推导了边缘论证,并运行了另写的有界模拟。模拟检查有限情形;关于全部时刻的结论依赖证明及其 Lean 验证。
陈述与证据
R30-CHECKERBOARD-COMPLETION 已提供证明
对任意二进制行 u,若其最右占用位置 R≥1,则存在右尾最终呈棋盘交替排列的行 v,使所有 t≥0、n≤0 都满足 F^t(v)(n)=F^t(u)(n);u 的左尾不受限制。
- 形式化验证
- 已在声明范围内完成形式化验证
- 审查状态
- 内部核查
- 证据
- 固定源版本 85d7d83c06f692f3fa7d19af42b6c988e0f58ca0:proofs/phase20_explicit_checkerboard_completion.md 和 formal/Phase20ExplicitCompletion.lean;对应的准确定理为 Rule30.full_checkerboard_completion_exists。2026 年 10 月 8 日的内部报告 review/math-audit.md 在独立重建证明并重新构建 Lean 模块后,对所述定理给出 PASS。Phase20ExplicitCompletion.lean 的 SHA-256:afaba14b19f00aa57747bf9d8c42ea03e2b7bb2ec6acf423eebf0b893a8fadaf。后续提供的数据提交 7cd3e0cdebf3802942d1579a96387ef1ece92374 仅作背景材料,本证明不依赖它。
- 范围
- 定义在全部整数位置上的二进制初始行。对每条最右侧的 1 位于 R≥1 的行 u,都存在 S≥1 和一条行 v,使得对 n≥S,v(n)=1 当且仅当 n-S 为偶数,且对所有 t≥0、n≤0 都有 F^t(v)(n)=F^t(u)(n)。u 的左侧尾部不受限制。R=0 的单种子情形另行核查;这里不对所有 R=0 的行作出断言。
- 假设
- 在以整数为位置的无限行上同步运行 Rule 30:下一状态 = 左 XOR (中 OR 右)。假设 u(R)=1、所有 n>R 均有 u(n)=0,且 R≥1。不要求左侧只有有限个 1,也不对初始中央位作任何假设。
- 工具链
- Lean 4.34.0,x86_64-w64-windows-gnu,提交 293d5d0c0c3f3dded4688b3ccd6a33939ac5102b。2026 年 10 月 8 日重新构建了十个固定版本的模块,构建通过。Lean 可执行文件的 SHA-256:a8040e2cab341c12116ab591fed9f761816f5f6b08554f6cc1680e86dfbba0a2。所述定理使用的公理:propext、Classical.choice、Quot.sound。
- 审查者
- 一名独立工作的 AI 子代理于 2026 年 10 月 8 日核查了证明:重新推导论证,核对 Lean 定理的准确假设,重新构建固定版本的依赖模块,并运行另行编写的有界模拟。这仅是内部 AI 审查;未声称经过人类审查、外部审查或同行评议。
R30-SINGLE-SEED-CHECKERBOARD 已提供证明
仅在 0 处为 1 的行与恰在 0、2、4、…… 处为 1 的行,在 Rule 30 下对全部 t≥0、n≤0 的演化相同,因此中央序列相同。
- 形式化验证
- 已在声明范围内完成形式化验证
- 审查状态
- 内部核查
- 证据
- 固定源版本 85d7d83c06f692f3fa7d19af42b6c988e0f58ca0:formal/Phase17InfiniteFiber.lean 中的 Rule30.infiniteEvenRow_same_left_trace 和 Rule30.infiniteEvenRow_same_center。该文件的 SHA-256:b85bedaa8878aa67f10b5270f4d575c76eff6d60a4b0f7ff9bd6cb9c9104264c。内部报告 review/math-audit.md 单独核查 R=0 的这一情形,并在重新构建时纳入该模块。另行编写的独立有界模拟还检查了这两行在 t≤128、n=-128,...,0 范围内的相等性;这只是补充检查,不能代替对所有时刻的证明。
- 范围
- 仅限于这两条明确指定的、在全部整数位置上定义的二进制初始行;所有负数位置初始均为 0。结论适用于全部 t≥0 和所有整数位置 n≤0。这是在 R=0 且 u(R−1)=0 时直接补全得到的结果,并非把适用于 R≥1 的一般定理推广到所有 R=0 的行。
- 假设
- 在以整数为位置的无限行上同步运行 Rule 30。u(n)=1 当且仅当 n=0;v(n)=1 当且仅当 n 是非负偶整数。特别地,u(-1)=0。
- 工具链
- Lean 4.34.0,x86_64-w64-windows-gnu,提交 293d5d0c0c3f3dded4688b3ccd6a33939ac5102b。2026 年 10 月 8 日重新构建了十个固定版本的模块,构建通过。Lean 可执行文件的 SHA-256:a8040e2cab341c12116ab591fed9f761816f5f6b08554f6cc1680e86dfbba0a2。所述定理使用的公理:propext、Classical.choice、Quot.sound。
- 审查者
- 一名独立工作的 AI 子代理于 2026 年 10 月 8 日核查了证明:重新推导论证,核对 Lean 定理的准确假设,重新构建固定版本的依赖模块,并运行另行编写的有界模拟。这仅是内部 AI 审查;未声称经过人类审查、外部审查或同行评议。
R30-PRIZE-STILL-OPEN 未解决
该构造没有解决单种子中央列的非最终周期性问题,也没有排除任何候选周期字。
- 形式化验证
- 无形式化验证
- 审查状态
- 内部核查
- 证据
- 依据固定源版本 85d7d83c06f692f3fa7d19af42b6c988e0f58ca0 中 proofs/phase20_explicit_checkerboard_completion.md 的适用范围,以及 2026 年 10 月 8 日的内部报告 review/math-audit.md。两条初始行的轨迹相同,并不能判定它们共有的中央序列是否最终周期性。
- 范围
- 另一项关于 Rule 30 单种子中央列的悬赏问题。
- 审查者
- 由 AI 进行的内部数学与编辑范围核查;未声称解决这一开放问题。
文件与复现
校验和用于识别确切文件。代码仅作为下载文件提供,本站不会执行这些代码。
贡献与 AI 辅助
贡献
Jordi Gartner 通过 Beedbyte 发布这项工作。
AI 辅助
AI 参与了证明、代码、文献检索和翻译。上文列明了 Lean 构建过程及另一次对边界论证的核查。
评论
讨论版本 4
暂无评论。
此版本的评论保留在这里。 在当前版本下评论 →