超立方体Ramsey（openai/math 家族171）攻坚日志｜Lean 4 形式化证明超立方体 Ramsey 暴露尾界：三阶段攻坚复盘

摘要：本文记录一项超立方体 Ramsey 方向概率估计在 Lean 4 中的形式化攻坚过程：从异质乘积律尾界、护栏失效条件估计，到存活路径上的窗口对数望远镜恒等式，三个阶段逐步闭合。全文给出定理骨架、显式前提、玩具控制规模、当前 OPEN 清单与阶段门止损规则，并沉淀五条可复用的形式化工程法则。所有结论均标注成立条件；有限玩具控制不冒充渐近证明；未过门不发布、不入库。

关键词：Lean 4 · 形式化证明 · Ramsey 问题 · 尾概率界 · 异质乘积律 · 对数望远镜 · 白名单基线 · 阶段门验收

0. TL;DR（一分钟读完）

• 做了什么：把暴露过程Z(length)的三类关键估计逐步接进完整有序暴露结构——异质乘积律尾界、护栏失效概率支付、窗口对数望远镜恒等式。
• 当前基线（最新阶段 B3）：7 条定理、1030 条白名单输出，零 warning / 零 error，对上一基线逐字节保持；全部 clean PASS。
• 两个核心概率结论（均带显式前提，不外供外部概率上限）：
  • 护栏失效：P[¬guard(length)] ≤ length · exp(-budget/2)；
  • 绝对失败：P[Z(length) < exp(-2·length)] ≤ length · exp(-budget/2)，无需新增 drift / codegree / 概率 cap 前提。
• 当前位置：前序 G1–G5 已关闭；主门 G6 及其内部子门 G6a / G6b均 OPEN；目标问题PARTIAL / HOLD。下一阶段为技术验收门 Gate-1：验收通过且语义路线可实施，才允许有条件续至 Gate-2；未过则 INCOMPLETE 止损，保留全部成果，不自动 commit、不发布、不提升方法库。
• 给读者的最大价值：不是某个漂亮不等式，而是一套"条件不外推、玩具不冒充证明、基线只增不重置"的形式化推进纪律。

阅读导航：第 1 节背景与误区 → 第 2 节总体路线 → 第 3–5 节三阶段技术细节 → 第 6 节 OPEN 清单 → 第 7 节验证体系 → 第 8–9 节方法论与避坑 → 第 10 节行动看板。

1. 问题背景：为什么把 Ramsey 暴露尾界搬进形式化证明器

1.1 研究对象与公共模型

超立方体图QnQ_nQn​的顶点是所有nnn维 0/1 向量，两个顶点恰好在一个坐标上不同时连边。围绕该结构的 Ramsey 型问题通常需要回答：在多长的随机暴露序列上，某些"过大暴露 / 过早命中"事件会以多大概率失败。

工程上把随机暴露过程抽象为一个随步数增长的比值序列Z(0),Z(1),…,Z(ℓ)Z(0), Z(1), \dots, Z(\ell)Z(0),Z(1),…,Z(ℓ)，并关心两类事件：

1. 护栏事件（guard）：每一步的增量都落在预设带宽内；护栏被击穿意味着后续估计不再被支付保护。
2. 绝对失败事件：Z(ℓ)Z(\ell)Z(ℓ)跌破某个指数级下界（本文使用exp⁡(−2ℓ)\exp(-2\ell)exp(−2ℓ)作为基准线）。

形式化证明器要解决的问题不是"大概对"，而是：每一个不等式成立所依赖的前提（漂移量、范围、带宽宽度、预算量）都必须在定理签名里显式出现，依赖面被白名单审计，历史结论逐字节可重放。

动手前已完成论文对象—模型对象的对照审计：10 项对象与 law 逐一核对，冻结技术接口与语义接口；技术接口验收不等于语义结论关闭，这一边界贯穿全文。

1.2 三个最容易踩的认知误区

形式化概率推进最容易在三个地方"自我感觉良好"，先把误区摆在前面：

后文三阶段正好对应"先建异质律、再付护栏价、最后做望远镜"的补位顺序。

2. 总体路线：阶段门合同与当前位置

2.1 阶段门状态总览

推进采用阶段门（stage-gate）合同，而不是无限连续产出：每个阶段先闭合可验证的数学块与基线，再由门决定是否放行下一阶段。

纪律约束（硬规则）：

• 不自动 commit：基线增量必须经验收后手动进入受管历史；
• 不自动发布：任何对外结论不得早于对应门关闭；
• 不提升方法库：未过门定理不得进入可复用方法库；
• 未过 Gate-1 不自动续至 Gate-2：止损时保留全部中间成果，仅停止前推。

2.2 基线演进与验证口径

基线（baseline）是一组可重放的验证快照：新阶段只能增量叠加定理与白名单输出，历史文件逐字节保持不变。

口径说明：白名单输出指验证器在白名单规则下实际产出的允许依赖条目计数；它衡量"证明用了哪些被许可的基础事实"，不是定理总数。两者并列计数、互不替代。

3. 阶段 M1：异质乘积律与裁剪对数增量

3.1 数学脉络

本阶段把真实的 stopped squared-prefix 裁剪对数增量接入完整有序暴露结构，替代早期占位假设，证明链分四步：

1. 冻结来源量：漂移量（drift）与波动范围（range）从冻结的来源 law 取得，不允许在证明内部临时放宽；
2. 异质坐标：各步坐标的条件分布不必同分布，乘积律在异质（heterogeneous）条件下成立；
3. 裁剪（clipping）：对数增量先被裁剪到有界区间，再进入乘积，避免长尾坐标污染指数尾界；
4. 尾界导出：在异质乘积律下得到指数尾界：

P(暴露过大事件) ≤ exp(- 9 · a² · length / 1600)

其中a是偏离目标均值的偏差量，length是暴露步数。该阶段不对外提供 fixed-list（固定列表）概率上限——固定列表的上界控制量（hcaps）仍在后续 OPEN 清单中。

3.2 形式化接线骨架（脱敏）

下面只展示声明形态与依赖关系，不含内部实现细节，便于理解"前提如何显式进签名"：

-- 定理骨架（脱敏示意）：异质乘积律尾界 -- 前提全部写在签名里：漂移量、范围、裁剪边界均为显式参数 theorem heterogeneous_product_tail {Z : ℕ → ℝ} (a : ℝ) (length : ℕ) (h_drift : source_drift_frozen a) (h_range : source_range_bounded) (h_clip : log_increment_clipped) : probability_of_large_exposure length ≤ exp (- 9 * a^2 * length / 1600) := by sorry

要点：sorry仅用于展示声明；真实闭证在工程基线中全部关闭，验收以验证器结果为准。

3.3 精确玩具控制与边界声明

为了抓局部代数错误，构造了BigInt 精确玩具状态（不取浮点近似）：

• 24 次未来坐标局部性检查：验证当前步结论不依赖未来坐标的提前泄露；
• 6 个首次越界异常见证：覆盖首次穿出裁剪区间时的行为边界。

边界声明（必须随结论一并写出）：

玩具控制是有限状态上的精确检查，用于捕捉接线错误与异常分支；它不是来源 2 的渐近概率证明，渐近尾界的合法性只能由一般定理承担。

4. 阶段 M2：护栏失效（Guard Catastrophe）的条件支付

4.1 尾界与显式前提

M1 解决了"正常步增量"的尾部估计；M2 解决"护栏被击穿本身"的概率估计。核心结论：

P[¬guard(length)] ≤ length · exp(-budget / 2)

该不等式显式依赖三个前提，缺一不可：

关键立场：不引入外供概率 cap。也就是说，不存在一个"先给定的普适常数上限"；每个数字都由budget / width前提现场支付。

4.2 接线清单

本阶段完成三项工程接线：

1. 实际坐标重采样（coordinate-resampling）：重采样分支进入主证明链，而非旁路脚本；
2. 有限步并集（finite-step union）："某一步击穿护栏"的并集事件被显式打包，避免逐步裸加；
3. 等价性接线：最终护栏失败事件与首次越界（first crossing）事件建立等价，两个事件视图共用同一份证明。

4.3 控制集覆盖

精确重采样控制集：62 个状态、20 次精确重采样控制，并刻意覆盖三类退化输入：

• 零原子（zero atom）：某坐标无质量时的乘积行为；
• 零证据（zero evidence）：无信息更新时的不变性；
• 空乘积（empty product）：零步与空列表的边界定义。

这些退化分支是有限实现最容易 silently 出错的位置，必须在控制集里有见证。

4.4 为什么坚持"不外供概率上限"

形式化工程中最省事、也最危险的动作，就是在签名外用一个经验常数"压住"尾部。代价是：前提缺口被常数掩盖，后续一旦更换分布假设，证明链整体悬空。M2 的处理是把依赖写进定理签名，让"这个界在什么预算、什么带宽下成立"成为可审计事实，而不是注释里的口头约定。

5. 阶段 M3：存活路径 Shifted-Window 望远镜恒等式

5.1 恒等式与保持性

M3 的主成果是存活路径上**任意平移窗口（shifted window）**的精确对数望远镜恒等式：

Σ_{j = 0}^{count-1} stoppedLog(start + j) = log Z(start + count) − log Z(start)

两条保持性要求同时成立：

• 命中集保留：窗口内的已命中集合（hit set）在望远镜展开过程中原样保留，不被重排丢弃；
• 前缀不重置（no prefix reset）：窗口滑动不把此前累积的对数总量清零，前后端点严格相减。

这一定义把"局部窗口和"与"总暴露对数差"绑定，是后续做删除顺序证明的代数地基。

5.2 失败事件归约与绝对尾界

有限输入下，乘法窗口直接验证会在两类位置失败：护栏失败，或中心计数项出现偏差。归约后更直接地得到绝对失败事件的尾界：

P[Z(length) < exp(-2 · length)] ≤ length · exp(-budget / 2)

重要性质：该绝对失败界不需要新增 drift、codegree（码度）或概率 cap 前提——它由已支付的护栏界直接转运，不额外假设分布结构。

5.3 玩具规模与"不替代"声明

本轮精确玩具检查规模（全部 BigInt 精确、无采样随机数）：

声明：上述计数验证的是恒等式在有限状态集合上的可重放正确性；它不替代通用删除顺序证明。删除顺序（任意 erase-list / order）层面的 law 运输仍在 OPEN 清单中。

6. 当前 OPEN 清单（P0 / P1 行动看板）

按是否阻塞 Gate-1 技术验收分级。P0 未闭合前不进入发布讨论；P1 在 Gate-1 通过后排期。

验收门判定规则：

1. P0 全部闭合且验证器 clean PASS → Gate-1 进入技术验收；
2. 技术验收通过且语义路线具备实施条件 → 有条件续推 Gate-2（最晚节点）；
3. 任一 P0 无法闭合或验收不过 →INCOMPLETE 止损：冻结现状、保留全部成果与基线，不自动前推。

7. 验证体系：clean PASS 口径与可重放检查

7.1 clean PASS 的四个并列条件

7.2 验证器输出形态（脱敏示意）

== baseline check (B3, latest) == theorems : 7 definitions : carried over, no new override whitelist out : 1030 warnings : 0 errors : 0 baseline diff : byte-identical to previous baseline verdict : clean PASS

7.3 发布前自检命令形态（按本机工程替换路径）

# 1. 全量构建：期望零 warning / errorlake build# 2. 白名单审计：输出条目数与基线表核对（M3 = 1030）lake check-whitelist# 3. 精确玩具控制：有限状态全量重放lake check-toy-controls# 4. 基线隔离：期望历史文件零改动，仅新增文件进入差异gitdiff--statprevious-baseline HEAD

7.4 玩具控制的使用规则

• 玩具用精确整数（BigInt），不用随机采样；
• 每个玩具必须绑定一个具体的一般定理命题（局部性、首越界、望远镜相等）；
• 玩具通过只提升信心，不进入结论；结论以一般定理为准。

8. 方法论沉淀：五条可复用法则

1. 证据闭环：每条结论必须挂到已冻结接口与已闭定理；论文对象与模型对象先做 10 项对照审计，再动手接线。
2. 条件不外推：概率界携带全部显式前提（budget、width、length）；前提缺失时停在条件式，不引入外部 cap 救场。
3. 玩具只证局部：精确小状态控制只用于抓接线错误与异常分支，永不冒充渐近证明。
4. 基线只增不重置：新定理增量叠加，历史基线逐字节保持；白名单输出只做审计计数，不做语义膨胀。
5. 未过门不升级：技术接口验收 ≠ 语义结论关闭；未过 Gate-1 不发布、不进方法库、不自动续阶段。

9. 避坑清单（8 条高频误读）

10. 下一步路线与止损原则

10.1 近期行动看板

10.2 止损与放行规则

• 放行：P0 全闭 → clean PASS → Gate-1 技术验收 → 语义路线评估通过 → 有条件进入 Gate-2；
• 止损：验收不过即 INCOMPLETE，冻结当前基线与全部玩具控制记录，问题定位到最小责任单元后再重启；
• 禁止动作：自动 commit、自动发布、定理提前提升方法库、用玩具结果代替一般证明。

10.3 给同行的交流方向

如果你的工作同样涉及"形式化概率证明 + 有限玩具控制"，最值得交流的三个问题是：白名单基线如何审计依赖面、条件概率界如何在签名中显式化、删除顺序证明如何从窗口恒等式逐步运输。欢迎在评论区交换工程口径。

附录 A. 术语对照表