Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4
For researchers in quantum Schubert calculus and formal verification, this work provides a foundational formalization of curve neighborhoods, though it is incremental as it applies existing methods to a specific case.
This paper presents a complete, axiom-free formalization of combinatorial curve neighborhoods for type A1(1) in Lean 4, building on the moment graph of the infinite dihedral group. The formalization explicitly computes length functions and degree maps, and provides a fully computable version by restricting to finite sets.
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.