An AI Proof of 18-Variable Undecidability for Diophantine Equations over $\mathbb Z[i]$

Sintesi Tecnica: Una prova IA dell'indecidibilità a 18 variabili per equazioni diofantee su $\mathbb{Z}[i]$

Enunciato del Problema
Questo articolo affronta il decimo problema di Hilbert sull'anello degli interi gaussiani, $\mathbb{Z}[i]$. Il problema chiede se esista un algoritmo per decidere se un'equazione polinomiale arbitraria su un dato anello possiede una soluzione. Mentre l'indecidibilità di questo problema sugli interi $\mathbb{Z}$ è stata stabilita dal teorema di Matiyasevich, Davis, Putnam e Robinson, un naturale perfezionamento riguarda il numero minimo di incognite necessario per mantenere l'indecidibilità. Il lavoro precedente di Matiyasevich e Sun ha stabilito che l'indecidibilità sussiste per equazioni con 20 incognite su $\mathbb{Z}[i]$. Questo articolo presenta una prova che riduce tale limite a 18 incognite.

Metodologia e Framework
La prova mantiene il framework generale stabilito da Matiyasevich e Sun, che si basa su tre componenti fondamentali:

1. Il Teorema delle Variabili Fisse di Sun: Utilizzando un insieme $A \subseteq \mathbb{N}$ ricorsivamente enumerabile ma non ricorsivo e un polinomio $P(Z_0, \dots, Z_{10})$ tale che l'appartenenza ad $A$ sia equivalente all'esistenza di soluzioni intere per $P(a, z_1, \dots, z_{10}) = 0$ con $z_{10} \neq 0$.
2. Test Diofantico per gli Interi Razionali: Utilizzando un particolare test polinomiale (Lemma 3) per determinare se gli elementi in $\mathbb{Z}[i]$ siano effettivamente interi razionali.
3. Criterio di Razionalità: Applicando un criterio (Lemma 4) su $\mathbb{Q}(i)$ per forzare le variabili a essere interi razionali sulla base della razionalità di una specifica somma costruita.

Gli autori ottengono la riduzione da 20 a 18 variabili introducendo due specifiche modifiche alla precedente costruzione:

Contributi Chiave e Modifiche Tecniche

1. Eliminazione della Variabile di Eliminazione dei Denominatori:
   Nella costruzione a 20 variabili, una variabile ausiliaria veniva introdotta per eliminare i denominatori durante l'applicazione del criterio di razionalità. Gli autori sostituiscono questa con due condizioni intere dirette imposte sulle variabili $Z_1, \dots, Z_{10}$.
   Sia $Y = 2 \prod_{k=1}^{10} (3Z_k + 1)$. Invece di aggiungere una variabile per eliminare i denominatori, la prova impone le condizioni:
   $$Y^{10} \in \mathbb{Z} \quad \text{e} \quad Y^{11} + \sum_{k=1}^{10} Z_k Y^{10-k} \in \mathbb{Z}.$$
   Poiché $Y \neq 0$, queste condizioni assicurano che la quantità $Y + \sum Z_k Y^{-k}$ sia un numero razionale. Per il criterio di razionalità, ciò forza tutte le $Z_k$ a essere interi razionali. Questa modifica risparmia una variabile.

2. Assorbimento della Condizione di Non-Zero tramite un Gadget a Una Variabile:
   La precedente costruzione richiedeva due variabili per imporre una condizione di non-zero (specificamente per il prodotto $Z_{10}V_0V_1$). Gli autori introducono un gadget polinomiale a una variabile $Q(R) = (2R + 1)(3R + 1)$.

• Proprietà: $Q(R)$ non si annulla mai su $\mathbb{Z}[i]$. Inoltre, per ogni intero non nullo $n$, esiste un intero $R$ tale che $n \mid Q(R)$.
• Applicazione: Questo gadget è integrato nel "lemma di combinazione delle relazioni" (Lemma 2). Invece di un'equazione separata per imporre il non-annullamento, la condizione è assorbita nella singola equazione $f(C_0, C_1, N, Q(R), M) = 0$. Se $N=0$, l'equazione si riduce a $Q(R)^4 = 0$, il che è impossibile. Pertanto, l'equazione forza implicitamente $N \neq 0$ senza richiedere una variabile extra. Questa modifica risparmia una seconda variabile.

Suddivisione delle Variabili
Il sistema risultante utilizza esattamente 18 variabili:

• $Z_1, \dots, Z_{10}$: Le 10 variabili dall'input a variabili fisse di Sun.
• $V_0, X_0, Y_0$ e $V_1, X_1, Y_1$: Due set di 3 variabili usate per i test sugli interi su $U_0 = Y^{10}$ e $U_1 = W$ (dove $W$ è derivato dalla somma).
• $M$: La variabile di combinazione dal lemma di combinazione delle relazioni.
• $R$: L'unica variabile dal gadget di non-zero.
  Totale: $10 + 3 + 3 + 1 + 1 = 18$.

Risultato Principale
L'articolo dimostra il Teorema 1: Non esiste un algoritmo per decidere se un'equazione polinomiale arbitraria $F(X_1, \dots, X_{18}) = 0$ con coefficienti in $\mathbb{Z}$ possiede una soluzione in $\mathbb{Z}[i]^{18}$.

La prova dimostra che l'appartenenza all'insieme non ricorsivo $A$ può essere rappresentata da una singola equazione polinomiale su $\mathbb{Z}[i]$ in 18 incognite. Per il Lemma 1, il sistema finito di equazioni derivato dalla costruzione può essere combinato in una singola equazione polinomiale senza introdurre nuove variabili, preservando i coefficienti interi.

Significato e Rivendicazioni
Gli autori affermano che questo risultato migliora il teorema delle 20 incognite di Matiyasevich e Sun riducendo il conteggio delle variabili di due. L'articolo nota esplicitamente di non rivendicare l'ottimalità assoluta; abbassare ulteriormente il conteggio (ad esempio, a 17) richiederebbe miglioramenti aggiuntivi, come un test intero più piccolo, un testimone condiviso per le condizioni intere, un input a variabili fisse più forte o un diverso meccanismo di combinazione. Il lavoro funge da raffinamento tecnico all'interno del framework stabilito per l'indecidibilità diofantica sugli interi gaussiani.