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

Yihe Huang; Sizhe Cui; Jiaqi Wang; Jujian Zhang

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

Yihe Huang, Sizhe Cui, Jiaqi Wang, Jujian Zhang

arXivarxiv/2604.23211Apr 25, 2026math.COscore 0

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…

Source JSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/arxiv/2604.23211
curl -X POST /api/v1/records/arxiv/2604.23211/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2604.23211/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'