💻 logic

Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound

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

मूल लेखक: Shayaan Siddique, Ibrahim Mian

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

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

मूल लेखक: Shayaan Siddique, Ibrahim Mian

✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप अदृश्य, जादुई ब्लॉकों से एक घर बनाने की कोशिश कर रहे हैं। क्वांटम भौतिकी की दुनिया में, इन ब्लॉकों को "वेक्टर्स" (vectors) कहा जाता है, और उनका एक बहुत ही अजीब नियम है: यदि दो ब्लॉक एक-दूसरे के बिल्कुल समकोण (right angle) पर हैं, तो वे दोनों एक ही समय में "ऑन" (on) नहीं हो सकते। यह कोचेन-स्पेक्टर प्रमेय (Kochen–Specker theorem) का मूल है, एक प्रसिद्ध विचार जो यह सिद्ध करता है कि ब्रह्मांड केवल एक विशाल, अनुमानित मशीन नहीं है जहाँ हर हिस्से का एक पूर्व-निर्धारित गुप्त स्विच होता है। इसके बजाय, यह सुझाव देता है कि एक क्वांटम सिस्टम को देखने की क्रिया उसके व्यवहार को बदल देती है।

दशकों से, भौतिक विज्ञानी "हम इसे कितना छोटा बना सकते हैं?" के एक उच्च-दांव वाले खेल को खेल रहे हैं। वे इन जादुई ब्लॉकों के सबसे छोटे संभावित सेट को खोजने का प्रयास कर रहे हैं जो एक विरोधाभास पैदा करता है—एक ऐसी स्थिति जहाँ खेल के नियम भौतिकी के नियमों को तोड़े बिना "ऑन" या "ऑफ" अवस्थाओं को निर्धारित करना असंभव बना देते हैं। सबसे छोटे ज्ञात सेट का वर्तमान रिकॉर्ड 31 ब्लॉक है। लेकिन बड़ा सवाल यह है: पूर्ण न्यूनतम क्या है? क्या यह 25 के साथ किया जा सकता है? 24 के साथ? या इससे भी कम?

इसका उत्तर देने के लिए, शोधकर्ता हजारों संभावित ब्लॉक व्यवस्थाओं को उत्पन्न करने के लिए शक्तिशाली कंप्यूटर प्रोग्रामों का उपयोग करते हैं और फिर यह सिद्ध करने का प्रयास करते हैं कि उनमें से कोई भी वास्तव में हमारी 3D दुनिया में मौजूद नहीं हो सकता। यह एक जासूस की तरह है जो यह सिद्ध करने की कोशिश कर रहा है कि एक संदिग्ध ने अपराध नहीं किया होगा, यह दिखाकर कि उसका बहाना (alibi) गणितीय रूप से असंभव है। समस्या यह है कि, इस प्रमाण के सबसे कठिन हिस्से के लिए, पिछले जासूसों को एक "ब्लैक बॉक्स" कंप्यूटर सॉल्वर पर भरोसा करना पड़ा था। उन्होंने कंप्यूटर से पूछा, "क्या यह व्यवस्था संभव है?" और कंप्यूटर ने कहा, "नहीं।" लेकिन कंप्यूटर ने अपना कार्य (work) नहीं दिखाया, जिससे तर्क में एक छोटा सा अंतर रह गया जहाँ एक गलती छिप सकती थी।

यह शोध पत्र (paper) उस अंतर को भरने के बारे में है। लेखक, शयान सिद्दीकी और इब्राहिम मियां, प्रत्येक एकल असंभव व्यवस्था के लिए एक नए प्रकार का "रसीद" (receipt) बनाने का निर्णय लेते हैं। केवल कंप्यूटर के "नहीं" पर भरोसा करने के बजाय, उन्होंने एक चरण-दर-चरण, गणितीय रूप से पूर्ण प्रमाण-पत्र (certificate) बनाया जिसे कोई भी (या कोई अन्य कंप्यूटर) परिणाम को सत्यापित करने के लिए जांच सकता है। उन्होंने केवल एक या दो की जांच नहीं की; उन्होंने 291 विशिष्ट मामलों की जांच की (जो 180 अद्वितीय आकृतियों का प्रतिनिधित्व करते हैं) जो वर्तमान सर्वोत्तम निचले स्तर (lower bound) का आधार बनाते हैं: 24 वेक्टर्स।

यहाँ बताया गया है कि उन्होंने यह कैसे किया और उन्हें क्या मिला:

जादुई रसीद
कल्पना कीजिए कि आप यह सिद्ध करने की कोशिश कर रहे हैं कि ब्लॉकों से बनी एक विशिष्ट आकृति अस्तित्व में नहीं हो सकती। पुराना तरीका एक सुपर-स्मार्ट AI से पूछना था, जो संख्याओं की गणना करता और कहता, "असंभव।" नया तरीका, जो इस शोध पत्र में आविष्कार किया गया है, AI से एक कहानी लिखने के लिए कहना है। यह कहानी एक "केस-ट्री सर्टिफिकेट" (case-tree certificate) है। यह कुछ बुनियादी ब्लॉकों के साथ शुरू होती है और फिर एक "चूज़-योर-ओन-एडवेंचर" (choose-your-own-adventure) पुस्तक की तरह शाखाओं में बंट जाती है। सड़क के हर मोड़ पर, कहानी बताती है कि एक निश्चित पथ विरोधाभास की ओर क्यों ले जाता है।

लेखकों ने इन कहानियों को अविश्वसनीय रूप से कठोर बनाया। उन्होंने "सटीक परिमेय अंकगणित" (exact rational arithmetic) का उपयोग किया, जिसका अर्थ है कि उन्होंने अनुमान या अंदाज़ों का उपयोग नहीं किया (जैसे यह कहना कि "यह लगभग 3.14 है")। इसके बजाय, उन्होंने पूर्ण भिन्नों (fractions) का उपयोग किया। यदि कहानी कहती है कि एक संख्या शून्य है, तो वह बिल्कुल शून्य है, न कि "शून्य के करीब"। उन्होंने इन कहानियों को पढ़ने के लिए दो स्वतंत्र "चेकर्स" बनाए—एक पायथन (Python) में लिखा गया और एक लीन 4 (Lean 4) नामक एक औपचारिक प्रमाण भाषा में—ताistically कि ये चेकर सख्त पुस्तकालयाध्यक्षों की तरह हैं जो कहानी के हर एक चरण को सत्यापित करते हैं। यदि कहानी में कोई टाइपो या तार्किक छलांग है, तो पुस्तकालयाध्यक्ष उसे अस्वीकार कर देता है।

पुस्तकालय में आश्चर्य
जब लेखकों ने अपने नए, सख्त चेकर के साथ पुराने "ब्लैक बॉक्स" परिणामों को पढ़ना शुरू किया, तो उन्हें कुछ ऐसे आश्चर्य मिले जो मूल शोधकर्ताओं से छूट गए थे क्योंकि वे कंप्यूटर पर बहुत अधिक भरोसा कर रहे थे।

"विशिष्टता" का जाल (The "Distinctness" Trap): मूल कंप्यूटर प्रोग्राम ने यह मान लिया था कि सेट में प्रत्येक ब्लॉक को अद्वितीय होना चाहिए, भले ही वे एक-दूसरे को छू न रहे हों। लेखकों ने पाया कि कुछ आकृतियों के लिए, एकमात्र कारण यह था कि वे "असंभव" थीं क्योंकि दो ब्लॉक गलती से एक ही ब्लॉक बन गए थे। यदि आप उस नियम को ढीला कर देते, तो वह आकृति वास्तव में काम कर सकती थी! इसका मतलब था कि मूल प्रमाण "इंजेक्टिविटी" (injectivity - यह सुनिश्चित करना कि चीजें विशिष्ट हैं) के बारे में एक छिपे हुए नियम पर निर्भर था जो स्पष्ट नहीं था।
छिपे हुए डेड एंड्स (Hidden Dead Ends): कंप्यूटर सॉल्वर कभी-कभी "डिजेनरेट" (degenerate) मामलों को छोड़ देता था—अजीब, एज-केस परिदृश्य जहाँ गणित जटिल हो जाता है। नए प्रमाण-पत्रों ने लेखकों को इन जटिल मामलों को स्पष्ट रूप से लिखने के लिए मजबूर किया, यह सिद्ध करते हुए कि सबसे अजीब कोनों में भी, आकृतियाँ अभी भी अस्तित्व में नहीं रह सकतीं।
गणना की त्रुटियाँ: मूल शोध पत्र ने दावा किया था कि जांच के लिए 41 अंतिम उम्मीदवार आकृतियाँ बची हैं। डेटा के नए, कठोर पुनरावृत्ति (replay) ने दिखाया कि वास्तव में 43 थीं। पता चला कि मूल गणना दो से गलत थी। हालांकि यह बड़े चित्र को नहीं बदलता है (सीमा अभी भी 24 है), यह दर्शाता है कि इन पूर्ण रसीदों के बिना, हम पहेली के दो महत्वपूर्ण हिस्सों को मिस कर रहे होते।

परिणाम
यह शोध पत्र सफलतापूर्वक प्रमाणित करता है कि 180 विशिष्ट ज्यामितीय आकृतियाँ (जो 291 डेटा लाइनों से ली गई हैं) हमारी 3D दुनिया में नहीं बनाई जा सकतीं। उन्होंने यह अनवेरिफाइड "ब्लैक बॉक्स" उत्तरों को 291 वेरिफाइड, मशीन-चेकेबल प्रमाण-पत्रों से बदलकर किया।

उन्होंने यह भी सिद्ध किया कि वेक्टर्स की न्यूनतम संख्या के लिए 44 अंतिम उम्मीदवारों में से 42 को खारिज किया जा सकता है क्योंकि उनमें इनमें से एक प्रमाणित असंभव आकृति मौजूद है। इससे केवल 2 उम्मीदवार बचते हैं जो अभी भी अप्रामाणित हैं, लेकिन अब हम जानते हैं कि वे क्या हैं, और उन्हें सिद्ध करने का मार्ग स्पष्ट है।

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

तकनीकी सारांश: मिनिमम कोचेन-स्पेक्टर (Kochen–Specker) बाउंड के ज्यामितीय आधे भाग के लिए मशीन-चेक्ड सर्टिफिकेट

समस्या विवरण

न्यूनतम कोचेन-स्पेक्टर (KS) समस्या $\mathbb{R}^3$ में गैर-शून्य वेक्टर्स की न्यूनतम संख्या $n$ की खोज करती है, जो किरणों (rays) के रूप में युग्मवार भिन्न (pairwise distinct) हों, ताकि उनका ऑर्थोगोनैलिटी ग्राफ किसी भी $\{0, 1\}$ -कलरिंग को स्वीकार न करे जहाँ प्रत्येक ऑर्थोगोनल जोड़ी में अधिकतम एक $1$ हो और प्रत्येक ऑर्थोगोनल ट्रायड (triad) में ठीक एक $1$ हो। ज्ञात सर्वोत्तम निचली सीमा (lower bound) $n \ge 24$ है, जिसे Li et al. और Kirchweger et al. द्वारा कम्प्यूटेशनल रूप से स्थापित किया गया है।

यह प्रमाण दो भागों में विभाजित है:

संयोजन संबंधी आधा भाग (Combinatorial Half): क्रम 23 तक के उम्मीदवार ग्राफों का एक इसोमोर्फ-मुक्त (isomorph-free) SAT एन्यूमरेशन। असंतोषजनकता (Unsatisfiability) के परिणामों के साथ DRAT प्रमाण भी दिए गए हैं, जो स्वतंत्र रूप से जांचने योग्य हैं।
ज्यामितीय आधा भाग (Geometric Half): यह प्रदर्शन कि प्रत्येक एन्यूमरेटेड उम्मीदवार ग्राफ $\mathbb{R}^3$ में एम्बेडेबल (embeddable) नहीं है। यह आधा भाग यह निर्धारित करने के लिए Z3 के नॉन-लीनियर रियल अरिथमेटिक (NRA) सॉल्वर पर निर्भर करता है कि गैर-शून्य, किरण-भिन्न वेक्टर्स का कोई भी असाइनमेंट ऑर्थोगोनैलिटी बाधाओं को संतुष्ट नहीं करता है।

इस कार्य में पहचानी गई महत्वपूर्ण कमी यह है कि ज्यामितीय आधा भाग कोई जांचने योग्य प्रमाण ऑब्जेक्ट (proof object) उत्पन्न नहीं करता है। विश्वास की श्रृंखला एक $\exists\mathbb{R}$ -हार्ड थ्योरी के लिए Z3 की निर्णय प्रक्रिया (decision procedure) पर समाप्त हो जाती है, जिससे समुदाय को गैर-एम्बेडेबिलिटी के निर्णयों को विश्वास के आधार पर स्वीकार करना पड़ता है। इसके अलावा, प्रकाशित पाइपलाइन न्यूनतम गैर-एम्बेडेबल सबग्राफ के "ब्लॉकिंग डेटाबेस" पर निर्भर करती है, जो स्वयं Z3-व्युत्पन्न और unverifiable है।

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

लेखक वास्तविक गैर-एम्बेडेबिलिटी के लिए सटीक परिमेय केस-ट्री सर्टिफिकेट (exact rational case-tree certificates) उत्पन्न करने और सत्यापित करने के लिए एक ढांचा प्रस्तुत करते हैं। यह कार्यप्रणाली अपारदर्शी Z3 निर्णय प्रक्रिया को एक पारदर्शी, बीजगणितीय सत्यापन प्रक्रिया से बदल देती है।

1. सर्टिफिकेट संरचना
एक सर्टिफिकेट एक स्व-निहित वस्तु है जिसमें शामिल हैं:

एंकर और प्रोपेगेशन (Anchor and Propagation): एक नॉर्मलाइजेशन चरण (एक ऑर्थोगोनल ट्रायड या एज को एंकर करना) जिसके बाद एक प्रोपेगेशन शेड्यूल होता है जो क्रॉस-प्रोडक्ट्स और प्लेन पैरामीट्राइजेशन का उपयोग करके कुछ मापदंडों के संदर्भ में सभी वर्टेक्स वेक्टर्स को व्यक्त करता है।
केस ट्री (Case Tree): एक ट्री संरचना जहाँ आंतरिक नोड्स निम्नलिखित के आधार पर विभाजन (splits) का प्रतिनिधित्व करते हैं:
- गुणनखंडन (Factorization): $p = \prod f_k$ , जिसे विस्तार (expansion) द्वारा सत्यापित किया जाता है।
- वर्गों का योग (Sum-of-Squares - SOS): $p = \sum c_k m_k^2$ जहाँ $c_k \in \mathbb{Q}_{>0}$ , जिसे विस्तार द्वारा सत्यापित किया जाता है।
लीव्स (Leaves): शाखाओं को चार तंत्रों में से एक द्वारा बंद किया जाता है:
- इन्जेक्टिविटी कोलिजन (Injectivity Collision): यह सिद्ध करना कि दो अलग-अलग वर्टेक्स समानांतर किरणों (parallel rays) पर मैप होते हैं।
- ऑब्लिगेशन कोलैप्स (Obligation Collapse): यह दिखाना कि एक आवश्यक गैर-शून्य बहुपद (polynomial) शून्य के समान है।
- आइडियल मेंबरशिप (Ideal Membership): स्पष्ट को-फैक्टर्स जो सिद्ध करते हैं कि एक बहुपद बाधाओं द्वारा उत्पन्न आइडियल (ideal) में है।
- पॉजिटिवस्टेलेंसाट-आकार की पॉज़िटिविटी (Positivstellensatz-shaped Positivity): एक सामान्यीकृत तर्क जो दिखाता है कि धनात्मक पदों (इन्जेक्टिविटी पॉलिनोमिअल्स) का योग वर्गों के योग के बराबर है, जो वास्तविक बिंदुओं पर एक विरोधाभास की ओर ले जाता है।

2. सत्यापन आर्किटेक्चर (Verification Architecture)
यह प्रणाली दो स्वतंत्र चेकरों का उपयोग करती है जिनका सर्टिफिकेट जनरेटर के साथ कोई कोड साझा नहीं है:

प्योर-पायथन रीप्ले (Pure-Python Replay): सटीक परिमेय अंकगणित का उपयोग करके सर्टिफिकेट लॉजिक को निष्पादित करता है।
लीन 4 टोटल चेकर (Lean 4 Total Checker): लीन 4 प्रूफ असिस्टेंट में कार्यान्वित एक रिफ्लेक्टिव फंक्शन Cert.check|
- कर्नेल-रिड्यूसिबिलिटी (Kernel-Reducibility): यह सुनिश्चित करने के लिए कि निर्णय एक क्लोज्ड कर्नेल प्रमेय है, लेखकों ने एक gcd-free परिमेय अंकगणित परत (KRat) और फ्यूल-स्ट्रक्चरल रिकर्सन लागू किया है। यह पूरी गणना को बिना नेटिव रिडक्शन या कस्टम एक्सिओम्स के लीन कर्नेल द्वारा कम करने की अनुमति देता है।
- एक्सिओम क्लोजर (Axiom Closure): साउंडनेस प्रमेय केवल {propext, Classical.choice, Quot.sound} पर निर्भर करता है, जिससे अनवेरिफाइड नेटिव रिडक्शन से बचा जा सके।

3. साउंडनेस प्रमेय (Soundness Theorem)
मुख्य प्रमेय, check_sound, कहता है कि यदि check c = true, तो ग्राफ का कोई वास्तविक रूप (realization) मौजूद नहीं है। एक 'रियलाइजेशन' को $\mathbb{R}^3$ में एक मैप के रूप में परिभाषित किया गया है जो गैर-शून्य वेक्टर्स, किनारों पर ऑर्थोगोनैलिटी, और सभी वर्टेक्स जोड़ों के लिए युग्मवार किरण-विशिष्टता (pairwise ray-distinctness/injectivity) को संतुष्ट करता है।

मुख्य योगदान

सटीक परिमेय सर्टिफिकेट: एक सर्टिफिकेट फॉर्मेट का परिचय जो संख्यात्मक अनुमानों और अपारदर्शी सॉल्वरों को सटीक परिमेय अंकगणित, बहुपद गुणनखंडन और SOS अपघटन (decompositions) से बदल देता है।
ब्लॉकिंग डेटाबेस का पूर्ण कवरेज: प्रकाशित PhysicsCheck ब्लॉकिंग सूचियों (क्रम 10–13) से सभी 291 स्रोत लाइनों (जो 180 विशिष्ट ग्राफ का प्रतिनिधित्व करती हैं) का प्रमाणन, प्रत्येक Z3 निर्णय को मशीन-चेक्ड प्रमेय से बदलना।
दोहरा स्वतंत्र रीप्ले: दो अलग-अलग चेकरों (Python और Lean) द्वारा सत्यापन जो 115 प्रतिकूल उत्परिवर्तनों (जैसे, छेड़छाड़ किए गए गुणांक, हटाए गए ब्रांच) को अस्वीकार करते हैं, जबकि वास्तविक सर्टिफिकेट को स्वीकार करते हैं।
फॉर्मलाइजेशन-संचालित निष्कर्ष: कठोर फॉर्मलाइजेशन ने मूल पाइपलाइन में विशिष्ट समस्याओं को उजागर किया:
- इन्जेक्टिविटी भार-वहन करने वाली है (Injectivity is Load-Bearing): मूल Z3 एनकोडिंग ने केवल आसन्न (adjacent) जोड़ों के लिए ही नहीं, बल्कि सभी जोड़ों के लिए युग्मवार किरण-विशिष्टता लागू की थी। डेटाबेस के कई ग्राफ केवल इसी इन्जेक्टिविटी बाधा के कारण गैर-एम्बेडेबल हैं, जो मानक ज्यामितीय सॉल्वरों के लिए अदृश्य है।
- छिपे हुए WLOG मामले: मूल पाइपलाइन में उपयोग किए गए ऑर्थोप्लेन पैरामीट्राइजेशन ने डिजेनरेट मामलों (समानांतर वेक्टर्स) को छिपा दिया था, जिन्हें इन्जेक्टिविटी तर्कों द्वारा स्पष्ट रूप से सिद्ध किया जाना चाहिए।
- अनुभवजन्य अनुकूलन (Empirical Optimization): मूल पाइपलाइन में एक "नॉन-कलरैबिलिटी" अनुकूलन को भार-वहन करने वाले लेम्मा के बजाय अनुभवजन्य पाया गया।
- पुनरुत्पादक गणना (Reproducible Counts): अंतिम क्रम-23 उम्मीदवारों की प्रकाशित संख्या (41) आर्टिफ़ैक्ट्स से पुनरुत्पादित नहीं की जा सकी; सही संख्या 43 है, जिसमें 42 को नए क्रम-13 सर्टिफिकेट द्वारा सिद्ध किया गया है।

परिणाम

सत्यापन कवरेज: ब्लॉकिंग डेटाबेस के सभी 180 विशिष्ट ग्राफों के पास अब उनकी गैर-एम्बेडेबिलिटी सिद्ध करने वाले क्लोज्ड कर्नेल प्रमेय हैं।
प्रदर्शन: एक मानक लैपटॉप पर क्रम-10/11/12 ग्राफों के लिए कर्नेल मूल्यांकन लागत लगभग 0.5 सेकंड और क्रम-13 ग्राफों के लिए 1.8 सेकंड है। संपूर्ण सत्यापन सूट मिनटों में चलता है।
बाउंड पर प्रभाव: सात नए क्रम-13 सर्टिफिकेट, सत्यापित सबग्राफ मोनोटोनिसिटी के माध्यम से क्रम-22/23 एन्यूमरेशन के 44 अंतिम उम्मीदवारों में से 42 को सिद्ध करते हैं। शेष दो उम्मीदवारों को स्पष्ट, मशीन-पठनीय दायित्वों (obligations) के रूप में ट्रैक किया गया है।
प्रतिकूल मजबूती (Adversarial Robustness): दोनों चेकर निरंतर एकीकरण (continuous integration) में सभी 115 उत्परिवर्तित सर्टिफिकेट को सफलतापूर्वक अस्वीकार करते हैं, जो यह दर्शाता है कि सत्यापन तर्क केवल जनरेटर के आउटपुट का रीप्ले नहीं है बल्कि एक वास्तविक स्वतंत्र जांच है।

महत्व

यह शोध पत्र दावा करता है कि ब्लॉकिंग डेटाबेस के संबंध में मिनिमम KS बाउंड के ज्यामितीय आधे भाग के लिए विश्वास की कमी (trust gap) को समाप्त करता है। अनवेरिफाइड Z3 निर्णयों को क्लोज्ड कर्नेल प्रमेयों में बदलकर, यह कार्य सुनिश्चित करता है कि महत्वपूर्ण सबग्राफ की गैर-एम्बेडेबिलिटी अब ब्लैक-बॉक्स सॉल्वर में विश्वास का मामला नहीं है।

लेखक इस बात पर जोर देते हैं कि फॉर्मलाइजेशन प्रक्रिया स्वयं मूल्य का प्राथमिक स्रोत थी, जिसने छिपे हुए धारणाओं (इन्जेक्टिविटी), छिपे हुए केस दायित्वों और डेटा विसंगतियों को सामने लाया जो मूल वर्कफ़्लो के लिए अदृश्य थे। हालांकि यह शोध पत्र अभी तक $n \ge 24$ के लिए पूरी तरह से सत्यापित एंड-टू-एंड प्रमेय का निर्माण नहीं करता है (SAT एन्यूमरेशन और कैनोनिसिटी प्रमाण के पैमाने के कारण), यह सत्यापित ज्यामितीय आधार स्थापित करता है और आगे का स्केलेबल मार्ग प्रदान करता है। यह कार्य प्रदर्शित करता है कि क्वांटम फाउंडेशन में जटिल ज्यामितीय तर्क को सटीक अंकगणित और न्यूनतम एक्सिओम्स के साथ पूरी तरह से मशीन-चेकेबल बनाया जा सकता है।