在 Lean 4 中形式化 $A_1^{(1)}$ 曲线邻域

组合曲线邻域在为仿射旗形流形建立量子 Schubert 微积分时具有一定基础性。在 $A_1^{(1)}$ 类型情况下，这些邻域可完全编码于无限双面群 $D_\infty$ 的moment图中。基于 Mihalcea 与 Norton 开发的框架，本文在 Lean 4 中对这些组合曲线邻域进行完整、无公理化的形式化。与仅包装数学陈述不同，我们直接将 $D_\infty$ 形式化为 Coxeter 系统，以显式计算长度函数与度映射。通过由特定度数界限的边链定义可达集，最终以这些集合中最大顶点来特征化曲线邻域。此工作的核心在于形式化验证任意元素的曲线邻域的显式组合公式。有趣的是，通过限制搜索空间为有限集，我们还成功提取了这些邻域的可计算版本。