Scott《连续格》(1972) 的 Lean 4 形式化

我们呈现了 Dana Scott 具有里程碑意义的 1972 年论文《连续格》\textbf{[Sco72]} 的完整机器检查形式化，该工作在 Lean 4 中针对 mathlib 完成，并包含了 \textbf{[Sco72]}（第 135--136 页）中 1972 年 3 月的 Milner 修正。Scott 的论文从拓扑起点出发发展了 $\lambda$-演算的模型。他定义了内射 $T_0$-空间——即对连续映射具有强扩张性质的空间——并证明它们恰好就是连续格：其 Scott 拓扑由远低于关系（$\ll$）通过序确定的完备格。在此基础之上，他研究了投影、收缩、积、函数空间和逆极限。作为顶点（定理 4.4），他构造了函数空间逼近元的逆极限 $D_\infty$ 并证明了 $D_\infty \cong [D_\infty \to D_\infty]$，从而为 Church 的无类型 $\lambda$-演算提供了一个纯数学模型。我们的开发形式化了 Scott 第 1--4 节中的 \textbf{43 个编号结果}（命题、推论、引理和定理），每一个都作为无 sorry 的 Lean 定理实现，并附带了支持性基础设施（阶梯函数、Scott 开集的 $\Uparrow a$ 基、Milner 的粗于 Scott 假设、函数空间塔以及 $i_\infty$/$j_\infty$ 对）。该形式化是经典的（传递性地使用了 \texttt{Classical.choice}）并遵循 Scott 的证明依赖顺序。在 Lean 证明需要原论文中不可见的选择——或遇到死胡同的地方——我们在第 5 节记录了详细的说明。所有证明均在标准基址 $\texttt{[propext, Classical.choice, Quot.sound]}$ 下通过检查。