A Finite Certificate for the Positive $n=9$ Vasc Inequality

Resumo Técnico: Um Certificado Finito para a Desigualdade Positiva de Vasc $n = 9$

Enunciado do Problema
Este artigo aborda o caso de reais positivos da desigualdade cíclica de Vasc para $n=9$. A expressão de Vasc é definida como $C_n(x_1, \dots, x_n) = \sum_{i=1}^n \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}}$ com indexação cíclica. Embora a conjectura $C_n \ge 0$ tenha sido provada para $n=3,4,5,7$ e refutada para $n=6, 13$ (e, consequentemente, para todos os $n$ pares $\ge 6$ e ímpares $\ge 13$), os casos para $n=9$ e $n=11$ permaneceram em aberto. Especificamente, o caso $n=9$ representa uma fronteira crítica onde os métodos anteriores de Substituição de Diferença Sucessiva (SDS) encontram uma explosão combinatória, exigindo a análise de $8! = 40.320$ regiões de ordenação distintas.

Metodologia
A estratégia de prova desacopla reduções algébricas verificáveis por humanos de um certificado finito gerado por máquina. O fluxo de trabalho procede em cinco estágios distintos:

1. Eliminação de Denominadores: A desigualdade racional é transformada em uma desigualdade polinomial homogênea $P_9(x) \ge 0$ multiplicando-a pelo produto positivo de todos os denominadores, $D_9(x) = \prod (x_{i+1} + x_{i+2})$.
2. Redução de Máximo Cíclico: Aproveitando a invariância cíclica, o domínio de verificação é restrito a tuplas onde a primeira coordenada é o máximo ($x_1 \ge x_i$ para todo $i$).
3. Parametrização de Cone Ordenado: Dentro do cone de máximo fixo, as oito variáveis restantes são ordenadas de acordo com todas as permutações possíveis ($\sigma \in S_8$). Isso cria $40.320$ "cones ordenados".
4. Transformação de Coordenadas de Lacuna (Gap): Cada cone ordenado é parametrizado usando coordenadas de lacuna cumulativas ($y_1, \dots, y_9$), onde $y_i \ge 0$ representa a diferença entre variáveis adjacentes ordenadas. Isso mapeia o problema para um ortante não negativo com uma lacuna total positiva.
5. Verificação de Certificado Finito: Para cada um dos $40.320$ cones ordenados, uma "linha terminal" específica é gerada. A validade da desigualdade em cada cone é estabelecida pela verificação de um de três mecanismos de consistência:
   • Não Negatividade de Coeficientes: Todos os coeficientes do polinômio em coordenadas de lacuna são não negativos.
   • Multiplicador de Polya: O polinômio é multiplicado por um fator positivo (multiplicador de Polya) para resultar em um polinômio com coeficientes não negativos.
   • Sobreposição de Ponto Médio AM-GM: O polinômio é verificado via sobreposições de circuitos de Média Aritmética-Média Geométrica (AM-GM).

Contribuições Principais e Execução
A principal contribuição é a geração e verificação de um certificado exato finito que cobre todo o espaço de reais positivos para $n=9$.

• Colaboração Humano-IA: A prova foi obtida com assistência guiada por humanos da Equipe de Agentes MechMath, um agente impulsionado por LLM. O agente executou autonomamente a fase de verificação do certificado, incluindo a escrita de programas de verificação em Python, geração de divisões de casos e organização de classificações terminais.
• Escala do Certificado: O certificado publicado contém 36.815 folhas de coeficientes, 2.236 folhas de multiplicador de Polya ordinário e 1.269 folhas de sobreposição de ponto médio AM-GM.
• Rigor de Verificação: Os autores enfatizam que o certificado não é um registro computacional bruto, mas um artefato formal. Ele inclui um verificador independente (escrito em Python usando apenas a biblioteca padrão) que recomputa fluxos de máximo fixo, hashes de polinômios e verificações residuais diretamente dos dados armazenados, garantindo o isolamento do código que gerou o certificado.

Resultos
O artigo prova com sucesso o Teorema 1: Para quaisquer números reais positivos $x_1, \dots, x_9$, a desigualdade $\sum_{i=1}^9 \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}} \ge 0$ é válida.

• A prova resolve a primeira entrada aberta na tabela de status das desigualdades de Vasc (Tabela 1).
• O caso $n=11$ permanece em aberto, com apenas resultados positivos parciais em um pequeno cone atualmente disponíveis.

Significância
O artigo afirma significância ao resolver um problema de longa data em prova de desigualdades automatizada que estava anteriormente bloqueado pela complexidade combinatória. Ao demonstrar que um certificado finito pode ser gerado e independentemente verificado para um problema que requer a análise de mais de 40.000 regiões, o trabalho valida uma abordagem híbrida onde agentes de IA lidam com o pesado trabalho computacional (divisão de casos, geração de programas e verificação), enquanto autores humanos auditam as reduções matemáticas e a lógica de verificação. O trabalho fornece um caminho reproduzível, incluindo o certificado, um verificador independente e um caminho de reconstrução da fonte, estabelecendo um novo marco para a desigualdade de Vasc $n=9$.