Formalizing A1(1) Curve Neighborhoods in Lean 4. - Yihe Huang; Sizhe Cui; Jiaqi Wang; Jujian Zhang (CoRR, 2026)