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

Résumé Technique : Un certificat fini pour l'inégalité de Vasc positive pour $n = 9$

Énoncé du Problème
Cet article traite le cas des réels positifs de l'inégalité cyclique de Vasc pour $n=9$. L'expression de Vasc est définie par $C_n(x_1, \dots, x_n) = \sum_{i=1}^n \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}}$ avec un indexage cyclique. Alors que la conjecture $C_n \ge 0$ a été prouvée pour $n=3,4,5,7$ et infirmée pour $n=6, 13$ (et par conséquent pour tous les $n$ pairs $\ge 6$ et tous les $n$ impairs $\ge 13$), les cas pour $n=9$ et $n=11$ restaient ouverts. Spécifiquement, le cas $n=9$ représente une frontière critique où les méthodes antérieures de Substitution de Différence Successive (SDS) se heurtent à une explosion combinatoire, nécessissant l'analyse de $8! = 40\,320$ régions d'ordonnancement distinctes.

Méthodologie
La stratégie de preuve découple les réductions algébriques vérifiables par l'humain d'un certificat fini généré par machine. Le flux de travail se déroule en cinq étapes distinctes :

1. Élimination des Dénominateurs : L'inégalité rationnelle est transformée en une inégalité polynomiale homogène $P_9(x) \ge 0$ en multipliant par le produit positif de tous les dénominateurs, $D_9(x) = \prod (x_{i+1} + x_{i+2})$.
2. Réduction au Maximum Cyclique : En exploitant l'invariance cyclique, le domaine de vérification est restreint aux tuples où la première coordonnée est le maximum ($x_1 \ge x_i$ pour tout $i$).
3. Paramétrage par Cône Trié : À l'intérieur du cône à maximum fixé, les huit variables restantes sont triées selon toutes les permutations possibles ($\sigma \in S_8$). Cela crée $40\,320$ « cônes triés ».
4. Transformation en Coordonnées d'Écart : Chaque cône trié est paramétré à l'aide de coordonnées d'écart cumulatives ($y_1, \dots, y_9$), où $y_i \ge 0$ représente la différence entre les variables adjacentes triées. Cela projette le problème vers un orthant non négatif avec un écart total positif.
5. Vérification du Certificat Fini : Pour chacun des $40\,320$ cônes triés, une « ligne terminale » spécifique est générée. La validité de l'inégalité sur chaque cône est établie en vérifiant l'un des trois mécanismes de validité :
   • Non-négativité des Coefficients : Tous les coefficients du polynôme dans les coordonnées d'écart sont non nuls.
   • Multiplicateur de Polya : Le polynôme est multiplié par un facteur positif (multiplicateur de Polya) pour obtenir un polynôme avec des coefficients non négatifs.
   • Recouvrement de Point Médian AM-GM : Le polynôme est vérifié via des recouvrements de circuits AM-GM (Moyenne Arithmétique-Moyenne Géométrique).

Contributions Clés et Exécution
La contribution principale est la génération et la vérification d'un certificat exact fini qui couvre tout l'espace des réels positifs pour $n=9$.

• Collaboration IA-Humain : La preuve a été obtenue avec l'assistance guidée par l'humain de l'Équipe d'Agents MechMath, un agent piloté par un LLM. L'agent a exécuté de manière autonome la phase de vérification du certificat, incluant l'écriture de programmes de vérification en Python, la génération de divisions de cas et l'organisation des classifications terminales.
• Échelle du Certificat : Le certificat publié contient 36 815 feuilles de coefficients, 2 236 feuilles de multiplicateur de Polya ordinaire et 1 269 feuilles de recouvrement de point médian AM-GM.
• Rigueur de la Vérification : Les auteurs soulignent que le certificat n'est pas un simple compte rendu computationnel mais un artefact formel. Il inclut un vérificateur indépendant (écrit en Python utilisant uniquement la bibliothèque standard) qui recompute les flux à maximum fixé, les hachages de polynômes et les vérifications de résidus directement à partir des données stockées, assurant ainsi l'isolement vis-à-vis du code ayant généré le certificat.

Résultats
L'article prouve avec succès le Théorème 1 : Pour tous nombres réels positifs $x_1, \dots, x_9$, l'inégalité $\sum_{i=1}^9 \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}} \ge 0$ est vérifiée.

• La preuve résout la première entrée ouverte dans le tableau de statut des inégalités de Vasc (Tableau 1).
• Le cas $n=11$ reste ouvert, seuls des résultats positifs partiels sur un petit cône étant actuellement disponibles.

Signification
L'article affirme sa signification en résolvant un problème ouvert de longue date dans la preuve d'inégalités automatisées, qui était auparavant bloqué par la complexité combinatoire. En démontrant qu'un certificat fini peut être généré et vérifié indépendamment pour un problème nécessitant l'analyse de plus de 40 000 régions, ce travail valide une approche hybride où des agents d'IA gèrent la lourde charge de calcul (division de cas, génération de programmes et vérification) tandis que les auteurs humains auditent les réductions mathématiques et la logique de vérification. Le travail fournit une voie reproductible, incluant le certificat, un vérificateur indépendant et un chemin de reconstruction de la source, établissant un nouveau standard pour l'inégalité de Vasc $n=9$.