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

Resumo Técnico: Uma Prova de IA de Indecidibilidade de 18 Variáveis para Equações Diofantinas sobre $\mathbb{Z}[i]$

Enunciado do Problema
Este artigo aborda o Décimo Problema de Hilbert sobre o anel dos inteiros gaussianos, $\mathbb{Z}[i]$. O problema questiona se existe um algoritmo para decidir se uma equação polinomial arbitrária sobre um determinado anel possui uma solução. Embora a indecidibilidade deste problema sobre os inteiros $\mathbb{Z}$ tenha sido estabelecida pelo teorema de Matiyasevich, Davis, Putnam e Robinson, um refinamento natural diz respeito ao número mínimo de incógnitas necessárias para manter a indecidibilidade. Trabalhos anteriores de Matiyasevich e Sun estabeleceram que a indecidibilidade ocorre para equações com 20 incógnitas sobre $\mathbb{Z}[i]$. Este artigo apresenta uma prova reduzindo esse limite para 18 incógnitas.

Metodologia e Estrutura
A prova mantém a estrutura geral estabelecida por Matiyasevich e Sun, que se baseia em três componentes principais:

1. Teorema de Variável Fixa de Sun: Utilizando um conjunto recursivamente enumerável, mas não recursivo, $A \subseteq \mathbb{N}$ e um polinômio $P(Z_0, \dots, Z_{10})$ tal que a pertinência em $A$ é equivalente à existência de soluções inteiras para $P(a, z_1, \dots, z_{10}) = 0$ com $z_{10} \neq 0$.
2. Teste Diofantino para Inteiros Racionais: Utilizando um teste polinomial específico (Lema 3) para determinar se elementos em $\mathbb{Z}[i]$ são, de fato, inteiros racionais.
3. Critério de Racionalidade: Aplicando um critério (Lema 4) sobre $\mathbb{Q}(i)$ para forçar variáveis a serem inteiros racionais com base na racionalidade de uma soma específica construída.

Os autores alcançam a redução de 20 para 18 variáveis introduzindo duas modificações específicas na construção anterior:

Contribuições Principais e Modificações Técnicas

1. Eliminação da Variável de Eliminação de Denominadores:
   Na construção de 20 variáveis, uma variável auxiliar era introduzida para eliminar denominadores ao aplicar o critério de racionalidade. Os autores substituem isso por duas condições inteiras diretas impostas às variáveis $Z_1, \dots, Z_{10}$.
   Seja $Y = 2 \prod_{k=1}^{10} (3Z_k + 1)$. Em vez de adicionar uma variável para eliminar denominadores, a prova impõe as condições:
   $$Y^{10} \in \mathbb{Z} \quad \text{e} \quad Y^{11} + \sum_{k=1}^{10} Z_k Y^{10-k} \in \mathbb{Z}.$$
   Como $Y \neq 0$, essas condições garantem que a quantidade $Y + \sum Z_k Y^{-k}$ seja um número racional. Por meio do critério de racionalidade, isso força todos os $Z_k$ a serem inteiros racionais. Esta modificação economiza uma variável.

2. Absorção da Condição de Não-Nulidade via um Gadget de Uma Variável:
   A construção anterior exigia duas variáveis para impor uma condição de não-nulidade (especificamente para o produto $Z_{10}V_0V_1$). Os autores introduzem um gadget polinomial de uma variável $Q(R) = (2R + 1)(3R + 1)$.

   • Propriedades: $Q(R)$ nunca se anula em $\mathbb{Z}[i]$. Além disso, para cada inteiro não nulo $n$, existe um inteiro $R$ tal que $n \mid Q(R)$.
   • Aplicação: Este gadget é integrado ao "lema de combinação de relações" (Lema 2). Em vez de uma equação separada para impor o não-anulamento, a condição é absorvida na única equação $f(C_0, C_1, N, Q(R), M) = 0$. Se $N=0$, a equação reduz-se a $Q(R)^4 = 0$, o que é impossível. Assim, a equação implicitamente força $N \neq 0$ sem exigir uma variável extra. Esta modificação economiza uma segunda variável.

Detalhamento da Contagem de Variáveis
O sistema resultante utiliza exatamente 18 variáveis:

• $Z_1, \dots, Z_{10}$: As 10 variáveis da entrada de variável fixa de Sun.
• $V_0, X_0, Y_0$ e $V_1, X_1, Y_1$: Dois conjuntos de 3 variáveis usados para os testes de inteiros em $U_0 = Y^{10}$ e $U_1 = W$ (onde $W$ é derivado da soma).
• $M$: A variável de combinação do lema de combinação de relações.
• $R$: A única variável do gadget de não-nulidade.
  Total: $10 + 3 + 3 + 1 + 1 = 18$.

Resultado Principal
O artigo prova o Teorema 1: Não existe um algoritmo para decidir se uma equação polinomial arbitrária $F(X_1, \dots, X_{18}) = 0$ com coeficientes em $\mathbb{Z}$ possui uma solução em $\mathbb{Z}[i]^{18}$.

A prova demonstra que a pertinência no conjunto não recursivo $A$ pode ser representada por uma única equação polinomial sobre $\mathbb{Z}[i]$ em 18 incógnitas. Pelo Lema 1, o sistema finito de equações derivado da construção pode ser combinado em uma única equação polinomial sem introduzir novas variáveis, preservando os coeficientes inteiros.

Significância e Alegações
Os autores afirmam que este resultado melhora o teorema de 20 incógnitas de Matiyasevich e Sun, reduzindo a contagem de variáveis em duas. O artigo observa explicitamente que não reivindica otimalidade absoluta; reduzir a contagem ainda mais (por exemplo, para 17) exigiria melhorias adicionais, como um teste de inteiro menor, uma testemunha compartilhada para as condições de inteiro, uma entrada de variável fixa mais forte ou um mecanismo de combinação diferente. O trabalho serve como um refinamento técnico dentro da estrutura estabelecida da indecidibilidade diofantina sobre os inteiros gaussianos.