# 证明命名迁移基线

本文档记录源码命名重构前的稳定快照。统计只覆盖 Git 跟踪的 Lean 文件，
排除 `.lake` 和其他构建产物；字节数把换行统一为 LF 后按无 BOM UTF-8 计算，
避免 CRLF 差异掩盖真实的命名变化。命名规则见 [ProofNaming.md](ProofNaming.md)。

## 基线快照

| 项目 | 数值 |
| --- | ---: |
| 测量日期 | 2026-09-07 |
| 基线提交 | `2b83adc` |
| Git 跟踪的 Lean 文件 | 29 |
| LF 归一化 UTF-8 字节 | 1,203,365 |
| LF 归一化源码行 | 28,805 |

## 最大模块

| 文件 | 工作区字节 | 行数 |
| --- | ---: | ---: |
| `PcfProject/CanonicalProduct.lean` | 299,641 | 7,055 |
| `PcfProject/Stationary.lean` | 114,829 | 3,064 |
| `PcfProject/RankClosureConstruction.lean` | 109,002 | 2,335 |
| `PcfProject/PcfTransitiveGenerators.lean` | 103,109 | 2,092 |
| `PcfProject/LocalRank.lean` | 63,077 | 1,537 |

大文件不作为首批迁移目标。命名迁移按依赖自底向上进行，优先选择小型、
完整、调用面可穷尽的公开接口。每批必须同步更新全部调用点，不保留旧名别名，
并在完整 `lake build` 通过后记录新快照。

## 第一批：主超滤接口

目标模块为 `PcfProject/PrincipalPcf.lean`。迁移将“所有超滤为主”改为可作为
命名空间的数学谓词 `AllUltrafiltersPrincipal`，并将其唯一公开定理改为
`AllUltrafiltersPrincipal.pcf_below_alephOmega4`。新名不再重复规范表示的实现名，
而是由命名空间表达前件、定理词根表达结论。

迁移同时覆盖有限指标集给出的标准见证：
`AllUltrafiltersPrincipal.of_finite`。旧谓词名、旧定理名及全部旧调用点均已删除，
没有加入兼容别名。

## 第一批完成快照

| 项目 | 数值 | 相对基线 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 29 | 0 |
| LF 归一化 UTF-8 字节 | 1,203,683 | +318 |
| LF 归一化源码行 | 28,816 | +11 |

本批增加的 11 行均为命名空间边界和面向读者的语义注释，不是证明包装层。
默认构建通过 1017/1017 个任务；核心定理的公理集合保持为
`propext`、`Classical.choice`、`Quot.sound`。

## 第二批：模块职责说明

基础接口与关键构造模块的标题改为数学职责，不再沿用开发阶段编号；说明文字
删除“旧骨架”“占位符”等实现历史，只保留结论、前提与未覆盖范围。此批没有
改动任何 Lean 声明或证明项。

| 项目 | 数值 | 相对第一批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 29 | 0 |
| LF 归一化 UTF-8 字节 | 1,203,096 | -587 |
| LF 归一化源码行 | 28,808 | -8 |

默认构建再次通过 1017/1017 个任务。

## 第三批：无警告基础接口

把两处已弃用的 Mathlib API 更新为当前等价接口，并按 Lean 检查器建议精简三处
证明表达。四个受影响模块分别通过检查，全库构建也未再报告这些警告。

| 项目 | 数值 | 相对第二批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 29 | 0 |
| LF 归一化 UTF-8 字节 | 1,202,939 | -157 |
| LF 归一化源码行 | 28,807 | -1 |

所有定理类型保持不变；核心定理的公理集合仍为 `propext`、
`Classical.choice`、`Quot.sound`。

## 第四批：基数集合和值的大小写

将四个返回集合或基数的公开定义统一为函数和值的小驼峰命名：
`InterCardSet` 改为 `interCardSet`，`UnionCardSet` 改为 `unionCardSet`，
`FinsetUnionCardSet` 改为 `finsetUnionCardSet`，`ContinuumAtAlephOmega`
改为 `continuumAtAlephOmega`。这些声明不是类型、结构或主要谓词，因此不应使用
大驼峰；数学含义及全部定理类型均未改变。旧名称和旧调用点已全部删除，未增加
兼容别名。

| 项目 | 数值 | 相对第三批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 29 | 0 |
| LF 归一化 UTF-8 字节 | 1,202,939 | 0 |
| LF 归一化源码行 | 28,807 | 0 |

本批只改变同长度标识符的首字母大小写，所以源码规模不变。默认构建通过
1017/1017 个任务；核心定理的公理集合仍为 `propext`、
`Classical.choice`、`Quot.sound`。

## 第五批：数据构造器命名

自动命名检查找出六个采用定理式下划线名称的数据构造器。它们统一改为
`lowerCamelCase`：商尺度构造器改为 `CardinalProductQuotientScale.ofScale`，
五个一致子集覆盖构造器改为 `uniformSubsetCoverOf...`。对应的存在性定理继续
使用下划线名称，以明确区分“证明存在”与“选择一个非可计算见证”。旧构造器名
及旧调用点均已删除，没有兼容别名。

| 项目 | 数值 | 相对第四批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 29 | 0 |
| LF 归一化 UTF-8 字节 | 1,202,884 | -55 |
| LF 归一化源码行 | 28,807 | 0 |

项目级 `defsWithUnderscore` 检查已无报错；直接依赖模块均已重新生成并通过。

## 第六批：核心语义注释

为四个基础模块中直接决定最终定理含义的 21 个公开抽象补充简短 docstring，覆盖
基数集合、PCF 表示、目标基数、点态界、生成子系统和最大 PCF 见证。每条注释
说明对象“是什么”或命题“断言什么”，不复述 tactic 步骤，也不把条件性结论描述
为无条件结论。本批只增加注释，所有声明类型与证明项保持不变。

| 项目 | 数值 | 相对第五批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 29 | 0 |
| LF 归一化 UTF-8 字节 | 1,204,409 | +1,525 |
| LF 归一化源码行 | 28,828 | +21 |

注释增量被限制在核心入口，而不是为消除检查器提示给每个内部实现机械加说明。

## 第七批：约化积与真共尾度语义

为 `IdealProduct` 与 `TcfScale` 的核心关系补充语义 docstring：理想的包含、等价、
真性与“最终成立”，约化积框架及其元素、最终比较、尺度和精确上界。注释特别
区分约化积预序的非对称严格部分与逐坐标最终严格关系；后者才是在扩大理想时
保持的关系。此批不改变声明类型或证明项。

| 项目 | 数值 | 相对第六批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 29 | 0 |
| LF 归一化 UTF-8 字节 | 1,205,591 | +1,182 |
| LF 归一化源码行 | 28,843 | +15 |

## 第八批：删除 Theorem 24.16 的未接线替代路线

删除五个没有进入默认证明链的命题接口及其五个条件转换定理：非稳理想尺度、
顶部精确上界、共尾族、尺度上界和有向共尾上界。它们只表达“若给出这一替代
输入，则可推出已经另行证明的结论”，没有被核心定理或其他模块调用。

实际路线保持为：由已证明的 Lemma 24.10 构造基本序列尺度，再传递到包含所有
俱乐部的超滤对偶理想。同期修正 `CanonicalProduct` 中已经过期的模块边界说明；
没有改变任何保留声明的类型或证明项。

| 项目 | 数值 | 相对第七批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 29 | 0 |
| LF 归一化 UTF-8 字节 | 1,194,737 | -10,854 |
| LF 归一化源码行 | 28,621 | -222 |

默认构建通过 1017/1017 个任务；核心定理的公理集合保持为 `propext`、
`Classical.choice`、`Quot.sound`。

## 第九批：集中公开成果的公理审计

将 528 个分散在证明模块中的 `#print axioms` 命令收束到新的
`PcfProject.AxiomAudit`。集中模块逐项检查 `TROPHIES.md` 的九个公开成果，仍由
默认入口导入；因此信任边界没有缩小，而构建日志不再重复打印数百个内部引理。
删除命令时同时合并其留下的重复空行，没有改动声明、定理类型或证明项。

| 项目 | 数值 | 相对第八批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | +1 |
| LF 归一化 UTF-8 字节 | 1,160,333 | -34,404 |
| LF 归一化源码行 | 27,464 | -1,157 |

默认构建通过 1018/1018 个任务。九个公开成果的公理集合均未超出
`propext`、`Classical.choice`、`Quot.sound`。

## 第十批：压平小颜色集稳纤维包装族

保留“小于环境共尾度的稳集并族必有一个稳分量”这一核心引理，以及项目真正
使用的“小颜色集着色在某个稳子集上为常值”结论。删除二者之间 19 个只改变
存在见证返回格式、且仓库外没有调用者的包装定理；最终结论改为直接调用核心
引理。保留结论的陈述和数学含义不变。

| 项目 | 数值 | 相对第九批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | 0 |
| LF 归一化 UTF-8 字节 | 1,145,666 | -14,667 |
| LF 归一化源码行 | 27,053 | -411 |

默认构建通过 1018/1018 个任务；集中审计的九个公开成果仍只依赖
`propext`、`Classical.choice`、`Quot.sound`。

## 第十一批：压平对角俱乐部稳纤维包装族

保留对角俱乐部假设下的稳纤维核心证明，以及秩闭包模块实际调用的小初段
Fodor 结论。后者直接组合“小初段给出对角共尾性”“对角共尾性给出对角
俱乐部性”和核心稳纤维定理；删除其间 25 个无人调用、仅改变见证附加字段的
包装结论。保留入口的陈述和前提不变。

| 项目 | 数值 | 相对第十批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | 0 |
| LF 归一化 UTF-8 字节 | 1,130,311 | -15,355 |
| LF 归一化源码行 | 26,635 | -418 |

默认构建通过 1018/1018 个任务；九项集中公理审计保持不变。

## 第十九批：删除孤立的尺度与共尾度投影

删除 19 个全仓只服务于自身声明的辅助端点，包括正则非平稳理想、重索引
乘积、统一子集覆盖、局部秩，以及商尺度到较弱存在性结论的包装。保留所有
实际调用的源级构造：Zorn 超滤扩张、推前真共尾度、商尺度构造、一般最大
PCF 见证的阿列夫指标等式，以及最终定理使用的俱乐部和尺度结论。

本批先发现一次自动范围切分错误并整批回滚；随后把候选拆成单声明步骤，手工
核对下一条顶层命令和文件末尾。每个代码步骤都独立完成一次 1018/1018 全量
构建后才提交，因此任一提交均是可复核的稳定证明状态。

| 项目 | 数值 | 相对第十八批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | 0 |
| LF 归一化 UTF-8 字节 | 1,041,284 | -17,969 |
| LF 归一化源码行 | 24,669 | -432 |

默认构建通过 1018/1018 个任务；九项集中公理审计保持不变。

## 第二十批：收束递归暴露的孤立分支

在删除第十九批端点后重新计算引用，继续逐层移除随之失去调用者的中间包装：
普通序数严格链、eventual 坐标短族、重索引推前尺度、正则基数专用非平稳
理想，以及商尺度到 PCF 成员的投影。每删除一层便重新全量构建，再检查上游
是否仍有独立调用，避免一次性裁掉共享基础设施。

保留三条虽不作为内部调用点、但直接解释数学结构的刻画性定理：原始尺度与
商尺度的存在等价、正则长度真共尾度与商序共尾度等价，以及生成器给出的局部
Corollary 24.30。它们是面向人工复核的语义接口，不按“引用一次”规则删除。

| 项目 | 数值 | 相对第十九批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | 0 |
| LF 归一化 UTF-8 字节 | 1,022,189 | -19,095 |
| LF 归一化源码行 | 24,227 | -442 |

本批每个代码提交均通过 1018/1018 个任务；九项集中公理审计保持不变，且
源码中没有 `sorry`、`admit`、新增 `axiom` 或 `constant`。

## 第十八批：删除弱版本的局部上界接口

删除四个全仓只出现于自身声明的弱版本：后继 aleph 的两个局部尺度界、一个
闭原则尺度入口，以及一个精确上界的共尾子结论。实际使用的后继 aleph 版本、
局部化闭精确上界构造和超滤扩张结论保持不变。

| 项目 | 数值 | 相对第十七批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | 0 |
| LF 归一化 UTF-8 字节 | 1,059,253 | -6,180 |
| LF 归一化源码行 | 25,101 | -123 |

默认构建通过 1018/1018 个任务；九项集中公理审计保持不变。

## 第十七批：保留俱乐部限制与正规递归版本

删除 `Stationary` 中已被更强源级版本取代的六个无人调用定理：同宇宙不可注入
特例、普通严格单调反证、三层普通小值重复坐标包装，以及非连续推进序列。
主线使用的宇宙提升不可注入定理、俱乐部限制重复坐标矛盾和正规推进序列全部
保留。

| 项目 | 数值 | 相对第十六批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | 0 |
| LF 归一化 UTF-8 字节 | 1,065,433 | -9,512 |
| LF 归一化源码行 | 25,224 | -221 |

默认构建通过 1018/1018 个任务；九项集中公理审计保持不变。

## 第十六批：收束未使用的 PCF 接口包装

删除 13 个全仓只在自身声明处出现的 PCF 接口定理。它们把已有的尺度、商
共尾度或坐标上界改写成不同的成员资格与基数不等式格式，但没有调用者。
保留实际使用的 `mem_pcf_iff`、尺度见证、坐标乘积上界和最终共尾度估计。

| 项目 | 数值 | 相对第十五批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | 0 |
| LF 归一化 UTF-8 字节 | 1,074,945 | -14,829 |
| LF 归一化源码行 | 25,445 | -304 |

默认构建通过 1018/1018 个任务；九项集中公理审计保持不变。

## 第十五批：删除已被源级构造取代的特例

删除六个全仓只出现一次的特例或旧中间构造：无 support 的闭坐标抽取、两种
旧失败递归、全坐标共尾度包装、一个奇异下界推论和一个非严格 PCF 下界推论。
保留的源级 support 定理、带指定最终集的坐标抽取以及主线使用的严格 PCF
下界均不变。

| 项目 | 数值 | 相对第十四批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | 0 |
| LF 归一化 UTF-8 字节 | 1,089,774 | -13,363 |
| LF 归一化源码行 | 25,749 | -277 |

默认构建通过 1018/1018 个任务；九项集中公理审计保持不变。

## 第十四批：删除两条陈旧的替代支路

删除一个无人调用的 `omega_1` 型俱乐部共尾子序构造，以及一个无人调用的
约化积精确上界分解。两处旧注释曾称其服务于后续反射或分解步骤，但当前证明
链已使用更直接的构造；全文引用核验表明两声明都只在定义位置出现。

| 项目 | 数值 | 相对第十三批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | 0 |
| LF 归一化 UTF-8 字节 | 1,103,137 | -5,944 |
| LF 归一化源码行 | 26,026 | -141 |

默认构建通过 1018/1018 个任务；九项集中公理审计保持不变。

## 第十三批：删除孤立的商共尾度估计

删除两个只有定义位置出现的商共尾度下界变体，以及一个无人调用的闭精确上界
基数估计。保留证明链实际使用的正则商共尾度定理和
`lift_cardinal_le_of_cofinalBelow` 版本；没有改动任何调用点。

| 项目 | 数值 | 相对第十二批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | 0 |
| LF 归一化 UTF-8 字节 | 1,109,081 | -6,454 |
| LF 归一化源码行 | 26,167 | -149 |

默认构建通过 1018/1018 个任务；九项集中公理审计保持不变。

## 第十二批：保留唯一接线的支配阶段定理

`CanonicalProduct` 的五个支配阶段版本中，后续构造只使用带显式 support 的
源级定理。删除三个独立但无人调用的早期版本，以及由 support 定理立即推出、
同样无人调用的全坐标包装。实际使用的定理及其源级语义注释保持不变。

| 项目 | 数值 | 相对第十一批 |
| --- | ---: | ---: |
| Git 跟踪的 Lean 文件 | 30 | 0 |
| LF 归一化 UTF-8 字节 | 1,115,535 | -14,776 |
| LF 归一化源码行 | 26,316 | -319 |

默认构建通过 1018/1018 个任务；九项集中公理审计保持不变。