دليل آلي لبناء طريقة الفلتر للأعداد الحقيقية

تقدم هذه الورقة تحققًا آليًا من نظرية الأعداد الحقيقية حيث يتم بناء الأعداد الحقيقية باستخدام مفاهيم تتعلق بالمرشحات. تشمل النظرية فلترًا خاصًا، وهو الفلتر الأريثمي غير الرئيسي الذي يمكن إثبات وجوده مع فرضية الكونتينوم، لإقامة عدة مجموعات أعداد غير قياسية: *N، *Z و *Q. يتم الحصول على مجموعة الأعداد الحقيقية، R، من خلال تصنيف المكافئات لمجموعة فرعية محددة من *Q. يتم تضمين النظرية برمتها بشكل شامل، حيث يتم التحقق من كل التفاصيل لضمان الدقة والصرامة. يتم تنفيذ التحقق باستخدام مساعد الإثبات Coq ويستند إلى نظرية المجموعات الأكسيومية لموريس- كيلي. يساهم هذا العمل في توفير مجموعة جديدة من المواد التأسيسية لتشكيل النظريات الرياضية.