A Lean-Certified Proof of $K_8(4, 2) = 23$

Riepilogo Tecnico: Una prova certificata in Lean di $K_8(4,2) = 23$

Enunciato del Problema
Il documento affronta la determinazione del numero esatto di copertura $K_q(n,r)$, definito come la dimensione minima di un codice di copertura di raggio $r$ nello spazio di Hamming $q$-ario di lunghezza $n$. Nello specifico, risolve il valore per il caso ottonario con lunghezza 4 e raggio 2: $K_8(4,2)$. Prima di questo lavoro, i limiti esistenti (nello specifico le tabelle di Kéri) collocavano questo valore nell'intervallo $[22, 23]$. Il limite inferiore era derivato dal limite del dominio della torre di Rodemich, mentre il limite superiore era supportato da limiti per alfabeti grandi. L'obiettivo era chiudere questo intervallo dimostrando che il limite inferiore è $K_8(4,2) \ge 23$.

Metodologia
La prova è formalizzata nel theorem prover Lean 4 utilizzando la libreria mathlib. Essa impiega un approccio "proof-carrying" (con prova inclusa) in cui il risultato è stabilito tramite due certificati indipendenti: un limite superiore esplicito e un limite inferiore strutturale.

1. Limite Superiore ($K_8(4,2) \le 23$):
   Gli autori forniscono un codice esplicito composto da 23 parole in $(\text{Fin } 8)^4$. La prova formale verifica due condizioni: la cardinalità dell'insieme è al massimo 23, e ogni parola nello spazio ambiente (4096 parole) è entro distanza di Hamming 2 da almeno una parola del codice. Si tratta di un controllo finito esaustivo.

2. Limite Inferiore ($K_8(4,2) \ge 23$):
   Il cuore del documento è un argomento di non esistenza strutturale per qualsiasi ipotetica copertura $C^*$ con $|C^*| \le 22$. La prova procede attraverso una sequenza di riduzioni:

   • Conteggio delle Fibre (Fiber Counting): Per una ipotetica copertura, gli autori definiscono le "fibre" $C^*_{i,a}$ (parole con il simbolo $a$ alla coordinata $i$). Dimostrano che ogni fibra deve contenere almeno due parole. Ciò stabilisce una base di 16 parole ($8 \text{ simboli} \times 2$) per coordinata, lasciando un "budget" di al massimo 6 parole eccedenti per il caso $|C^*|=22$ (o 5 per $|C^*| \le 21$).
   • Grafi delle Coppie Mancanti (Missing-Pair Graphs): La prova si sposta su un punto di vista "inverso", analizzando quali coppie di simboli sono mancanti nelle proiezioni del codice sulle coppie di coordinate. Queste coppie mancanti formano grafi $E_{ij}$.
   • Caso $|C^*| \le 21$: Utilizzando il piccolo budget di eccedenza, gli autori dimostrano tramite conteggio combinatorio che i grafi delle coppie mancanti devono contenere un "clique quattro-partito simultaneo" (un insieme di quattro simboli $a,b,c,d$ tali che tutte e sei le coppie di coordinate siano mancanti). Il Lemma 7 dimostra che tale clique non può esistere in una copertura di raggio 2 valida, escludendo così coperture di dimensione 21 o inferiore.
   • Caso $|C^*| = 22$: Per il caso rimanente, la prova riduce il problema a una classificazione finita del "profilo" dei grafi delle coppie mancanti. Gli autori mostrano che ogni profilo valido deve esibire una specifica "struttura a blocchi comune $3+3+2$".
   • Integrazione SAT/LRAT: La classificazione di questi profili è troppo vasta per una enumerazione manuale. Gli autori codificano i vincoli (limiti di grado riga/colonna e la condizione di assenza di clique) in istanze CNF (Conjunctive Normal Form). Utilizzano un risolutore SAT non fidato per generare rifutazioni LRAT (Linear RAT) — ovvero prove di insoddisfacibilità.
   • Verifica Formale: Lean analizza i certificati LRAT e riproduce meccanicamente le rifutazioni per dimostrare che non esiste un profilo valido per una copertura di 22 parole.
   • Contraddizione Finale: Anche se si assumesse una struttura a blocchi comune, gli autori derivano una contraddizione nella "componente a 2 simboli" di tale struttura. Questa componente richiederebbe un array binario di forza-2 di lunghezza 4 con al massimo 4 righe, il che è matematicamente impossibile.

Contributi Chiave

• Valore Esatto: Il documento stabilisce il valore esatto $K_8(4,2) = 23$, chiudendo l'intervallo precedentemente noto $[22, 23]$.
• Limite Inferiore Formalizzato: Fornisce una prova completamente formalizzata in Lean 4 che esclude tutte le coperture di 22 parole. Ciò viene ottenuto non tramite argomenti di volume, ma tramite ostacoli strutturali derivati dai conteggi delle fibre e dai grafi delle coppie mancanti.
• Artefatto Proof-Carrying: Il risultato è confezionato come un artefatto Lean contenente il codice esplicito, i lemmi strutturali, le istanze CNF e le rifutazioni LRAT. Fondamentalmente, il risolutore SAT non fa parte del sistema di calcolo fidato; Lean verifica internamente i certificati LRAT.
• Modello per Limiti Inferiori Computazionali: Il documento introduce un modello riutilizzabile per allegare evidenze prodotte da un solver a limiti inferiori di codici di copertura. Esso separa la "scoperta" (solver non fidato) dalla "verifica" (kernel di Lean fidato), permettendo a grandi problemi di classificazione finita di essere risolti computazionalmente pur mantenendo la correttezza formale.

Risultati
Il risultato primario è il teorema $K_8(4,2) = 23$.

• Limite Superiore: Dimostrato da un codice esplicito di 23 parole.
• Limite Inferiore: Dimostrato mostrando che una copertura di dimensione 22 conduce a una contraddizione tramite una forzata "struttura a blocchi comune $3+3+2$" che implica l'esistenza di un array binario impossibile.
• Performance: La verifica formale comporta risorse computazionali significative. Il replay in modalità kernel del file di prova principale ha richiesto circa 143 GiB di RAM, mentre la modalità nativa ha ridotto il consumo a circa 5,5 GiB. La fase di controllo LRAT ha richiesto circa 17 minuti in modalità kernel.

Significatività e Rivendicazioni
Il documento rivendica la propria significatività principalmente nell'ambito della matematica formalizzata e della metodologia di combinazione di ragionamenti combinatori con certificati computazionali.

• Spostamento Metodologico: Dimostra che la combinatoria strutturale può essere combinata con evidenze computazionali "proof-carrying". Il risolutore SAT viene utilizzato per scoprire ostacoli finiti, ma il ponte matematico e la verifica dell'output del solver sono gestiti interamente dal theorem prover.
• Confine di Fiducia: Il lavoro chiarisce il confine di fiducia nei confronti delle prove formali che coinvolgono i risolutori SAT. Il risolutore è non fidato; il kernel di Lean controlla i certificati LRAT e la deduzione logica che collega tali certificati all'enunciato del codice di copertura.
• Scalabilità: Il risultato funge da caso di test per la gestione di problemi di codici di copertura troppo grandi per una prova manuale ma sufficientemente piccoli da essere ridotti a problemi di classificazione finita risolvibili tramite risolutori SAT.
• Nessuna Nuova Applicazione: Il documento non rivendica nuove applicazioni per il valore $K_8(4,2)=23$ in sé, né propone nuovi protocolli sperimentali. Il suo contributo è strettamente la risoluzione di un problema specifico nelle tabelle della teoria dei codici e la dimostrazione di un workflow di verifica formale per tali problemi.