🔢 mathematics

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0

यह शोध पत्र वास्तविक डिफरेंशियल-फॉर्म पुलबैक (differential-form pullbacks) का उपयोग करते हुए स्मूथ सिंगुलर क्यूब्स के लिए स्टोक्स प्रमेय का एक व्यापक, त्रुटिहीन (sorry-free) Lean 4 औपचारिक रूप (formalization) प्रस्तुत करता है, साथ ही mathlib4 के साथ सेतु स्थापित करता है, $d^2=0$ जैसी चेन-लेवल (chain-level) गुणों को सत्यापित करता है, और हैरिसन के HOL Light औपचारिक रूप के साथ कार्यान्वयन की तुलना करता है।

मूल लेखक: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

प्रकाशित 2026-05-05

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आपके पास एक बहुत ही जटिल, बहु-आयामी आकार है, जैसे कागज का एक मुड़ा हुआ टुकड़ा या अंतरिक्ष में तैरता हुआ एक घुमावदार रिबन। गणित में, एक प्रसिद्ध नियम है जिसे स्टोक्स का प्रमेय (Stokes' Theorem) कहा जाता है। इसे एक "सार्वभौमिक लेखांकन नियम" के रूप में सोचें। यह कहता है कि यदि आप किसी आकार के भीतर होने वाली कुल "गतिविधि" को जानना चाहते हैं (जैसे कि एक बवंडर के भीतर घूम रही कुल हवा), तो आपको उस आकार के हर बिंदु को मापने की आवश्यकता नहीं है। इसके बजाय, आपको केवल उस आकार के "किनारे" या "सीमा" (boundary) को मापने की आवश्यकता है। उस सीमा पर होने वाली कुल गतिविधि, आकार के भीतर की कुल गतिविधि के बराबर होती है।

लंबे समय तक, कंप्यूटर (विशेष रूप से एक प्रोग्राम जिसे Lean 4 कहा जाता है) इस नियम को हर संभव आकार के लिए सिद्ध करने में सक्षम नहीं थे, विशेष रूप से उन अजीब, मुड़े हुए आकारों के लिए जिन्हें गणितज्ञ "सिंगुलर क्यूब्स" (singular cubes) कहते हैं।

यह शोध पत्र इस बारे में एक रिपोर्ट है कि कैसे तीन शोधकर्ताओं ने अंततः कंप्यूटर को उन पेचीदा आकारों के लिए इस नियम को सिद्ध करना सिखाया, और वह भी बिना किसी गलती या कदम छोड़े।

यहाँ उन्होंने जो किया है उसका विवरण दिया गया है, सरल उपमाओं का उपयोग करते हुए:

1. लक्ष्य: "किनारे बनाम अंदर" का नियम

कल्पना कीजिए कि आप एक कमरे में पेंट कर रहे हैं। स्टोक्स का प्रमेय एक जादू की तरह है जो कहता है: "यदि आप जानते हैं कि दीवारों से कितना पेंट टपका है (सीमा), तो आप स्वतः ही जान सकते हैं कि पूरे कमरे को ढकने के लिए कितना पेंट इस्तेमाल किया गया था (आंतरिक भाग)।"

शोधकर्ताओं ने यह सिद्ध करना चाहा कि यह जादू तब भी काम करता है जब "कमरा" एक अजीब, खिंचा हुआ आकार हो, जिसे एक चिकपे (smooth), घुमावदार मानचित्र (map) द्वारा परिभाषित किया गया हो (जैसे कि एक रबर की शीट को खींचा और मरोड़ा जा रहा हो)।

2. तीन-चरणीय जादू का खेल

कंप्यूटर पूरे आकार को एक साथ "देख" नहीं सकता था, इसलिए शोधकर्ताओं ने प्रमाण को तीन तार्किक चरणों में विभाजित किया, जैसे कि एक रेसिपी:

चरण 1: "अनुवाद" (पुलबैक - Pullback)
कल्पना कीजिए कि आपके पास एक शहर का नक्शा है, लेकिन शहर विकृत (distorted) है। शोधकर्ताओं ने एक उपकरण बनाया जो विकृत आकार से गणित को वापस एक आदर्श, मानक घन (standard cube) में "अनुवादित" कर सके (जैसे कि एक पूर्ण पासा/die)। उन्होंने एक विशिष्ट गणितीय उपकरण का उपयोग किया जिसे "पुलबैक" कहा जाता है (जो एक हाई-टेक फोटोकॉपीयर की तरह है जो आकार के नियमों को एक मानक ग्रिड पर कॉपी करता है)।
चरण 2: "मानक बॉक्स" का नियम
एक बार जब आकार को एक आदर्श घन पर अनुवादित कर दिया गया, तो वे एक सरल, पहले से ज्ञात नियम का उपयोग कर सकते थे जो पूर्ण बक्सों के लिए काम करता है। उन्होंने सिद्ध किया कि इस आदर्श घन पर "आंतरिक गतिविधि" इस आदर्श घन की "किनारे की गतिविधि" के बराबर है।
चरण 3: "चेहरा मिलान" (Face Matching)
अंत में, उन्हें यह सिद्ध करना था कि आदर्श घन के किनारे (अनुवादित संस्करण) मूल, अजीब आकार के किनारों के साथ पूरी तरह से मेल खाते हैं। उन्होंने दिखाया कि जब आप अजीब आकार के किनारों को जोड़ते हैं, तो वे आपस में रद्द हो जाते हैं और सटीक रूप से आदर्श घन के किनारों के साथ संरेखित होते हैं।

3. "चेन" (Chain) का संबंध

शोधकर्ताओं ने इसे केवल एक आकार के लिए सिद्ध नहीं किया। उन्होंने सिद्ध किया कि यह आपस में जुड़े हुए आकारों की एक पूरी "चेन" के लिए भी काम करता है।

उपमा: ईंटों से एक दीवार बनाने की कल्पना करें। यदि आप दो ईंटों को एक साथ रखते हैं, तो जहाँ वे आपस में मिलती हैं, वह किनारा दीवार के अंदर होने के कारण गायब हो जाता है। शोधकर्ताओं ने सिद्ध किया कि यदि आपके पास इन आकारों की एक चेन है, तो "आंतरिक" किनारे हमेशा एक-दूसरे को रद्द कर देते हैं, जिससे केवल बाहरी सीमा बचती है। यह गणित का एक मौलिक नियम है जिसे $\partial^2 = 0$ (एक सीमा की सीमा शून्य होती है) कहा जाता है। उन्होंने यह सिद्ध किया कि प्रत्येक बार जब कोई किनारा दिखाई देता है, तो वह विपरीत संकेतों के साथ दो बार आता है, जिससे वह स्वयं को मिटा देता है।

4. यह क्यों महत्वपूर्ण है (कंप्यूटर की दुनिया में)

"सॉरी" (Sorry) की अनुमति नहीं: कंप्यूटर प्रमाण प्रणालियों में, प्रोग्रामर कभी-कभी यह कहने के लिए "sorry" लिखते हैं कि, "मैं जानता हूँ कि यह सच है, लेकिन मैंने अभी तक इसे सिद्ध नहीं किया है।" यह शोध पत्र विशेष है क्योंकि इसमें शून्य "sorry" कथन हैं। कंप्यूटर ने हर चरण की जांच की और पाया कि कोई त्रुटि नहीं है।
सेतु (The Bridge): शोधकर्ताओं ने कंप्यूटर में गणित करने के दो अलग-अलग तरीकों के बीच एक "सेतु" बनाया। एक तरीका सरल निर्देशांकों (coordinates) का उपयोग करता है (जैसे एक स्प्रेडशीट), और दूसरा अधिक अमूर्त (abstract) और उन्नत परिभाषाओं का। उन्होंने सिद्ध किया कि दोनों तरीके बिल्कुल एक ही उत्तर की ओर ले जाते हैं, जिससे यह सुनिश्चित होता है कि कंप्यूटर केवल अनुमान नहीं लगा रहा है।
वास्तविक चिकनापन (Real Smoothness): उन्होंने आकारों के लिए "ग्लोबली स्मूथ" (globally smooth) होने की आवश्यकता रखी, जिसका अर्थ है कि वे न केवल बीच में, बल्कि हर जगह पूरी तरह से चिकने हैं। इसने गणित को कंप्यूटर के लिए संभालने में आसान बना दिया, भले ही यह मानवों द्वारा आमतौर पर आवश्यक नियमों की तुलना में अधिक सख्त नियम है।

5. यह क्या नहीं है

यह शोध पत्र अपनी सीमाओं के बारे में बहुत ईमानदार है:

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

सारांश

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

तकनीकी सारांश: स्मूथ सिंगुलर क्यूब्स के लिए स्टोक्स का प्रमेय (Stokes' Theorem) - Lean 4 में

समस्या विवरण
अप्रैल 2026 तक, Lean 4 इकोसिस्टम (विशेष रूप से mathlib4) सीमा वाले स्मूथ मैनिफोल्ड्स या सिंगुलर चेन्स पर डिफरेंशियल फॉर्म्स के लिए स्टोक्स के प्रमेय के पूर्ण औपचारिकीकरण (formalization) से रहित था। जबकि mathlib4 के पास एक्सिस-अलाइन्ड बॉक्स के लिए डाइवर्जेंस थ्योरम और एक एब्स्ट्रैक्ट एक्सटीरियर डेरिवेटिव (extDeriv) मौजूद था, लेकिन इसमें एक स्मूथ सिंगुलर क्यूब (एक यूनिट क्यूब से किसी भी यूक्लिडियन स्पेस तक का एक स्मूथ मैप) पर डिफरेंशियल फॉर्म के पुलबैक (pullback) को एकीकृत करने और उसे बाउंड्री फेसेस के ऊपर इंटीग्रल्स के अल्टरनेटिंग सम के बराबर करने वाला प्रमेय अभी तक उपलब्ध नहीं था। मौजूदा औपचारिकीकरण, जैसे कि HOL Light में हैरिसन का कार्य, उत्तल (convex) और पॉलीहेड्रल डोमेन को कवर करते थे, लेकिन उन्होंने स्मूथ सिंगुलर पैरामीट्रिज़ेशन या mathlib4 के एब्स्ट्रैक्ट एक्सटीरियर अलजेब्रा के विशिष्ट इंफ्रास्ट्रक्चर को संबोधित नहीं किया था।

कार्यप्रणाली (Methodology)
लेखक एक "सॉरी-फ्री" (sorry-free) औपचारिकीकरण (शून्य अपुष्ट धारणाएं) प्रस्तुत करते हैं जो कोऑर्डिनेट-आधारित इंटीग्रेशन और एब्स्ट्रैक्ट डिफरेंशियल ज्योमेट्री के बीच के अंतर को पाटता है। यह विकास तीन प्राथमिक पद्धतिगत स्तंभों पर आधारित है:

फ्रैच डेरिवेटिव (Fréchet Derivative) के माध्यम से वास्तविक पुलबैक: मुख्य निर्माण एक ग्लोबली $C^\infty$ मैप $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ के लिए फ्रैच डेरिवेटिव ($fderiv $) का उपयोग करके एक डिफरेंशियल फॉर्म$ \sigma^*\omega $के पुलबैक को परिभाषित करता है। साधारण कोएफिशिएंट प्री-कंपोजिशन के विपरीत, यह परिभाषा फॉर्म को इमेज पॉइंट$ \sigma(x) $पर$ D\sigma(x)$ द्वारा पुश-फॉरवर्डेड वेक्टर्स पर लागू करती है, जो मानक डिफरेंशियल-जियोमेट्रिक परिभाषाओं का पालन करती है।
बॉक्स स्टोक्स में न्यूनीकरण (Reduction to Box Stokes): प्रमाण रणनीति सिंगुलर केस को एक्सिस-अलाइन्ड बॉक्स केस में कम करती है। mathlib4 के extDeriv_pullback प्रमेय का लाभ उठाते हुए, लेखक नैचुरलिटी आइडेंटिटी $d(\sigma^*\omega) = \sigma^*(d\omega)$ स्थापित करते हैं। यह उन्हें पैरामीटर डोमेन $[0,1]^{n+1}$ पर पुल-बैक किए गए फॉर्म $\sigma^*\omega$ पर मौजूदा बॉक्स स्टोक्स थ्योरम को लागू करने की अनुमति देता है।
फेस-मैचिंग और चेन-लेवल अलजेब्रा: एक महत्वपूर्ण तकनीकी घटक "फेस-मैचिंग आइडेंटिटी" है, जो यह सिद्ध करता है कि बॉक्स बाउंड्री फेस पर पुल-बैक किए गए फॉर्म का इंटीग्रल, संगत सिंगुलर फेस पर फॉर्म के इंटीग्रल के बिल्कुल बराबर है। इसके अलावा, लेखक सिंगुलर चेन्स के लिए चेन कॉम्प्लेक्स आइडेंटिटी $\partial(\partial\sigma) = 0$ को औपचारिक रूप देते हैं। यह अनडेकोरेटेड बॉक्स पर बाउंडरी होमोमोर्फिज्म को परिभाषित करके नहीं, बल्कि डबल-बाउंड्री इंडेक्स सेट पर एक साइन-रिवर्सिंग, फिक्स्ड-पॉइंट-फ्री इनवोल्यूशन (involution) का निर्माण करके किया जाता है, जिससे यह सिद्ध होता है कि युग्मित पद (paired terms) बीजगणितीय रूप से रद्द हो जाते हैं।

मुख्य योगदान
यह शोध पत्र 44 Lean मॉड्यूल्स (लगभग 4,000 लाइनें) के साथ एक व्यापक औपचारिकीकरण प्रदान करता है जिसमें 205 नामित डिक्लेरेशन शामिल हैं। विशिष्ट योगदान निम्नलिखित हैं:

सिंगुलर स्टोक्स थ्योरम: एक प्रमेय जो बताता है कि किसी भी ग्लोबली $C^\infty$ मैप $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ और किसी $C^\infty$ $n$ -फॉर्म $\omega$ के लिए, यूनिट क्यूब पर $\sigma^*(d\omega)$ का इंटीग्रल, $2(n+1)$ फेसेस पर $\sigma^*\omega$ के इंटीग्रल्स के अल्टरनेटिंग सम के बराबर होता है।
ब्रिज थ्योरम: एक औपचारिक प्रमाण जो यह मान्य करता है कि लेखकों का कोऑर्डिनेट-आधारित एक्सटीरियर डेरिवेटिव (extDerivCoord) मानक बेसिस वेक्टर्स पर मूल्यांकन के समय mathlib4 के एब्स्ट्रैक्ट extDeriv के साथ सुसंगत है। यह सुनिश्चित करता है कि कोऑर्डिनेट कार्यान्वयन लाइब्रेरी के एब्स्ट्रैक्ट API के सापेक्ष गणितीय रूप से सुदृढ़ है।
चेन-लेवल एक्सटेंशन: सिंगुलर क्यूब्स (सिंगुलर चेन्स) के औपचारिक $\mathbb{Z}$ -लीनियर कॉम्बिनेशन के लिए स्टोक्स के प्रमेय का विस्तार।
$\partial^2 = 0$ प्रमाण: सिंगुलर चेन्स के लिए चेन कॉम्प्लेक्स आइडेंटिटी $\partial(\partial\sigma) = 0$ का औपचारिक प्रमाण, जो डबल-फेसेस के इंडेक्स सेट पर एक कॉम्बिनेटोरियल इनवोल्यूशन का उपयोग करता है।
डायमेंशनल स्पेशलाइजेशन: फंडामेंटल थ्योरम ऑफ कैलकुलस (FTC), ग्रीन्स थ्योरम, डाइवर्जेंस थ्योरम, और 3D गॉस थ्योरम को रिकवर करने वाले मुख्य प्रमेय के प्रत्यक्ष इंस्टेंशिएशन। इसके साथ ही इंटीग्रेशन बाय पार्ट्स और लीबनिज नियम भी शामिल हैं।
एक्सियम ऑडिट: सत्यापन कि संपूर्ण विकास केवल तीन मानक Lean 4 एक्सिओम्स (propext, Classical.choice, Quot.sound) पर निर्भर करता है, जिसे 79 व्यवस्थित #print axioms जांचों के माध्यम से पुष्टि की गई है।

परिणाम और दायरा
औपचारिकीकरण सफलतापूर्वक निम्नलिखित के लिए स्टोक्स थ्योरम सिद्ध करता है:

स्मूथ सिंगुलर क्यूब्स: मैप $\sigma$ जो $\mathbb{R}^{n+1}$ पर ग्लोबली स्मूथ हैं, जिन्हें पैरामीटर क्यूब $[0,1]^{n+1}$ पर इंटीग्रेट किया गया है।
एक्सिस-अलाइन्ड बॉक्स: बॉक्स $[a,b] \subset \mathbb{R}^{n+1}$ पर कोऑर्डिनेट $n$ -फॉर्म्स।

शोध पत्र स्पष्ट रूप से निम्नलिखित सीमाओं और दायरे को नोट करता है:

मैनिफोल्ड थ्योरी का अभाव: इंटीग्रेशन डोमेन सख्ती से पैरामीटर क्यूब या एक बॉक्स है। यह कार्य सामान्य स्मूथ मैनिफोल्ड्स पर इंटीग्रेशन को औपचारिक नहीं करता है, और न ही यह पार्टिशन ऑफ यूनिटी, चार्ट्स या एटलस का उपयोग करता है।
ग्लोबल स्मूथनेस: सिंगुलर मैप्स को $\mathbb{R}^{n+1}$ पर ग्लोबली $C^\infty$ होना आवश्यक है, जो क्लोज्ड क्यूब पर स्मूथ होने की तुलना में एक अधिक मजबूत स्थिति है। यह निर्णय बाउंड्री रेगुलैरिटी तर्कों से बचने और यह सुनिश्चित करने के लिए लिया गया था कि फ्रैच डेरिवेटिव हर जगह अच्छी तरह से परिभाषित (well-defined) हो।
इमेज-डोमेन सिमेंटिक्स का अभाव: थ्योरम इंटीग्रेशन को पैरामीटर डोमेन पर एक ऑपरेशन के रूप में मानता है। यह यह सिद्ध नहीं करता कि $\sigma$ का इमेज टारगेट स्पेस में एक सब-मैनिफोल्ड या एक ओरिएंटेड ज्योमेट्रिक चेन बनाता है।

महत्व और दावे
लेखक दावा करते हैं कि यह कार्य "ट्रू" डिफरेंशियल-फॉर्म पुलबैक के साथ स्मूथ सिंगुलर क्यूब्स के लिए स्टोक्स थ्योरम का पहला पूर्ण Lean 4 औपचारिकीकरण प्रदान करता है। इसका महत्व यहाँ है:

ठोस और अमूर्त के बीच सेतु बनाना: "ब्रिज थ्योरम" पैटर्न एक ठोस कोऑर्डिनेट कार्यान्वयन को mathlib4 के एब्स्ट्रेक्ट एक्सटीरियर डेरिवेटिव के विरुद्ध मान्य करता है, जो भविष्य के औपचारिकीकरण के लिए एक पुन: प्रयोज्य पद्धति प्रदान करता है।
इंफ्रास्ट्रक्चर का पुन: उपयोग: यह विकास मौजूदा mathlib4 इंफ्रास्ट्रक्चर (डाइवर्जेंस थ्योरम, extDeriv_pullback) पर भारी रूप से निर्भर करता है, जो यह दर्शाता है कि कैसे उच्च-स्तरीय लाइब्रेरी घटकों का उपयोग जटिल ज्यामितीय प्रमेयों को सिद्ध करने के लिए किया जा सकता है।
पूरकता: यह कार्य हैरिसन के HOL Light औपचारिकीकरण के पूरक है। जहाँ हैरिसन गेज इंटीग्रेशन के साथ उत्तल/पॉलीहेड्रल डोमेन को कवर करते हैं, वहीं यह कार्य बोचन इंटीग्रेशन और mathlib4 के डिफरेंशियल ज्योमेट्री API का उपयोग करके स्मूथ सिंगुलर पैरामीट्रिज़ेशन को कवर करता है।
फाउंडेशनल रेडीनेस: $\partial^2=0$ को सिद्ध करके और चेन-लेवल स्टोक्स थ्योरम स्थापित करके, लेखक स्मूथ मैनिफोल्ड्स विद बाउंड्री पर पूर्ण स्टोक्स थ्योरम के भविष्य के औपचारिकीकरण के लिए एक आवश्यक स्थानीय बिल्डिंग ब्लॉक प्रदान करते हैं।

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