On the paucity of lattice triangles

1. Contexte et Problématique

Le papier aborde un problème central en géométrie et en dynamique : la classification des triangles rationnels de réseau (lattice triangles).

• Définition : Un triangle rationnel $T$ est un triangle dont les angles intérieurs sont des multiples rationnels de $\pi$. En « dépliant » ce triangle (processus d'unfold), on obtient une surface de translation $(X_T, \omega_T)$.
• Le problème : Classifier les triangles rationnels pour lesquels cette surface de translation est une surface de Veech (ou surface de réseau). Cela signifie que le groupe affine d'automorphismes de la surface est un réseau dans $SL_2(\mathbb{R})$, ce qui implique que l'orbite de la surface sous l'action de $SL_2(\mathbb{R})$ est fermée (projetant sur une courbe de Teichmüller dans l'espace de modules).
• État de l'art : Les cas des triangles acutangles et rectangles sont entièrement résolus. Pour les triangles obtus, deux familles infinies et un exemple sporadique (celui de Hooper) sont connus.
• La conjecture : Il est conjecturé que la liste des triangles obtus de réseau est complète. Le défi majeur réside dans la fenêtre dite « dure » (hard window), où l'angle obtus $\theta$ appartient à l'intervalle $(\pi/2, 2\pi/3]$. Dans cette région, on soupçonne qu'aucun triangle de réseau n'existe, mais une preuve rigoureuse fait défaut.

2. Méthodologie

Les auteurs utilisent une approche combinant la géométrie des surfaces de translation, la théorie des nombres et l'analyse de Fourier.

A. Reformulation Arithmétique (Obstruction de Rang)

Le point de départ est la reformulation de l'obstruction de rang de Mirzakhani-Wright par Larsen, Norton et Zykoski.

• Ils établissent un critère arithmétique effectif : un triangle obtus n'est pas un triangle de réseau s'il existe une unité « utilisable » $a$ (un entier premier avec $n$ tel que $2a \not\equiv 2 \pmod n$) satisfaisant au moins deux des trois inégalités modulaires suivantes pour les angles $(p\pi/n, q\pi/n, r\pi/n)$ :
  $$[ap]_n < [2p]_n, \quad [aq]_n < [2q]_n, \quad [ar]_n < [2r]_n$$
  où $[x]_n$ désigne le reste non négatif de $x$ modulo $n$.

B. Fonction de Comptage et Analyse de Fourier

Pour prouver l'existence d'une telle unité $a$, les auteurs définissent une fonction de comptage $S(p, q)$ qui compte le nombre d'unités $a$ satisfaisant simultanément les deux premières inégalités :
$$S(p, q) = \sum_{a \in U_n} \mathbf{1}_{I_{mp}}(ap) \cdot \mathbf{1}_{I_{mq}}(aq)$$
où $I_m = \{1, \dots, m\}$ et $U_n$ est le système de résidus réduits modulo $n$.
L'objectif est de montrer que $S(p, q) \ge 5$ pour presque tous les couples $(p, q)$, ce qui garantirait l'existence d'une unité « utilisable » (puisque $a=1$ est souvent exclu, il faut plusieurs solutions).

La fonction $S(p, q)$ est décomposée en utilisant l'analyse de Fourier discrète :
$$S(p, q) = M(p, q) + E(p, q)$$

• Terme principal $M(p, q)$ : Proportionnel à $\phi(n)$, il représente la valeur attendue si les résidus étaient uniformément distribués.
• Terme d'erreur $E(p, q)$ : Une somme oscillatoire impliquant des sommes de Ramanujan $c_n(kp + \ell q)$.

C. Rôle des Facteurs Premiers Grands

La clé de la démonstration réside dans l'exploitation de la structure arithmétique de $n$. Les auteurs montrent que si $n$ possède un grand facteur premier $P = P^+(n)$, alors les sommes de Ramanujan s'annulent sur la majorité des fréquences.

• Ils décomposent le terme d'erreur selon la valuation $P$-adique.
• En utilisant des estimations fines sur la masse de Fourier dans les classes résiduelles (Lemme 4.2), ils prouvent que le terme d'erreur $E(p, q)$ devient négligeable par rapport au terme principal, à condition que $P$ soit suffisamment grand (de l'ordre de $n^{1/\log \log n}$).

3. Résultats Principaux

Théorème 1.1 (Rareté Quantitative)

Soit $\Omega^+$ l'ensemble des entiers $n$ dont le plus grand facteur premier $P^+(n)$ est supérieur ou égal à $n^{1/\log \log n}$. Cet ensemble a une densité naturelle égale à 1.
Pour $n \in \Omega^+$, la proportion de couples $(p, q)$ dans la région obtuse $H_n$ correspondant à des triangles de réseau tend vers 0 lorsque $n \to \infty$.
$$\lim_{\substack{n \to +\infty \\ n \in \Omega^+}} \frac{\#L_n}{\#H_n} = 0$$
où $L_n$ est l'ensemble des paires correspondant à des triangles de réseau.

Corollaire 1.2

La proportion de triangles de réseau dans la fenêtre « dure » tend vers 0 le long d'un ensemble de dénominateurs de densité 1. Cela confirme quantitativement l'hypothèse que les triangles de réseau sont extrêmement rares, voire inexistants, dans cette région pour presque tous les cas.

4. Contributions Clés

1. Preuve Quantitative de la Conjecture : Le papier ne prouve pas que aucun triangle n'existe dans la fenêtre dure (ce qui reste une conjecture ouverte), mais il démontre que l'ensemble des contre-exemples potentiels a une densité nulle. C'est une avancée majeure par rapport aux résultats précédents qui ne couvraient que la région « fortement obtuse » ($\theta > 2\pi/3$).
2. Méthodologie Analytique : L'utilisation combinée de l'obstruction de rang, de l'analyse de Fourier sur les groupes cycliques et des propriétés des nombres lisses (smooth numbers) pour contrôler les sommes de Ramanujan.
3. Vérification Formelle par IA :
   • Le moteur principal de la preuve (le Théorème 6.1, une version paramétrée du résultat analytique) a été auto-formalisé et vérifié par un système d'intelligence artificielle nommé AxiomProver dans l'assistant de preuves Lean (avec la bibliothèque mathlib).
   • L'IA a non seulement formalisé la preuve, mais a également corrigé des erreurs mineures présentes dans l'ébauche initiale de l'un des auteurs (Ken Ono).
   • Cela marque une étape significative dans l'utilisation de l'IA pour la vérification rigoureuse de preuves mathématiques complexes en théorie analytique des nombres.

5. Signification et Impact

• Pour la théorie des surfaces de translation : Ce travail renforce considérablement la conjecture selon laquelle la classification des triangles de réseau est presque complète, en éliminant la quasi-totalité des candidats dans la région la plus difficile.
• Pour la théorie des nombres : Il démontre la puissance des méthodes analytiques modernes (sommes de Ramanujan, densité des nombres lisses) pour résoudre des problèmes géométriques dynamiques.
• Pour l'informatique mathématique : La collaboration avec AxiomProver sert de cas d'essai pour l'automatisation de la recherche mathématique. Le fait qu'un système autonome puisse non seulement formaliser mais aussi corriger et vérifier une preuve complexe d'analyse de Fourier et de théorie des nombres ouvre de nouvelles perspectives pour l'assistance à la recherche mathématique.

En résumé, ce papier établit que les triangles de réseau dans la fenêtre obtuse difficile sont d'une rareté extrême (densité nulle), et valide cette conclusion grâce à une preuve rigoureuse assistée et vérifiée par une intelligence artificielle.