🔢 mathematics

Lean-verified lower bounds for the Shannon capacity of odd cycles

تقدم هذه الورقة حدوداً دنيا جديدة، مصاغة بالكامل في لغة Lean، لسعات شانون لعدة دورات فردية صغيرة ( $C_7, C_{11}, C_{13}, C_{15}, C_{19}, C_{21}, C_{23}$ ) مشتقة باستخدام إجراء تكراري يعتمد على طرق حديثة من قبل غاو وآخرين (Gao and Itty et al.).

المؤلفون الأصليون: Pjotr Buys, Sven Polak, Jeroen Zuiddam

نُشر 2026-08-03

📖 6 دقيقة قراءة🧠 قراءة متعمّقة

CC BY 4.0

المؤلفون الأصليون: Pjotr Buys, Sven Polak, Jeroen Zuiddam

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أنك تحاول إرسال رسالة سرية عبر مدينة صاخبة وفوضوية. المدينة مليئة بالمشتتات، وأحياناً تختلط إشارتك بأسماء شوارع خاطئة. في عالم نظرية المعلومات، هذه مشكلة حقيقية: كيف ترسل بيانات بشكل مثالي دون أي أخطاء؟ في الخمسينيات، اكتشف عالم رياضيات يدعى كلود شانون أنه إذا كان لديك قناة "صاخبة"، فلا يزال بإمكانك إرسال الرسائل بشكل مثالي، ولكن فقط إذا كنت ذكياً في كيفية تجميع حروفك معاً. لقد قدم مفهوماً يسمى "سعة شانون" (Shannon capacity)، وهو باختصار درجة تخبرك بالسرعة القصوى التي يمكنك بها إرسال رسائل مثالية عبر نوع معين من الشبكات الصاخبة.

لتصور ذلك، تخيل لعبة تُلعب على خريطة للمدينة. الخريطة عبارة عن رسم بياني (graph)، حيث التقاطعات هي نقاط والشوارع هي خطوط. بعض الشوارع "آمنة" للسفر فيها معاً، بينما الشوارع الأخرى خطيرة وستتسبب في حادث إذا خلطت بينها. الهدف هو اختيار أكبر مجموعة ممكنة من التقاطعات (مجموعة مستقلة - independent set) يمكنك زيارتها دون أن تسلك أبداً شارعاً خطيراً بين أي اثنين منهما. تسأل "سعة شانون" سؤالاً صعباً: إذا لعبت هذه اللعبة ليس لمرة واحدة فقط، بل من خلال تكديم نسخ متعددة من الخريطة فوق بعضها البعض لإنشاء مدينة ضخمة متعددة الأبعاد، فكم يمكن أن تصبح مجموعتك الآمنة أكبر؟ بالنسبة لبعض الأشكال، نحن نعرف الإجابة. أما بالنسبة لأشكال أخرى، وتحديداً الحلقات ذات الأشكال الفردية (مثل الخماسي أو السباعي)، فقد ظل الإجابة لغزاً لعقود. الأمر يشبه معرفة الحد الأقصى للسرعة على طريق مستقيم، بينما ليس لديك أدنى فكرة عن السرعة التي يمكنك بلوغها في مسار متعرج بسبعة زوايا.

هذه الورقة البحثية تتعلق بفك هذا اللغز لعدة من تلك المسارات المتعرجة (ذات السبع زوايا أو أكثر). لقد وجد المؤلفون، وهم فريق من علماء الرياضيات وعلماء الحاسوب، طرقاً جديدة وأسرع قليلاً لإرسال رسائل مثالية عبر هذه الحلقات المحددة. لم يكتفوا بالتخمين؛ بل استخدموا وصفة ذكية ومنظمة لبناء مجموعات أكبر وأكبر من التقاطعات الآمنة. وللتأكد من أنهم لم يرتكبوا خطأ واحداً في حساباتهم المعقدة، استعانوا بحكم رقمي صارم للغاية يسمى "لين" (Lean) للتحقق من كل خطوة في عملهم. والنتي نتيجة ذلك؟ لقد أثبتوا أنه بالنسبة لهذه الحلقات الفردية، فإن سعة التواصل المثالي أعلى مما تم حسابه سابقاً.

لعبة التقاطعات الآمنة

دعونا نفكك ما قام به المؤلفون بالفعل. كانوا يبحثون في رسوم بيانية تبدو كحلقات بسيطة بعدد فردي من النقاط: حلقة من 7 نقاط، وحلقة من 11، وحلقة من 13، وهكذا. لفترة طويلة، عرف علماء الرياضيات "الحد الأقصى للسرعة" (سعة شانون) لحلقة من 5 نقاط. ولكن بالنسبة للحلقات التي تحتوي على 7 نقاط أو أكثر، كانت الإجابة عالقة في الضباب. كنا نعرف أنها على الأقل تصل إلى رقم معين، لكننا لم نكن نعرف ما إذا كان يمكن أن تكون أعلى من ذلك.

استخدم المؤلفون طريقة تشبه وصفة سحرية لتنمية مجموعتك الآمنة. تخيل أن لديك نادياً صغيراً وآمناً من الأصدقاء (مجموعة من النقاط) على خريطة واحدة. تصف الورقة البحثية "نظرية الضرب" (product theorem)، وهي مثل آلة تأخذ خريطتين وتدمجهما معاً لإنشاء خريطة جديدة أكبر. إذا كان لديك نادٍ آمن على الخريطة الأولى ونادٍ آمن على الخريطة الثانية، يمكنك دمجهما لصنع نادٍ آمن على الخريطة الجديدة الأكبر. عادةً، يكون حجم هذا النادي الجديد هو حجم النادي الأول مضروباً في حجم النادي الثاني. لكن المؤلفين وجدوا "أداة" خاصة أو خدعة. باستخدام نمط محدد من الاتصالات (يسمى "الزوج الصحيح" - valid tuple)، استطاعوا جعل النادي الجديد أكبر مما قد يوحي به الضرب البسيط.

فكر في الأمر هكذا: إذا كان لديك فريق من شخصين يمكنهما العمل معاً دون شجار، ودمجت فريقين كهذه، قد تتوقع الحصول على فريق من 4 أشخاص. ولكن مع هذه الخدعة الخاصة، وجد المؤلفون طريقة لدمجهم والحصول على فريق من 5 أشخاص يتفاهمون جميعاً بشكل مثالي. ومن خلال تكرار هذه الخدعة مراراً وتكراراً، وتكديس الخرائط للأعلى، استطاعوا تنمية هذه الفرق الآمنة إلى مجموعات ضخمة.

الأرقام القياسية الجديدة

طبق الفريق هذه الوصفة على سبع حلقات فردية مختلفة: تلك التي تحتوي على 7، 11، 13، 15، 19، 21، و23 نقطة. لكل منها، بدأوا بمجموعة آمنة معروفة وشغلوا "آلة التكديس" الخاصة بهم عدة مرات. وكانت النتيجة حداً أدنى جديداً وأعلى للسعة.

إليكم ما وجدوه، بالأرقام تماماً كما حسبوها:

بالنسبة لـ الحلقة ذات الـ 7 نقاط، أثبتوا أن السعة لا تقل عن 3.258805369885. وهذا أعلى بقليل من أفضل تخمين سابق.
بالنسبة لـ الحلقة ذات الـ 11 نقطة، الحد الأدنى الجديد هو 5.294502522149.
بالنسبة لـ الحلقة ذات الـ 13 نقطة، دفعوا الحد إلى 6.302455083464.
بالنسبة لـ الحلقة ذات الـ 15 نقطة، الرقم هو 7.301600534487.
بالنسبة لـ الحلقة ذات الـ 19 نقطة، وصلوا إلى 9.357192705918.
بالنسبة لـ الحلقة ذات الـ 21 نقطة، الحد هو 10.342455853338.
وبالنسبة لـ الحلقة ذات الـ 23 نقطة، وجدوا سعة لا تقل عن 11.328224257774.

قد تبدو هذه الأرقام كسلسلة من الأرقام العشوائية، ولكن في عالم نظرية المعلومات، هي تمثل تحسناً ملموساً. هذا يعني أنه بالنسبة لهذه الشبكات المحددة، أصبحنا نعلم بالتأكيد أنه يمكننا إرسال الرسائل بسرعة أكبر قليلاً مما كنا نعتقد أنه ممكن من قبل.

الحكم الرقمي

ما يجعل هذه الورقة مميزة ليس فقط الأرقام، بل الطريقة التي حصلوا بها عليها. الرياضيات المتضمنة معقدة للغاية، وتتضمن مجموعات ضخمة من البيانات وآلاف الخطوات. إنه النوع من العمل الذي قد يسهل فيه على البشر ارتكاب خطأ صغير. ولحل هذه المشكلة، كتب المؤلفون برهانهم بالكامل بلغة حاسوبية تسمى Lean.

تخيل "لين" كحكم رقمي شديد الصرامة لا يقبل جملة "أعتقد أن هذا صحيح" أو "يبدو جيداً بالنسبة لي". إنه يتطلب برهاناً منطقياً مطلقاً لكل خطوة. إذا ارتكب المؤلفون خطأ في منطقهم، فسوف يتوقف "لين" ويقول: "لا، هذا لا يتبع ذلك". حقيقة أن الورقة "موثقة بواسطة لين" تعني أن حاسوباً قد فحص كل سطر من استدلالاتهم وأكد أن حدودهم الجديدة سليمة رياضياً. هم لم يقوموا بمجرد محاكاة النتائج؛ بل أثبتوا ذلك رسمياً.

يذكر المؤلفون أيضاً أنهم استخدموا نماذج لغوية كبيرة (مثل روبوتات الدردشة المتقدمة بالذكال الاصطناعي) لمساعدتهم في العثور على الأنماط والوصفات الأولية لهذه المجموعات الآمنة. الأمر يشبه امتلاك مساعد مبدع يقترح فكرة جامحة، ثم يستخدم علماء الرياضيات أدواتهم الصارمة لاختبار ما إذا كانت تلك الفكرة صالحة بالفعل. في هذه الحالة، اقترح الذكاء الاصطناعي مساراً، ثم سلك فريق (الإنسان-عالم الرياضيات-الذكاء الاصطناعي) هذا المسار حتى وصلوا إلى خط النهاية الموثق.

لماذا يهم هذا الأمر؟

قد تتساءل: "ما الفائدة؟ لقد عرفنا فقط أن الرقم أعلى قليلاً". الإجابة تكمن في طبيعة المشكلة. لعقود من الزمن، كانت سعة هذه الحلقات الفردية سؤالاً مفتوحاً. كنا نعرف أن الإجابة تقع في مكان ما بين حد أدنى وحد أقصى (حد لوفاز - Lovász bound)، لكننا لم نتمكن من تحديدها بدقة. في كل مرة نرفع فيها الحد الأدنى، ولو بجزء ضئيل، فإننا نضيق الفجوة. نحن نقترب من الإجابة الحقيقية.

يوضح هذا العمل أنه حتى بالنسبة للمشكلات التي ظلت عالقة لفترة طويلة، لا يزال هناك مجال للتحسين إذا كنت تملك الأدوات المناسبة والصبر للتحقق من عملك بأكثر المعايير صرامة ممكنة. لم يحل المؤلفون لغز سعة شانون لجميع الحلقات الفردية، لكنهم أزالوا بعض الزوايا الضبابية، مثبتين أنه بالنسبة للحلقات ذات 7، 11، 13، 15، 19، 21، و23 نقطة، يمكننا التواصل بسرعة أكبر قليلاً مما كنا نعتقد سابقاً.

ملخص تقني: حدود دنيا مُتحقق منها عبر نظام Lean لسعة شانون للدورات الفردية

بيان المشكلة
تتناول الورقة البحثية المشكلة المفتوحة طويلة الأمد المتمثلة في تحديد سعة شانون، $\Theta(G)$ ، للدورات الفردية $C_n$ حيث $n \geq 7$ . تُعرف سعة شانون بـ $\Theta(G) := \sup_{d \geq 1} \alpha(G^{\boxtimes d})^{1/d}$ ، حيث $\alpha$ تمثل عدد الاستقلال و $\boxtimes$ يمثل حاصل الضرب القوي للرسوم البيانية. بينما حدد لوفاتز (Lovász) أن $\Theta(C_5) = \sqrt{5}$ باستخدام دالة ثيتا $\vartheta(G)$ ، فإن السعات الدقيقة لجميع الدورات الفردية التي يبلغ طولها سبعة أو أكثر لا تزال غير معروفة. ويكمن التحدي الرئيسي في إيجاد مجموعات مستقلة أكبر في القوى القوية العليا لهذه الدورات لتحسين الحدود الدنيا المعروفة.

المنهجية
يستخدم المؤلفون إجراءً تكراريًا يعتمد على "بناء أداة" (gadget construction) و"لمّة حاصل الضرب" (product lemma) التي اقترحها غاو (Gao 2026) مؤخرًا، والتي تعتمد هي نفسها على أساليب إيتي، روسين، كارستنسن، وريكمان (Itty, Rosin, Carstensen, and Reichman 2026). يتضمن جوهر المنهجية ما يلي:

الرُّتَب الصالحة (Valid Tuples): بالنسبة لرسم بياني $G$ ، يتم تعريف الرُّتبة الصالحة $\tau = (I, S, f_0, f_1, X)$ ، حيث $I$ هي مجموعة مستقلة، و $S \subseteq I$ ، و $f_0, f_1$ هما تطبيقان محددان يستوفيان قيود الجوار الصارمة. تولد هذه الرُّتبة "ملف تعريف" (profile) يُرمز له بـ $\Pi(\tau) = (|I|, |S|, |X|, |X \setminus (N_G[f_0(S)] \cup N_G[f_1(S)])|)$ .
عملية الضرب: يتم تعريف عملية ثنائية $\star$ على ملفات التعريف. تثبت النظرية 1 أنه إذا كانت $\tau$ و $\tau'$ رُتَبًا صالحة للرسوم البيانية $G$ و $H$ ، فإنه توجد رُتبة صالحة لحاصل الضرب القوي $G \boxtimes H$ يكون ملف تعريفها هو حاصل ضرب $\star$ لملفات التعريف الفردية.
البناء التكراري: بدءًا من رُتبة صالحة تم اكتشافها حاسوبيًا في قوة محددة لدورة فردية، يطبق المؤلفون عملية $\star$ -product بشكل تكراري لتوليد ملفات تعريف لقوى أعلى. وتعمل هذه العملية على بناء مجموعات مستقلة في القوى القوية $C_n^{\boxtimes d}$ تكون أكبر مما يمكن الحصول عليه من خلال حاصل الضرب الديكارتي البسيط للمجموعات المستقلة الأساسية.
التحقق الرسمي: يعد التحقق الكامل من هذه الحدود في نظام الإثبات الآلي Lean مكونًا حاسمًا للمنهجية. يتم ترميز الرُّتَب الأساسية (المجموعات $I, S, X$ والخرائط $f_0, f_1$ ) كرموز صريحة (explicit literals)، ويتم التحقق من صلاحيتها ميكانيكيًا داخل بيئة Lean.

المساهمات والنتائج الرئيسية
تقدم الورقة حدودًا دنيا جديدة ومحسنة لسعات شانون لسبع دورات فردية صغيرة ( $C_7, C_{11}, C_{13}, C_{15}, C_{19}, C_{21}, C_{23}$ ). تم اشتقاق هذه الحدود من خلال تحديد رُتَب أساسية صالحة وتطبيق إجراء الضرب التكراري. النتائج هي:

$\Theta(C_7)$ : تحسنت إلى $\geq 3.258805369885\dots$ (كانت سابقًا $3.2587891\dots$ بواسطة Gao 2026). يستخدم البناء رُتبة أساسية في $C_7^{\boxtimes 5}$ مكررة إلى القوة 200.
$\Theta(C_{11})$ : تحسنت إلى $\geq 5.294502522149\dots$ (كانت سابقًا $5.2897736\dots$ بواسطة Itty et al. 2026). الرُّتبة الأساسية في $C_{11}^{\boxtimes 3}$ ، مكررة إلى القوة 174.
$\Theta(C_{13})$ : تحسنت إلى $\geq 6.302455083464\dots$ (كانت سابقًا $6.3001091\dots$ بواسطة Itty et al. 2026). الرُّتبة الأساسية في $C_{13}^{\box 6}$ ، مكررة إلى القوة 432.
$\Theta(C_{15})$ : تحسنت إلى $\geq 7.301600534487\dots$ (كانت سابقًا $7.3013990\dots$ بواسطة Itty et al. 2026). الرُّتبة الأساسية في $C_{15}^{\boxtimes 4}$ ، مكررة إلى القوة 4096.
$\Theta(C_{19})$ : تحسنت إلى $\geq 9.357192705918\dots$ (كانت سابقًا $9.3571200\dots$ بواسطة Baumert et al. 1971). الرُّتبة الأساسية في $C_{19}^{\boxtimes 4}$ ، مكررة إلى القوة 16384.
$\Theta(C_{21})$ : تحسنت إلى $\geq 10.342455853338\dots$ (كانت سابقًا $10.3422729\dots$ بواسطة Baumert et al. 1971). الرُّتبة الأساسية في $C_{21}^{\boxtox 4}$ ، مكررة إلى القوة 4096.
$\Theta(C_{23})$ : تحسنت إلى $\geq 11.328224257774\dots$ (كانت سابقًا $11.3278379\dots$ بواسطة Baumert et al. 1971). الرُّتبة الأساسية في $C_{23}^{\boxtimes 4}$ ، مكررة إلى القوة 2048.

وعلى الرغم من أن التحسينات ضئيلة عددياً (تتراوح بين $10^{-5}$ و $10^{-3}$ )، إلا أنها تمثل أحدث ما توصل إليه العلم لهذه الدورات المحددة.

الأهمية والادعاءات
تزعم الورقة أهميتها بشكل أساسي من خلال التحقق الصارم من هذه النتائج. فمن خلال صياغة البناء بأكمله والحدود الناتجة رسميًا في نظام Lean، يضمن المؤلفون أن الحجج التوليفية المعقدة وبناءات المجموعات المحددة خالية من الخطأ البشري. يتبع هذا العمل مسار الأبحاث الأخيرة التي تستخدم نماذج اللغات الكبيرة (LLMs) لاكتشاف البناءات الأولية (كما في [IRCR26] و [Gao26])، ولكنه يتميز بتقديم إثبات كامل مُصاغ آليًا وصحيح رياضيًا لصلاحية الرُّتَب الأساسية وصحة تطبيق نظرية حاصل الضرب التكرارية. لا يدعي المؤلفون حل المشكلة العامة لسعة شانون للدورات الفردية، ولا يقترحون أطرًا نظرية جديدة تتجاوز تطبيق لمّة حاصل الضرب الموجودة لغاو؛ بل يقدمون أفضل الحدود الدنيا العددية المعروفة حاليًا لهذه الحالات المحددة، والمحققة بيقين رياضي.

لعبة التقاطعات الآمنة

الأرقام القياسية الجديدة

الحكم الرقمي

لماذا يهم هذا الأمر؟

أبحاث مشابهة