Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4

Sintesi Tecnica: Fondamenta Formali e Certificati Portatori di Dimostrazione per i Codici di Copertura $q$-ari in Lean 4

Enunciato del Problema
I codici di copertura negli spazi di Hamming finiti cercano l'insieme più piccolo di parole (parole codice) tali che l'unione delle loro sfere di Hamming di raggio $r$ copra l'intero spazio $A^n$. La quantità centrale è il numero di copertura $q$-ario $K_q(n,r)$, definito come la dimensione minima di un tale codice. Sebbene la definizione sia elementare, determinare i valori esatti o i limiti stretti per $K_q(n,r)$ si basa tipicamente su un misto di costruzioni esplicite, argomenti di conteggio, relazioni ricorsive e ricerche computazionali. Una sfida significativa nel campo è che le affermazioni esatte $K_q(n,r) = k$ richiedono due componenti indipendenti: una costruzione esplicita che dimostri un limite superiore ($K_q(n,r) \le k$) e una dimostrazione che non esista un codice più piccolo (un limite inferiore $K_q(n,r) \ge k$). Queste componenti spesso provengono da fonti disperate, rendendo difficile la verifica dei valori esatti.

Metodologia
Il documento presenta una formalizzazione della teoria elementare dei codici di copertura nel theorem prover Lean 4. La metodologia è caratterizzata da tre scelte progettuali fondamentali:

1. Rappresentazione delle Parole: Le parole sono modellate come funzioni dipendenti da un tipo di coordinata a un tipo di alfabeto. Lo spazio di Hamming $q$-ario generale di lunghezza $n$ è rappresentato come Fin n → Fin q. Questa rappresentazione funzionale preserva un'interfaccia generale per tipi di coordinate astratti semplificando al contempo la specializzazione $q$-aria.
2. Predicati di tipo Certificato: Invece di definire $K_q(n,r)$ come una funzione di minimizzazione non computabile, la formalizzazione utilizza predicati logici per rappresentare asserzioni riguardanti i numeri di copertura.
   • KUpper r k: Asserisce l'esistenza di un codice di copertura finito di dimensione al massimo $k$ (limite superiore).
   • KLower r k: Asserisce che ogni codice di copertura finito ha dimensione almeno $k$ (limite inferiore).
   • KSpec r k: Combina entrambi per asserire l'esattezza ($K_q(n,r) = k$).
     Questo approccio modulare permette di assemblare indipendentemente limiti superiori e inferiori provenienti da fonti diverse.
3. Database Portatore di Dimostrazione: Il documento implementa un database in cui le asserzioni memorizzate non sono meri valori numerici, ma oggetti "portatori di dimostrazione" (proof-carrying). Ogni voce include una traccia di derivazione. Riprodurre questa traccia in Lean ricostruisce una dimostrazione formale del corrispondente predicato QaryKUpper o QaryKLower. Il sistema distingue tra teoremi matematici scritti a mano (controllati dal kernel) e dati generati (produttori non fidati il cui output viene validato tramite la riproduzione della traccia).

Contributi Chiave
Il documento stabilisce una base riutilizzabile e verificabile per i certificati dei codici di copertura controllati dalla macchina. I suoi contributi specifici includono:

• Infrastruttura Formale: Un framework completo in Lean 4 per gli spazi di Hamming finiti, la distanza di Hamming, le sfere chiuse e i predicati di copertura, gestendo rigorosamente i casi limite (ad es. $q=0$, $n=0$, $r \ge n$) all'interno delle definizioni piuttosto che come convenzioni informali.
• Risultati Analitici: Dimostrazioni formali della formula del volume della sfera di Hamming $q$-aria e del classico limite inferiore di copertura della sfera. Il limite di copertura della sfera è incapsulato come una funzione computabile sphereLower che genera certificati di limite inferiore certificati.
• Teoremi Strutturali: Formalizzazione di casi esatti elementari (ad es. $K_q(n,0) = q^n$, $K_q(n, n-1) = q$) e costruzioni strutturali, inclusa una costruzione di copertura prodotto e varie relazioni di vicinato (punzonatura, allungamento, proiezione dell'alfabeto e concatenazione) che trasportano i limiti tra triple di parametri.
• Caso di Studio (Van Laarhoven et al.): Un flusso di lavoro end-to-end che dimostra la formalizzazione di codici espliciti pubblicati. Gli autori hanno trascritto i codici di copertura da un articolo del 1989 (Van Laarhoven et al.) in Lean, codificandoli come array compatti per evitare i limiti di elaborazione (elaboration limits). Il sistema ha verificato la proprietà di copertura e la cardinalità, producendo certificati di limite superiore controllati dalla macchina per $K_3(6,1) \le 73$, $K_3(7,1) \le 186$ e $K_3(8,1) \le 486$.
• Implementazione del Database: Un database portatore di dimostrazione contenente 52.822 voci per parametri $0 \le q \le 21$, $0 \le n \le 48$ e $0 \le r \le 48$. Questo database include certificati esatti per casi piccoli (ad es. $K_2(5,1)=7$, $K_3(3,1)=5$) e intervalli derivati dalla riproduzione della traccia.

Risultati
La formalizzazione verifica con successo:

• La formula del volume della sfera $q$-aria e il limite inferiore di copertura della sfera.
• Valori esatti elementari come $K_2(5,1)=7$, $K_2(6,2)=4$, $K_3(3,1)=5$ e $K_4(3,1)=8$.
• Limiti superiori per il problema ternario del "football-pool" derivati da codici espliciti, specificamente $K_3(6,1) \le 73$, $K_3(7,1) \le 186$ e $K_3(8,1) \le 486$.
• Una costruzione ciclica a due blocchi uniforme che dimostra $K_q(3,1) \le \lceil q^2/2 \rceil$.

Il processo di chiusura del database ha propagato con successo queste fonti primitive attraverso regole di relazione certificate per generare una tabella coerente di limiti. Il sistema supporta due modalità di prova: una "modalità kernel" che utilizza lo standard decide per garanzie di riproduzione più forti, e una "modalità nativa" che utilizza l'evaluator compilato di Lean per uno sviluppo più veloce, con confini di fiducia chiaramente definiti per ciascuna.

Significato e Rivendicazioni
Il documento afferma esplicitamente che il suo contributo primario non è la scoperta di nuovi limiti record o la riproduzione di tabelle della letteratura esistente. Invece, la sua importanza risiede nel fornire un interfaccia formale e una fondazione verificabile per i certificati dei codici di copertura.

Il lavoro colma il divario tra la letteratura classica dei codici di copertura e i futuri certificati computazionali. Separando i testimoni dei limiti superiori, gli argomenti dei limiti inferiori e i predicati di esattezza, la formalizzazione consente ai risultati derivanti da costruzioni esplicite, conteggi combinatori e (potenzialmente) futuri risolutori SAT o di programmazione intera di essere controllati e composti all'interno di un unico framework fidato. La natura "portatrice di dimostrazione" del database assicura che ogni limite riportato possa essere ricondotto a una dimostrazione controllata dalla macchina, affrontando le sfide di riproducibilità e verifica inerenti al campo. Il documento si pone come un passo fondamentale verso un futuro in cui i risultati della ricerca computazionale possano essere integrati senza soluzione di continuità nelle librerie matematiche formali.