Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound
تغلق هذه الورقة فجوة تحقق حرجة في حد كوشين-سبيكر الأدنى من خلال تقديم شهادات شجرة-حالة عقلانية دقيقة وفاحصين مستقلين (أحدهما بلغة بايثون والآخر مثبت رسميًا بلغة Lean 4) للتحقق آليًا من عدم القابلية للاندماج الهندسي لجميع الرسوم البيانية الـ 180 المتميزة في قاعدة بيانات الحجب المنشورة، مما يستبدل قرارات Z3 غير المتحقق منها بنظريات مدققة عبر النواة، بينما يكشف في الوقت نفسه عن عدة عيوب وتناقضات خفية في مسار الإثبات الأصلي ويعالجها.