Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4

TL;DR

This paper formalizes combinatorial curve neighborhoods for affine flag manifolds of type $A_1^{(1)}$ in Lean 4, enabling explicit computation and verification of formulas within a rigorous proof assistant framework.

Contribution

It provides the first axiom-free formalization of $A_1^{(1)}$ curve neighborhoods in Lean 4, including explicit formulas and a computable approach.

Findings

Formalized $D_ _ ext{infty}$ as a Coxeter system in Lean 4.

Derived explicit combinatorial formulas for curve neighborhoods.

Developed a fully computable version by restricting to finite sets.

Abstract

Combinatorial curve neighborhoods are somewhat foundational when setting up the quantum Schubert calculus for affine flag manifolds. In the specific case of type $A_1^{(1)}$, you can encode these neighborhoods entirely within the moment graph of the infinite dihedral group $D_\infty$. Building on the framework developed by Mihalcea and Norton, this paper presents a complete, axiom-free formalization of these combinatorial curve neighborhoods in Lean 4. Rather than just wrapping mathematical statements, we formalized $D_\infty$ directly as a Coxeter system to explicitly compute length functions and degree maps. Reachable sets are defined through edge chains bounded by specific degrees, and we ultimately characterize the curve neighborhood by the maximal vertices inside these sets. The core effort here lies in formally verifying the explicit combinatorial formulas for curve neighborhoods of arbitrary elements. Interestingly, by restricting our search space to finite sets, we also managed to extract a fully computable version of these neighborhoods.