Proof by Mechanization: Cubic Diophantine Equation Satisfiability is $Σ^0_1$-Complete

यहाँ मिलान रोस्को (Milan Rosko) के शोध पत्र "Proof by Mechanization: Cubic Diophantine Equation Satisfiability is $\Sigma^0_1$-Complete" का विस्तृत तकनीकी सारांश दिया गया है।

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

यह शोध पत्र कम घात (low degree) वाले डिओफैन्टीन समीकरणों (Diophantine equations) के संबंध में गणितीय तर्क और संख्या सिद्धांत की एक दीर्घकालिक खुली समस्या पर काम करता है, जो हिल्बर्ट की दसवीं समस्या (H10) से संबंधित है।

• संदर्भ: यह सर्वविदित है (MRDP प्रमेय के माध्यम से) कि प्राकृतिक संख्याओं में किसी डिओफैन्टीन समीकरण के समाधान का निर्धारण करने की सामान्य समस्या अनिर्णय योग्य ($\Sigma^0_1$-complete) है। हालाँकि, इसकी जटिलता घात ($d$) और चरों की संख्या ($n$) पर निर्भर करती है।
• ज्ञात सीमाएँ (Known Bounds):
  • घात 2 (Degree 2): निर्णायक (Hasse-Minkowski जैसे शास्त्रीय संख्या सिद्धांत विधियों के माध्यम से)।
  • घात 4 (Degree 4): अनिर्णय योग्य (जोन्स, 1980 ने दिखाया कि 58 चरों वाला एक सार्वभौमिक समीकरण मौजूद है)।
  • घात 3 (Degree 3): चरों की एक निश्चित संख्या वाले एक एकल क्यूबिक (cubic) डिओफैन्टीन समीकरण की स्थिति एक खुली समस्या थी। घात 3 में पिछले रिडक्शन (reductions) अक्सर समीकरणों के सिस्टम पर आधारित थे या उनमें अनबाउंडेड (unbounded) चरों की आवश्यकता थी, जिससे एक निश्चित अरिटी (arity) वाले एकल सार्वभौमिक क्यूबिक समीकरण को बनाने में विफलता मिली।
• लक्ष्य: लेखक का लक्ष्य यह सिद्ध करना है कि प्राकृतिक संख्याओं ($\mathbb{N}$) पर कुल घात $\le 3$ वाले एक एकल डिओफैन्टीन समीकरण की संतुष्टि (satisfiability), जहाँ चरों की संख्या इनपुट में एनकोडेड है, $\Sigma^0_1$-complete (और इस प्रकार अनिर्णय योग्य) है।

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

यह शोध पत्र कमजोर अंकगणित (weak arithmetic), मशीनीकृत प्रमाण सत्यापन (mechanized proof verification), और रचनात्मक डिओफैन्टिक एनकोडिंग को संयोजित करते हुए एक कठोर, बहु-स्तरीय दृष्टिकोण अपनाता है।

A. सैद्धांतिक ढांचा: रजिस्टर अंकगणित (Register Arithmetic - RA)

लेखक प्रथम-क्रम अंकगणित (first-order arithmetic) के एक विशिष्ट खंड को रजिस्टर अंकगणित (RA) के रूप में परिभाषित करते हैं, जो बिना गुणन वाली भाषा ($L_{RA} = \{0, S, +, =\}$) के साथ $I\Delta_0 + B\Sigma_1$ का प्रतिबंध है।

• मुख्य अंतर्दृष्टि: जबकि RA में गुणन एक मूल तत्व (primitive) नहीं है, इसे पुनरावृत्त योग (iterated addition) के माध्यम से एक $\Sigma^1$ संबंध के रूप में दर्शाया जा सकता है। यह RA को रोबिन्सन अंकगणित ($Q$) की व्याख्या करने और केवल बाउंडेड जोड़ और सक्सेसर ऑपरेशन्स का उपयोग करके परिमित गणना ट्रेसेस (finite computation traces) को सिम्युलेट करने की अनुमति देता है।
• तंत्र: प्रमाण जाँचकर्ता (proof checker) के परिमित निष्पादन ट्रेसेस को ज़ेकेंडोर्फ प्रतिनिधित्व (Zeckendorf representations - फाइबोनैसी आधार) पर आधारित कैरिलैस पेयरिंग (Carryless Pairing) का उपयोग करके प्राकृतिक संख्याओं के रूप में एनकोड किया जाता है। यह अंकगणितीय 'कैरी' (carries) से बचता है, जिससे एनकोडिंग बाधाएं द्विघातीय (quadratic) बनी रहती हैं।

B. कंपाइलर: प्रमाणों से बहुपदों तक (From Proofs to Polynomials)

मुख्य योगदान एक समान प्रिमिटिव रिकर्सिव कंपाइलर (uniform primitive recursive compiler) है जो अंकगणितीय वाक्यों (और उनके प्रमाणों) के कोड को डिओफैन्टिक बाधा प्रणालियों (Diophantine constraint systems) में मैप करता है।

1. अंकगणित (Arithmetization): प्रमाण जाँच (Axiom matching, Modus Ponens verification) को बहुपदीय बाधाओं में अनुवादित किया जाता है।
2. घात नियंत्रण रणनीति (Degree Control Strategy):
   • द्विघातीय परत (Quadratic Layer): सिंटैक्टिक जाँच (समानता, अनुक्रम निष्कर्षण, बुलियन लॉजिक) $\le 2$ घात के बाधाओं में संकलित होती है।
   • क्यूबिक ट्रिगर (Cubic Trigger): एकमात्र घात-3 पद एक विशिष्ट "गार्ड" तंत्र से उत्पन्न होते हैं। एक रैखिक चयन चर ($a_i \in \{0,1\}$) एक द्विघातीय बाध्यता ($Q(\vec{x}) = 0$) को उत्पाद $a_i \cdot Q(\vec{x}) = 0$ के माध्यम से सक्रिय करता है। चूँकि $a_i$ घात 1 का है और $Q$ घात 2 का है, इसलिए उत्पाद घात 3 का होता है। महत्वपूर्ण बात यह है कि कोई भी द्विघातीय गार्ड द्विघातीय पद को गुणा नहीं करता है।
3. एकत्रीकरण (The "Collapse"):
   • कंपाइलर क्यूबिक समीकरणों का एक परिमित सिस्टम बनाता है।
   • समीकरणों के सिस्टम को एक एकल क्यूबिक समीकरण में बदलने के लिए लेखक 'सम-ऑफ-स्क्वेयर्स' (sum-of-squares) विधि का उपयोग करने के बजाय, फाइबोनैसी बैंड्स पर आधारित मिक्स्ड-रेडिक्स एकत्रीकरण (Mixed-Radix Aggregation) तकनीक का उपयोग करते हैं।
   • बाधाओं को $A_i = B_i$ (गैर-ऋणात्मक चैनल) के रूप में फिर से लिखा जाता है। क्षमता संबंधी बाधाएं अंक सीमाओं ($0 \le A_i, B_i < B$) को लागू करती हैं।
   • एक एकल समीकरण एक भारित योग द्वारा बनाया जाता है: $\sum B^i (A_i - B_i) = 0$। बेस-$B$ प्रतिनिधित्व की विशिष्टता के कारण, यह एकल समीकरण तभी संतुष्ट होता है जब मूल की सभी बाधाएं संतुष्ट हों।
   • परिणाम: एकत्रीकरण मूल घात को 3 पर बनाए रखता है।

C. Rocq में मशीनीकरण (Mechanization in Rocq)

इस जटिल निर्माण की वैधता सुनिश्चित करने के लिए, पूरी पाइपलाइन को Rocq (एक प्रूफ असिस्टेंट, संभवतः Coq का एक संस्करण) में मशीनीकृत किया गया है।

• परतें (Layers):
  1. आधार (Foundations): फाइबोनैसी अंकगणित और कैरिलैस पेयरिंग।
  2. सत्यापन (Verification): हिल्बर्ट-एकरमैन (Hilbert-Ackermann) प्रमाण प्रणाली को बहुपदीय बाधाओं में अनुवादित करना।
  3. एकत्रीकरण (Aggregation): घात-संरक्षण वाले कोलैप्स (degree-preserving collapse) को सिद्ध करना।
  4. प्रमाण सिद्धांत (Proof Theory): कमजोर अंकगणित के संदर्भ में डायगोनल तर्क (diagonal argument) और गोडेल के दूसरे अपूर्णता प्रमेय (Gödel's Second Incompleteness Theorem) को औपचारिक रूप देना।
• आउटपुट: मशीनीकरण एक "पिन्ड" (pinned) गुणांक तालिका (coefficient table) का उत्पादन करता है जो एक सार्वभौमिक क्यूबिक बहुपद के लिए है, जिसे कर्नेल द्वारा घात $\le 3$ के रूप में सत्यापित किया गया है।

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

1. घात 3 की समस्या का समाधान: यह शोध पत्र एक एकल सार्वभौमिक क्यूबिक डिओफैन्टीन समीकरण का निर्माण करता है जिसमें चरों की संख्या निश्चित है (मुख्य निर्माण में 9,692 चर), हालांकि इस सीमा को कम किया जा सकता है। यह सिद्ध करता है कि $\mathbb{N}$ पर सार्वभौमिकता के लिए घात 3 पर्याप्त है।
2. प्रत्यक्ष प्रमाण-से-बहुपद कंपाइलर: पिछले रिडक्शन जो MRDP प्रमेय को एक ब्लैक बॉक्स के रूप में उपयोग करते थे, उनके विपरीत, यह कार्य सीधे प्रूफ चेकिंग के डिओफैन्टिक प्रतिनिधित्व का निर्माण करता है, जिसमें प्रत्येक चरण में बहुपदीय घात पर स्पष्ट और स्थानीय नियंत्रण होता है।
3. घात-संरक्षण एकत्रीकरण (Degree-Preserving Aggregation): "फाइबोनैसी-बैंडेड" एकत्रीकरण विधि का परिचय जो घात को बढ़ाए बिना (सम-ऑफ-स्क्वेयर्स के कारण होने वाले घात-दोहरीकरण से बचते हुए) क्यूबिक समीकरणों के सिस्टम को एक एकल क्यूबिक समीकरण में समाहित करती है।
4. मशीनीकृत सत्यापन (Mechanized Verification): पूरा रिडक्शन, जिसमें डिग्री सर्टिफिकेट और अंकगणितीय प्रमाण योग्यता तथा बहुपदीय समाधान के बीच का सिमेंटिक ब्रिज शामिल है, Rocq में औपचारिक रूप से सत्यापित है। यह निर्माण के "हाथ से लिखे" (hand-waving) होने की संभावना को समाप्त करता है।
5. ठोस आर्टिफैक्ट्स (Concrete Artifacts): शोध पत्र सार्वभौमिक क्यूबिक के बद्ध संस्करणों के लिए स्पष्ट, मशीन-पठनीय गुणांक तालिकाएं (Python द्वारा जनरेट और Rocq द्वारा सत्यापित) प्रदान करता है, जो दर्शाता है कि परिणाम केवल अस्तित्ववादी (existential) नहीं बल्कि रचनात्मक (constructive) है।

4. परिणाम (Results)

• $\Sigma^0_1$-पूर्णता ($\Sigma^0_1$-Completeness): यह सिद्ध होता है कि प्राकृतिक संख्याओं ($\mathbb{N}$) पर एक एकल क्यूबिक डिओफैन्टीन समीकरण की संतुष्टि $\Sigma^0_1$-complete है।
• अनिर्णय योग्यता (Undecidability): फलस्वरूप, यह समस्या अनिर्णय योग्य है। कोई भी ट्यूरिंग मशीन ऐसे सभी समीकरणों की समाधान क्षमता को तय नहीं कर सकती।
• चरों की संख्या (Variable Count): निर्माण एक विशिष्ट सार्वभौमिक बहुपद प्रदान करता है जिसमें 9,692 चर हैं। शोध पत्र नोट करता है कि यह एक 'वर्स्ट-केस' सीमा है और उपयोग किए गए चतुर्थांश-से-त्रिक (quartic-to-cubic) रिडक्शन को अनुकूलित करके इसे कम किया जा सकता है।
• बद्ध सार्वभौमिकता (Bounded Universality): किसी भी निश्चित संसाधन सीमा $k$ (जैसे, प्रमाण की लंबाई) के लिए, एक निर्णायक स्लाइस (एक विशिष्ट क्यूबिक समीकरण) मौजूद है जो इस सीमा के भीतर प्रमाण योग्यता को दर्शाता है। अनिर्णय योग्यता किसी भी इनपुट के लिए संसाधन पैरामीटर $k$ को कंप्यूट योग्य रूप से सीमित करने में असमर्थता से उत्पन्न होती है।

5. महत्व (Significance)

• सैद्धांतिक पूर्णता (Theoretical Closure): यह ज्ञात चतुर्थातीय (quartic) अनिर्णय योग्य मामले और निर्णायक द्विघातीय (quadratic) मामले के बीच के अंतर को पाटता है, जिससे घात 3 को $\mathbb{N}$ पर एकल डिओफैन्टीन समीकरणों में अनिर्णय योग्यता के सटीक थ्रेशोल्ड (threshold) के रूप में स्थापित करता है।
• प्रमाण-सैद्धांतिक अंतर्दृष्टि (Proof-Theoretic Insight): यह कार्य प्रदर्शित करता है कि अनिर्णय (undecidability) को परिभाषित करने के लिए आवश्यक तार्किक संसाधन (स्व-संदर्भ, डायगोनलाइजेशन) ठीक उन्हीं बीजगणितीय संसाधनों के बराबर हैं जो क्यूबिक पदों (द्विघातीय बाधाओं के सेलेक्टर एक्टिवेशन) को उत्पन्न करने के लिए आवश्यक हैं।
• पद्धतिगत बदलाव (Methodological Shift): मशीनीकरण का उपयोग करके, यह शोध पत्र डिओफैन्टिक अनुसंधान को "अस्तित्व प्रमाणों" (existence proofs) से "रचनात्मक आर्टिफैक्ट्स" (constructive artifacts) की ओर ले जाता है। सार्वभौमिक बहुपद केवल एक सैद्धांतिक वस्तु नहीं है; यह एक ठोस, सत्यापन योग्य डेटा संरचना है।
• सीमा की अप्रत्याशितता (Impredicativity of the Boundary): यह शोध पत्र तर्क देता है कि अनिर्णय की सीमा "इम्प्रेडिकेटिव" (impredicative) है—आप उस सटीक बिंदु को निर्धारित नहीं कर सकते जहाँ अनिर्णय शुरू होता है, जब तक कि आप उस एनकोडिंग का निर्माण न करें जो इसे उत्पन्न करता है। क्यूबिक थ्रेशोल्ड एक कॉम्बिनेटरियल दुर्घटना नहीं है, बल्कि स्व-संदर्भ को एनकोड करने की एक संरचनात्मक आवश्यकता है।

संक्षेप में, मिलान रोस्को का शोध पत्र एक मशीनीकृत प्रमाण प्रदान करता है कि एकल क्यूबिक डिओफैन्टीन समीकरण अनिर्णय योग्य हैं, जो एक विशिष्ट, सत्यापित सार्वभौमिक बहुपद का निर्माण करके और एक नवीन, घात-संरक्षण एकत्रीकरण तकनीक का प्रदर्शन करके दशकों पुरानी खुली समस्या को हल करता है।