فرمالیزاسیون Lean 4 از همگرایی لایه خروجی Collatz

من در حال به اشتراک‌گذاری یک رکورد روش‌شناختی (methodological record) جدید در Lean 4 هستم.

این اثر، بخش خاصی از دینامیک Collatz را فرمالیزه می‌کند. ما این بخش را «قطعه لایه خروجی» (exit-layer fragment) می‌نامیم. این بخش شامل اعداد فردی است که در یک مرحله به توانی از دو (power-of-two) می‌رسند.

این اثبات کامل حدس Collatz نیست؛ بلکه یک ثبت رسمی از یک مشاهده ریاضی شناخته‌شده است.

جزئیات فنی کلیدی:

• ما از کالایبرهای (coalgebras) از نوع Stream' هم‌ایندکتیو (coinductive) برای نمایش مدارها (orbits) استفاده می‌کنیم. • ما یک نسخه halt-at-1 از گام Collatz را تعریف می‌کنیم. • این کار باعث می‌شود مدار در نهایت در یک جریان (stream) ثابت در عدد ۱ قرار گیرد. • ما ثابت می‌کنیم که اعداد لایه خروجی به این جریان ثابت می‌رسند. • اثبات بر پایه سه‌گانه اصول (axiom triple) استاندارد Mathlib استوار است.

یک نتیجه قابل توجه:

قضیه head_collatzOrbit کاملاً بدون اصول موضوعه (axiom-free) است. اجرای دستور #print axioms روی این قضیه، یک مجموعه تهی را برمی‌گرداند. این امر آن را در سطحی پایین‌تر از پایه اصول کلاسیک استاندارد قرار می‌دهد.

آنچه این مقاله انجام نمی‌دهد:

هدف، ارائه یک فرمالیزاسیون تمیز و بدون اصول موضوعه (axiom-free) در محدوده مشاهده‌شده است. ما از دیدگاه کالایبریک (coalgebraic) کیم (Kim, 2008) استفاده کرده و آن را در Lean 4 به کار می‌بریم.

این یک مشارکت روش‌شناختی در سری Rei-AIOS است و بر کمینه‌سازی پایه اصول (axiom-base minimization) و فرمالیزه کردن ساختارهای شناخته‌شده تمرکز دارد.

منبع: https://dev.to/fc0web/paper-166-v01-a-lean-4-axiom-free-formalization-of-exit-layer-collatz-convergence-as-a-stream-8oi

انجمن یادگیری اختیاری: https://t.me/GyaanSetuAi