Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number

तकनीकी सारांश: प्रत्येक गैर-ऋणात्मक पूर्णांक एक त्रिकोणीय, एक पंचकोणीय और एक सप्तकोणीय संख्या का योग है

समस्या विवरण
यह शोध पत्र एक अनुमान (conjecture) को संबोधित करता है जिसे OEIS A287616 के रूप में दर्ज किया गया है, जिसे मूल रूप से ज़ी-वेई सन (Zhi-Wei Sun) द्वारा प्रस्तावित किया गया था। यह अनुमान दावा करता है कि प्रत्येक गैर-ऋणात्मक पूर्णांक $n$ को एक त्रिकोणीय संख्या, एक दूसरी पंचकोणीय संख्या और एक दूसरी सप्तकोणीय संख्या के योग के रूप में दर्शाया जा सकता है। औपचारिक रूप से, प्रत्येक $n \in \mathbb{N}$ के लिए, $x, y, z \in \mathbb{N}$ विद्यमान हैं कि:
$$n = \frac{x(x+1)}{2} + \frac{y(3y+1)}{2} + \frac{z(5z+1)}{2}$$
लेखक इसे "सामान्यीकृत" बहुभुज संख्या समस्याओं से अलग करते हैं जहाँ चर (variables) सभी पूर्णांकों के लिए हो सकते हैं; यहाँ, चर सख्ती से गैर-ऋणात्मक हैं।

कार्यप्रणाली और प्रमाण रणनीति
प्रमाण एक विकर्ण त्रिक द्विघात रूप (diagonal ternary quadratic form) के लिए एक प्रतिबन्धित प्रतिनिधित्व समस्या में इस योगात्मक समस्या को रूपांतरित करके आगे बढ़ता है।

1. वर्ग न्यूनीकरण (Square Reduction):
   प्राथमिक सर्वसमिकाओं ($8T(x)+1=(2x+1)^2$, आदि) का उपयोग करते हुए, समस्या को $m = 120n + 23$ के रूप में पूर्णांकों को द्विघात रूप $Q(u, v, w) = 15u^2 + 5v^2 + 3w^2$ द्वारा निरूपित करने में बदल दिया जाता है। लक्ष्य एक ऐसा निरूपण खोजना है जहाँ $u$ धनात्मक और विषम हो, $v \equiv 1 \pmod 6$ हो, और $w \equiv 1 \pmod{10}$ हो।

2. प्रारंभिक बीज (अस्तित्व):
   प्रमाण पहले यह स्थापित करता है कि प्रत्येक $m \equiv 23 \pmod{120}$ $Q$ द्वारा एक प्रिमिटिव (primitive) पूर्णांक निरूपण स्वीकार करता है (जहाँ $\gcd(u,v,w)=1$)।

   • स्थानीय-वैश्विक सिद्धांत (Local-Global Principle): लेखक $Q$ के हैसे-मिंकोव्स्की (Hasse–Minkowski) प्रमेय और $Q$ के विशिष्ट जेनस (genus) ढांचे का उपयोग करते हैं। $Q$ का जेनस ठीक दो वर्गों से बना है: $Q$ का स्वयं का वर्ग और एक "मेट" (mate) रूप $g_2(x,y,z) = 2x^2 - 2xy + 8y^2 + 15z^2$ का वर्ग।
   • स्थानांतरण (Transfer): यदि $m$ मेट $g_2$ द्वारा निरूपित होता है, तो रूपांतरणों की एक श्रृंखला (इनवोल्यूशन और परिमेय समरूपता/rational isometries को शामिल करते हुए) इस निरूपण को $Q$ में स्थानांतरित करती है, जो प्रिमिटिविटी को सुरक्षित रखती है। यह चरण शास्त्रीय संख्या सिद्धांत के परिणामों पर निर्भर करता है जो उद्धृत हैं लेकिन इस औपचारिकीकरण (formalization) के भीतर पुनः सिद्ध नहीं किए गए हैं।

3. परिमित अवतरण (Finite Descent):
   एक बार प्रिमिटिव निरूपण सुरक्षित हो जाने के बाद, प्रमाण एक "अच्छी" स्थिति (विशिष्ट सर्वांगसमता शर्तों को संतुष्ट करने वाली) तक पहुँचने के लिए एक अवतरण एल्गोरिदम (descent algorithm) का उपयोग करता है।

   • संभावित फलन (Potential Function): निर्देशांकों की समता (parity) और सर्वांगसमता स्थिति के आधार पर एक लेक्सिकोग्राफिक पोटेंशियल $\Phi(u,v,w)$ को परिभाषित किया गया है।
   • मूव कैलकुलस (Move Calculus): तीन पूर्णांक मैट्रिक्स ($P_{uv}, P_{uw}, P_{vw}$) "मूव्स" को परिभाषित करते हैं जो $Q$ के मान और निरूपण की प्रिमिटिविटी को बनाए रखते हुए $\Phi$ को सख्ती से कम करते हैं।
   • प्रारंभिक अवतरण (Elementary Descents): अधिकांश अवस्थाओं के लिए, एक एकल मूव पर्याप्त होता है।
   • अवशेष शंकु (Residual Cone): अवशेषों का एक छोटा समूह (residual cone) प्रारंभिक अवतरण का विरोध करता है। इनके लिए, लेखक एक फिनिट-की डिटरमिनेंसी (finite-key determinacy) तर्क का उपयोग करते हैं। वे सिद्ध करते हैं कि किसी भी लघु मूव अनुक्रम की सफलता केवल शुरुआती वेक्टर के संकेतों और अवशेषों (एक "चाबी" या key) के एक परिमित सेट पर निर्भर करती है।
   • कंप्यूटर-सहायता प्राप्त आवरण (Computer-Assisted Cover): अवशेष शंकु को "साइन कोन्स" (sign cones) के एक परिमित सेट द्वारा कवर किया गया है। प्रत्येक शंकु के लिए, एक सटीक रैखिक प्रोग्रामिंग (LP) प्रमाण सत्यापित करता है कि एक 'एस्केप वर्ड' (मूव्स का एक अनुक्रम) मौजूद है। यह सत्यापन सटीक पूर्णांक और परिमेय अंकगणित का उपयोग करके किया जाता है, जिससे फ्लोटिंग-पॉइंट सन्निकटन (approximations) से बचा जा सके।

प्रमुख योगदान और परिणाम

• अनुमान A287616 का प्रमाण: यह शोध पत्र पूर्ण प्रमाण प्रदान करता है कि ट्रिपल $(T, P, H)$ गैर-ऋणात्मक पूर्णांकों के लिए सार्वभौमिक (universal) है।
• Lean 4 में औपचारिकीकरण (Formalization in Lean 4): प्रमाण के एक बड़े हिस्से (अनुभाग 2-5 और अवतरण तर्क) को Mathlib लाइब्रेरी के ऊपर Lean 4 में औपचारिक रूप दिया गया है।
  • औपचारिकीकरण में वर्ग न्यूनीकरण, परिवहन नियम (transport laws), प्रारंभिक अवतरण और समाप्ति तर्क (termination argument) शामिल हैं।
  • अनुमान को स्वयं मशीन-चेक किया गया है।
  • एकमात्र अपवाद पूर्ण औपचारिकीकरण के हैं:
    1. शास्त्रीय जेनस स्थानीय-वैश्विक सिद्धांत (हासे-मिंकोव्स्की + दो-वर्ग जेनस तथ्य), जिसे एक एक्सिओम (axiom) के रूप में उद्धृत किया गया है।
    2. अवशेष शंकु का परिमित आवरण, जिसे एक कंप्यूटर-सत्यापित इनपुट (एक एक्सिओम जो सटीक प्रमाणों से प्राप्त है) के रूप में माना गया है।
  • शोधकर्ताओं की "मेकमैथ एजेंट टीम" (MechMath Agent Team) ने प्राकृतिक भाषा वाले प्रमाण और Lean औपचारिकीकरण को उत्पन्न किया है, जो कठोर, मशीन-सत्यापनीय गणितीय प्रमाण बनाने की AI एजेंटों की क्षमता को प्रदर्शित करता है।

महत्व और दावे
यह शोध पत्र शास्त्रीय संख्या सिद्धांत और कठोर कंप्यूटर-सहायता प्राप्त सत्यापन के संयोजन के माध्यम से OEIS A287616 अनुमान को हल करने का दावा करता है। इसका महत्व निम्नलिखित में निहित है:

1. कठोर सत्यापन: प्रमाण को Lean में औपचारिक रूप देकर, लेखक यह सुनिश्चित करते हैं कि तार्किक संरचना, अवतरण तंत्र और तुल्यता रूपांतरण मानवीय त्रुटि से मुक्त हैं।
2. हाइब्रिड प्रमाण पद्धति: यह कार्य एक "हाइब्रिड" दृष्टिकोण का उदाहरण देता है जहाँ गहरे सैद्धांतिक परिणामों (जेनस थ्योरी) को व्यापक, सटीक कंप्यूटर सत्यापन (रैखिक प्रोग्रामिंग कवर) के साथ जोड़ा जाता है ताकि एक ऐसी समस्या को हल किया जा सके जो विशुद्ध रूप से मैन्युअल या विशुद्ध रूप से ह्यूरिस्टिक (heuristic) तरीकों से कठिन है।
3. निर्भरता की पारदर्शिता: औपचारिकीकरण स्पष्ट रूप से गैर-औपचारिक इनपुट (उद्धृत शास्त्रीय प्रमेय और कंप्यूटर प्रमाण) को अलग करता है, जिससे प्रमाण की निर्भरता संरचना ऑडिट योग्य (auditable) हो जाती है। लेखक इस बात पर जोर देते हैं कि "गणितीय मुख्य भाग" पूरी तरह से औपचारिक है, जबकि "संगणनात्मक इनपुट" को एक परिमित, सटीक प्रमाण तक सीमित कर दिया गया है।

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