Mathématiques formelles · Lean 4 + Mathlib

Un gap de masse vérifié par machine pour la théorie de jauge SU(2) sur réseau en dimension 4, au-delà du seuil publié

Le noyau de Lean vérifie la preuve entière. Le résultat vaut pour un couplage de Wilson β < 1/9, uniformément en le volume du réseau, avec une masse explicite. Le meilleur seuil de la littérature publiée est β < 1/12.

Le théorème

theorem latticeMassGap_su2_d4_ninth (β : ℝ) (hβ : 0 < β) (hβ' : β < 1 / 9) :
    LatticeMassGap 2 4 β (-Real.log (9 * β))

-- 'latticeMassGap_su2_d4_ninth' depends on axioms:
--   [propext, Classical.choice, Quot.sound]

En clair : pour la théorie de jauge de Wilson SU(2) sur un tore périodique quelconque de dimension 4, prenons deux observables continues sur une boîte finie fixée. Si l'on décale l'une de t pas le long d'un axe du réseau, leur corrélation connexe est au plus C·(9β)^t, et la constante C ne dépend pas de la taille du tore. Le théorème n'utilise que les trois axiomes standard de Lean : aucun sorry, aucune hypothèse propre au projet.

Où il se situe

Seuils de gap de masse prouvés pour Yang–Mills sur réseau en dimension 4, en couplage de Wilson β = 4/g² pour SU(2), à l'échelle. Points pleins : résultats publiés ou vérifiés par machine. Points creux : nos preuves sur papier, qui ont passé une relecture adverse interne mais ne sont pas encore formalisées. La région physique (β ≈ 2,3–2,8) se trouve environ dix fois plus à droite que la fin de cet axe.

Ce que contient le corpus

Chaîne de preuve: 36 fichiers · 10,8 k lignes
Bibliothèque entière: 61 fichiers · 15,9 k lignes
Compilation: 3 347 tâches, sans erreur
Version: Lean 4.35.0-rc3

Un argument complet de type Dobrushin pour Yang–Mills sur réseau, entièrement rédigé et formalisé. Shen–Zhu–Zhu (2023) notent que cette approche n'avait pas été menée en détail pour ce modèle.
Une infrastructure absente de Mathlib : la mesure de Wilson sur des tores SU(N), l'invariance de jauge et par translation, la positivité par réflexion, l'identification de SU(2) à S³, les lois conditionnelles comme lois de von Mises–Fisher, et la décroissance des covariances à partir d'une borne d'influence.
Une réduction de toute la chaîne à une seule inégalité de covariance sur une sphère de dimension 3. Chaque amélioration de cette inégalité relève le seuil prouvé.
Un dossier de recherche : revue de littérature vérifiée à la source, rapports de relecture adverse, scripts de falsification numérique et protocole d'audit écrit. Des agents d'IA (Claude) l'ont construit selon ce protocole. Chaque affirmation Lean a été recompilée à la main, et chaque citation vérifiée mot pour mot dans sa source.

Ce qui est proposé

Une licence du corpus Lean, exclusive ou non exclusive. Usages possibles : données d'entraînement et d'évaluation, banc d'essai difficile en mathématiques formelles au niveau de la recherche, base pour d'autres formalisations.
Le dossier de recherche, avec sa méthode de vérification.
Des travaux sous contrat sur les étapes suivantes : formaliser les seuils √3/9 et 2/9 et l'argument par blocs à 0,2413, et passer du gap euclidien au trou spectral de la matrice de transfert.

Sous accord de confidentialité, avant tout accord, nous pouvons communiquer le fichier complet des énoncés et le rapport d'axiomes. Vous pouvez ainsi vérifier exactement ce que couvrirait la licence, sans voir les preuves.

Portée, sans détour

C'est un résultat de couplage fort. Il ne dit rien de la limite continue et ne constitue pas un progrès vers le problème du prix du millénaire de l'Institut Clay.
« Gap de masse » désigne ici la décroissance exponentielle uniforme des corrélations euclidiennes sur des tores périodiques. Le lien avec le trou spectral de la matrice de transfert est standard mais pas encore formalisé. Aucune mesure en volume infini n'est construite. La décroissance est énoncée le long des axes du réseau, avec une constante non explicite.
« Au-delà du seuil publié » concerne le gap de masse, d'après une recherche bibliographique allant jusqu'à octobre 2026. La loi d'aire, une propriété différente, est déjà prouvée jusqu'à β < 1/6 (Cao–Nissim–Sheffield, 2025). Le résultat ne couvre que SU(2).
Un travail voisin existe : le projet mrdouglasny/lgt formalise un gap de masse pour U(n) à β < 1/96 dans cette normalisation. Ce n'est donc pas le premier gap de masse sur réseau en Lean. C'est le premier, à notre connaissance, au-delà du seuil publié.