⚛️ quantum physics

Formalizing CHSH Rigidity in Lean 4

यह शोध पत्र CHSH रिजिडिटी प्रमेय का Lean 4 में एक औपचारिकीकरण प्रस्तुत करता है, जो यह प्रदर्शित करता है कि कोई भी रणनीति जो निकट-इष्टतम CHSH मान प्राप्त करती है, वह मानक क्वबिट रणनीति के स्थानीय समरूप (locally isometric) है, और साथ ही मैके, यांग और स्कारानी के मूल प्रमाण में एक अंतराल की पहचान करता है।

मूल लेखक: Tianrun Zhao, Nengkun Yu

प्रकाशित 2026-04-07

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

CC BY 4.0

मूल लेखक: Tianrun Zhao, Nengkun Yu

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

कल्पना कीजिए कि आप एक जासूस हैं जो एक ऐसे रहस्य को सुलझाने की कोशिश कर रहे हैं जहाँ वास्तविकता के नियम थोड़े अजीब हैं। यह पेपर एक विशिष्ट रहस्य के बारे में है जिसे CHSH गेम कहा जाता है, जो एक प्रसिद्ध परीक्षण है जिसका उपयोग यह साबित करने के लिए किया जाता है कि दो लोग (मान लीजिए एलिस और बॉब) एक "डराविया" (spooky) क्वांटम संबंध साझा कर रहे हैं जिसे क्लासिकल भौतिकी नहीं समझा सकती।

यहाँ कहानी है कि लेखकों ने क्या किया, जिसे सरल रूप में समझाया गया है:

1. रहस्य: "परफेक्ट" स्कोर

क्वांटम दुनिया में, एलिस और बॉब एक खेल खेलते हैं। यदि वे सामान्य, रोज़मर्रा के तर्क (क्लासिकल भौतिकी) का उपयोग करके खेलते हैं, तो वे अधिकतम 2 का स्कोर प्राप्त कर सकते हैं। लेकिन यदि वे क्वांटम जादू (एंटैंगल्ड कणों) का उपयोग करते हैं, तो वे एक उच्च स्कोर प्राप्त कर सकते हैं, जो कि 2.82 ( $2\sqrt{2}$ ) तक जा सकता है। इस अधिकतम स्कोर को त्सीरलसन बाउंड (Tsirelson's bound) कहा जाता है।

बड़ा सवाल यह है: यदि एलिस और बॉब एक लगभग "परफेक्ट" स्कोर प्राप्त करते हैं (जैसे कि 2.81), तो क्या इसका मतलब यह है कि वे निश्चित रूप से "परफेक्ट" क्वांटम सेटअप का उपयोग कर रहे हैं?

इसका उत्तर हाँ है। इसे रिजिडिटी (Rigidity) कहा जाता है। यह कुछ ऐसा कहने जैसा है: "यदि आप 2 घंटे और 1 मिनट में मैराथन दौड़ते हैं (जब विश्व रिकॉर्ड 2 घंटे है), तो आप निश्चित रूप से उसी परफेक्ट फॉर्म के साथ दौड़ रहे होंगे जैसा कि विश्व रिकॉर्ड धारक का होता है, शायद बस थोड़ा सा थके हुए।"

2. समस्या: पुराने मानचित्र में एक खामी

वर्षों से, वैज्ञानिकों के पास एक "मानचित्र" (एक गणितीय प्रमाण) था जो यह समझाता था कि यह रिजिडिटी क्यों काम करती है। उन्होंने कहा था, "यदि आपको एक उच्च स्कोर मिलता है, तो हम आपके सेटअप को गणितीय रूप से बदलकर बिल्कुल परफेक्ट वाले जैसा बना सकते हैं।"

हालाँकि, इस पेपर के लेखकों ने एक मानचित्र में छेद पाया।

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

3. समाधान: एक "डिजिटल ट्विन" बनाना

अपने बिंदु को सिद्ध करने के लिए, लेखकों ने केवल कागज पर प्रमाण नहीं लिखा। उन्होंने इसे Lean 4 नामक एक कंप्यूटर प्रोग्राम के भीतर बनाया।

Lean 4 को एक अत्यंत सख्त अकाउंटेंट या एक रोबोट रेफरी के रूप में सोचें।

सामान्य गणित में, आप कह सकते हैं "और इसी तरह" या "यह स्पष्ट है।"
Lean 4 में, आप ऐसा नहीं कर सकते। आपको हर एक चरण, हर एक सूक्ष्म धारणा और हर एक तार्किक छलांग को लिखना होगा। यदि आप एक भी चरण छोड़ देते हैं, तो रोबोट कहता है, "त्रुटि! मुझे समझ नहीं आया।"

प्रमाण को इस तरह सख्त बनाकर, उन्होंने सुनिश्चित किया कि तर्क अभेद्य हो।

4. उन्होंने यह कैसे किया (द "एक्सट्रैक्शन" ट्रिक)

उनके प्रमाण का मूल हिस्सा एक्सट्रैक्शन (Extraction) की प्रक्रिया है।

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

5. यह क्यों मायने रखता है

आप पूछ सकते हैं, "हमें इस काम के लिए कंप्यूटर की आवश्यकता क्यों है?"

मानवीय त्रुटि: क्वांटम भौतिकी जटिल गणित की लंबी श्रृंखलाओं से जुड़ी होती है। एक इंसान के लिए गणना में एक छोटी सी गलती करना बहुत आसान है जो पूरे निष्कर्ष को बर्बाद कर सकती है।
विश्वास: Lean 4 का उपयोग करके, लेखकों ने एक प्रमाणित प्रमाण (certified proof) बनाया। यह एक कानूनी दस्तावेज़ पर नोटरी पब्लिक के हस्ताक्षर लेने जैसा है। हम 100% आश्वस्त हो सकते हैं कि तर्क सही है क्योंकि कंप्यूटर ने हर एक चरण की जांच की है।
भविष्य की तकनीक: यह क्वांटम क्रिप्टोग्राफी के लिए महत्वपूर्ण है। यदि हम क्वांटम भौतिकी पर आधारित अटूट कोड बनाना चाहते हैं, तो हमें पूरी तरह से आश्वस्त होना चाहिए कि हम जिस "डराविया" (spooky) कनेक्शन का उपयोग कर रहे हैं वह वास्तविक है, न कि कोई चाल। यह पेपर हमें वह निश्चितता देता है।

सारांश

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

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

"Formalizing CHSH Rigidity in Lean 4" (तियान्रुन झाओ और नेंगकुन यू द्वारा) के आधार पर, यहाँ समस्या, कार्यप्रणाली, प्रमुख योगदान, परिणाम और महत्व को कवर करने वाला एक विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

यह शोध पत्र क्वांटम सूचना सिद्धांत के एक मौलिक परिणाम, Robust CHSH Rigidity Theorem को संबोधित करता है। CHSH असमानता (inequality) शास्त्रीय और क्वांटम सहसंबंधों (correlations) के बीच अंतर करती है। जबकि यह ज्ञात है कि अधिकतम क्वांटम उल्लंघन (Tsirelson's bound, $2\sqrt{2}$ ) विशिष्ट रूप से एक विशेष कैनोनिकल रणनीति (विशिष्ट पाउली ऑब्जर्वेबल्स के साथ एक EPR पेयर) द्वारा प्राप्त किया जाता है, rigidity (कठोरता) का गुण यह दावा करता है कि $2\sqrt{2}$ के निकट मान प्राप्त करने वाली कोई भी रणनीति इस कैनोनिकल रणनीति के स्थानीय आइसोमेट्रिक (locally isometric) होती है (एक "जंक" सिस्टम को छोड़कर)।

संबोधित की गई विशिष्ट चुनौतियाँ हैं:

औपचारिक सटीकता (Formal Precision): साहित्य (विशेष रूप से क्लीव के नोट्स और [9] के कार्य) में पाए जाने वाले अक्सर संक्षिप्त और उच्च-स्तरीय गणितीय तर्कों को एक कठोर, मशीन-चेकेबल प्रारूप में अनुवादित करना।
मजबूती (Robustness): "निकट-इष्टतम" (near-optimal) मामले को संभालना जहाँ CHSH मान $2\sqrt{2} - \epsilon$ होता है, जिसके लिए सटीक स्पेक्ट्रल अनुमान और नॉर्म बाउंड्स की आवश्यकता होती है।
साहित्यिक अंतराल (Literature Gaps): उन सूक्ष्म त्रुटियों की पहचान करना और सुधारना जो ऑब्जर्वेबल्स के गैर-व्युत्क्रमणीय (not invertible) होने पर निकाले गए ऑपरेटरों की परिभाषा के संबंध में मौजूदा प्रमाणों में पाई जाती हैं।

2. कार्यप्रणाली (Methodology)

लेखकों ने पूरे प्रमाण को औपचारिक रूप देने के लिए एक इंटरैक्टिव थ्योरम प्रूवर, Lean 4 का उपयोग किया। कार्यप्रणाली में शामिल था:

मॉड्यूलर आर्किटेक्चर: प्रमाण को एक एकल मोनोलिथिक प्रमाण के बजाय कंपोजेबल और पुन: प्रयोज्य घटकों में विभाजित किया गया था। वर्कफ़्लो एक पाइपलाइन का अनुसरण करता है:
1. Bias Assumption: यह मानना कि CHSH मान निकट-इष्टतम है।
2. Ideal Expectation Bound: स्पेक्ट्रल अनुमान प्राप्त करना।
3. Extracted Qubit Analysis: निकाले गए ऑब्जर्वेबल्स की संरचना का विश्लेषण करना।
4. Bell-State Overlap: यह सिद्ध करना कि अवस्था आदर्श बेल स्टेट के करीब है।
5. State/Operator Extraction: भौतिक रणनीति को कैनोनिकल रणनीति पर मैप करने के लिए स्थानीय आइसोमेट्रियों का निर्माण करना।
Mathlib एकीकरण: विकास ने बुनियादी रैखिक बीजगणित (linear algebra), नॉर्मेड स्पेस और टेंसर उत्पाद हेरफेर के लिए Mathlib इकोसिस्टम का लाभ उठाया, जिससे बुनियादी गणित को शून्य से औपचारिक रूप देने की आवश्यकता समाप्त हो गई।
स्पष्ट टेंसर प्रबंधन (Explicit Tensor Management): औपचारिककरण के एक बड़े हिस्से को टेन्सर पुनर्संयोजन (regrouping factors) को कठोरता से संभालने के लिए समर्पित किया गया था। अनौपचारिक प्रमाणों में, $regSwap $जैसे मानचित्र (जैसे$ (C^2 \otimes H_A) \otimes (C^2 \otimes H_B) $को$ (C^2 \otimes C^2) \otimes (H_A \otimes H_B)$ में पुनर्व्यवस्थित करना) अक्सर निहित होते हैं। Lean में, इन्हें स्पष्ट रैखिक मानचित्र होना चाहिए।
संशोधित बॉब-साइड निर्माण (Modified Bob-Side Construction): लेखकों ने क्लीव के नोट्स के मानक प्रमाण को संशोधित किया है, जिसमें रोटेशन $R$ को अंतिम सफाई चरण के रूप में लागू करने के बजाय, सीधे बॉब के एक्सट्रैक्टर यूनिटरी $U_B$ और ऑन्साइला स्टेट $|aux\rangle$ में शामिल किया गया है। यह सुनिश्चित करता है कि निकाले गए ऑब्जर्वेबल्स मध्यवर्ती चरण में मानक CHSH ऑब्जर्वेबल्स ( $H, H'$ ) के साथ बिल्कुल मेल खाते हैं।

3. प्रमुख योगदान (Key Contributions)

A. साहित्य में अंतराल की पहचान

लेखकों ने संदर्भ [9] में प्रस्तुत तर्क में एक महत्वपूर्ण दोष की पहचान की।

दोष: मूल लेखकों ने बॉब के निकाले गए ऑपरेटरों $X'_B$ और $Z'_B$ को एक मोडुलस कन्वेंशन का उपयोग करके परिभाषित किया जहाँ ऑपरेटर डिनोमिनेटर (denominator) के कर्नेल (kernel) पर आइडेंटिटी के रूप में कार्य करता है। उन्होंने दावा किया कि ये ऑपरेटर एंटी-कम्यूट (anticommute) करते हैं ( $\{X'_B, Z'_B\} = 0$ )।
प्रति-उदाहरण (Counterexample): लेखकों ने एक प्रति-उदाहरण बनाया (आयाम 2, $B_0 = B_1 = \sigma_z$ ) जहाँ डिनोमिनेटर शून्य है, और "आइडेंटिटी ऑन कर्नेल" कन्वेंशन के तहत, परिणामी ऑपरेटर $I$ और $\sigma_z$ हैं, जो एंटी-कम्यूट नहीं करते हैं।
समाधान: Lean औपचारिककरण एक कंजुगेशन ट्रिक (आधार को $R$ के माध्यम से रोटेट करना) का उपयोग करके इस अस्पष्टता से बचता है ताकि निकाले गए ऑपरेटर निर्माण द्वारा यूनिटरी (unitary) सुनिश्चित हों, जिससे मनमाने कर्नेल कन्वेंशन की आवश्यकता समाप्त हो जाती है।

B. रिगिडिटी थ्योरम का औपचारिककरण

यह शोध पत्र 'रोबस्ट CHSH रिगिडिटी थ्योरम' का पहला मशीन-चेक्ड प्रमाण प्रदान करता है। यह औपचारिक रूप से स्थापित करता है कि किसी भी रणनीति $S$ के लिए जिसका बायस $\beta(S) \geq 2\sqrt{2} - \epsilon$ है, वहां स्थानीय आइसोमेट्रियां $V_A, V_B$ और एक जंक स्टेट मौजूद हैं ताकि:

State Extraction: रूपांतरित अवस्था $|\Phi^+\rangle \otimes |\Phi_{junk}\rangle$ के $O(\sqrt{\epsilon})$ के भीतर है।
Operator Extraction: रूपांतरित ऑब्जर्वेबल्स $A_0, A_1, B_0, B_1$ निकाले गए क्वबिट पर कार्य करने वाले कैनोनिकल पाउली/हैडामार्ड ऑपरेटरों के $O(\sqrt{\epsilon})$ के भीतर हैं (विशिष्ट स्थिरांकों के साथ)।

C. स्पष्ट स्थिरांक और सीमाएँ (Explicit Constants and Bounds)

अनौपचारिक प्रमाणों के विपरीत जो बिग-ओ नोटेशन का ढीले ढंग से उपयोग करते हैं, यह औपचारिककरण ठोस स्थिरांकों के साथ स्पष्ट असमानताएं (जैसे, $c = 128\sqrt{2}$ ) उत्पन्न करता है, जिससे मजबूती की सीमाएं पूरी तरह से सत्यापन योग्य हो जाती हैं।

4. परिणाम (Results)

सत्यापित प्रमेय (Verified Theorem): मुख्य प्रमेय (पेपर में थ्योरम 3.1) Lean 4 में पूरी तरह से सिद्ध है। यह पुष्टि करता है कि निकट-इष्टतम CHSH रणनीतियाँ संरचनात्मक रूप से कैनोनिकल EPR रणनीति के समान हैं।
सुधारित प्रमाण पथ: औपचारिककरण एक सुधारा गया प्रमाण पथ मान्य करता है जो मूल साहित्य में गैर-व्युत्क्रमणीयता (non-invertibility) के मुद्दे को हल करता है, यह सुनिश्चित करता है कि एंटी-कम्यूटेशन संबंध सख्ती से लागू होते हैं।
कोड उपलब्धता: औपचारिककरण मॉड्यूलर है और एक सार्वजनिक रिपॉजिटरी में उपलब्ध है, जो भविष्य के क्वांटम सूचना औपचारिकीकरण के लिए एक पुन: प्रयोज्य लाइब्रेरी के रूप में कार्य करता है।

5. महत्व (Significance)

क्वांटम प्रमाणों की विश्वसनीयता: यह पेपर दर्शाता है कि औपचारिक सत्यापन क्वांटम सूचना सिद्धांत के लिए एक महत्वपूर्ण उपकरण है, जहाँ गणनाओं की लंबी श्रृंखला अक्सर सूक्ष्म त्रुटियों को छिपा देती है (जैसा कि [9] में मिले अंतराल से सिद्ध हुआ है)।
सेल्फ-टेस्टिंग का आधार: रोबस्ट रिगिडिटी, डिवाइस-इंडिपेंडेंट क्वांटम क्रिप्टोग्राफी और सेल्फ-टेस्टिंग की सैद्धांतिक रीढ़ है। इसे औपचारिक रूप देकर, लेखक उन प्रोटोकॉल के लिए एक प्रमाणित आधार प्रदान करते हैं जो उनके आंतरिक कामकाज पर भरोसा किए बिना क्वांटम उपकरणों को सत्यापित करने पर निर्भर करते हैं।
मेथोडोलॉजिकल बदलाव: यह कार्य "एजेंटिक ऑटोफॉर्मलाइजेशन" (agentic autoformalization) की ओर एक बदलाव को दर्शाता है, जहाँ AI सहायक लेम्मा ड्रा करने में मदद करते हैं, लेकिन मानव विशेषज्ञों को एल्गोरिदम के गलत हाइपोथीसिस जोड़ने से रोकने के लिए बीजगणितीय संरचनाओं को कठोरता से परिभाषित करना और तर्क को सत्यापित करना आवश्यक है।
सामुदायिक संसाधन: Mathlib इकोसिस्टम का निर्माण और विस्तार करके, यह कार्य Lean में क्वांटम यांत्रिकी के लिए एक विशेष लाइब्रेरी में योगदान देता है, जिससे इस क्षेत्र में भविष्य के औपचारिकीकरण के लिए बाधा कम होती है।

संक्षेप में, यह पेपर न केवल क्वांटम फाउंडेशन के एक प्रमुख प्रमेय को प्रमाणित करता है बल्कि साहित्य में पहले से अनदेखे त्रुटि को भी उजागर करता है, जो सैद्धांतिक भौतिकी की विश्वसनीयता बढ़ाने के लिए औपचारिक विधियों (formal methods) की शक्ति को प्रदर्शित करता है।