Kernel : Python 3 (vérifications exécutables sympy + extraction Steiner) + Lean 4 via WSL (galois_lean, source de vérité formelle — sections 3 et 4)
Les deux énoncés — à ne jamais confondre
Ce notebook démontre à l’écran deux énoncés de nature mathématique très différente :
#
Énoncé
Statut dans ce dépôt
Comment il est établi
1
M₂₃ est un groupe simple d’ordre 10 200 960 : card_M23, simple_M23
PROUVÉ (mécaniquement, sous Lean 4 + Mathlib)
Théorèmes du lake galois_lean exécutés ci-dessous, #print axioms affiché
2
M₂₃ est un groupe de Galois sur ℚ : il existe une extension galoisienne de ℚ de groupe M₂₃
CITÉ (préprint arXiv 2608.08538) — NON formalisé
Polynôme explicite f₁ de degré 23, vérifié computationnellement (irréductibilité, discriminant, factorisations mod p) ; l’identification du groupe de Galois 23T5 = M₂₃ requiert Magma et n’est pas reproduite
La confusion entre ces deux énoncés serait la même que celle entre « ce groupe existe et est simple » et « ce groupe apparaît comme groupe de symétries d’une équation polynomiale à coefficients rationnels ». Le premier est un fait de théorie des groupes finis ; le second est un fait de théorie des nombres algébriques — et il a résisté quarante ans de plus.
1. L’histoire : de Hilbert au 9 août 2026
Le problème inverse de Galois, posé dans l’ère Hilbert (1890s), demande : tout groupe fini est-il le groupe de Galois d’une extension de ℚ ? Hilbert lui-même contribue l’irréductibilité de Hilbert (1892), l’outil qui permet de spécialiser des extensions régulières de ℚ(t) en extensions de ℚ.
Le cas des groupes sporadiques — les 26 exceptions de la classification des groupes simples finis — a concentré la difficulté. Entre 1984 et 1989, une vague de travaux (déclenchée par Thompson pour le Monstre en 1984) réalise 25 des 26 sporadiques comme groupes de Galois sur ℚ, essentiellement par le critère de rigidité : quand une classe de conjugaison triple du groupe est rigide, elle force une extension régulière de ℚ(t) unique.
M₂₃ a été le dernier. Pourquoi lui ? Parce qu’il est non rigide — aucune triple classe rigide ne le capture, et les méthodes de la vague 1984-1989 s’arrêtent à sa porte. Il a fallu attendre le 9 août 2026 : Huang, Jackson, Lee, Poonen, Pries et Zhang (The Mathieu group M₂₃ is a Galois group over ℚ, arXiv:2608.08538) referment le programme en utilisant une triple de classes non rigide et des applications de Belyi calculées numériquement (algorithme de Klug–Musty–Schiavone–Sijsling–Voight). Le programme des sporadiques est complet.
M₂₃ lui-même naît plus tôt : c’est le groupe d’automorphismes du système de Steiner S(4,7,23) — le design de Witt — découvert par Ernst Witt (1938) via la construction de Leech. C’est par ce système combinatoire que la preuve Lean ci-dessous l’attrape.
2. Attributions — qui a prouvé quoi, et sous quelle licence
Ce notebook assemble trois couches de travail, chacune crédité à sa source :
Couche
Auteurs
Référence
Licence
Preuve Lean « M₂₃ simple d’ordre 10 200 960 »
Kenta (KitaKen1)
Dépôt KitaKen1/finite-simple-groups-lean, dernier commit 2026-08-06 — vendored dans galois_lean/Galois/M23Lean4Web.lean (dérivation CoursIA, 2026-08-11, PR #10486)
Apache-2.0 (en-tête préservé verbatim dans le fichier)
Politique d’axiomes du dépôt amont (mesurée à l’import, cf section 3) : aucun sorry, aucun native_decide, aucun axiom déclaré — la preuve repose uniquement sur les axiomes standard de Mathlib (propext, Classical.choice, Quot.sound). L’en-tête amont mentionne une assistance « Claude Code (Fable 5, 1M context) » dans le développement — conservée telle quelle.
import sys, re, timefrom pathlib import Path# Pattern de la serie : utilitaires Lean cross-plateforme (Epic #2314)sys.path.insert(0, str(Path.cwd()))from lean_notebook_utils import ( find_lean_project, get_lean_project_path, run_lake, run_lean_snippet, count_sorry,)GALOIS = find_lean_project('galois_lean') # Path Windows (operations fichier)GALOIS_WSL = get_lean_project_path('galois_lean') # chemin WSL (appels lake/lean)print('Lake galois_lean : .../'+ GALOIS.name +" (chemin tronque, convention serie)")print('Toolchain :', (GALOIS /'lean-toolchain').read_text().strip())vendored = GALOIS /'Galois'/'M23Lean4Web.lean'src = vendored.read_text(encoding='utf-8')# Metrique de position de preuve (cf #10478) : sorry en position de terme compte,# les occurrences dans les commentaires d'en-tete (licence) ne comptent pas.lines = [l.split('--')[0] for l in src.splitlines()] # code sans commentaires lignecode_only =chr(10).join(lines)bs =chr(92) # backslash, pour ecrire les regex sans escape de transportrx_sorry ='(:='+ bs +'s*|by'+ bs +'s+|^'+ bs +'s*)sorry(?![A-Za-z])'n_sorry_term =len(re.findall(rx_sorry, code_only, re.M))n_textual = src.count('sorry')print('M23Lean4Web.lean :', len(src.splitlines()), 'lignes')print(' sorry en position de preuve :', n_sorry_term,' (occurrences textuelles :', n_textual, ", toutes en commentaire d'en-tete)")print(' native_decide :', len(re.findall('native_decide', code_only)), '; axiom declares :', len(re.findall('^axiom [A-Za-z]', code_only, re.M)))print("En-tete licence :", src.splitlines()[1][:75])
Lake galois_lean : .../galois_lean (chemin tronque, convention serie)
Toolchain : leanprover/lean4:v4.33.0
M23Lean4Web.lean : 8115 lignes
sorry en position de preuve : 0 (occurrences textuelles : 2 , toutes en commentaire d'en-tete)
native_decide : 0 ; axiom declares : 0
En-tete licence : Copyright (c) 2026 Kenta. — upstream: https://github.com/KitaKen1/finite-si
Interprétation
Le lake galois_lean (toolchain v4.33.0, Mathlib épinglé) porte la preuve amont vendored : le fichier M23Lean4Web.lean contient toute la couche M₂₂ dont dépend M₂₃, la construction de M₂₃ comme sous-groupe de Perm(23), sa cardinalité et sa simplicité. Le compteur d’import confirme la politique d’axiomes annoncée : aucune preuve trouée, aucune décision déléguée au noyau natif sans preuve.
3. M₂₃ exécuté — le groupe prouvé à l’écran
L’énoncé 1 n’est pas raconté : il est exécuté. La cellule suivante fait trois choses :
lake build sur le lake — la preuve compile sous notre épingle (preuve de buildabilité) ;
#check les deux théorèmes — Lean affiche leurs énoncés complets ;
#print axioms — la liste exhaustive des axiomes sur lesquels repose la preuve. C’est l’audit d’intégrité : tout ce qui n’est pas dans la liste blanche standard (propext, Classical.choice, Quot.sound) viderait le théorème (règle §B du dépôt).
import timet0 = time.time()rc_build, out_build, err_build = run_lake(GALOIS_WSL, 'build', timeout=1200)combined = (out_build or'') + (err_build or'')tail = combined.strip().splitlines()[-4:] if combined.strip() else ['(aucune sortie = deja a jour)']print(f"lake build rc={rc_build}")print('\n'.join(tail))print(f"[lake build en {time.time()-t0:.1f}s]")
lake build rc=0
But this is not relevant for proofs because of proof irrelevance.
Note: This linter can be disabled with `set_option linter.style.haveILetI false`
Build completed successfully (2479 jobs).
[lake build en 38.8s]
snippet ="""import Galois.M23Lean4Web-- Les deux theoremes, enonces par Lean lui-meme#check @Sporadic.card_M23#check @Sporadic.simple_M23-- Audit d'integrite : axiomes exacts de chaque preuve#print axioms Sporadic.card_M23#print axioms Sporadic.simple_M23-- Le systeme de Steiner S(4,7,23) du depot amontopen Sporadic.M23Certificates.SteinerSystem#check @heptadList_length#check @PreservesHeptads#check @PreservesHeptads.one#check @PreservesHeptads.mul"""t0 = time.time()out = run_lean_snippet(GALOIS_WSL, snippet, timeout=900, snippet_id='m23_thms')print(out)print(f"[lean: {time.time()-t0:.1f}s]")
Sporadic.card_M23 : Nat.card M23 = 10200960 — l’ordre du groupe, calculé par une chaîne de stabilisateurs Schreier–Sims matérialisée dans la preuve : c’est du comptage combinatoire déroulé, pas une table consultée.
Sporadic.simple_M23 : IsSimpleGroup M23 — la simplicité. La stratégie amont : exclure tout sous-groupe normal non trivial, y compris un éventuel sous-groupe normal régulier d’ordre 23 par un certificat de conjugaison.
#print axioms ne rend que propext, Classical.choice, Quot.sound — les trois axiomes standard de Mathlib. Pas de sorryAx (qui signalerait un trou), pas d’axiome native_decide (qui signalerait une décision non prouvée). La preuve est close au sens mécanique.
heptadList_length : heptadList.length = 253 — le système de Steiner : les 253 heptades du design de Witt S(4,7,23), et le fait que la liste en contient exactement 253. PreservesHeptads définit le sous-groupe de Perm(23) qui préserve le système — c’est la définition combinatoire de M₂₃ — avec sa structure de groupe (one, mul).
4. Le design de Witt S(4,7,23) — l’objet combinatoire
M₂₃ se définit comme groupe d’automorphismes du système de Steiner S(4,7,23) : 23 points, des blocs de 7 points (les heptades), tels que tout sous-ensemble de 4 points est contenu dans exactement une heptade. L’aridmétrie force le nombre de blocs : C(23,4)/C(7,4) = 8855/35 = 253 — exactement ce que heptadList_length énonce.
Extrayons les 253 heptades du fichier Lean et vérifions la propriété définaire indépendamment (en Python, sans Lean) — deux sources de vérité qui se recoupent.
import itertools# Extraction des heptades depuis la source Lean (notation zero-based {a, b, ..., f, g})blocks_src = re.findall(r'\{(\d+(?:,\s*\d+){6})\}', src)# Les blocs du systeme S(4,7,23) : la deuxieme occurrence du pattern (zone SteinerSystem M23)heptads = [tuple(int(v) for v in b.split(',')) for b in blocks_src]# Deduplication conservant l'ordre (la couche M22 contient des blocs a 7 elements distincts)seen, heptads_uniq =set(), []for h in heptads:if h notin seen: seen.add(h); heptads_uniq.append(h)print(f"Blocs extraits : {len(heptads)} occurrences, {len(heptads_uniq)} distincts")print("Premieres heptades :", heptads_uniq[:3])# Verifications structurelles elementairesassertall(len(h) ==7for h in heptads_uniq), "heptade de taille != 7"assertall(max(h) <=22andmin(h) >=0for h in heptads_uniq), "point hors de {0..22}"n_heptads =len(heptads_uniq)print(f"\n253 attendu (heptadList_length) <-> {n_heptads} extraits : "f"{'CONCORDANT'if n_heptads ==253else'ECART'}")print(f"Arithmetique du design : C(23,4)/C(7,4) = {len(list(itertools.combinations(range(23),4)))}"f"//{len(list(itertools.combinations(range(7),4)))} = "f"{len(list(itertools.combinations(range(23),4)))//len(list(itertools.combinations(range(7),4)))}")
# Propriete definatoire (verification partielle, sous-ensemble des 4-subsets)# La verification COMPLETE (8855 quadruplets) est l'Exercice 2.heptad_sets = [frozenset(h) for h in heptads_uniq]quads =list(itertools.combinations(range(23), 4))import randomrandom.seed(42)sample_quads = random.sample(quads, 200)bad =0for q in sample_quads: qs =frozenset(q) containing =sum(1for H in heptad_sets if qs <= H)if containing !=1: bad +=1print(f" ANOMALIE : {q} contenu dans {containing} heptades")print(f"Echantillon de 200 quadruplets : {200- bad}/200 dans exactement 1 heptade"+ (" -- PROPRIETE S(4,7,23) VERIFIEE SUR L'ECHANTILLON"if bad ==0else" -- DEFAUT"))
Echantillon de 200 quadruplets : 200/200 dans exactement 1 heptade -- PROPRIETE S(4,7,23) VERIFIEE SUR L'ECHANTILLON
Interprétation
L’extraction rend 253 heptades distinctes, chacune de taille 7 sur les points {0..22} — concordant avec heptadList_length prouvé en Lean.
Sur un échantillon aléatoire de 200 quadruplets, chacun est contenu dans exactement une heptade : le comportement S(4,7,23). La vérification exhaustive (8 855 quadruplets) est l’Exercice 2 — la propriété est faite pour être re-vérifiée par l’étudiant, pas crue.
Le pont conceptuel : le groupe des permutations de {0..22} préservant l’ensemble des 253 heptades est M₂₃. PreservesHeptads (Lean) en est la définition formelle exacte ; blockMap en est l’action sur les blocs. La théorie des groupes finis rencontre la combinatoire des designs : c’est par ce chemin que Witt a construit M₂₃ en 1938, bien avant l’ordinateur.
5. La réalisation galoisienne — citée, pas formalisée
L’énoncé 2 (M₂₃ groupe de Galois sur ℚ) repose sur une chaîne théorique que ce dépôt ne formalise pas. Elle est citée ici pour être honnête sur la frontière entre prouvé et rapporté :
Application de Belyi et triple non rigide. Le préprint part d’une extension galoisienne régulière de ℚ(t) avec groupe M₂₃, construite par une triple de classes de conjugaison non rigide — c’est précisément ce qui a bloqué M₂₃ pendant 40 ans : la rigidité, l’outil de la vague 1984-1989, ne s’applique pas.
Existence de Riemann (forme revêtements finis étales ↔︎ quotients finis de π₁) : le pont topologie ↔︎ arithmétique qui transporte la monodromie en groupe de Galois.
Corps des modules ℚ et descente du revêtement (références [CH85] et [DD97] du préprint) : prouver que l’extension descend de ℚ̄(t) à ℚ(t).
Spécialisation (irréductibilité de Hilbert) : de ℚ(t) vers le ℚ du polynôme f₁.
Le dépôt porte déjà le socle géométrique de cette chaîne dans grothendieck_lean : sites, faisceaux, cohomologie — mais pas le π₁ étale ni l’existence de Riemann. La phrase qui doit rester noir sur blanc : « M₂₃ est un groupe de Galois sur ℚ » n’est PAS formalisé dans ce dépôt — il est prouvé dans le préprint, et vérifié computationnellement ci-dessous au niveau du polynôme, pas au niveau du groupe de Galois.
# Le socle grothendieckien du depot : ce qui existe deja cote formel# (modules reels : la convention i18n #4980 adjoint un sibling _en a chaque# module - exclu du denombrement pour que le compte reste celui des modules)gro = find_lean_project('grothendieck_lean')gro_modules =sorted(p.stem for p in (Path(gro) /'Grothendieck').rglob('*.lean') ifnot p.stem.endswith('_en'))print(f"grothendieck_lean : {len(gro_modules)} modules reels (siblings i18n _en exclus) sous Grothendieck/")for m in gro_modules[:14]:print(" -", m)print(" ..."iflen(gro_modules) >14else"")print("\nChainon MANQUANT pour l'enonce 2 : pi1 etale / existence de Riemann -> non formalise")
grothendieck_lean : 78 modules reels (siblings i18n _en exclus) sous Grothendieck/
- Adjunction
- Basic
- Calibration
- CanonicalProps
- CategoryAndSites
- Cech
- Classifier
- Comma
- Conservative
- ConstantSheaf
- Construction
- Cover
- CoverageGen
- CoversArrow
...
Chainon MANQUANT pour l'enonce 2 : pi1 etale / existence de Riemann -> non formalise
6. Le polynôme f₁ — manipulé pour de vrai
Le préprint produit un polynôme explicite de degré 23 à coefficients entiers dont le corps de décomposition sur ℚ a pour groupe de Galois M₂₃. Le dépôt compagnon shaowuz/m23isgalois le publie au format PARI/GP (polynomial_f1.gp), avec un auto-contrôle : une empreinte à six champs calculable indépendamment. Le fichier dit, pour f1 : degré 23, 23 monômes, 219 chiffres de coefficients au total, 14 chiffres pour le plus grand, contenu 1, et f1(3) mod (2^61−1) = 92254275456192.
Nous chargeons les coefficients ci-dessous et recalculons l’empreinte de toutes pièces. C’est la vérification d’intégrité de la transcription : une seule erreur de chiffre casse l’empreinte.
# Coefficients de f1, transcrits de polynomial_f1.gp (shaowuz/m23isgalois)# coeff_f1[i] = coefficient de x^i ; l'entree x^22 est absente du fichier (coefficient 0)coeff_f1 = [-3150159884154, 19169943578802, -46185312415788, 53599151839311,-28142323927002, 1949980486716, 3961650395556, -1023887308293,-194398310718, 35123826654, 3700476348, 10550424369,290615166, -1333395744, -42732528, 67672923,1545462, -1808490, 18400, 26151,-1150, -184, 0, 1,]import mathnz = [abs(c) for c in coeff_f1 if c !=0]digits = [len(str(a)) for a in nz]content =0for c in coeff_f1: content = math.gcd(content, c)M61 =2**61-1f1_at_3 =sum(c *pow(3, i, M61) for i, c inenumerate(coeff_f1)) % M61fingerprint = [23, len(nz), sum(digits), max(digits), content, f1_at_3]expected = [23, 23, 219, 14, 1, 92254275456192] # f1_expect de polynomial_f1.gpprint("empreinte calculee :", fingerprint)print("empreinte attendue :", expected)print("TRANSCRIPTION INTEGRE"if fingerprint == expected else"ECART -- retranscrire !")
from sympy import Poly, symbols, factor_list, discriminant, GFx = symbols('x')f1 =sum(c * x**i for i, c inenumerate(coeff_f1))poly = Poly(f1, x)# 1. Degreprint(f"degre de f1 : {poly.degree()}")# 2. Irreductibilite sur Q (factorisation complete -- 1 facteur = irreductible)fl = factor_list(f1)n_factors =len(fl[1])print(f"factorisation sur Q : {n_factors} facteur(s) -> "f"{'IRREDUCTIBLE'if n_factors ==1and fl[1][0][1] ==1else'REDUCTIBLE'}")# 3. Discriminant (383 chiffres, signe +) : 23 racines distinctesdisc = discriminant(f1, x)print(f"discriminant : {len(str(abs(disc)))} chiffres, signe {'+'if disc >0else'-'}")print(f" (non nul -> f1 separable : 23 racines complexes distinctes)")
degre de f1 : 23
factorisation sur Q : 1 facteur(s) -> IRREDUCTIBLE
discriminant : 383 chiffres, signe +
(non nul -> f1 separable : 23 racines complexes distinctes)
# 4. Factorisations modulo quelques premiers -- les cycles de Frobenius# factor_list(modulus=...) declenche en interne (sympy >= 1.13) une comparaison# d'entiers modulaires depreciee ; le warning associe imprime le chemin# site-packages de la machine d'execution. On le filtre : la comparaison vit# dans sympy, pas dans ce notebook.import warningsfrom sympy.utilities.exceptions import SymPyDeprecationWarningwarnings.filterwarnings("ignore", category=SymPyDeprecationWarning)print(f"{'p':>4} | degres des facteurs (deg x mult) | somme")print("-"*52)for p in (2, 3, 5, 7, 11): flp = factor_list(f1, modulus=p) degs =sorted(int(Poly(g, x, domain=GF(p)).degree()) *int(m) for g, m in flp[1])print(f"{p:>4} | {str(degs):<28} | {sum(degs)}")
Irréductible sur ℚ : f₁ n’a aucun facteur rationnel — le corps ℚ(α) engendré par une racine est de degré 23, et le groupe de Galois (du corps de décomposition) agit transitivement sur les 23 racines. C’est la signature d’un groupe transitif de degré 23.
Discriminant ≠ 0 (383 chiffres, positif) : f₁ est séparable — 23 racines distinctes, pas de ramification résiduelle. Le préprint démontre plus fort : le corps de décomposition n’est ramifié qu’en {2, 3, 23}.
Factorisation mod p : les degrés des facteurs modulo p donnent la décomposition des cycles d’un élément de Frobenius — une fenêtre sur la structure du groupe de Galois. Les motifs observés (ex. 11+11+1 mod 5, ou 8+8+4+2+1 mod 7) sont cohérents avec des substitutions paires à point fixe — le comportement attendu d’un sous-groupe de A₂₃ comme M₂₃.
Ce que ces vérifications NE démontrent PAS : l’identification du groupe de Galois à M₂₃ (transitive group 23T5). Elle requiert Magma (verify.m du dépôt compagnon, GaloisGroup + GaloisProof certifiant) et n’est pas reproduite ici. Notre chaîne sympy établit : degré 23 ✓, irréductible ✓, séparable ✓, Frobenius pairs ✓ — le socle computationnel, pas le théorème.
7. Exercices
# EXERCICE 1 : l'arithmetique de l'ordre de M23.# Objectif : verifier la decomposition multiplicative 10200960 = 253 * 40320# et la factorisation premiere |M23| = 2^7 * 3^2 * 5 * 7 * 11 * 23, puis expliquer# pourquoi 253 et 40320 apparaissent chacun naturellement dans le design de Witt.# Indice : 253 = nombre d'heptades (section 4) ; 40320 = 8! -- chaque point fixe une# structure de "octade + coordonnees" heritee de M24 ; le stabilisateur dans M23# d'un point est M22, d'ordre |M23|/23.# Etape 1 : verifier l'egalite 253 * 40320 == 10200960 (contre Sporadic.card_M23)# Etape 2 : calculer la factorisation premiere de 10200960 et la comparer a 2^7*3^2*5*7*11*23# Etape 3 : verifier |M23| / 23 == 443520 et chercher a quoi correspond ce nombre pour M22result =None# TODO etudiantprint("Exercice 1 a completer : arithmetique de |M23|")
Exercice 1 a completer : arithmetique de |M23|
# EXERCICE 2 : la propriete definatoire S(4,7,23) -- verification EXHAUSTIVE.# Objectif : verifier que CHACUN des C(23,4) = 8855 quadruplets de points est contenu# dans exactement une heptade (la section 4 ne l'a fait que sur un echantillon de 200).# Indice : construire un index heptade -> frozenset, puis pour chaque quadruplet# compter les heptades le contenant ; assert count == 1 pour TOUS.# Etape 1 : generer les 8855 quadruplets avec itertools.combinations(range(23), 4)# Etape 2 : pour chaque quadruplet q, compter sum(1 for H in heptad_sets if set(q) <= H)# Etape 3 : assert sur la totalite, et afficher le compte de quadruplets verifiesresult =None# TODO etudiantprint("Exercice 2 a completer : verification exhaustive S(4,7,23)")
Exercice 2 a completer : verification exhaustive S(4,7,23)
# EXERCICE 3 : le second polynome f2 du depot compagnon.# Objectif : recuperer polynomial_f2.gp depuis https://github.com/shaowuz/m23isgalois,# transcrire les coefficients de f2, puis reproduire sur f2 les memes verifications# que la section 6 (empreinte, degre, irreductibilite sur Q, discriminant, factorisation# mod 2, 3, 5). Le preprint precise : f2 est de hauteur plus petite, a ramification# dans {2, 7, 23} (contre {2, 3, 23} pour f1).# Indice : le fichier .gp de f2 embarque sa propre ligne f2_expect -- l'utiliser comme# oracle d'empreinte, comme f1_expect en section 6.# Etape 1 : transcrire coeff_f2 depuis polynomial_f2.gp# Etape 2 : recalculer l'empreinte et la comparer a f2_expect# Etape 3 : degre / irreductibilite / discriminant / factorisation mod p, meme formatresult =None# TODO etudiantprint("Exercice 3 a completer : empreinte et verifications de f2")
Exercice 3 a completer : empreinte et verifications de f2
Annexe A — La complétion adique : approcher un anneau local par ses troncatures
Le problème inverse de Galois vit dans les extensions locales : pour comprendre un groupe de Galois global, on le regarde une prime à la fois, dans la complétion. Le module Galois.AdicCompletionLocalRing (portage pédagogique du dépôt anthropics/fermats-last-theorem, commit aa2d8b34, Apache-2.0) pose la première couche de cette arithmétique locale : la complétion adique d’un anneau local A par son idéal maximal.
L’idée tient en une image. Un anneau local A d’idéal I est un monde qu’on ne voit jamais en entier — on n’en observe que des troncatures : le quotient A ⧸ I^n, « A vu modulo la puissance n-ième de l’idéal ». La complétion adique AdicCompletion I A est l’objet qui est compatible avec toutes les troncatures à la fois : un élément de la complétion, c’est une famille cohérente de classes modulo I^n pour chaque n. L’évaluation evalₐ I n projette la complétion sur sa troncature de degré n.
Le module établit quatre briques : Kernel (le noyau de evalₐ I n est exactement l’image de I^n — la caractérisation « noyau d’évaluation = puissance de l’idéal »), Exemple (la troncature 2-adique de ℤ), Local (pour A local noethérien, l’idéal maximal de la complétion est le noyau de l’évaluation en degré 1, et les quotients par ses puissances s’identifient à ceux de A), Transport (ces identités survivent aux isomorphismes de complétions).
snippet_adic ="""import Galois.AdicCompletionLocalRing-- Kernel : troncature, noyau, unites (6 declarations)#check @AdicCompletion.evalₐ_algebraMap#check @AdicCompletion.mem_ker_evalₐ_iff#check @AdicCompletion.ker_evalₐ_eq_map_pow#check @AdicCompletion.exists_eq_algebraMap_add#check @AdicCompletion.isUnit_one_add_of_mem_map#check @AdicCompletion.isUnit_add_of_mem_map-- Local : l'ideal maximal de la completion (7 declarations)#check @AdicCompletion.isUnit_of_isUnit_algebraMap#check @AdicCompletion.isUnit_one_add_of_mem_map_maximalIdeal#check @AdicCompletion.maximalIdeal_fg#check @AdicCompletion.instIsLocalRingMaximalIdeal#check @AdicCompletion.maximalIdeal_pow_eq_ker_evalₐ#check @AdicCompletion.maximalIdeal_eq_ker_evalₐ_one#check @AdicCompletion.mem_maximalIdeal_iff-- Scalars : les quotients de la completion s'identifient a ceux de A (6)#check @AdicCompletion.quotientMaximalIdealPowAlgHom#check @AdicCompletion.quotientMaximalIdealPowAlgHom_mk#check @AdicCompletion.quotientMaximalIdealPowAlgHom_bijective#check @AdicCompletion.quotientMaximalIdealPowAlgEquiv#check @AdicCompletion.quotientMaximalIdealPowAlgEquiv_mk#check @AdicCompletion.quotientMaximalIdealPowAlgEquiv_mk_algebraMap-- Transport : tout survit aux isomorphismes de completions (8)#check @AdicCompletion.isUnit_algEquiv_iff#check @AdicCompletion.comap_maximalIdeal_algEquiv#check @AdicCompletion.map_maximalIdeal_algEquiv#check @AdicCompletion.maximalIdeal_eq_map_algEquiv#check @AdicCompletion.maximalIdeal_pow_eq_map_algEquiv#check @AdicCompletion.algEquiv_algebraMap_mem_maximalIdeal#check @AdicCompletion.quotientMaximalIdealPowAlgEquivOfAlgEquiv#check @AdicCompletion.quotientMaximalIdealPowAlgEquivOfAlgEquiv_mk-- Audit d'integrite : axiomes exacts de trois preuves representatives#print axioms AdicCompletion.ker_evalₐ_eq_map_pow#print axioms AdicCompletion.quotientMaximalIdealPowAlgEquiv_mk#print axioms AdicCompletion.isUnit_algEquiv_iff"""t0 = time.time()out = run_lean_snippet(GALOIS_WSL, snippet_adic, timeout=900, snippet_id='adic_thms')print(out)print(f"[lean: {time.time()-t0:.1f}s]")
@AdicCompletion.evalₐ_algebraMap : ∀ {A : Type u_1} [inst : CommRing A] (I : Ideal A) (n : ℕ) (a : A),
(AdicCompletion.evalₐ I n) ((algebraMap A (AdicCompletion I A)) a) = (Ideal.Quotient.mk (I ^ n)) a
@AdicCompletion.mem_ker_evalₐ_iff : ∀ {A : Type u_1} [inst : CommRing A] (I : Ideal A) (n : ℕ) (x : AdicCompletion I A),
x ∈ RingHom.ker (AdicCompletion.evalₐ I n) ↔ x ∈ (AdicCompletion.eval I A n).ker
@AdicCompletion.ker_evalₐ_eq_map_pow : ∀ {A : Type u_1} [inst : CommRing A] (I : Ideal A),
I.FG → ∀ (n : ℕ), RingHom.ker (AdicCompletion.evalₐ I n) = Ideal.map (algebraMap A (AdicCompletion I A)) (I ^ n)
@AdicCompletion.exists_eq_algebraMap_add : ∀ {A : Type u_1} [inst : CommRing A] (I : Ideal A),
I.FG →
∀ (n : ℕ) (x : AdicCompletion I A),
∃ a, ∃ y ∈ Ideal.map (algebraMap A (AdicCompletion I A)) (I ^ n), x = (algebraMap A (AdicCompletion I A)) a + y
@AdicCompletion.isUnit_one_add_of_mem_map : ∀ {A : Type u_1} [inst : CommRing A] (I : Ideal A),
I.FG → ∀ {x : AdicCompletion I A}, x ∈ Ideal.map (algebraMap A (AdicCompletion I A)) I → IsUnit (1 + x)
@AdicCompletion.isUnit_add_of_mem_map : ∀ {A : Type u_1} [inst : CommRing A] (I : Ideal A),
I.FG → ∀ {u x : AdicCompletion I A}, IsUnit u → x ∈ Ideal.map (algebraMap A (AdicCompletion I A)) I → IsUnit (u + x)
@AdicCompletion.isUnit_of_isUnit_algebraMap : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {a : A},
IsUnit ((algebraMap A (AdicCompletion (IsLocalRing.maximalIdeal A) A)) a) → IsUnit a
@AdicCompletion.isUnit_one_add_of_mem_map_maximalIdeal : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A],
(IsLocalRing.maximalIdeal A).FG →
∀ {x : AdicCompletion (IsLocalRing.maximalIdeal A) A},
x ∈ Ideal.map (algebraMap A (AdicCompletion (IsLocalRing.maximalIdeal A) A)) (IsLocalRing.maximalIdeal A) →
IsUnit (1 + x)
@AdicCompletion.maximalIdeal_fg : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [IsNoetherianRing A],
(IsLocalRing.maximalIdeal A).FG
@AdicCompletion.instIsLocalRingMaximalIdeal : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[IsNoetherianRing A], IsLocalRing (AdicCompletion (IsLocalRing.maximalIdeal A) A)
@AdicCompletion.maximalIdeal_pow_eq_ker_evalₐ : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[inst_2 : IsNoetherianRing A] (n : ℕ),
IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal A) A) ^ n =
RingHom.ker (AdicCompletion.evalₐ (IsLocalRing.maximalIdeal A) n)
@AdicCompletion.maximalIdeal_eq_ker_evalₐ_one : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[inst_2 : IsNoetherianRing A],
IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal A) A) =
RingHom.ker (AdicCompletion.evalₐ (IsLocalRing.maximalIdeal A) 1)
@AdicCompletion.mem_maximalIdeal_iff : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[inst_2 : IsNoetherianRing A] (x : AdicCompletion (IsLocalRing.maximalIdeal A) A),
x ∈ IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal A) A) ↔
(AdicCompletion.evalₐ (IsLocalRing.maximalIdeal A) 1) x = 0
@AdicCompletion.quotientMaximalIdealPowAlgHom : {A : Type u_1} →
[inst : CommRing A] →
[inst_1 : IsLocalRing A] →
[inst_2 : IsNoetherianRing A] →
(k : Type u_2) →
[inst_3 : CommRing k] →
[inst_4 : Algebra k A] →
(n : ℕ) →
AdicCompletion (IsLocalRing.maximalIdeal A) A ⧸
IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal A) A) ^ n →ₐ[k]
A ⧸ IsLocalRing.maximalIdeal A ^ n
@AdicCompletion.quotientMaximalIdealPowAlgHom_mk : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[inst_2 : IsNoetherianRing A] (k : Type u_2) [inst_3 : CommRing k] [inst_4 : Algebra k A] (n : ℕ)
(x : AdicCompletion (IsLocalRing.maximalIdeal A) A),
(AdicCompletion.quotientMaximalIdealPowAlgHom k n)
((Ideal.Quotient.mk (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal A) A) ^ n)) x) =
(AdicCompletion.evalₐ (IsLocalRing.maximalIdeal A) n) x
@AdicCompletion.quotientMaximalIdealPowAlgHom_bijective : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[inst_2 : IsNoetherianRing A] (k : Type u_2) [inst_3 : CommRing k] [inst_4 : Algebra k A] (n : ℕ),
Function.Bijective ⇑(AdicCompletion.quotientMaximalIdealPowAlgHom k n)
@AdicCompletion.quotientMaximalIdealPowAlgEquiv : {A : Type u_1} →
[inst : CommRing A] →
[inst_1 : IsLocalRing A] →
[inst_2 : IsNoetherianRing A] →
(k : Type u_2) →
[inst_3 : CommRing k] →
[inst_4 : Algebra k A] →
(n : ℕ) →
(AdicCompletion (IsLocalRing.maximalIdeal A) A ⧸
IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal A) A) ^ n) ≃ₐ[k]
A ⧸ IsLocalRing.maximalIdeal A ^ n
@AdicCompletion.quotientMaximalIdealPowAlgEquiv_mk : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[inst_2 : IsNoetherianRing A] (k : Type u_2) [inst_3 : CommRing k] [inst_4 : Algebra k A] (n : ℕ)
(x : AdicCompletion (IsLocalRing.maximalIdeal A) A),
(AdicCompletion.quotientMaximalIdealPowAlgEquiv k n)
((Ideal.Quotient.mk (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal A) A) ^ n)) x) =
(AdicCompletion.evalₐ (IsLocalRing.maximalIdeal A) n) x
@AdicCompletion.quotientMaximalIdealPowAlgEquiv_mk_algebraMap : ∀ {A : Type u_1} [inst : CommRing A]
[inst_1 : IsLocalRing A] [inst_2 : IsNoetherianRing A] (k : Type u_2) [inst_3 : CommRing k] [inst_4 : Algebra k A]
(n : ℕ) (a : A),
(AdicCompletion.quotientMaximalIdealPowAlgEquiv k n)
((Ideal.Quotient.mk (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal A) A) ^ n))
((algebraMap A (AdicCompletion (IsLocalRing.maximalIdeal A) A)) a)) =
(Ideal.Quotient.mk (IsLocalRing.maximalIdeal A ^ n)) a
@AdicCompletion.isUnit_algEquiv_iff : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {k : Type u_2}
[inst_2 : CommRing k] [inst_3 : Algebra k A] {B : Type u_3} [inst_4 : CommRing B] [inst_5 : Algebra k B]
(Φ : AdicCompletion (IsLocalRing.maximalIdeal A) A ≃ₐ[k] B) (x : AdicCompletion (IsLocalRing.maximalIdeal A) A),
IsUnit (Φ x) ↔ IsUnit x
@AdicCompletion.comap_maximalIdeal_algEquiv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[inst_2 : IsNoetherianRing A] {k : Type u_2} [inst_3 : CommRing k] [inst_4 : Algebra k A] {B : Type u_3}
[inst_5 : CommRing B] [inst_6 : IsLocalRing B] [inst_7 : Algebra k B]
(Φ : AdicCompletion (IsLocalRing.maximalIdeal A) A ≃ₐ[k] B),
Ideal.comap (↑Φ) (IsLocalRing.maximalIdeal B) =
IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal A) A)
@AdicCompletion.map_maximalIdeal_algEquiv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[inst_2 : IsNoetherianRing A] {k : Type u_2} [inst_3 : CommRing k] [inst_4 : Algebra k A] {B : Type u_3}
[inst_5 : CommRing B] [inst_6 : IsLocalRing B] [inst_7 : Algebra k B]
(Φ : AdicCompletion (IsLocalRing.maximalIdeal A) A ≃ₐ[k] B),
Ideal.map (↑Φ) (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal A) A)) = IsLocalRing.maximalIdeal B
@AdicCompletion.maximalIdeal_eq_map_algEquiv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[IsNoetherianRing A] {k : Type u_2} [inst_3 : CommRing k] [inst_4 : Algebra k A] {B : Type u_3} [inst_5 : CommRing B]
[inst_6 : IsLocalRing B] [inst_7 : Algebra k B] (Φ : AdicCompletion (IsLocalRing.maximalIdeal A) A ≃ₐ[k] B),
IsLocalRing.maximalIdeal B =
Ideal.map ((↑Φ).comp (algebraMap A (AdicCompletion (IsLocalRing.maximalIdeal A) A))) (IsLocalRing.maximalIdeal A)
@AdicCompletion.maximalIdeal_pow_eq_map_algEquiv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[IsNoetherianRing A] {k : Type u_2} [inst_3 : CommRing k] [inst_4 : Algebra k A] {B : Type u_3} [inst_5 : CommRing B]
[inst_6 : IsLocalRing B] [inst_7 : Algebra k B] (Φ : AdicCompletion (IsLocalRing.maximalIdeal A) A ≃ₐ[k] B) (n : ℕ),
IsLocalRing.maximalIdeal B ^ n =
Ideal.map ((↑Φ).comp (algebraMap A (AdicCompletion (IsLocalRing.maximalIdeal A) A)))
(IsLocalRing.maximalIdeal A ^ n)
@AdicCompletion.algEquiv_algebraMap_mem_maximalIdeal : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A]
[IsNoetherianRing A] {k : Type u_2} [inst_3 : CommRing k] [inst_4 : Algebra k A] {B : Type u_3} [inst_5 : CommRing B]
[inst_6 : IsLocalRing B] [inst_7 : Algebra k B] (Φ : AdicCompletion (IsLocalRing.maximalIdeal A) A ≃ₐ[k] B) {a : A},
a ∈ IsLocalRing.maximalIdeal A →
Φ ((algebraMap A (AdicCompletion (IsLocalRing.maximalIdeal A) A)) a) ∈ IsLocalRing.maximalIdeal B
@AdicCompletion.quotientMaximalIdealPowAlgEquivOfAlgEquiv : {A : Type u_1} →
[inst : CommRing A] →
[inst_1 : IsLocalRing A] →
[IsNoetherianRing A] →
{k : Type u_2} →
[inst_3 : CommRing k] →
[inst_4 : Algebra k A] →
{B : Type u_3} →
[inst_5 : CommRing B] →
[inst_6 : IsLocalRing B] →
[inst_7 : Algebra k B] →
(AdicCompletion (IsLocalRing.maximalIdeal A) A ≃ₐ[k] B) →
(n : ℕ) → (B ⧸ IsLocalRing.maximalIdeal B ^ n) ≃ₐ[k] A ⧸ IsLocalRing.maximalIdeal A ^ n
@AdicCompletion.quotientMaximalIdealPowAlgEquivOfAlgEquiv_mk : ∀ {A : Type u_1} [inst : CommRing A]
[inst_1 : IsLocalRing A] [inst_2 : IsNoetherianRing A] {k : Type u_2} [inst_3 : CommRing k] [inst_4 : Algebra k A]
{B : Type u_3} [inst_5 : CommRing B] [inst_6 : IsLocalRing B] [inst_7 : Algebra k B]
(Φ : AdicCompletion (IsLocalRing.maximalIdeal A) A ≃ₐ[k] B) (n : ℕ) (a : A),
(AdicCompletion.quotientMaximalIdealPowAlgEquivOfAlgEquiv Φ n)
((Ideal.Quotient.mk (IsLocalRing.maximalIdeal B ^ n))
(Φ ((algebraMap A (AdicCompletion (IsLocalRing.maximalIdeal A) A)) a))) =
(Ideal.Quotient.mk (IsLocalRing.maximalIdeal A ^ n)) a
'AdicCompletion.ker_evalₐ_eq_map_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'AdicCompletion.quotientMaximalIdealPowAlgEquiv_mk' depends on axioms: [propext, Classical.choice, Quot.sound]
'AdicCompletion.isUnit_algEquiv_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
[lean: 121.4s]
# La troncature 2-adique de Z, jouee en Python : eval_3(20) = classe de 4 dans Z/8# (l'example de la section Exemple du module, rejouee hors Lean)print("eval_3(20) =", 20%8, " (classe de 4 dans Z/2^3 = Z/8, comme dans le module)")print("eval_3(8) =", 8%8, " (8 est multiple de 2^3 : image de I^3, dans le noyau)")# La completion vue comme limite projective : l'inverse de 3 dans Z/2^n# se STABILISE chiffre binaire apres chiffre binaire quand n croit.print("\nL'inverse de 3 modulo 2^n, pour n croissant :")prev =Nonefor n in [3, 5, 8, 12]: inv =pow(3, -1, 2**n) agree =""if prev isnotNoneand inv % (2** (n //2if n //2>=3else3)) == prev % (2** (n //2if n //2>=3else3)): agree =f" <- garde les chiffres de n={prev_n}"print(f" n={n:2d} : 3^-1 = {inv:5d} = {inv:0{n}b}b{agree}") prev, prev_n = inv, nprint("\nChaque troncature ETEND la precedente en poids faibles : la suite est")print("coherente pour le systeme projectif Z/2^n -> Z/2^{n-1}. La complétion Z_2")print("est exactement la limite de ce systeme -- c'est elle que le module formalise.")
eval_3(20) = 4 (classe de 4 dans Z/2^3 = Z/8, comme dans le module)
eval_3(8) = 0 (8 est multiple de 2^3 : image de I^3, dans le noyau)
L'inverse de 3 modulo 2^n, pour n croissant :
n= 3 : 3^-1 = 3 = 011b
n= 5 : 3^-1 = 11 = 01011b <- garde les chiffres de n=3
n= 8 : 3^-1 = 171 = 10101011b <- garde les chiffres de n=5
n=12 : 3^-1 = 2731 = 101010101011b <- garde les chiffres de n=8
Chaque troncature ETEND la precedente en poids faibles : la suite est
coherente pour le systeme projectif Z/2^n -> Z/2^{n-1}. La complétion Z_2
est exactement la limite de ce systeme -- c'est elle que le module formalise.
Interprétation
Les #check rendent les signatures vivantes : ker_evalₐ_eq_map_pow dit que le noyau de la troncature de degré n est l’image de I^n — la phrase « noyau d’évaluation = puissance de l’idéal » devient un énoncé Lean imprimé par Lean. Les trois #print axioms ne listent que propext, Classical.choice, Quot.sound : aucun sorry, aucune tricherie — la couche est close.
La démo Python porte le même contenu dans ℤ : evalₐ (2) 3 envoie 20 sur sa classe mod 8, l’inverse de 3 se stabilise chiffre après chiffre. C’est le pont entre le formalisme (une limite de systèmes projectifs) et le geste de tous les jours en calcul modulaire. Et isUnit_one_add_of_mem_map_maximalIdeal est le germe de Hensel : dans un anneau local, tout 1 + x avec x dans l’idéal maximal de la complétion est inversible — la lemme qui fait converger Newton p-adiquement, et qui rend possible la suite de la théorie locale.
Annexe B — Groupes de ramification inférieure : la tour qui mesure l’inertie
Quand un groupe G agit sur un anneau local R, tout ne se passe pas « près du point » au même degré. Le module Galois.LowerRamificationGroup (même provenance : portage anthropics/fermats-last-theorem, Apache-2.0) construit l’objet qui gradue cette action : les groupes de ramification inférieure de Serre (Local Fields, ch. IV).
Trois étages s’emboîtent :
Décomposition — les éléments de G qui laissent l’idéal maximal stable ;
InertieI.inertia G — ceux qui agissent trivialement sur le corps résiduel : chaque élément est envoyé sur un congru modulo l’idéal maximal. Le module prouve sa monotonie (Ideal.inertia_mono), son cas trivial (inertia_top) et sa normalité dès que l’idéal est stable (inertia_normal_of_forall_smul_eq) ;
Ramification inférieure — la tour lowerRamificationGroup R G i : les σ ∈ G qui fixent Rmodulo 𝔪^(i+1). On obtient G ⊇ LRG(0) ⊇ LRG(1) ⊇ ⋯, antitone (lowerRamificationGroup_antitone), dont le niveau 0 est exactement l’inertie (lowerRamificationGroup_zero_eq_inertia) et dont l’intersection est triviale (iInf_lowerRamificationGroup_eq_bot).
Le lien avec l’annexe A est structurel : la tour LRG(i) est définie par l’action sur les niveaux de la tour de troncatures que la complétion adique construit. LRG(i) = les automorphismes invisibles au degré i de résolution.
snippet_ram ="""import Galois.LowerRamificationGroup-- Inertie : monotonie, cas trivial, normalite (6 declarations)#check @AddSubgroup.inertia_mono#check @Ideal.inertia_mono#check @Ideal.inertia_top#check @Ideal.inertia_normal_of_forall_smul_eq#check @IsLocalRing.pointwise_smul_maximalIdeal#check @IsLocalRing.pointwise_smul_maximalIdeal_pow-- La tour des groupes de ramification inferieure (9)#check @IsLocalRing.lowerRamificationGroup#check @IsLocalRing.mem_lowerRamificationGroup#check @IsLocalRing.lowerRamificationGroup_antitone#check @IsLocalRing.lowerRamificationGroup_normal#check @IsLocalRing.lowerRamificationGroup_zero_eq_ker#check @IsLocalRing.lowerRamificationGroup_zero_eq_inertia#check @IsLocalRing.lowerRamificationGroup_le_zero#check @IsLocalRing.iInf_lowerRamificationGroup_le_ker_toRingAut#check @IsLocalRing.iInf_lowerRamificationGroup_eq_bot-- Cas d'un anneau de valuation (6)#check @ValuationSubring.lowerRamificationGroup#check @ValuationSubring.mem_lowerRamificationGroup#check @ValuationSubring.lowerRamificationGroup_antitone#check @ValuationSubring.lowerRamificationGroup_normal#check @ValuationSubring.lowerRamificationGroup_zero#check @ValuationSubring.lowerRamificationGroup_le_inertiaSubgroup-- Audit d'integrite : axiomes exacts de trois preuves representatives#print axioms IsLocalRing.lowerRamificationGroup_antitone#print axioms IsLocalRing.lowerRamificationGroup_zero_eq_ker#print axioms IsLocalRing.iInf_lowerRamificationGroup_eq_bot"""t0 = time.time()out = run_lean_snippet(GALOIS_WSL, snippet_ram, timeout=900, snippet_id='ramif_thms')print(out)print(f"[lean: {time.time()-t0:.1f}s]")
@AddSubgroup.inertia_mono : ∀ {M : Type u_1} [inst : AddGroup M] {G : Type u_2} [inst_1 : Group G]
[inst_2 : MulAction G M] {I J : AddSubgroup M}, I ≤ J → I.inertia G ≤ J.inertia G
@Ideal.inertia_mono : ∀ {R : Type u_1} [inst : CommRing R] {G : Type u_2} [inst_1 : Group G]
[inst_2 : MulSemiringAction G R] {I J : Ideal R}, I ≤ J → Ideal.inertia G I ≤ Ideal.inertia G J
@Ideal.inertia_top : ∀ {R : Type u_1} [inst : CommRing R] {G : Type u_2} [inst_1 : Group G]
[inst_2 : MulSemiringAction G R], Ideal.inertia G ⊤ = ⊤
@Ideal.inertia_normal_of_forall_smul_eq : ∀ {R : Type u_1} [inst : CommRing R] {G : Type u_2} [inst_1 : Group G]
[inst_2 : MulSemiringAction G R] {I : Ideal R}, (∀ (g : G), g • I = I) → (Ideal.inertia G I).Normal
@IsLocalRing.pointwise_smul_maximalIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] {G : Type u_2}
[inst_2 : Group G] [inst_3 : MulSemiringAction G R] (g : G),
g • IsLocalRing.maximalIdeal R = IsLocalRing.maximalIdeal R
@IsLocalRing.pointwise_smul_maximalIdeal_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R]
{G : Type u_2} [inst_2 : Group G] [inst_3 : MulSemiringAction G R] (g : G) (n : ℕ),
g • IsLocalRing.maximalIdeal R ^ n = IsLocalRing.maximalIdeal R ^ n
IsLocalRing.lowerRamificationGroup : (R : Type u_1) →
[inst : CommRing R] → [IsLocalRing R] → (G : Type u_2) → [inst_2 : Group G] → [MulSemiringAction G R] → ℕ → Subgroup G
@IsLocalRing.mem_lowerRamificationGroup : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] {G : Type u_2}
[inst_2 : Group G] [inst_3 : MulSemiringAction G R] {i : ℕ} {σ : G},
σ ∈ IsLocalRing.lowerRamificationGroup R G i ↔ ∀ (x : R), σ • x - x ∈ IsLocalRing.maximalIdeal R ^ (i + 1)
@IsLocalRing.lowerRamificationGroup_antitone : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R]
{G : Type u_2} [inst_2 : Group G] [inst_3 : MulSemiringAction G R], Antitone (IsLocalRing.lowerRamificationGroup R G)
@IsLocalRing.lowerRamificationGroup_normal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R]
{G : Type u_2} [inst_2 : Group G] [inst_3 : MulSemiringAction G R] (i : ℕ),
(IsLocalRing.lowerRamificationGroup R G i).Normal
@IsLocalRing.lowerRamificationGroup_zero_eq_ker : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R]
{G : Type u_2} [inst_2 : Group G] [inst_3 : MulSemiringAction G R],
IsLocalRing.lowerRamificationGroup R G 0 = (MulSemiringAction.toRingAut G (IsLocalRing.ResidueField R)).ker
@IsLocalRing.lowerRamificationGroup_zero_eq_inertia : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R]
{G : Type u_2} [inst_2 : Group G] [inst_3 : MulSemiringAction G R],
IsLocalRing.lowerRamificationGroup R G 0 = Ideal.inertia G (IsLocalRing.maximalIdeal R)
@IsLocalRing.lowerRamificationGroup_le_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R]
{G : Type u_2} [inst_2 : Group G] [inst_3 : MulSemiringAction G R] (i : ℕ),
IsLocalRing.lowerRamificationGroup R G i ≤ IsLocalRing.lowerRamificationGroup R G 0
@IsLocalRing.iInf_lowerRamificationGroup_le_ker_toRingAut : ∀ {R : Type u_1} [inst : CommRing R]
[inst_1 : IsLocalRing R] {G : Type u_2} [inst_2 : Group G] [inst_3 : MulSemiringAction G R],
⨅ n, IsLocalRing.maximalIdeal R ^ n = ⊥ →
⨅ i, IsLocalRing.lowerRamificationGroup R G i ≤ (MulSemiringAction.toRingAut G R).ker
@IsLocalRing.iInf_lowerRamificationGroup_eq_bot : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R]
{G : Type u_2} [inst_2 : Group G] [inst_3 : MulSemiringAction G R],
⨅ n, IsLocalRing.maximalIdeal R ^ n = ⊥ → ∀ [FaithfulSMul G R], ⨅ i, IsLocalRing.lowerRamificationGroup R G i = ⊥
ValuationSubring.lowerRamificationGroup : (K : Type u_1) →
{L : Type u_2} →
[inst : Field K] →
[inst_1 : Field L] →
[inst_2 : Algebra K L] → (A : ValuationSubring L) → ℕ → Subgroup ↥(ValuationSubring.decompositionSubgroup K A)
@ValuationSubring.mem_lowerRamificationGroup : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L]
[inst_2 : Algebra K L] {A : ValuationSubring L} {i : ℕ} {σ : ↥(ValuationSubring.decompositionSubgroup K A)},
σ ∈ ValuationSubring.lowerRamificationGroup K A i ↔ ∀ (a : ↥A), σ • a - a ∈ IsLocalRing.maximalIdeal ↥A ^ (i + 1)
@ValuationSubring.lowerRamificationGroup_antitone : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L]
[inst_2 : Algebra K L] {A : ValuationSubring L}, Antitone (ValuationSubring.lowerRamificationGroup K A)
@ValuationSubring.lowerRamificationGroup_normal : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L]
[inst_2 : Algebra K L] {A : ValuationSubring L} (i : ℕ), (ValuationSubring.lowerRamificationGroup K A i).Normal
@ValuationSubring.lowerRamificationGroup_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L]
[inst_2 : Algebra K L] {A : ValuationSubring L},
ValuationSubring.lowerRamificationGroup K A 0 = ValuationSubring.inertiaSubgroup K A
@ValuationSubring.lowerRamificationGroup_le_inertiaSubgroup : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K]
[inst_1 : Field L] [inst_2 : Algebra K L] {A : ValuationSubring L} (i : ℕ),
ValuationSubring.lowerRamificationGroup K A i ≤ ValuationSubring.inertiaSubgroup K A
'IsLocalRing.lowerRamificationGroup_antitone' depends on axioms: [propext, Classical.choice, Quot.sound]
'IsLocalRing.lowerRamificationGroup_zero_eq_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'IsLocalRing.iInf_lowerRamificationGroup_eq_bot' depends on axioms: [propext, Classical.choice, Quot.sound]
[lean: 125.8s]
# Les niveaux que fixe la tour : dans Z, l'ideal maximal (2) et ses puissances.# LRG(i) agit trivialement sur Z/2^{i+1} -- chaque groupe de la tour est "invisible"# a un etage de la tour de troncatures de l'annexe A.print("Etage | quotient | ce que LRG(i) respecte")for i inrange(4): mod =2** (i +1)print(f" i={i} | Z/{mod:<4d} | les sigma de LRG({i}) fixent chaque classe mod {mod}")# La meme suite 2-adique qu'en annexe A, vue a travers trois etages de la tour :x =pow(3, -1, 2**12) # l'inverse de 3, vu au niveau 12print(f"\nLe meme element de Z_2 projete sur les etages 5, 8 et 12 :")print(f" niveau 12 : {x}")print(f" niveau 8 : {x %2**8}")print(f" niveau 5 : {x %2**5}")print("Projeter d'un etage au suivant = oublier les chiffres 2-adiques de poids fort :")print("c'est le systeme projectif dont la completion est la limite, et la tour LRG(i)")print("gradue les automorphismes selon le niveau ou ils cessent d'etre visibles.")
Etage | quotient | ce que LRG(i) respecte
i=0 | Z/2 | les sigma de LRG(0) fixent chaque classe mod 2
i=1 | Z/4 | les sigma de LRG(1) fixent chaque classe mod 4
i=2 | Z/8 | les sigma de LRG(2) fixent chaque classe mod 8
i=3 | Z/16 | les sigma de LRG(3) fixent chaque classe mod 16
Le meme element de Z_2 projete sur les etages 5, 8 et 12 :
niveau 12 : 2731
niveau 8 : 171
niveau 5 : 11
Projeter d'un etage au suivant = oublier les chiffres 2-adiques de poids fort :
c'est le systeme projectif dont la completion est la limite, et la tour LRG(i)
gradue les automorphismes selon le niveau ou ils cessent d'etre visibles.
Interprétation
La signature de lowerRamificationGroup_antitone imprimée par Lean dit l’essentiel : Antitone (lowerRamificationGroup R G) — plus on monte dans la tour, plus le groupe rétrécit. Et lowerRamificationGroup_zero_eq_inertia ancre le pied de la tour : le niveau 0 EST l’inertie, la ramification inférieure est son raffinement quantitatif. Enfin iInf_lowerRamificationGroup_eq_bot ferme la tour : un automorphisme invisible à tous les niveaux est l’identité — la filtration sépare les points de G.
Là encore, les #print axioms ne listent que la liste blanche standard. Ces déclarations étaient le « trou » de visibilité du lake galois_lean au scanner de l’EPIC #11703 : elles sont désormais exécutées, auditées, et reliées à la complétion adique qui les motive — la théorie locale de Serre, lisible depuis le companion du problème inverse de Galois.
Conclusion
Ce notebook a établi
Méthode
Statut
Énoncé 1
M₂₃ simple, d’ordre 10 200 960
Théorèmes Lean exécutés (card_M23, simple_M23), #print axioms = liste blanche standard
Complétion adique (AdicCompletionLocalRing) + tour de ramification inférieure (LowerRamificationGroup)
#check + #print axioms exécutés par Lean (axiomes = liste blanche), troncatures 2-adiques rejouées en Python
EXÉCUTÉ (mécaniquement)
Le problème inverse de Galois sporadique est refermé au sens mathématique (préprint du 9 août 2026) — mais sa formalisation complète (existence de Riemann, descente, spécialisation de Hilbert) reste ouverte côté Lean, et le socle grothendieck_lean en marque le point d’arrivée naturel. Une noix de plus à grignoter.
Prérequis pour rejouer : WSL avec elan/lake (build de galois_lean, Mathlib v4.33 via cache), Python 3 avec sympy. Durée d’exécution : ~2 min une fois le lake construit.