Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound

Sintesi Tecnica: Certificati Verificati da Macchina per la Metà Geometrica del Limite Minimo di Kochen–Specker

Enunciato del Problema

Il problema del limite minimo di Kochen–Specker (KS) cerca il minor numero $n$ di vettori non nulli in $\mathbb{R}^3$, distinti a coppie come raggi, tali per cui il loro grafo di ortogonalità non ammetta una colorazione $\{0, 1\}$ in cui ogni coppia ortogonale contenga al massimo un $1$ e ogni triade ortogonale contenga esattamente un $1$. Il miglior limite inferiore noto è $n \ge 24$, stabilito computazionalmente da Li et al. e Kirchweger et al.

Questa dimostrazione consiste in due metà:

1. Metà Combinatoria: Un'enumerazione SAT isomorfo-free di grafi candidati fino all'ordine 23. I risultati di insoddisfacibilità sono accompagnati da prove DRAT, che sono verificabili in modo indipendente.
2. Metà Geometrica: Una dimostrazione che ogni grafo candidato enumerato non è incorporabile in $\mathbb{R}^3$. Questa metà si affida al solver di aritmetica reale non lineare (NRA) di Z3 per determinare che nessuna assegnazione di vettori non nulli e distinti come raggi soddisfa i vincoli di ortogonalità.

Il gap critico identificato in questo lavoro è che la metà geometrica non produce oggetti di prova verificabili. La catena di fiducia termina nella procedura decisionale di Z3 per una teoria $\exists\mathbb{R}$-hard, richiedendo alla comunità di accettare i verdetti di non-incorporabilità sulla base della fede. Inoltre, la pipeline pubblicata si affida a "database di blocco" di sottografi minimi non incorporabili, che sono anch'essi derivati da Z3 e non verificati.

Metodologia

Gli autori introducono un framework per generare e verificare certificati di albero di casi razionali esatti per la non-incorporabilità reale. La metodologia sostituisce l'opaca procedura decisionale di Z3 con un processo di verifica algebrica trasparente.

1. Struttura del Certificato
Un certificato è un oggetto autosufficiente che comprende:

• Ancoraggio e Propagazione: Un passaggio di normalizzazione (ancoraggio di una triade o di un arco ortogonale) seguito da un programma di propagazione che esprime tutti i vettori dei vertici in termini di pochi parametri utilizzando prodotti vettiali e parametrizzazioni di piani.
• Albero di Casi: Una struttura ad albero dove i nodi interni rappresentano scissioni basate su:
  • Fattorizzazione: $p = \prod f_k$, verificata tramite espansione.
  • Somma di Quadrati (SOS): $p = \sum c_k m_k^2$ con $c_k \in \mathbb{Q}_{>0}$, verificata tramite espansione.
• Foglie: I rami sono chiusi da uno di quattro meccanismi:
  • Collisione di Iniettività: Dimostrare che due vertici distinti mappano su raggi paralleli.
  • Collasso di Obbligo: Dimostrare che un polinomio non nullo richiesto è identicamente zero.
  • Appartenenza all'Ideale: Cofattori espliciti che dimostrano che un polinomio appartiene all'ideale generato dai vincoli.
  • Positività di tipo Positivstellensatz: Un argomento generalizzato che mostra come una somma di termini positivi (polinomi di iniettività) sia uguale a una somma di quadrati, portando a una contraddizione nei punti reali.

2. Architettura di Verifica
Il sistema impiega due checker indipendenti che non condividono codice con il generatore di certificati:

• Replay in Pure-Python: Esegue la logica del certificato utilizzando l'aritmetica razionale esatta.
• Total Checker in Lean 4: Una funzione riflessiva Cert.check implementata nell'assistente alla dimostrazione Lean 4.
  • Riducibilità del Kernel: Per garantire che il verdetto sia un teorema di kernel chiuso, gli autori hanno implementato uno strato di aritmetica razionale gcd-free (KRat) e una ricorsione strutturale con fuel. Ciò consente che l'intero calcolo sia ridotto dal kernel di Lean senza riduzione nativa o assiomi personalizzati.
  • Chiusura degli Assiomi: Il teorema di correttezza si affida solo a {propext, Classical.choice, Quot.sound}, evitando riduzioni native non verificate.

** 3. Teorema di Correttezza**
Il teorema centrale, check_sound, afferma che se check c = true, allora non esiste alcuna realizzazione del grafo. Una realizzazione è definita come una mappa in $\mathbb{R}^3$ che soddisfa vettori non nulli, ortogonalità sugli archi e distinzione dei raggi a coppie (iniettività) per tutte le coppie di vertici.

Contributi Chiave

1. Certificati Razionali Esatti: L'introduzione di un formato di certificato che sostituisce le approssimazioni numeriche e i solver opachi con l'aritmetica razionale esatta, le fattorizzazioni polinomiali e le decomposizioni SOS.
2. Copertura Completa del Database di Blocco: Certificazione di tutte le 291 righe sorgente (che rappresentano 180 grafi distinti) dalle liste di blocco pubblicate di PhysicsCheck (ordini 10–13), sostituendo ogni verdetto di Z3 con un teorema verificato da macchina.
3. Dual Independent Replay: Validazione tramite due checker distinti (Python e Lean) che rifiutano 115 mutazioni avversarie (ad esempio, coefficienti alterati, rami rimossi) accettando al contempo i certificati genuini.
4. Risultati Guidati dalla Formalizzazione: La rigorosa formalizzazione ha rivelato problemi specifici nella pipeline originale:
   • L'Iniettività è Fondamentale: L'originale codifica Z3 imponeva la distinzione dei raggi a coppie per tutte le coppie, non solo per quelle adiacenti. Diversi grafi nel database sono non-incorporabili esclusivamente a causa di questo vincolo di iniettività, una sfumatura invisibile ai solver geometrici standard.
   • Casi WLOG Nascosti: La parametrizzazione dell'ortoplano usata nella pipeline originale celava casi degeneri (vettori paralleli) che devono essere esplicitamente risolti tramite argomenti di iniettività.
   • Ottimizzazione Empirica: È stato scoperto che un'ottimizzazione di "non-colorabilità" nella pipeline originale era empirica piuttosto che un lemma fondamentale.
   • Conteggi Riproducibili: Il conteggio pubblicato dei candidati finali di ordine 23 (41) è risultato irreproducibile dagli artefatti; il conteggio corretto è 43, con 42 risolti dai nuovi certificati di ordine 13.

Risultati

• Copertura di Verifica: Tutti i 180 grafi distinti nel database di blocco hanno ora teoremi di kernel chiusi che ne dimostrano la non-incorporabilità.
• Prestazioni: L'evaluazione del kernel richiede circa 0,5 secondi per i grafi di ordine 10/11/12 e 1,8 secondi per i grafi di ordine 13 su un laptop standard. L'intera suite di verifica si esegue in pochi minuti.
• Impatto sul Limite: I sette nuovi certificati di ordine 13 risolvono 42 dei 44 candidati finali nell'enumerazione ordine-22/23 tramite la monotonia verificata dei sottografi. I restanti due candidati sono tracciati come obblighi espliciti e leggibili da macchina.
• Robustezza Avversaria: Entrambi i checker hanno rifiutato con successo tutti i 115 certificati mutati nella continuous integration, dimostrando che la logica di verifica non è una semplice riproduzione dell'output del generatore ma un vero controllo indipendente.

Significato

L'articolo sostiene di chiudere il gap di fiducia per la metà geometrica del limite minimo KS riguardo al database di blocco. Convertendo i veretti non verificati di Z3 in teoremi di kernel chiusi, il lavoro assicura che la non-incorporabilità dei sottografi critici non sia più una questione di fede in un solver a scatola nera.

Gli autori sottolineano che il processo di formalizzazione stesso è stato una fonte primaria di valore, facendo emergere assunzioni nascoste (iniettività), obblighi di casi nascosti e discrepanze nei dati che erano invisibili al flusso di lavoro originale. Sebbene l'articolo non componga ancora un teorema end-to-end completamente verificato per $n \ge 24$ (a causa della scala dell'enumerazione SAT e delle prove di canonicità), esso stabilisce la base geometrica verificata e fornisce un percorso scalabile per il futuro. Il lavoro dimostra che il ragionamento geometrico complesso nelle fondamenta quantistiche può essere reso completamente verificabile da macchina con aritmetica esatta e assiomi minimi.