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

तकनीकी सारांश: Lean 4 में $A_1^{(1)}$ वक्र परिवेशों (Curve Neighborhoods) का औपचारिककरण

समस्या विवरण

एफाइन फ्लैग मैनिफोल्ड्स के क्वांटम शूबर्ट कैलकुलस (quantum Schubert calculus) के अध्ययन में, संयोजन वक्र परिवेश (combinatorial curve neighborhoods) मौलिक ज्यामितीय वस्तुएं हैं। विशेष रूप से $A_1^{(1)}$ के मामले में, इन परिवेशों को अनंत डायहेड्रल समूह $D_\infty$ के मोमेंट ग्राफ (moment graph) के भीतर एनकोड किया जा सकता है। हालांकि इन परिवेशों के लिए स्पष्ट संयोजन सूत्र (विशेष रूप से मिहाल्शिया और नॉर्टन द्वारा) मौजूद हैं, लेकिन उनके प्रमाण जटिल संयोजन तर्कों—जैसे कि पैरिटी चेक (parity checks), शब्द लंबाई सत्यापन (word length verifications), और ब्रुअट ऑर्डर (Bruhat order) हेरफेर—पर आधारित हैं, जिनमें मानवीय त्रुटि की संभावना बनी रहती है। मुख्य चुनौती इन परिवेशों और उनके शासी सूत्रों का एक कठोर, मशीन-चेक्ड औपचारिककरण (formalization) प्रदान करना है।

कार्यप्रणाली

लेखक एक पूर्ण, बिना-स्वयंसिद्ध (axiom-free) औपचारिककरण बनाने के लिए Lean 4 और Mathlib का उपयोग करते हैं। उनका दृष्टिकोण एक पदानुदीय निर्माण का अनुसरण करता है:

1. बीजगणितीय आधार: $D_\infty$ को एक साधारण समूह के रूप में मानने के बजाय, वे इसे $\text{Fin } 2$ पर एक विशिष्ट कॉक्स टर सिस्टम (Coxeter matrix) को परिभाषित करके एक CoxeterSystem इंस्टेंस प्रदान करते हैं। यह उन्हें अमूर्त कॉक्स टर सिद्धांत का लाभ उठाने और साथ ही सीधे ज्यामितीय समूह से जुड़े रहने की अनुमति देता है।
2. रचनात्मक लंबाई फलन (Constructive Length Functions): गैर-रचनात्मक अमूर्त परिभाषाओं और व्यावहारिक गणना के बीच के अंतर को पाटने के लिए, वे जेनरेटर्स ($s_0, s_1$) के वैकल्पिक अनुक्रमों पर आधारित एक explicit_length फलन लागू करते हैं। वे औपचारिक रूप से सिद्ध करते हैं कि यह रचनात्मक फलन अमूर्त कॉक्स टर लंबाई के समकक्ष है।
3. ग्राफ-सैद्धांतिक मॉडलिंग: मोमेंट ग्राफ को HasIncreasingChain की एक आगमनात्मक (inductive) परिभाषा का उपयोग करके मॉडल किया गया है, जहाँ किनारे (edges) रूट रिफ्लेक्शन द्वारा परिभाषित होते हैं और डिग्री को घटक-वार योज्य मोनोइड (component-wise additive monoid) के माध्यम से ट्रैक किया जाता है।
4. अंकगणितीय न्यूनीकरण (Arithmetic Reduction): पैरिटी लेम्मा (जो अक्सर अनौपचारिक प्रमाणों में सहजता से संभाले जाते हैं) को संभालने के लिए, लेखक ज्यामितीय बाधाओं को $\mathbb{N}$ में प्रेसबर्गर अंकगणित (Presburger arithmetic) में कम करते हैं। यह जटिल रैखिक अंकगणितीय लक्ष्यों को हल करने के लिए Lean के omega टैक्टिक का उपयोग करने की अनुमति देता है।
5. संगणनात्मक सेतु (Computational Bridge): अस्तित्व संबंधी प्रमाणों से वास्तविक गणना की ओर बढ़ने के लिए, वे तर्क के एक "संगणनीय स्लाइस" (computable slice) को लागू करते हैं। $A_d(u)$ के तत्वों की कॉक्स टर लंबाई पर स्पष्ट सीमाएं स्थापित करके, वे अनंत खोज स्थानों को परिमित सेटों (Finset) में बदल देते हैं, जिससे प्रत्यक्ष गणना के लिए #eval का उपयोग सक्षम होता है।

मुख्य योगदान

• बिना-स्वयंसिद्ध औपचारिककरण: एक पूर्ण Lean 4 लाइब्रेरी जो $D_\infty$ को एक कॉक्स टर सिस्टम के रूप में परिभाषित करती है और अंतर्निहित मोमेंट ग्राफ को औपचारिक बनाती है।
• मुख्य लेम्मा का सत्यापन: पैरिटी ऑफ चेन्स (Parity of Chains) लेम्मा का औपचारिक प्रमाण, जो यह निर्धारित करता है कि मोमेंट ग्राफ में किनारों के माध्यम से डिग्री कैसे संचित होती है।
• मुख्य प्रमेय का प्रमाण: वक्र परिवेश $\Gamma_d(u)$ के लक्षण वर्णन के रूप में बीजगणितीय रूप से परिभाषित सेट $A_d(u)$ (गुना $u$) के अधिकतम तत्वों के सेट के रूप में चरित्र चित्रण का एक मशीन-चेक्ड प्रमाण।
• निष्पादन योग्य कार्यान्वयन: वक्र परिवेश एल्गोरिदम का एक पूरी तरह से सत्यापित, संगणनीय संस्करण विकसित करना जिसे Lean वातावरण के भीतर निष्पादित किया जा सकता है।

परिणाम

औपचारिककरण सफलतापूर्वक मिहाल्शिया और नॉर्टन के परिणामों को पुनः प्राप्त और सत्यापित करता है। विशेष रूप से:

• लेखकों ने सिद्ध किया कि वक्र परिवेशों की अमूर्त परिभाषा (ग्राफ पहुंच पर आधारित) बीजगणितीय परिभाषा (लंबाई और डिग्री पर आधारित) के समकक्ष है।
• कार्यान्वयन परिवेशों की तात्कालिक गणना की अनुमति देता है। उदाहरण के लिए, सिस्टम सही ढंग से $\Gamma_{\langle 2,2 \rangle}(1) = \{r(2), r(-2)\}$ और $\Gamma_{\langle 2,3 \rangle}(s_0) = \{sr(-3)\}$ का मूल्यांकन करता है, जो ज्ञात गणितीय अपेक्षाओं से मेल खाता है।

महत्व

यह कार्य प्रदर्शित करता है कि जटिल संयोजन ज्यामिति और क्वांटम शूबर्ट कैलकुलस औपचारिक सत्यापन के योग्य हैं। उच्च-स्तरीय ज्यामितीय तर्क को निम्न-स्तरीय सूची हेरफेर (list manipulation) और संगणनात्मक निष्पादन के साथ सफलतापूर्वक जोड़कर, यह शोध पत्र अन्य काक-मीडर (Kac-Moody) समूह संरचनाओं को औपचारिक बनाने के लिए एक ब्लूप्रिंट प्रदान करता है। यह एक पुन: प्रयोज्य, यांत्रिक रूप से सत्यापित ढांचा प्रदान करता है जो बीजगणितीय परिवेशों की गणना में पूर्ण निश्चितता सुनिश्चित करता है, जो क्वांटम K-थ्योरी और प्रतिनिधित्व सिद्धांत (representation theory) में आगे के अनुसंधान के लिए महत्वपूर्ण है।