A Formalization of the Laplace Transform and Its Inversion in Lean 4

कल्पना कीजिए कि एक ऐसी दुनिया है जहाँ चीजों के बदलने की अस्त-व्यस्त, अराजक गति—जैसे एक झूलता हुआ पेंडुलम, एक गिटार के तार का कंपन, या एक तार के माध्यम से यात्रा करता सिग्नल—को तुरंत एक साफ, स्थिर बीजगणितीय (algebraic) समस्या में बदला जा सकता है। यह लाप्लास ट्रांसफॉर्म (Laplace transform) का जादू है, जो एक गणितीय उपकरण है जिसका उपयोग इंजीनियरों और वैज्ञानिकों द्वारा एक सदी से अधिक समय से किया जा रहा है। इसे एक सार्वभौमिक अनुवादक के रूप में सोचें जो "समय" की भाषा में लिखी गई कहानी (जहाँ चीजें चलती हैं, तेज होती हैं और धीमी होती हैं) को "कॉम्प्लेक्स नंबर्स" (जटिल संख्याओं) की भाषा में लिखी गई कहानी में बदल देता है (जहाँ वे वही गतियाँ सरल गुणा और भाग बन जाती हैं)।

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

---

डिजिटल प्रूफ-चेकर

कल्पना कीजिए कि आपका एक बहुत ही सख्त, बहुत ही शाब्दिक रोबोट मित्र है जिसे गणित पसंद है लेकिन अनुमान लगाना नापसंद है। आप उसे बताते हैं, "यहाँ एक सूत्र है जो एक टेढ़ी-मेढ़ी रेखा को एक चिकनी वक्र (curve) में बदल देता है," और वह पूछता है, "क्या आप सुनिश्चित हैं? क्या होगा अगर रेखा बहुत अधिक टेढ़ी-मेढ़ी हो जाए? क्या होगा अगर यह अनंत तक चली जाए?" यह शोध पत्र दो शोधकर्ताओं, डैनियल और एंटोनी के उस रोबोट मित्र को लाप्लास ट्रांसफॉर्म के बारे में वह सब कुछ सिखाने का परिणाम है जिसे उसे जानने की आवश्यकता है।

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

अनुवादक और जादुई दर्पण

लाप्लास ट्रांसफॉर्म एक जादुई दर्पण की तरह है। आप एक फलन $f(t)$ (जो समय के साथ होने वाली किसी घटना का वर्णन करता है) को दर्पण में डालते हैं, और यह एक नया फलन $(Lf)(s)$ (जो उसी चीज़ का वर्णन "फ्रीक्वेंसी" की दुनिया में करता है) परावर्तित करता है।

• आगे की यात्रा (The Forward Trip): शोध पत्र सिद्ध करता है कि यदि आपके पास एक फलन है जो अच्छी तरह व्यवहार करता है (यह बहुत तेज़ी से अनंत की ओर नहीं भागता), तो दर्पण काम करता है। उन्होंने सिद्ध किया कि सरल चीजों जैसे स्थिरांक (constants), समय की घातों (powers of time), और यहाँ तक कि साइन तरंगों (sine waves) को कैसे अनुवादित किया जाता है। उदाहरण के लिए, उन्होंने दिखाया कि दर्पण कैसे अवकलज (derivative - परिवर्तन की दर) को संख्या $s$ के सरल गुणा और एक शुरुआती मान को घटाने में बदल देता है। यही वह "गुप्त नुस्खा" है जो डिफरेंशियल इक्वेशंस को हल करना इतना आसान बनाता है।
• वापसी की यात्रा (The Return Trip - Inversion): असली चुनौती उत्तर वापस पाना है। आप प्रतिबिंब को देखकर यह कैसे जान सकते हैं कि मूल वस्तु क्या थी? इसे इनवर्स लाप्लास ट्रांसफॉर्म कहा जाता है। यह शोध पत्र एक विशिष्ट विधि को सिद्ध करता है, जिसे ब्रूमविच फॉर्मूला (Bromwich formula) के रूप में जाना जाता है।

उन्होंने "आसान" रास्ता क्यों नहीं चुना?

आमतौर पर, गणितज्ञ कॉम्प्लेक्स कॉन्टूर इंटीग्रेशन (complex contour integration) नामक तकनीक का उपयोग करके इनवर्जन फॉर्मूला को सिद्ध करते हैं। कल्पना कीजिए कि आप एक मानचित्र पर किसी आकृति के चारों ओर एक लूप बनाते हैं और "रेसिड्यू थ्योरम" (Residue Theorem) का उपयोग करके उसके अंदर के "खजानों" को गिनते हैं। यह एक शक्तिशाली उपकरण है, लेकिन लेखकों ने पाया कि कंप्यूटर की लाइब्रेरी में अभी तक इन "मानचित्र बनाने वाले" उपकरणों की कमी थी।

इसलिए, उन्होंने एक अलग, अधिक जमीनी रास्ता अपनाया। कॉम्प्लेक्स प्ले में लूप बनाने के बजाय, उन्होंने समस्या को एक वास्तविक दुनिया के एक सीधे रेखा पर एकीकरण (integration) के रूप में माना। उन्होंने समस्या को छोटे, प्रबंधनीय टुकड़ों में विभाजित किया:

1. ट्रंकेशन (Truncation): उन्होंने कल्पना की कि अनंत रेखा केवल $-T$ से $T$ तक का एक छोटा, परिमित खंड है।
2. सिंक फंक्शन (The Sinc Function): जैसे-जैसे उन्होंने इस खंड को लंबा और लंबा बनाया, एक विशिष्ट पैटर्न उभरा जिसमें sinc नामक एक फलन शामिल था (जो एक ऐसी लहर की तरह दिखता है जो छोटी होती जाती है)।
3. डिरिचलेट इंटीग्रल (The Dirichlet Integral): वे इस सिंक वेव के नीचे के क्षेत्र के बारे में एक प्रसिद्ध, पूर्व-सिद्ध तथ्य (डिरिचलेट इंटीग्रल) पर निर्भर रहे, यह दिखाने के लिए कि जैसे-जैसे खंड अनंत रूप से लंबा होता है, परिणाम मूल फलन को पूरी तरह से पुनर्गठित करता है।

यह दृष्टिकोण सेटअप करने में कठिन था लेकिन कंप्यूटर के सत्यापन के लिए सुरक्षित था क्योंकि यह वास्तविक-संख्या कैलकुलस (real-number calculus) पर आधारित था, जिसमें कंप्यूटर पहले से ही बहुत अच्छा था।

झूलता हुआ पेंडुलम टेस्ट

यह सिद्ध करने के लिए कि उनका सिस्टम वास्तव में काम करता है, उन्होंने केवल अमूर्त गणित को ही नहीं जांचा; उन्होंने एक क्लासिक भौतिकी समस्या को हल किया: हार्मोनिक ऑसिलेटर (harmonic oscillator)। यह एक झूलते हुए पेंडुलम या ऊपर-नीचे उछलते हुए स्प्रिंग के पीछे का गणित है।

• सेटअप: उन्होंने एक स्प्रिंग को परिभाषित किया जो विश्राम की स्थिति में शुरू होता है लेकिन उसे एक त्वरित धक्का दिया जाता है, जिसे समीकरण $y''(t) + \omega^2 y(t) = 0$ द्वारा वर्णित किया गया है।
• अनुवाद: उन्होंने इस समीकरण को अपने कंप्यूटर-सत्यापित लाप्लास अनुवादक में डाला।
• परिणाम: कंप्यूटर ने सफलतापूर्वक इस जटिल डिफरेंशियल इक्वेशन को एक सरल बीजगणितीय समीकरण में बदल दिया: $(s^2 + \omega^2)Y(s) = \omega$।
• समाधान: $Y(s)$ के लिए हल करने पर उन्हें $\frac{\omega}{s^2 + \omega^2}$ प्राप्त हुआ।
• सत्यापन: कंप्यूटर ने फिर अपनी ही लाइब्रेरी की जांच की और पुष्टि की कि यह विशिष्ट परिणाम $\sin(\omega t)$ का लाप्लास ट्रांसफॉर्म है।

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

खेल के सख्त नियम

यह शोध पत्र इस बारे में भी एक सबक है कि जब आप अनुमान लगाना बंद कर देते हैं और सिद्ध करना शुरू करते हैं, तो आपको कितना सावधान रहना पड़ता है। लेखक उन कई "बारीकियों" (gotchas) पर प्रकाश डालते हैं जिन्हें अक्सर पाठ्यपुस्तकों में अनदेखा कर दिया जाता है:

• अनंत (Infinity) पेचीदा है: आप यह मान नहीं सकते कि एक इंटीग्रल अनंत तक जाता है। प्रमाण को स्पष्ट रूप से यह बताना पड़ा कि फलन इतनी तेज़ी से कम होना चाहिए कि इंटीग्रल की "पूंछ" (tail) समाप्त हो जाए।
• एज केसेस (The Edge Cases): गणित करते समय, कुछ विशिष्ट बिंदु होते हैं (जैसे समय $t=0$) जहाँ नियम बदल जाते हैं। कंप्यूटर ने उन्हें यह स्पष्ट करने के लिए मजबूर किया कि फलन ठीक कहाँ परिभाषित और निरंतर (continuous) है।
• क्रम बदलना (Swapping Order): इनवर्जन प्रूफ में, उन्हें दो इंटीग्रल के क्रम को बदलना पड़ा। अनौपचारिक गणित में, आप बस ऐसा कर सकते हैं। उनके औपचारिक प्रमाण में, उन्हें यह कठोरता से सिद्ध करना पड़ा कि संयुक्त सतह के नीचे का "क्षेत्रफल" बदलने से पहले परिमित (finite) है।

निष्कर्ष

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

उन्होंने सिद्ध किया कि "जादुई दर्पण" काम करता है, बशर्ते आप इस बात के सख्त नियमों का पालन करें कि फलन अनंत में और शुरुआत में कैसा व्यवहार करता है। उन्होंने दिखाया कि उत्तर तक पहुँचने का मार्ग शॉर्टकट के बजाय सावधानीपूर्वक, चरण-दर-चरण तर्क का है। उन लोगों के लिए जो इन गणितीय उपकरणों पर निर्भर अगली पीढ़ी के सॉफ्टवेयर का निर्माण कर रहे हैं, यह कार्य सुनिश्चित करता है कि उनका आधार न केवल मजबूत है, बल्कि अटूट भी है। हार्मोनिक ऑसिलेटर का उदाहरण अंतिम मुहर के रूप में कार्य करता है: कंप्यूटर मानव से सहमत है, और पहली बार, कंप्यूटर ने प्रमाण पर अपनी सहमति दे दी है।