Lean 4 形式化攻坚第三篇：五次 clean PASS 为何仍未过门——坏集损失 producer、合并清洗与排序块均值门
摘要：本篇记录 Phase A（闭合 G6a 四项义务）的五步推进：度偏差坏集损失 producer、行尾与度的合并清洗、方法候选抽取与同案应用、精确八等分均值门、以及把均值门从精确八等分推广到一般有限基数 ranked block。五步全部 clean PASS、零 warning / error，但技术门始终未通过：G6a INCOMPLETE、G6 OPEN，不进入 G6b，不晋级方法库。全文给出每步的显式前提、失败条件、基线计数与仍未闭合清单，强调"clean PASS 是局部证明质量，不是门关闭"。
作者：Valhalla Matrix治理实验室关键词：Lean 4 · 形式化证明 · 坏集损失 · 合并清洗 · 均值门 · 比较族预算 · 验收门 · 反例控制
0. TL;DR（一分钟读完）
- 五步推进、五种成果、一个共同结论：每步都产出可重放定理与依赖输出，但门状态连续保持G6a INCOMPLETE / G6 OPEN / 不进入 G6b。
- 计数链：依赖输出 1073 → 1086 → 1089 → 1092 → 1095；本轮新增定理累计
5 + 9 + 3 + 3 + 3，定义累计1 + 4，全程零诊断信息。 - 两条主线：
- 损失支付线：源 discrepancy → 度偏差坏集 → 双尾质量 / 点数损失 → 比较族（规模 ≤ exp(n^β)、β < η）共同阈值支付；
- 均值门线：精确八等分下"至少 1/8 行达 g/2 中点门" → 一般 ranked block 下只需
3·|top| ≤ |support|等三条前提即推出至少|top|行超中点。
- 纪律样本：方法抽取本轮抽 7 个候选（6 数学 / 1 治理），因跨案例收益NOT_MEASURED，明确不晋级冻结方法库；Fin2 内核反例证明 original-z 不能直接替换 cleaned-z。
- 当前位置：G1–G5 CLOSED；G6a INCOMPLETE；G6 OPEN；G6b 停在语义预检、物理构造未启动；目标问题 PARTIAL / HOLD。
阅读导航：第 1 节 Phase A 定位 → 第 2–6 节五步技术记录 → 第 7 节基线总表 → 第 8 节 OPEN 分组清单 → 第 9 节方法论 → 第 10 节避坑 → 第 11 节行动看板。
1. Phase A 定位：本篇在整个合同中的位置
前两篇分别闭合了窗口望远镜恒等式与移位窗口合成界，并记录了一次主动止损。新合同把后续工作切成两段：
- Phase A：集中闭合 G6a 的四项义务（删除顺序运输、全 slice 有效性合成、物理内部失败覆盖、共同阈值数值预算实例化）；
- Phase B：仅当 Phase A 全过，才启动 G6b 的物理 mesh / cleaned-law 构造。
本篇全部内容属于Phase A 执行段。评价每一步的标准不是"新写了多少定理"，而是它把哪一项义务向前推了多远、还缺什么才能过门。
2. 步骤 P1：度偏差坏集损失 producer
2.1 做了什么
从源 discrepancy（偏差量）出发，构造显式的度偏差坏集，并推出其双尾质量损失与点数损失；当比较族规模满足
|家族| ≤ exp(n^β), 且 β < η共同阈值即可一次性支付这一比较族的总损失。原均匀支持宽度由提取下界导出，且同一剩余支持同时满足全部比较律的度偏差、规模与 codegree 要求。
2.2 关键前提与边界
- 共同阈值支付的前提是指数尺度关系
β < η；尺度关系不满足时不能套用； - 本步只完成other-patch（另一类补丁）度数条件producer；其余三类补丁条件与合计预算未支付。
2.3 基线快照
5 条定理 / 1 条定义，1073 条白名单公理输出，零 warning / error。未闭合：另外三类 / 合计预算、实际补丁与源 discrepancy 的映射、原始 codegree 与 actual hcaps。
3. 步骤 P2：行尾与度的合并清洗（含 Fin2 反例）
3.1 raw-K 行测试
定义 raw-K 行测试：由原始 pair / far 尾 cap 推出加权平均与 Markov 损失；同一个支持同时满足 degree、row、规模、codegree 四类约束——"清洗一次、多处复用"是本步的工程价值。
3.2 预算分离：宽度 η 与行阈值 τ
共同尺度预算被拆成两个独立量：
宽度参数 η ←→ 行阈值 τ两者分别支付，并且明确不要求来源未提供的双侧 n^(1/5) discrepancy。这是"条件不外推"原则的又一次应用：来源没给的前提，不写进定理。
3.3 Fin2 内核反例（重要边界证据）
Fin2 内核反例证明：original-z 不能直接换成 cleaned-z。清洗前后的量不是同义词，直接替换会在该反例上失效。这条反例是后续所有"清洗"步骤必须携带的边界。
3.4 基线快照
9 条定理 / 4 条定义，1086 条白名单公理输出，零 warning / error。未闭合：raw 深层尾界、own-patch 两类 / 四类总预算、实际补丁与源参数映射、actual hcaps。
4. 步骤 P3：方法候选抽取并实际同案应用
4.1 候选卡结构化
本轮抽取7 个待人审候选：6 条数学方法 + 1 条治理方法，每条候选都结构化记录五个字段：
| 字段 | 作用 |
|---|---|
| 前提 | 方法成立所需条件 |
| 失效条件 | 什么情况下不能用 |
| 负路径 | 反面 / 反例方向 |
| 迁移方式 | 从原案例到本案的接线路径 |
| 声明哈希 | 内容版本指纹，防静默漂移 |
4.2 同案消费：第 6 号候选 → direct/uniform 分支
其中第 6 号候选被实际消费到直接 / 均匀分支：把真实矩形密度与行度数均值对齐；缺席大矩形时，显式给出"超限行点数小于正 minimum"的结论。本步新增 3 条定理，1089 项声明依赖输出，零 warning / error，且无新增公理。
4.3 NOT_MEASURED 纪律（容易被忽略的重点）
跨案例收益标注为NOT_MEASURED：候选方法在原案例与本案之间的迁移收益尚未量化，因此不晋级冻结方法库。可复用方法进入方法库的门槛是"收益已测量 + 证据可复现"，而不是"看起来能用"。
未闭合：源 absent-budget（缺席预算）与物理列支持、完整 own-degree 条件。
5. 步骤 P4：精确八等分均值门与抽象矩形预算接口
5.1 定理内容
把论文 direct-bias 小节的 top-eighth（顶部八分之一）加权平均反证及其抽象矩形预算接口形式化为 3 条 Lean 定理。推理链为：
精确八等分 ＋ 排序支配 ＋ top 块 2g 均值门 ＋ 全局 g 偏差见证 ⇒ 至少 1/8 的行达到 g/2 中点门5.2 抽象接口的价值
矩形预算被抽成独立接口，上层均值门结论不绑死在具体矩形实现上，便于后续替换实现层而不重写上层定理。
5.3 基线快照
在既有基线上新增 3 条定理，1092 项声明依赖输出，零 warning / error。未闭合：任意基数下的舍入、论文 absent-2g 预算的大小 / 宽度映射、等边采样、同一 cleaning 上的 lower bound。
6. 步骤 P5：拆除精确八等分限制——一般 ranked block 均值门
6.1 从"1/8"到"|top|"
P4 依赖"精确八等分"这一离散划分；P5 把限制拆掉，面向一般有限基数的 ranked block（排序块），只需三条前提：
① 3·|top| ≤ |support| ② 排序支配（ordering domination） ③ top 均值门（top mean gate） ⇒ 至少 |top| 个中点超限行同时，把所有达到 minimum 的行集的矩形边预算接到固定列 uniform 均值上，完成均值层与均匀列层的对接。
6.2 推广的意义与代价
- 意义：不再要求基数恰好可八等分，适用面扩展到任意有限支持；
- 代价：新引入尺度条件
3·|top| ≤ |support|，并且论文侧的 dyadic（二进）大小 / 宽度量词尚未对齐——推广不能以丢前提为代价。
6.3 基线快照与门裁决
新增 3 条定理，1095 项声明依赖输出，零 warning / error。但技术门裁决为未通过：实际 top-eighth 选取、论文 dyadic 大小 / 宽度量词、源 absent-2g 预算、等边抽取与同支持下界仍未闭合。G6a INCOMPLETE、G6 OPEN，不进入 G6b。
7. 基线演进总表
| 步骤 | 定理 | 定义 | 依赖输出 | 主线成果 | 门状态 | ||||
|---|---|---|---|---|---|---|---|---|---|
| P1 坏集损失 | 5 | 1 | 1073 | 比较族 β<η 共同阈值支付 | G6a INCOMPLETE | ||||
| P2 合并清洗 | 9 | 4 | 1086 | 同支持满足 degree/row/规模/codegree；Fin2 反例 | G6a INCOMPLETE | ||||
| P3 方法抽取 | +3 | — | 1089 | 7 候选结构化；第 6 号候选同案消费；无新增公理 | G6a INCOMPLETE | ||||
| P4 八等分均值门 | +3 | — | 1092 | ≥1/8 行达 g/2；矩形预算抽象接口 | G6a INCOMPLETE | ||||
| P5 一般 ranked block | +3 | — | 1095 | 3 | top | ≤ | support | 推广；边预算接 uniform 均值 | 技术门未过 |
口径备注：P1/P2 使用"白名单公理输出"口径，P3–P5 使用"声明依赖输出"口径；两者都是允许依赖的审计计数，不与定理数混算。
8. OPEN 分组清单（Phase A 剩余义务）
按技术主题归并，避免把缺口散落在五份记录里。
8.1 预算映射类（缺口最大）
| 缺口 | 关联步骤 |
|---|---|
| 源 absent-budget / absent-2g 预算的大小–宽度映射 | P3 / P4 / P5 |
| 比较族 total loss 的合计预算支付 | P1 |
| own-patch 两类 / 四类总预算 | P2 |
| 实际补丁 ↔ 源 discrepancy / 源参数映射 | P1 / P2 |
8.2 支持与 codegree 类
| 缺口 | 关联步骤 |
|---|---|
| 原始 codegree 与 actual hcaps | P1 / P2 |
| 同一支持上的 lower bound | P4 / P5 |
| 完整 own-degree 条件；物理列支持 | P3 |
8.3 选择、采样与量词对齐类
| 缺口 | 关联步骤 |
|---|---|
| 实际 top-eighth 选取；任意基数舍入 | P4 / P5 |
| 等边采样 / 等边抽取 | P4 / P5 |
| 论文 dyadic 大小 / 宽度量词与形式化侧对齐 | P5 |
8.4 尾界类
| 缺口 | 关联步骤 |
|---|---|
| raw 深层尾界（区别于已支付的加权平均 / Markov 损失） | P2 |
9. 方法论增量
- 推广先声明新增尺度条件：把"精确八等分"一般化时，新前提
3·|top| ≤ |support|必须显式进签名；推广 ≠ 放松。 - 清洗量不得裸替换：Fin2 反例说明 original-z 与 cleaned-z 有本质差异，跨层引用必须带清洗映射假设。
- 候选方法先入库观察、量化后晋级：候选卡五字段 + 声明哈希；收益 NOT_MEASURED 不进冻结方法库。
- 预算分账：宽度 η 与行阈值 τ 分开支付；来源未提供的 discrepancy 不假设。
- clean PASS ≠ 过门：局部证明质量合格（计数、零告警、基线保持）与门义务闭合是两套标准，本五步是连续示范。
10. 避坑清单（本篇 8 条）
| \# | 误读 | 正确理解 |
|---|---|---|
| 1 | “1095 输出说明证明很完整” | 输出是依赖审计计数；G6a 义务清单仍多项未付 |
| 2 | “Fin2 反例推翻了合并清洗” | 它只否定 original-z→cleaned-z 的直接替换；清洗本身成立 |
| 3 | “方法候选可以进方法库复用” | 收益 NOT_MEASURED，冻结库不接收 |
| 4 | “一般 ranked block 不需要 1/8 条件了” | 换成 `3 |
| 5 | “β<η 只是技术细节” | 它决定比较族总损失是否可被共同阈值支付，是支付资格条件 |
| 6 | “矩形预算接口可以脱离论文量词” | dyadic 量词未对齐前，接口只是形式层闭合 |
| 7 | “新增定理多 = 进度快” | 进度按 OPEN 缺口收敛度量，不按定理行数度量 |
| 8 | “P5 成功即可进 G6b” | G6b 启动要求 Phase A 全过；当前仅执行中 |
11. Phase A 剩余行动看板
| 动作 | 分组 | 完成判据 |
|---|---|---|
| 闭合 absent-2g / absent-budget 大小–宽度映射 | 预算映射 | 预算接口与论文量词双向对齐 |
| 支付比较族合计损失与 own-patch 总预算 | 预算映射 | 全部比较类共用一个总预算界 |
| 补齐原 codegree / actual hcaps 与同支持下界 | 支持 codegree | 消除外部 hcaps 依赖 |
| 完成实际 top 选取、舍入与等边抽取 | 采样量词 | 形式化选择规则对齐论文 dyadic 量词 |
| 补 raw 深层尾界 | 尾界 | 深层 tail 由显式 cap 支付 |
| Phase A 总验收 | — | 四类缺口清零 + clean PASS 方可放行 Phase B |
附录 A. 术语对照（本篇新增）
| 术语 | 含义 |
|---|---|
| bad set producer | 由源偏差显式产出坏集并计算其损失的构造 |
| comparison family | 一族比较对象；其规模 ≤ exp(n^β)、β<η 时可共用阈值支付 |
| raw-K row test | 基于原始尾部 cap 的行级加权平均 / Markov 测试 |
| Fin2 反例 | 否定清洗前后量直接互换的内核见证 |
| top-eighth | 排序后顶部八分之一块；均值门的原始离散划分 |
| ranked block / mean gate | 一般有限基数排序块与其顶部均值门槛 |
| NOT_MEASURED | 跨案例收益未量化，禁止晋级冻结方法库的标注 |
| hcaps | 外部列表上界控制量；未消除前相关结论保持条件式 |
