A Formalization of the Laplace Transform and Its Inversion in Lean 4

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

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

---

مدقق الإثبات الرقمي

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

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

المترجم والمرآة السحرية

تحويل لابلاس يشبه المرآة السحرية. تضع دالة $f(t)$ (التي تصف شيئاً يحدث بمرور الوقت) في المرآة، فتعكس لك دالة جديدة $(Lf)(s)$ (تصف الشيء نفسه في عالم "التردد").

• الرحلة الأمامية: تثبت الورقة أنه إذا كانت لديك دالة تسلك سلوكاً جيداً (لا تنفجر إلى ما لا نهاية بسرعة كبيرة)، فإن المرآة تعمل. لقد أثبتوا قواعد كيفية ترجمة الأشياء البسيطة مثل الثوابت، وقوى الزمن، وحتى موجات الجيب (sine waves). على سبيل المثال، أظهروا أن المرآة تحول المشتقة (معدل التغيير) إلى عملية ضرب بسيطة في العدد $s$، ناقص قيمة ابتدائية. هذا هو "السر الخفي" الذي يجعل حل المعادلات التفاضلية سهلاً للغاية.
• رحلة العودة (القلب): التحدي الحقيقي هو استعادة الإجابة. كيف تنظر إلى الانعكاس وتعرف بالضبط ما هو الشيء الأصلي؟ يسمى هذا تحويل لابلاس العكسي (inverse Laplace transform). تثبت الورقة طريقة محددة للقيام بذلك، تُعرف باسم صيغة برومويتش (Bromwich formula).

لماذا لم يسلكوا الطريق "السهل"

عادةً، يثبت الرياضيون صيغة القلب باستخدام تقنية تسمى التكامل الكنتوري المعقد (complex contour integration). تخيل رسم حلقة حول شكل على خريطة واستخدام نظرية خاصة (نظرية الرواسب/Residue Theorem) لعد "الكنوز" الموجودة بداخلها. إنها أداة قوية، لكن المؤلفين وجدوا أن مكتبة الكمبيوتر لم تكن تمتلك بعد ما يكفي من أدوات "رسم الخرائط" هذه.

لذلك، سلكوا مساراً مختلفاً، أكثر قرباً من الأرض. بدلاً من رسم حلقات في المستوى المركب، عاملوا المسألة كعملية تكامل في العالم الحقيقي فوق خط مستقيم. قاموا بتفكيك المسألة إلى قطع أصغر يمكن التحكم فيها:

1. القطع (Truncation): تظاهروا بأن الخط اللانهائي هو مجرد قطعة قصيرة ومحدودة من $-T$ إلى $T$.
2. دالة الـ sinc: مع جعل هذه القطعة تطول وتطول، ظهر نمط محدد يتضمن دالة تسمى sinc (والتي تبدو كموجة تصغر وتصغر تدريجياً).
3. تكامل ديريكليه (Dirichlet Integral): اعتمدوا على حقيقة مشهورة ومثبتة مسبقاً حول المساحة تحت موجة الـ sinc هذه (تكامل ديريكليه) لإظهار أنه مع جعل القطعة تطول إلى ما لا نهاية، فإن النتيجة تعيد بناء الدالة الأصلية بشكل مثالي.

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

اختبار البندول المتأرجح

لإثبات أن نظامهم يعمل حقاً، لم يكتفوا بالتحقق من رياضيات مجردة؛ بل حلوا مسألة فيزيائية كلاسيكية: المتذبذب التوافقي (harmonic oscillator). هذا هو الرياضيات الكامنة وراء بندول يتأرجح أو نابض (زمبرك) يرتد للأعلى والأسفل.

• الإعداد: حددوا نابضاً يبدأ من حالة السكون ولكن يتم دفعه دفعة سريعة، موصوفاً بالمعادلة $y''(t) + \omega^2 y(t) = 0$.
• الترجمة: أدخلوا هذه المعادلة التفاضلية في مترجم لابلاس الذي تم التحقق منه حاسوبياً.
• النتيجة: نجح الكمبيوتر في تحويل هذه المعادلة التفاضلية المعقدة إلى معادلة جبرية بسيطة: $(s^2 + \omega^2)Y(s) = \omega$.
• الحل: أعطاهم الحل لـ $Y(s)$ النتيجة $\frac{\omega}{s^2 + \omega^2}$.
• التحقق: تحقق الكمبيوتر بعد ذلك من مكتبته الخاصة وأكد أن هذه النتيجة المحددة هي بالضبط تحويل لابلاس لـ $\sin(\omega t)$.

كان هذا نجاحاً هائلاً. لقد يعني هذا أن الكمبيوتر لم يكتفِ بحساب الإجابة فحسب؛ بل أثبت أن الإجابة هي بالفعل موجة جيبية، مطابقة لما عرفه علماء الفيزياء البشر لقرون، ولكن بمستوى من اليقين لا يترك مجالاً للخطأ البشري.

القواعد الصارمة للعبة

الورقة هي أيضاً درس في مدى الحذر الذي يجب أن تكون عليه عندما تتوقف عن التخمين وتبدأ في الإثبات. يسلط المؤلفون الضوء على عدة "أفخاخ" غالباً ما يتم تجاهلها في الكتب المدرسية:

• اللانهاية مخادعة: لا يمكنك ببساطة افتراض أن التكامل يمتد إلى ما لا نهاية. كان على الإثبات أن ينص صراحة على أن الدالة يجب أن تضمحل بسرعة كافية بحيث تتلاشى "ذيول" التكامل.
• الحالات الحدية: عند إجراء الرياضيات، هناك نقاط محددة (مثل $t=0$) حيث تتغير القواعد. لقد أجبرهم الكمبيوتر على أن يكونوا دقيقين بشأن أين تُعرف الدالة وأين تكون مستمرة.
• تبديل الترتيب: في إثبات القلب، اضطروا لتبديل ترتيب تكاملين. في الرياضيات العادية، قد تفعل هذا ببساطة. أما في إثباتهم الرسمي، فقد توجب عليهم إثبات أن "المساحة" تحت السطح المشترك محدودة بشكل صارم قبل أن يُسمح لهم بتبديل الترتيب.

الخلاصة

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

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