Lean 4-এ Collatz Exit-Layer Convergence-এর Formalization
আমি Lean 4-এ একটি নতুন পদ্ধতিগত রেকর্ড শেয়ার করছি।
এই কাজটি Collatz dynamics-এর একটি নির্দিষ্ট অংশকে ফরম্যালাইজ করে। আমরা এটিকে exit-layer fragment বলি। এটি সেই সব বিজোড় সংখ্যাগুলোকে অন্তর্ভুক্ত করে যা এক ধাপেই একটি power-of-two-তে পৌঁছায়।
এটি সম্পূর্ণ Collatz conjecture-এর কোনো প্রমাণ নয়। এটি একটি পরিচিত গাণিতিক পর্যবেক্ষণের একটি ফরমাল রেকর্ড।
মূল প্রযুক্তিগত বিবরণ:
• আমরা orbits প্রকাশ করার জন্য coinductive Stream' coalgebras ব্যবহার করি। • আমরা Collatz step-এর একটি halt-at-1 variant সংজ্ঞায়িত করি। • এটি orbit-কে শেষ পর্যন্ত ১-এ স্থির (constant) করে তোলে। • আমরা প্রমাণ করি যে exit-layer সংখ্যাগুলো এই constant stream-এ পৌঁছায়। • প্রমাণটি standard Mathlib axiom triple-এর ওপর নির্ভরশীল।
একটি উল্লেখযোগ্য ফলাফল:
head_collatzOrbit থিওরেমটি সম্পূর্ণভাবে axiom-free। এই থিওরেমের ওপর #print axioms চালালে একটি empty set পাওয়া যায়। এটি একে standard classical axiom base-এর নিচে অবস্থান করায়।
এই পেপারটি যা করে না:
- এটি Collatz conjecture সমাধান করে না।
- এটি Cases 5–8 trailing-1-bits wall অতিক্রম করে না।
- এটি Terence Tao-এর অ্যানালিটিক ফলাফলগুলো পরিবর্তন করে না।
- এটি Janik (2026)-এর সমাধান না হওয়া অংশগুলো নিয়ে কাজ করে না।
লক্ষ্য হলো আমাদের পর্যবেক্ষণকৃত সীমার মধ্যে একটি পরিচ্ছন্ন, axiom-free ফরম্যালাইজেশন প্রদান করা। আমরা Kim (2008)-এর coalgebraic perspective ব্যবহার করি এবং এটি Lean 4-এ প্রয়োগ করি।
এটি Rei-AIOS সিরিজের একটি পদ্ধতিগত অবদান। এটি axiom-base minimization এবং পরিচিত কাঠামোসমূহকে ফরম্যালাইজ করার ওপর আলোকপাত করে।
ঐচ্ছিক লার্নিং কমিউনিটি: https://t.me/GyaanSetuAi