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

Yihe Huang, Sizhe Cui, Jiaqi Wang +1

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 c…