Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4

कल्पना कीजिए कि आप एक पुस्तकालय के एक कुशल संग्रहकर्ता (archivist) हैं जहाँ हर किताब संख्याओं से बनी एक विशाल, जटिल पहेली है। कभी-कभी, आपको नीचे छिपे एक सरल पैटर्न को खोजने के लिए इन पहेलियों के पन्नों को फिर से व्यवस्थित करने की आवश्यकता होती है। यह लीनियर अलजेब्रा (linear algebra) की दुनिया है, जो गणित की एक शाखा है जो संख्याओं के ग्रिड (जिन्हें मैट्रिक्स कहा जाता है) और उनके रूपांतरण से संबंधित है। एक मैट्रिक्स को पूर्णांकों (integers) के स्प्रेडशीट के रूप में सोचें। जिस तरह आप एक अव्यवस्थित नामों की सूची को वर्णानुक्रम में व्यवस्थित कर सकते हैं ताकि एक पैटर्न मिल सके, गणितज्ञ इन संख्या ग्रिडों को "स्मिथ नॉर्मल फॉर्म" (Smith Normal Form) में व्यवस्थित करने का प्रयास करते हैं—एक अत्यंत स्वच्छ, विकर्ण (diagonal) संस्करण जहाँ संख्याएँ जैसे-जैसे आप नीचे जाते हैं, बढ़ती जाती हैं और प्रत्येक संख्या अगली संख्या को पूरी तरह से विभाजित करती है।

लेकिन यहाँ एक पेच है: जबकि संख्याओं को व्यवस्थित करना वर्णन करना आसान है, वास्तव में गणित करना एक दुःस्वप्न हो सकता है। जैसे ही आप ग्रिड को साफ करने के लिए पंक्तियों (rows) और स्तंभों (columns) को इधर-उधर करते हैं, अंदर की संख्याएँ इतनी विशाल हो सकती हैं कि वे आपके कंप्यूटर को क्रैश कर दें या गणना करने में लाखों साल लगा दें। दशकों से, गणितज्ञ जानते थे कि इन ग्रिडों को कैसे व्यवस्थित किया जाए (एक विधि जिसे कन्नन-बामेच (Kannan–Bachem) एल्गोरिदम कहा जाता है), लेकिन उन्हें पूरी तरह से आश्वस्त होने की आवश्यकता थी कि यह प्रक्रिया अनंत लूप में नहीं फँसेगी और संख्याएँ नियंत्रण से बाहर नहीं होंगी। यह शोध पत्र इसी कमी को पूरा करता है, न केवल यह कहने के लिए कि "यह काम करता है," बल्कि यह बनाने के लिए कि यह एक डिजिटल, अटूट प्रमाण है कि यह काम करता है, और यह गिनने के लिए कि इसे करने में कितनी "कंप्यूटेशनल ऊर्जा" लगती है।

डिजिटल दोहरा जाँच (The Digital Double-Check)

इस शोध पत्र में, वॉशिंगटन विश्वविद्यालय के जुनी जी (Junye Ji) कन्नन-बामेच एल्गोरिदम—जो पूर्णांक मैट्रिसेस को व्यवस्थित करने की एक चतुर विधि है—को लेते हैं और लीन 4 (Lean 4) नामक उपकरण का उपयोग करके इसका एक मशीन-चेक किया गया प्रमाण तैयार करते हैं। लीन 4 को एक अत्यंत सख्त, रोबोटिक लाइब्रेरियन के रूप में सोचें जो किसी गणितीय प्रमाण को तब तक स्वीकार करने से इनकार कर देता है जब तक कि उसका हर एक कदम तार्किक रूप से अचूक न हो। यदि आप इसमें "शायद" या "यह शायद काम करेगा" जैसा कुछ डालने की कोशिश करते हैं, तो रोबोट दरवाजा बंद कर देता है। जी ने केवल कोड नहीं लिखा; उन्होंने रोबोट को यह सत्यापित करने के लिए मजबूर किया कि कोड हमेशा समाप्त होता है, कभी क्रैश नहीं होता, और हर बार बिल्कुल सही उत्तर देता है।

लक्ष्य यह सिद्ध करना था कि किसी भी गैर-शून्य पूर्णांकों के वर्गाकार ग्रिड के लिए, यह एल्गोरिदम इसे अपने स्वच्छ, विकर्ण "स्मिथ नॉर्मल फॉर्म" में बदल सकता है और साथ ही वहाँ तक पहुँचने के लिए किए गए सटीक कदमों का भी हिसाब रख सकता है। परिणाम केवल एक "हाँ, यह काम करता है" वाला नोट नहीं है; यह एक पूर्ण, सत्यापित पैकेज है जिसमें अंतिम व्यवस्थित ग्रिड, वहाँ तक पहुँचने का "फॉरवर्ड" मैप, और वापस मूल स्थिति में आने का "बैकवर्ड" मैप शामिल है। यह एक खजाने के नक्शे और वापसी के टिकट की तरह है, दोनों को एक रोबोट द्वारा यह सुनिश्चित करने के लिए सत्यापित किया गया है कि आप विशाल संख्याओं के जंगल में खो न जाएँ।

"पिवट" नृत्य और घटती संख्याएँ (The "Pivot" Dance and the Shrinking Numbers)

एल्गोरिदम का हृदय स्थिरीकरण (stabilization) नामक एक नृत्य है। कल्पना कीजिए कि आप एक अस्त-व्यस्त कमरे को व्यवस्थित करने की कोशिश कर रहे हैं। आप फर्श पर एक विशिष्ट स्थान (पिवट) चुनते हैं और उस पंक्ति और स्तंभ में बाकी सब कुछ गायब करने की कोशिश करते हैं। कभी-कभी, गणित जटिल हो जाता है, और आप सब कुछ पूरी तरह से गायब नहीं कर पाते। जब ऐसा होता है, तो एल्गोरिदम हार नहीं मानता; यह एक विशेष चाल चलता है जो वर्तमान पिवट को एक छोटी संख्या (एक "प्रॉपर डिवाइडर") से बदल देता है।

यह शोध पत्र एक महत्वपूर्ण तथ्य को सिद्ध करता है: हर बार जब यह विशेष चाल होती है, तो पिवट के बिट्स (बाइनरी "आकार") सख्ती से छोटे होते जाते हैं। यह एक खेल की तरह है जहाँ आपको एक भारी पत्थर को हल्के कंकड़ से बदलने की अनुमति है, और आप कभी भी कंकड़ को भारी पत्थर से नहीं बदल सकते। क्योंकि आप चीजों को अनंत काल तक छोटा नहीं कर सकते (आप अंततः शून्य पर पहुँच जाते हैं), इसलिए यह खेल अनिवार्य रूप से समाप्त होगा। लेखकों ने सिद्ध किया कि यह "गिरावट" (descent) सुनिश्चित है, जिसका अर्थ है कि एल्गोरिदम कभी भी अनंत लूप में नहीं फँसेगा।

लागत की गणना: "ट्रेस" (Counting the Cost: The "Trace")

इस कार्य का एक रोमांचक हिस्सा यह है कि उन्होंने लागत की गणना कैसे की। आमतौर पर, जब हम कहते हैं कि कोई एल्गोरिदम "तेज़" है, तो हम अनुमान लगाते हैं कि इसमें कुछ सेकंड लगेंगे। लेकिन यहाँ, लेखक जानना चाहते थे कि बाइनरी ऑपरेशन्स के संदर्भ में सटीक अंकगणितीय लागत क्या है। उन्होंने एक "फ्लैट ट्रेस" बनाया, जो एक रसीद की तरह है जो उन हर एक सूक्ष्म गणितीय क्रिया (जोड़, गुणा, विभाजन) को सूचीबद्ध करता है जो कंप्यूटर ने की।

उन्होंने सिद्ध किया कि इस रसीद की कुल लागत एक पॉलीनोमियल दर (polynomial rate) पर बढ़ती है। सरल शब्दों में, इसका अर्थ है कि भले ही आपका इनपुट मैट्रिक्स बहुत बड़ा हो जाए, इसे हल करने में लगने वाला समय अनंत में नहीं फटेगा; यह एक अनुमानित, प्रबंधनीय तरीके से बढ़ेगा। उन्होंने इस वृद्धि की विशिष्ट "डिग्री" की भी गणना की। शोध पत्र प्रकट करता है कि लागत 2,150,687 (किया गया कार्य) और 98,990 (आउटपुट का आकार) की डिग्री वाले एक पॉलीनोमियल द्वारा सीमित है।

अब, ये संख्याएँ डरावनी लग सकती हैं, लेकिन लेखक बहुत सावधानी से समझाते हैं कि उनका क्या अर्थ है। ये "शार्प" घातांक (exponents) नहीं हैं (जैसे यह कहना कि इसमें ठीक $n^2$ चरण लगेंगे); ये रूढ़िवादी गवाह (conservative witnesses) हैं। इन्हें सुरक्षा मार्जिन के रूप में समझें। यदि आप एक पुल बना रहे हैं, तो आप गणना कर सकते हैं कि इसे 100 टन सहने की आवश्यकता है, लेकिन आप सुरक्षा के लिए इसे 1,000 टन सहने के लिए डिज़ाइन करते हैं। ये विशाल संख्याएँ गणित की दुनिया के "1,000 टन" हैं—गारंटी कि एल्गोरिदम सुरक्षित और कुशल है, भले ही वास्तविक दुनिया का प्रदर्शन बहुत बेहतर हो।

क्या छोड़ दिया गया?

यह जानना महत्वपूर्ण है कि इस शोध पत्र ने क्या नहीं किया। लेखक अपने प्रमाण की सीमाओं के बारे में बहुत विशिष्ट थे। उन्होंने केवल अंकगणितीय संचालन (स्वयं गणित) की गणना की। उन्होंने यह गणना नहीं की कि डेटा को मेमोरी में लोड करने में कंप्यूटर को कितना समय लगता है, परिणामों को प्रिंट करने में कितना समय लगता है, या प्रोग्रामिंग भाषा का ओवरहेड कितना है। उन्होंने यह भी सिद्ध नहीं किया कि यह मैट्रिसेस को क्रमबद्ध करने का सबसे तेज़ तरीका है; उन्होंने केवल यह सिद्ध किया कि यह विशिष्ट तरीका सुरक्षित है, गारंटी के साथ समाप्त होता है, और उनके द्वारा गणना की गई पॉलीनोमियल सीमाओं से अधिक संसाधनों का उपयोग नहीं करता है।

अंतिम निर्णय (The Final Verdict)

तो, निष्कर्ष क्या है? यह शोध पत्र औपचारिक सत्यापन (formal verification) की एक विजय है। यह दशकों पुराने जटिल गणितीय नुस्खे को लेती है और हर एक कदम की जाँच करने के लिए एक रोबोट को सौंप देती है। रोबोट पुष्टि करता है कि नुस्खा हमेशा काम करता है, हमेशा समाप्त होता है, और कभी भी ऐसी बड़ी संख्याएँ पैदा नहीं करता जो सिस्टम को तोड़ दें। यह शुद्धता का एक "प्रमाणपत्र" प्रदान करता है जिसमें व्यवस्थित मैट्रिक्स, रूपांतरण मानचित्र और यह गणितीय रूप से सिद्ध गारंटी शामिल है कि इसे करने में कितना काम लगा।

एक जिज्ञासु किशोर के लिए, यह किसी ऐसे व्यक्ति को देखने जैसा है जो न केवल एक रोबोट बनाता है जो रुबिक क्यूब को हल करता है, बल्कि एक कानूनी अनुबंध भी लिखता है जो यह सिद्ध करता है कि वह कभी भी नहीं फँसेगा, कभी भी क्यूब को नहीं तोड़ेगा, और चाहे क्यूब कितना भी बिखरा हुआ क्यों न हो, वह इसे विशिष्ट संख्या में चालों के भीतर करेगा। यह गणित में एक "शायद" को "निश्चित रूप से" में बदल देता है, जिसे सबसे सख्त न्यायाधीश द्वारा सत्यापित किया गया है।