The lonely runner conjecture holds for nine runners

Technische Samenvatting: De Lonely Runner Conjecture voor negen renners

Probleemstelling
Het artikel behandelt de Lonely Runner Conjecture, een langlopend open probleem in de combinatorische getaltheorie dat in 1967 door Wills werd voorgesteld. De conjectuur stelt dat voor elke integer $k \ge 1$ en elke verzameling van $k$ verschillende integers (die de snelheden van de renners representeren: $v_1, \dots, v_k$), er een reële tijd $t$ bestaat waarbij elke renner "eenzaam" is. Wiskundig gezien betekent dit dat er een $t$ bestaat waar de afstand van elke renner tot de oorsprong op een eenheidscirkel ten minste $1/(k+1)$ is, uitgedrukt als $\|t v_i\| \ge 1/(k+1)$ voor alle $i$.

Hoewel de conjectuur is geverifieerd voor kleine waarden van $k$ (tot $k=7$), blijft zij in het algemene geval onopgelost. Dit artikel richt zich specifal op het geval van negen renners ($k=9$).

Methodologie
De bewijstrategie bouwt voort op het eerdere werk van de auteur waarin de conjectuur voor acht renners werd vastgesteld. De kern van het argument berust op een bewijs uit het ongerijmde met betrekking tot de eigenschappen van een hypothetische "minimale tegenvoorbeeld".

1. Reductie naar deelbaarheidsrestricties:
   Het bewijs maakt gebruik van een bovengrens afgeleid door Malikiosis, Santos en Schymura (Stelling 1), die impliceert dat als de conjectuur geldt voor $k$, deze ook geldt voor $k+1$, mits het product van de snelheden in elk minimaal tegenvoorbeeld een specifieke drempel overschrijdt. Bijgevolg volstaat het om te bewijzen dat er geen verzameling van $k$ snelheden bestaat die de "lonely runner property" (LR-eigenschap) schendt terwijl zij voldoet aan de deelbaarheidsrestricties opgelegd door de bovengrens, om de conjectuur voor $k+1$ te bewijzen.

2. Gegeneraliseerde Lemma voor delers:
   De auteurs introduceren Lemma 6, een versterkte en gegeneraliseerde versie van een eerdere lemma (Lemma 3). Deze lemma stelt voorwaarden vast waaronder een specifieke integer $d$ de product van de snelheden van elke verzameling van 8 integers moet delen die de LR-eigenschap mist.

   • De lemma introduceert een coëfficiënt $c$ en beschouwt snelheden modulo $9cd$.
   • Het incorporeert specifieke deelbaarheidsvoorwaarden met betrekking tot het aantal snelheden deelbaar door 3 en 9 (afgeleid van Lemma 5).
   • De voorwaarde vereist het verifiëren dat er voor elke verzameling van 8 snelheden die voldoet aan specifieke GCD- en deelbaarheidsrestricties, een tijd $t$ bestaat die de LR-eigenschap bevredigt.

3. Computer-ondersteerde verificatie (Set Cover Herformulering):
   Het verifiëren van de voorwaarden van Lemma 6 is computationeel intensief. De auteurs herformuleren het probleem als een set cover probleem (Lemma 7).

   • Een integer $v$ "dekt" een integer $j$ als $\| \frac{jv}{9cd} \| < 1/8$.
   • Het doel is te verifiëren dat er geen "slechte" 8-tuple bestaat die alle noodzakelijke integers dekt terwijl zij voldoet aan de deelbaarheidsrestricties.
   • De auteurs hebben een backtracking-algoritme geïmplementeerd met significante optimalisaties ten opzichte van hun eerdere werk voor $k=7$:
     • Precomputatie van bitsets voor gedekte posities.
     • Pruning-strategieën gebaseerd op het maximum aantal nieuwe integers dat een kandidaat-element kan dekken.
     • Memoïsatie om redundante zoekpaden te elimineren.
   • De auteurs hebben ook SAT-solver benaderingen getest (met behulp van Cardinality-CDCL en Minicard), maar stelden vast dat deze aanzienlijk trager waren dan hun eigen backtracking-implementatie voor deze specifieke probleemstructuur.

Belangrijkste bijdragen en resultaten

• Bewijs voor negen renners: Het artikel levert een volledig bewijs dat de Lonely Runner Conjecture geldt voor $k=9$.
• Identificatie van delers: Door Lemma 6 toe te passen met een computerprogramma, hebben de auteurs een verzameling $S$ van integers geïdentificeerd (inclusief priemfactoren zoals $64, 81, 25$ en priemgetallen tot 191) die het product van de snelheden in elk minimaal tegenvoorbeeld voor 9 renners moeten delen.
• Tegenstrijdigheid: Het product van de elementen in verzameling $S$ (die onderling relatief priem zijn) is ongeveer $9,09 \times 10^{79}$. Echter, de theoretische bovengrens voor het product van de snelheden in een minimaal tegenvoorbeeld (afgeleid van Corollary 2) is ongeveer $8,47 \times 10^{79}$. Aangezien het vereiste product van de delers de maximale mogelijke product van snelheden overstijgt, kan een dergelijk tegenvoorbeeld niet bestaan.
• Algoritmische verbeteringen: Het artikel beschrijft specifieke implementatieverbeteringen die de runtime voor de verificatie van het $k=7$ geval hebben verminderd van 32 uur naar 50 minuten, wat de complexere $k=9$ verificatie mogelijk maakte.

Betekenis en claims
De auteurs stellen dat dit resultaat de bekende reikwijdte van de Lonely Runner Conjecture uitbreidt van 7 naar 9 renners. Zij merken op dat de gebruikte techniek theoretisch toepasbaar is op elk specifiek aantal renners, hoewel de computationele kosten exponentieel toenemen.

• Onafhankelijkheid: De auteurs erkennen dat Trakulthongchai onafhankelijk bewijzen heeft aangekondigd voor $k=9$ en $k=10$ kort voor deze indiening. Het werk van Trakulthongchai bouwt eveneens voort op het $k=7$ bewijs en maakt gebruik van een "slimme sieefmethode" die naar even wordt geschat ongeveer 100 keer sneller te zijn dan de hier gepresenteerde methode.
• Toekomstperspectief: Het artikel bespreekt de haalbaarheid van het uitbreiden hiervan naar $k=10$. Hoewel de methode aanpasbaar is, wordt de computationele kost voor het verifiëren van priemgetallen tot ongeveer 263 geschat op twee jaar op een enkele processor-core. De auteurs suggereren dat het combineren van hun verbeteringen (zoals het overwegen van machten van kleine priemgetallen) met de sieefmethode van Trakulthongchai het $k=10$ geval hanteerbaarder zou kunnen maken, maar zij beweren dit niet zelf opgelost te hebben.

Samenvattend heeft het artikel de $k=9$ casus succesvol opgelost door een combinatie van verfijnde theoretische lemma's en hooggeoptimaliseerde computerverificatie, waarbij het werk bescheiden wordt gepositioneerd als een stap voorwaarts die zowel profiteert van als bijdraagt aan de bredere inspanning om de conjectuur voor hogere $k$ op te lossen.