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

Sintesi Tecnica: Un Certificato Finito per la Disuguaglianza Positiva di Vasc per $n = 9$

Enunciato del Probleo
Questo articolo affronta il caso dei reali positivi della disuguaglianza ciclica di Vasc per $n=9$. L'espressione di Vasc è definita come $C_n(x_1, \dots, x_n) = \sum_{i=1}^n \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}}$ con indicizzazione ciclica. Mentre la congettura $C_n \ge 0$ è stata dimostrata per $n=3,4,5,7$ e smentita per $n=6, 13$ (e di conseguenza per tutti i $n$ pari $\ge 6$ e tutti i $n$ dispari $\ge 13$), i casi per $n=9$ e $n=11$ rimanevano aperti. Nello specifico, il caso $n=9$ rappresenta una frontiera critica dove i precedenti metodi di Sostituzione di Differenza Successiva (SDS) incontrano un'esplosione combinatoria, richiedendo l'analisi di $8! = 40.320$ regioni di ordinamento distinte.

Metodologia
La strategia di prova scinde le riduzioni algebriche verificabili dall'uomo da un certificato finito generato dalla macchina. Il flusso di lavoro procede attraverso cinque fasi distinte:

1. Eliminazione dei Denominatori: La disuguaglianza razionale viene trasformata in una disuguaglianza polinomiale omogenea $P_9(x) \ge 0$ moltiplicando per il prodotto positivo di tutti i denominatori, $D_9(x) = \prod (x_{i+1} + x_{i+2})$.
2. Riduzione al Massimo Ciclico: Sfruttando l'invarianza ciclica, il dominio di verifica viene ristretto alle tuple in cui la prima coordinata è il massimo ($x_1 \ge x_i$ per ogni $i$).
3. Parametrizzazione del Cono Ordinato: All'interno del cono a massimo fisso, le restanti otto variabili sono ordinate secondo tutte le possibili permutazioni ($\sigma \in S_8$). Ciò crea $40.320$ "coni ordinati".
4. Trasformazione delle Coordinate di Gap: Ogni cono ordinato è parametrizzato utilizzando coordinate di gap cumulativo ($y_1, \dots, y_9$), dove $y_i \ge 0$ rappresenta la differenza tra variabili adiacenti ordinate. Ciò mappa il problema in un ortante non negativo con un gap totale positivo.
5. Verifica del Certificato Finito: Per ciascuno dei $40.320$ coni ordinati, viene generata una specifica "riga terminale". La validità della disuguaglianza su ciascun cono è stabilita verificando uno di tre meccanismi di affidabilità:
   • Non Negatività dei Coefficienti: Tutti i coefficienti del polinomio nelle coordinate di gap sono non negativi.
   • Moltiplicatore di Polya: Il polinomio viene moltiplicato per un fattore positivo (moltiplicatore di Polya) per ottenere un polinomio con coefficienti non negativi.
   • Overlay del Midpoint AM-GM: Il polinomio viene verificato tramite overlay di circuiti di Media Aritmetica-Media Geometrica (AM-GM).

Contributi Chiave ed Esecuzione
Il contributo primario è la generazione e la verifica di un certificato esatto finito che copre l'intero spazio dei reali positivi per $n=9$.

• Collaborazione Uomo-IA: La prova è stata ottenuta con l'assistenza guidata dall'uomo del MechMath Agent Team, un team di agenti guidati da LLM. L'agente ha eseguito autonomamente la fase di verifica del certificato, inclusa la scrittura di programmi di verifica in Python, la generazione di scissioni di casi (case splits) e l'organizzazione delle classificazioni terminali.
• Scala del Certificato: Il certificato pubblicato contiene 36.815 foglie di coefficienti, 2.236 foglie di moltiplicatore di Polya ordinario e 1.269 foglie di overlay di midpoint AM-GM.
• Rigore della Verifica: Gli autori sottolineano che il certificato non è un semplice trascritto computazionale, ma un artefatto formale. Esso include un verificatore indipendente (scritto in Python utilizzando solo la libreria standard) che ricalcola gli stream a massimo fisso, gli hash polinomiali e i controlli residui direttamente dai dati memorizzati, garantendo l'isolamento dal codice che ha generato il certificato.

Risultati
Il saggio dimostra con successo il Teorema 1: Per ogni numero reale positivo $x_1, \dots, x_9$, la disuguaglianza $\sum_{i=1}^9 \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}} \ge 0$ è soddisfatta.

• La prova risolve la prima voce aperta nella tabella di stato delle disuguaglianze di Vasc (Tabella 1).
• Il caso $n=11$ rimane aperto, con solo risultati positivi parziali su un piccolo cono attualmente disponibili.

Significatività
L'articolo sostiene di risolvere un problema aperto di lunga data nella dimostrazione automatizzata di disuguaglianze, precedentemente bloccato dalla complessità combinatoria. Dimostrando che un certificato finito può essere generato e verificato indipendentemente per un problema che richiede l'analisi di oltre 40.000 regioni, questo lavoro valida un approccio ibrido in cui gli agenti IA gestiscono il carico di lavoro computazionale pesante (scissione dei casi, generazione di programmi e verifica) mentre gli autori umani controllano le riduzioni matematiche e la logica di verifica. Il lavoro fornisce una via riproducibile, includendo il certificato, un verificatore indipendente e un percorso di ricostruzione della sorgente, stabilendo un nuovo standard per la disuguaglianza di Vasc $n=9$.