BEŞ CİSİM, SONLU SAYIDA KUSURSUZ DANS

Birkaç yıldız ya da gezegenin, bütün grup şeklini değiştirmeden katı bir nesne gibi dönebilecek kadar hassas biçimde dizildiğini düşünün. Bunun için her cisme etki eden kütleçekiminin tam olarak grubun kütle merkezine yönelmesi ve büyüklüğünün cismin merkeze uzaklığıyla orantılı olması gerekir. Bu tür dizilimlere merkezî konfigürasyonlar (central configurations) denir. Bunlar, cisimlerin aynı göreli düzeni koruduğu, katı biçimde dönen göreli dengeler (relative equilibria) de dahil olmak üzere, n-cisim probleminin özel çözümlerinin şekilleridir.

Bir düzen işe yarıyorsa, onun döndürülmüş, büyütülmüş ya da kaydırılmış her kopyası da işe yarar; bu yüzden matematikçiler bunları “benzerlik dışında” (up to similarity) sayar.

Smale’in altıncı problemi

Soruyu ifade etmek kolay: Her pozitif kütle seçimi için merkezî konfigürasyonların sayısı sonlu mudur? Bu, matematikçi Smale’in hazırladığı açık problemler listesindeki altıncı problem.

Makaleye göre durum şuydu:

Üç cisim: tam olarak beş — Lagrange’ın iki eşkenar üçgeni ve Euler’in üç doğrusal dizilimi.
Dört cisim: sonluluk, tüm pozitif kütleler için Hampton ve Moeckel tarafından kanıtlandı.
Düzlemde beş cisim: Albouy ve Kaloshin 2012’de sonluluğu kanıtladı, ama yalnızca istisnai bir kümenin dışındaki kütleler için — polinom denklemlerle tanımlanan ve argümanlarının çöktüğü ince bir kütle kombinasyonları ailesi.

İstisnai kümeyi kapatmak

Tejasvi Singh Tomar bu istisnai kümeyi ortadan kaldırıyor. Ana teorem: Beş pozitif kütlenin her seçimi için, düzlemsel beş-cisim probleminin benzerlik dışında sonlu sayıda merkezî konfigürasyonu vardır.

Strateji Albouy ve Kaloshin’in izinden gidiyor. Sonsuz sayıda konfigürasyon olsaydı, denklemler karmaşık sayılara genişletildiğinde bunlar sürekli bir çözüm eğrisi oluştururdu. Bu eğri “sonsuza” doğru izlendiğinde, cisimler arasındaki uzaklıklar hassas bir dengede birbirini götüren biçimlerde davranmak zorundadır. Cisimler, Albouy ve Kaloshin’in belirlediği on altı limit diyagramdan birine yaklaşır ve her biri kütlelere koşullar dayatır.

Yeni çalışma bu koşulları her pozitif kütle için keskinleştiriyor ve sorunlu durumları tek tek eliyor:

dört cismin sıkı bir küme oluşturduğu ve beşincinin bu kümeye yaklaştığı konfigürasyonlar, eğri boyunca sabit kalan potansiyel enerjinin giderek daha yüksek mertebeden açılımıyla dışlanıyor; pozitif kütleler için ortaya çıkan koşullar birbiriyle çelişiyor;
diğer iki diyagramın hiçbir zaman ortaya çıkmadığı gösteriliyor;
geri kalan her şey için yazar, tüm uyumlu kütle koşullarını kesin bilgisayar cebiriyle — 2.206 cebirsel sistem — tanımlıyor ve her biri için sayısal bir sertifika üretiyor: özellikleri kesin aritmetikle denetlendiğinde dengenin imkânsız olduğunu kanıtlayan bir rasyonel sayılar listesi.

Negatif kütlelerin kurduğu tuzak

Saf cebirin aşamayacağı bir pürüz var. Bir başka matematikçi, Roberts, biri negatif olan (1, 1, 1, 1, −¼) kütleleri için sonsuz sayıda merkezî konfigürasyon bulmuştu. Bazı işaretleri ters çevirmek bunu, (4, 4, 4, 4, 1) kütleleri için karmaşıklaştırılmış denklemlerin sonsuz sayıda çözümüne dönüştürüyor. Bunlar gerçek konfigürasyonlar değil, ama yalnızca karmaşık denklemleri gören bir argüman onları ayırt edemez.

Bu yüzden bu kütlelerde ve ilişkili (1, 1, 4, 4, 4) oranında yazar, gerçek konfigürasyonları garantili aralık aritmetiği kullanan bir bilgisayar aramasıyla doğrudan sayıyor:

(1, 4, 4, 4, 4) kütleleri için: dönme ve ölçekleme dışında 306 konfigürasyon — 60’ı düz bir çizgide, 24’ü dışbükey bir beşgen oluşturuyor, geri kalanların içinde bir ya da iki cisim var;
(1, 1, 4, 4, 4) için: 294.

Düz çizgideki 60 konfigürasyon, Moulton’ın daha önceki bir sayımıyla örtüşüyor.

Makinece denetlendi

Bu kadar çok hesaplamaya dayanan bir ispat güçlü bir doğrulama gerektirir. Her sertifika, makalenin tanımlarından yola çıkılarak yazılmış ayrı bir programla yeniden denetlendi. Hepsinden önemlisi, teorem her mantıksal adımı denetleyen bir program olan Lean 4 ispat asistanında kanıtlandı. Biçimsel ispat, Albouy ve Kaloshin’in sonuçlarını bile varsaymıyor: ihtiyaç duyduğunu yeniden türetiyor ve onların kurallarını sağlayan 1.376 etiketli diyagramı arama yoluyla buluyor. İspat, Lean ispatlarının iki ayrı bağımsız denetleyicisi tarafından da kabul ediliyor. Sıfırdan derlenmesi yaklaşık 860 CPU-saati sürüyor.

Makale kısa bir beyanla bitiyor: sonuçları bulmak ve kanıtlamak, programları ve Lean biçimselleştirmesini yazmak ve metnin taslağını hazırlamak için üretken yapay zekâ araçları kullanıldı. Araçların adı verilmiyor.

Ne söylüyor, ne söylemiyor

Sonuç düzlemdeki beş cisimle ilgili. Her pozitif kütle kümesi için konfigürasyon sayısının sonlu olduğunu kanıtlıyor, ama kesin sayıları yalnızca incelenen birkaç kütle oranında veriyor.