𝗟𝗲𝗮𝗻 𝟰 𝗶𝗹𝗲 𝗖𝗼𝗹𝗹𝗮𝘁𝘇 Çı𝗸ı𝘀-𝗞𝗮𝘁𝗺𝗮𝗻ı 𝗬𝗮𝗸ı𝗻𝘀𝗮𝗺𝗮𝘀ı𝗻ın 𝗙𝗼𝗿𝗺𝗮𝗹𝗶𝘇𝗲 𝗘𝗱𝗶𝗹𝗺𝗲𝘀𝗶
Lean 4'te yeni bir metodolojik kayıt paylaşıyorum.
Bu çalışma, Collatz dinamiklerinin belirli bir kısmını formalize ediyor. Buna çıkış-katmanı fragmanı (exit-layer fragment) diyoruz. Tek bir adımda iki kuvvetine ulaşan tek sayıları kapsıyor.
Bu, Collatz varsayımının tamamının bir kanıtı değildir. Bilinen bir matematiksel gözlemin formal bir kaydıdır.
Temel teknik detaylar:
• Yörüngeleri temsil etmek için koindüktif Stream koaljebralarını kullanıyoruz.
• Collatz adımının 1'de duran (halt-at-1) bir varyantını tanımlıyoruz.
• Bu, yörüngenin sonunda 1'de sabit kalmasını sağlar.
• Çıkış-katmanı sayılarının bu sabit akışa ulaştığını kanıtlıyoruz.
• Kanıt, standart Mathlib aksiyom üçlüsüne dayanmaktadır.
Dikkat çeken bir sonuç:
head_collatzOrbit teoremi tamamen aksiyomsuzdur. Bu teorem üzerinde #print axioms komutunu çalıştırmak boş bir küme döndürür. Bu da onu standart klasik aksiyom tabanının altına yerleştirir.
Bu makalenin yapmadıkları:
- Collatz varsayımını çözmez.
- 5–8 durumlarındaki sondaki 1-bitleri (trailing-1-bits) duvarını yıkmaz.
- Terence Tao'nun analitik sonuçlarını değiştirmez.
- Janik (2026)'nın çözülmemiş kısımlarını ele almaz.
Amaç, gözlemlediğimiz aralık dahilinde temiz, aksiyomsuz bir formalizasyon sağlamaktır. Kim (2008)'den gelen koaljebraik perspektifi kullanıyor ve bunu Lean 4'e uyguluyoruz.
Bu, Rei-AIOS serisine metodolojik bir katkıdır. Aksiyom tabanı minimizasyonuna ve bilinen yapıların formalize edilmesine odaklanır.
İsteğe bağlı öğrenme topluluğu: https://t.me/GyaanSetuAi