Proving Properties of $φ$-Representations with the Walnut Theorem-Prover

यहाँ जेफरी शालिट के शोध पत्र "Proving Properties of $\phi$-Representations with the Walnut Theorem-Prover" का विस्तृत तकनीकी सारांश दिया गया है।

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

यह शोध पत्र $\phi$-प्रतिनिधित्वों ($\phi$-representations या base-$\phi$ expansions) के विश्लेषण की जटिलता को संबोधित करता है, जहाँ $\phi = (1+\sqrt{5})/2$ स्वर्णिम अनुपात (golden ratio) है। जबकि जॉर्ज बर्गमैन (1957) ने यह स्थापित किया था कि गैर-ऋणात्मक वास्तविक संख्याओं को $\{0, 1\}$ अंकों का उपयोग करके base-$\phi$ में विस्तारित किया जा सकता है, और फ्रौग्नी और सकारोविच (2006) ने सिद्ध किया था कि एक पूर्णांक के कैनोनिकल $\phi$-प्रतिनिधित्व की गणना एक परिमित ऑटोमेटन (finite automaton) द्वारा की जा सकती है, मूल ऑटोमेटन का निर्माण निहित (implicit) था और इसे आगे के गुणों को प्राप्त करने के लिए उपयोग करना कठिन था।

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

• स्पष्ट ऑटोमाटा का अभाव: फ्रौग्नी-सकारोविच ऑटोमेटन को इस तरह से स्पष्ट रूप से निर्मित नहीं किया गया था जिससे उसे आसानी से हेरफेर या विस्तार किया जा सके।
• प्रमाणों की जटिलता: $\phi$-प्रतिनिधित्वों से संबंधित मौजूदा परिणाम (जैसे डेकिंग और वान लून द्वारा) अक्सर प्रतिनिधित्वों को गिनने, अंकों के योग को निर्धारित करने, या विशिष्ट पैटर्न (जैसे पैलिंड्रोम) को चरित्रित करने के लिए जटिल, थकाऊ गणितीय इंडक्शन (induction) पर निर्भर करते हैं।
• स्वचालन (Automation) की आवश्यकता: बिना किसी मैनुअल केस-दर-केस विश्लेषण के, प्रमेयों को सिद्ध करने, विस्तारों को सूचीबद्ध करने और नए गुणों की खोज करने के लिए एक समान, "स्वचालित" विधि की आवश्यकता है।

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

लेखक Walnut का उपयोग करते हैं, जो हामून मौसावी द्वारा विकसित एक फ्री थ्योरम-प्रूवर सॉफ्टवेयर है, जो ऑटोमैटिक अनुक्रमों (automatic sequences) के बारे में तर्क करने के लिए प्रेसबर ऑटोमैटिक (Presburger arithmetic) के विस्तारों के निर्णय प्रक्रियाओं (decision procedures) का उपयोग करता है।

मुख्य कार्यप्रवाह (Core Workflow):

1. प्रतिनिधित्व प्रणाली (Representation Systems): शोध पत्र दो पूर्णांक प्रतिनिधित्व प्रणालियों का उपयोग करता है:
   • जेकोडोर्फ सिस्टम (Zeckendorf System): फाइबोनैकी संख्याओं ($F_n$) का उपयोग करके गैर-ऋणात्मक पूर्णांकों का कैनोनिकल प्रतिनिधित्व, जिसमें लगातार दो 1 नहीं होते।
   • नेगाफाइबोनैकी सिस्टम (NegaFibonacci System): ऋणात्मक-इंडेक्स वाली फाइबोनैकी संख्याओं ($F_{-n}$) का उपयोग करके पूर्णांकों (धनात्मक, ऋणात्मक, शून्य) का प्रतिनिधित्व।
2. ऑटोमेटन निर्माण: मैन्युअल रूप से एक जटिल स्टेट मशीन डिजाइन करने के बजाय, लेखक Walnut में छोटे, मॉड्यूलर ऑटोमाटा को संयोजित करके फ्रौग्नी-सकारोविच ऑटोमेटन का निर्माण करते हैं। ये मॉड्यूल संभालते हैं:
   • सामान्यीकरण (Normalization - मनमाने बाइनरी स्ट्रिंग्स को कैनोनिकल जेकोडोर्फ/नेगाफाइबोनैकी रूपों में बदलना)।
   • शिफ्टिंग (प्रतिनिधित्वों का बाएँ/दाएँ शिफ्ट होना)।
   • बिट निष्कर्षण (last, second-to-last bits)।
   • जेकोडोर्फ और नेगाफाइबोनैकी प्रणालियों के बीच रूपांतरण।
3. तार्किक सूत्रीकरण (Logical Formulation): संबंध $n = [x.y]_\phi$ को प्रथम-क्रम तर्क (first-order logic) में व्यक्त किया गया है। पहचान $\phi^k = F_k\phi + F_{k-1}$ का उपयोग करते हुए, शोध पत्र यह व्युत्पन्न करता है कि पूर्णांक $n$ और $\phi$-विस्तार $x.y$ शिफ्ट किए गए प्रतिनिधित्वों को शामिल करने वाले विशिष्ट रैखिक समीकरणों को संतुष्ट करते हैं।
4. स्वचालित सत्यापन (Automated Verification): Walnut इन तार्किक शर्तों के प्रतिच्छेदन (intersection) की गणना करके एक परिमित ऑटोमेटन (विशेष रूप से, 116 अवस्थाओं वाला, जिसे कैनोनिकल रूपों के लिए 39 तक कम किया जा सकता है) उत्पन्न करता है।
5. परिणाम प्राप्त करना: एक बार ऑटोमेटन बन जाने के बाद, इसका उपयोग निम्नलिखित के लिए किया जाता है:
   • गणना कार्यों (counting functions) के लिए रैखिक प्रतिनिधित्व (matrix morphisms) की गणना करना।
   • यह जाँचकर कि विशिष्ट तार्किक सूत्र TRUE का मूल्यांकन करते हैं या नहीं, गुणों को सत्यापित करना।
   • विशिष्ट प्रकार के विस्तारों (जैसे Knott expansions, palindromes) को मुख्य ऑटोमेटन के साथ प्रतिच्छेद करके सूचीबद्ध करना।

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

• फ्रौग्नी-सकारोविच ऑटोमेटन का स्पष्ट निर्माण: शोध पत्र पहली बार $\phi$-प्रतिनिधित्व स्वीकार करने वाले ऑटोमेटन का एक स्पष्ट, मॉड्यूलर निर्माण प्रदान करता है, जो इसे एक सैद्धांतिक अस्तित्व प्रमाण से एक कम्प्यूटेशनल टूल में बदल देता है।
• एकीकृत प्रमाण ढांचा (Unified Proof Framework): यह प्रदर्शित करता है कि $\phi$-प्रतिनिधित्वों से संबंधित विविध परिणामों को ऑटोमाटा सिद्धांत का उपयोग करके समान रूप से सिद्ध किया जा सकता है, जिससे ad-hoc इंडक्शन प्रमाणों की आवश्यकता समाप्त हो जाती है।
• स्वचालित सूचीकरण (Automatic Enumeration): यह दिखाता है कि कैसे विशिष्ट प्रकार के विस्तारों (जैसे Knott expansions) को स्वचालित रूप से गिना जा सकता है और उनके एसिम्प्टोटिक व्यवहार (asymptotic behavior) की गणना की जा सकती है।
• नई खोजें: अंक योग (digit sums), प्रतिनिधित्व की लंबाई, 1 के वर्टिकल रन (vertical runs), और एंटीपैलिंड्रोमिक विस्तारों के संबंध में नए प्रमेय पहचानता है और सिद्ध करता है।

4. मुख्य परिणाम (Key Results)

शोध पत्र कई परिणाम प्राप्त करता है, जिनमें से कई नए हैं या मौजूदा अनुमानों के सरल प्रमाण प्रदान करते हैं:

• फाइबोनैकी और लुकास संख्याओं के कैनोनिकल प्रतिनिधित्व:
  • $F_{4i}, F_{4i+1}, F_{4i+2}, F_{4i+3}$ और $L_{2i}, L_{2i+1}$ के $\phi$-विस्तार के लिए स्पष्ट सूत्र प्रदान करता है।
  • सिद्ध करता है कि $F_n$ का $\phi$-प्रतिनिधित्व 4 के modulo में एक आवधिक पैटर्न (periodic pattern) का पालन करता है।
• अंकों का योग (Digit Sums):
  • प्रमेय 3.1: डेल गेर्डमैन के 2012 के एक अनुमान को सिद्ध करता है: $n$ के जेकोडोर्फ प्रतिनिधित्व में अंकों का योग हमेशा कैनोनिकल बेस-$\phi$ प्रतिनिधित्व में अंकों के योग के बराबर या उससे कम होता है।
  • विस्तार के बाएं और दाएं भाग में अंकों के योग के लिए रैखिक प्रतिनिधित्व की गणना करता है।
• प्रतिनिधित्व की लंबाई (Length of Representations):
  • $(n)_\phi$ के बाएं भाग की लंबाई को चरित्रित करता है। सिद्ध करता है कि $\ell(n) - \ell(n-1)$ का अंतर 1 है यदि और केवल यदि $n$ एक लुकास संख्या है या उनसे संबंधित है।
• व्यक्तिगत बिट्स और वर्टिकल रन (Individual Bits and Vertical Runs):
  • विशिष्ट बिट्स को स्टर्मियन अनुक्रमों (Sturmian sequences) और लुकास प्रतिनिधित्वों से जोड़ता है।
  • प्रमेय 5.4: $\phi$-विस्तार में 1 के "वर्टिकल रन" की सटीक लंबाई निर्धारित करता है, जो लुकास संख्याओं को शामिल करते हुए एक क्लोज्ड फॉर्म प्रदान करता है, जो डेकिंग और वान लून के इस दावे का खंडन करता है कि "ऐसी कोई नियमितता नहीं है।"
• पैलिंड्रोमिक और एंटीपैलिंड्रोमिक विस्तार (Palindromic and Antipalindromic Expansions):
  • पैलिंड्रोमिक और एंटीपैलिंड्रोमिक $\phi$-प्रतिनिधित्वों (कैनोनिकल और गैर-कैनोनिकल दोनों) को पहचानने के लिए ऑटोमाटा का निर्माण करता है।
• नॉट एक्सपेंशन (Knott Expansions):
  • डेकिंग और वान लून के "Knott expansions" (जो 011 पर समाप्त नहीं होते) से संबंधित परिणामों को पुनः प्राप्त करता है और सरल बनाता है।
  • $O(\log n)$ समय में Knott विस्तारों की कुल संख्या, $Tot_\kappa(n)$, की गणना करने के लिए एक रैखिक प्रतिनिधित्व व्युत्पन्न करता है।
  • अंतराल $[F_i, F_{i+1})$ में Knott विस्तारों की औसत संख्या के लिए एसिम्प्टोटिक परिणाम सिद्ध करता है।
• डेकिंग-वान लून (DVL) विस्तार:
  • ऑटोमाटा को "DVL-expansions" (जो विशिष्ट स्थानों में ही 11 की अनुमति देते हैं) को संभालने के लिए अनुकूलित करता है, जिससे वर्टिकल रन पर उनके परिणामों को स्वचालित रूप से पुनः प्राप्त किया जाता है।
• बीजगणितीय पूर्णांक (Algebraic Integers):
  • $m\phi + n$ (जहाँ $m, n \in \mathbb{Z}$) के रूप के बीजगणितीय पूर्णांकों के लिए $\phi$-प्रतिनिधित्व की गणना करने के लिए पद्धति का विस्तार करता है।

5. महत्व (Significance)

• कम्प्यूटेशनल नंबर थ्योरी: यह शोध पत्र सैद्धांतिक ऑटोमाटा परिणामों और व्यावहारिक गणना के बीच के अंतर को पाटता है। यह प्रदर्शित करता है कि $\phi$-विस्तार के जटिल संख्या-सिद्धांत संबंधी गुणों को परिमित ऑटोमाटा संचालन में बदला जा सकता है।
• इंडक्शन का उन्मूलन: Walnut थ्योरम-प्रूवर का उपयोग करके, लेखक लंबे, त्रुटि-प्रवण इंडक्शन प्रमाणों को एल्गोरिथमिक सत्यापन से बदल देते हैं। यह इस बात का सुझाव देता है कि भविष्य में ऐसी समस्याओं के प्रति दृष्टिकोण कैसे बदला जा सकता है।
• सामान्यीकरण (Generalizability): $\phi$ पर केंद्रित होने के बावजूद, लेखक नोट करते हैं कि ये तकनीकें किसी भी $\beta$-विस्तार के लिए लागू होती हैं जहाँ $\beta$ एक क्वाड्रेटिक पिसोट नंबर (quadratic Pisot number) है, बशर्ते आवश्यक अंकगणितीय ऑटोमाटा का निर्माण किया जा सके।
• OEIS योगदान: यह शोध पत्र $\phi$-प्रतिनिधित्वों से संबंधित कई नई पूर्णांक अनुक्रमों (जैसे A362970, A362716, A362780) को पहचानता और परिभाषित करता है, जिससे ऑन-लाइन एनसाइक्लोपीडिया ऑफ इंटीजर सीक्वेंसेज (OEIS) समृद्ध होता है।

संक्षेप में, यह शोध पत्र इस बात का एक शक्तिशाली प्रदर्शन है कि कैसे ऑटोमेटेड थ्योरम प्रोविंग का उपयोग संख्या सिद्धांत के क्लासिक समस्याओं पर पुनर्विचार करने के लिए किया जा सकता है, जिससे ज्ञात परिणामों के सरलीकृत प्रमाण और $\phi$-प्रतिनिधित्वों के नए संरचनात्मक गुणों की खोज दोनों प्राप्त होते हैं।