Lean-29 : les opérateurs de Hecke $T_p$ et $U_p$ — compagnon natif du lake `hecke_lean`

Série : SymbolicAI / Lean — companions natifs (cf. Lean-24 calibration, Lean-23b ERC-20)

Compagnon natif du lake hecke_lean : ici le lake est importé et exécuté dans un kernel Lean 4 réel (lean4-wsl), et chaque définition / théorème est interrogé par #check ou #print axioms — les sorties de ce notebook sont des sorties du compilateur Lean, pas de la prose à propos de Lean.

Le lake formalise les opérateurs de Hecke classiques sur le demi-plan supérieur $\mathbb{H}$ : pour un entier $p$ (usuellement premier), l’opérateur $T_p$ agit sur une fonction $f : \mathbb{H} \to \mathbb{C}$ par une somme finie de slashs sur des représentants explicites des classes $\Gamma(1) \backslash M_2(\mathbb{Z})$ de déterminant $p$, et l’opérateur $U_p$ n’en retient que la partie triangulaire. La formule induite sur les coefficients de Fourier — $a(np) + p^{k-1}\,a(n/p)$ selon que $p$ divise $n$ ou non — est portée par coeffHeckeT.

Provenance : le lake est un port du dépôt anthropics/fermats-last-theorem (opérateurs : Definitions/Def_ModularForm_HeckeOperator.lean ; routes cyclotomiques et FLT : P2M/Sol/S_IsCyclotomicExtension_Rat_{seven,eleven}_pid.lean, S_ModularForm_S2_Gamma0_2_eq_zero.lean ; commit aa2d8b34692b), docstrings pédagogiques en français et exemples calculables ajoutés ; licence Apache-2.0 préservée (voir hecke_lean/NOTICE.md).

Pourquoi ce lake dans CoursIA

L’enjeu de ce que le lake porte. Les opérateurs de Hecke ne sont pas un objet d’exposition : ils sont la charnière par laquelle une forme modulaire devient une suite de nombres comparable à autre chose. Une forme propre normalisée — un vecteur propre commun de tous les $T_p$ — a ses coefficients de Fourier $a(p)$ égaux à ses valeurs propres, et c’est cette suite que le théorème de modularité apparie aux comptages de points $\#E(\mathbb{F}_p)$ d’une courbe elliptique sur $\mathbb{Q}$. La chaîne courbe de Frey $\rightarrow$ abaissement du niveau $\rightarrow$ modularité, qui clôt le dernier théorème de Fermat, passe donc par la relation $a(np) + p^{k-1} a(n/p)$ — celle que coeffHeckeT porte ici, et que la section 5 fait calculer. Le dépôt amont dont ce lake est un port, anthropics/fermats-last-theorem, est un chantier de formalisation de cette chaîne. Le lake en formalise les opérateurs, pas la preuve : c’est un fragment de fondation, et la section 7 en prouve la dernière étape — $S_2(\Gamma_0(2)) = 0$ — pendant que la section 8 mesure exactement ce que le lake démontre et ce qu’il suppose.

Pourquoi ce module parmi environ 15 000 théorèmes du corpus FLT. Son choix n’est pas justifié par le seul fait qu’un énoncé non trivial puisse être soumis au noyau Lean — cet argument vaudrait pour n’importe quel module du corpus. Hecke prolonge deux objets déjà enseignés dans CoursIA. D’abord, Lean-12 et son compagnon Lean-12b introduisent les fonctions sur l’hypercube et le lake sensitivity_lean ; son module Sensitivity/Fourier.lean représente une fonction par une famille de coefficients de Walsh, établit leur orthogonalité puis une reconstruction par somme finie. Ensuite, ce même lake formalise dans Sensitivity/Operator.lean un opérateur linéaire $f_n$ et la relation $f_n^2=n\,\mathrm{Id}$, tandis que Lean-21, son compagnon Lean-21b et le lake mimo_lean manipulent matrices, applications linéaires, actions scalaires et sommes finies. Le passage pédagogique devient alors lisible : fonction décrite par des coefficients $\rightarrow$ opérateur additif et homogène agissant sur une fonction $\rightarrow$ transformation arithmétique explicite de ses coefficients. Hecke est le fragment du corpus FLT où ces deux fils déjà familiers se rencontrent dans un nouvel objet : les formes modulaires sur le demi-plan supérieur, leurs slash actions et la formule de coeffHeckeT.

Raccord conceptuel, dépendance réelle. Ce passage est une analogie structurante, pas une identification mathématique : les coefficients de Fourier booléens de Sensitivity/Fourier.lean décrivent une fonction sur un hypercube fini à l’aide des caractères de Walsh ; les coefficients $a(n)$ manipulés ici sont ceux d’une $q$-expansion de forme modulaire. De même, sensitivity_lean et mimo_lean préparent la lecture des matrices, sommes finies, actions scalaires, additivité et homogénéité, mais ne sont pas des dépendances Lean de ce notebook. La cellule d’import charge réellement Hecke.HeckeOperator, et ce module importe directement Mathlib.NumberTheory.ModularForms.SlashActions. Aucun lien historique ou formel particulier avec Galois, Belyi ou la théorie de l’information n’est revendiqué à partir de cette seule proximité de vocabulaire.

Pourquoi ce compagnon

Un notebook « natif » ne décrit pas le lake : il le charge. Chaque #check ci-dessous est résolu par le compilateur Lean contre les .olean compilés du lake — la signature affichée est celle qui vit dans Hecke/HeckeOperator.lean, pas une copie. La contrepartie pédagogique est précieuse pour la théorie des formes modulaires : les opérateurs de Hecke y sont souvent présentés comme des boîtes noires algébriques ; ici, chaque brique (représentants, slash, déterminants, coefficients) est interrogée séparément et son énoncé exact est affiché.

Plan du notebook

Le lake : architecture, provenance, conventions du kernel
Les représentants $\gamma_{p,j}$ et la partie diagonale
L’action sur $\mathbb{H}$ : slash, dénominateurs, homothéties
Les opérateurs $U_p$ et $T_p$ : définitions, lectures ponctuelles, linéarité
La formule des coefficients : coeffHeckeT et ses exemples calculables
La route cyclotomique : Kummer, $\mathbb{Z}[\zeta_p]$ principal pour $p = 7, 11, 13$
La route moderne : Frey, l’indice de $\Gamma_0(2)$, $S_2(\Gamma_0(2)) = 0$
Transparence axiomatique et limites

Conventions du notebook

Kernel : lean4-wsl (Lean 4 via WSL, exécuté depuis le répertoire du lake)
Imports : en tête de la première cellule code uniquement — le kernel partage un seul environnement entre cellules, où import n’est légal qu’en tête de session, comme en tête de fichier Lean (le chargement de la fermeture Mathlib prend de l’ordre de la minute)
Sorties : #check type, #print axioms vérifie la preuve, #eval calcule
Exercices : convention C.1 — le notebook s’exécute de bout en bout ; chaque cellule d’exercice énonce l’objectif en commentaire, le laisse ouvert sous un unique -- TODO étudiant (non résolu) et rappelle le lemme utile par un #check — aucun script de solution n’est fourni

Substance formelle

Notion	Symbole du lake	Énoncé clé
Représentant triangulaire	`heckeMatrix p j`	$\gamma_{p,j} = \begin{pmatrix} 1 & j \\ 0 & p \end{pmatrix}$, $\det = p$
Représentant diagonal	`heckeDiagMatrix p`	$\begin{pmatrix} p & 0 \\ 0 & 1 \end{pmatrix}$, $\det = p$
Partie triangulaire	`heckeU k p f`	$\sum_{j<p} f \mid [k]\ \gamma_{p,j}$
Opérateur de Hecke	`heckeT k p f`	$U_p f + f \mid [k]\ \text{diag}$
Coefficients	`coeffHeckeT k p a n`	$a(np) + p^{k-1} a(n/p)$ si $p \mid n$

Prérequis

Lean-5 Tactics (simp, rw, decide) et Lean-6 Mathlib
Théorie : action de $SL_2(\mathbb{Z})$ sur $\mathbb{H}$ par homographies ; le notebook rappelle ce qu’il utilise

Durée estimée

35 à 45 minutes en lecture interactive (kernel WSL requis pour l’exécution réelle).

Les sections 4 et 5 sont le cœur : on y voit la géométrie (le slash) devenir combinatoire (les coefficients de Fourier).

1. Le lake `hecke_lean` : un port pédagogique, trois familles d’énoncés

hecke_lean porte cinq modules et leurs miroirs i18n _en (convention sibling pair de l’EPIC #4980) : Hecke/HeckeOperator.lean — les sections 2 à 5 de ce compagnon, adossé à Mathlib via Mathlib.NumberTheory.ModularForms.SlashActions —, les trois routes cyclotomiques Hecke/SevenPid.lean, Hecke/ElevenPid.lean, Hecke/ThirteenPid.lean (section 6) et Hecke/FltRoute.lean, la route FLT en exercices guidés (section 7). Le fichier racine Hecke.lean les agrège tous par import. Pinné au commit db584cd6d46c sur la toolchain Lean v4.33.0.

Le module organise ses énoncés en trois familles :

Les représentants : upperTriangularGL, heckeMatrix, heckeDiagMatrix — la géométrie des classes $\Gamma(1) \backslash M_2(\mathbb{Z})$ de déterminant $p$ ;
Les opérateurs : heckeU, heckeT et leurs lectures ponctuelles — l’analyse sur $\mathbb{H}$ ;
Les coefficients : coeffHeckeT, coeffHeckeU — la combinatoire des suites de Fourier, avec une section Examples d’exemples calculables absents du dépôt amont.

Le produit de Petersson reste hors périmètre du lake ; les cusp forms, absentes du module HeckeOperator, sont visitées à la section 7 via FltRoute (norme cuspidale, $S_2(\Gamma_0(2)) = 0$).

Pourquoi la toolchain compte ici : le kernel lean4-wsl lance le REPL Lean avec le LEAN_PATH du lake — les .olean ne se chargent que si la version du compilateur qui les a produits correspond à celle du REPL. C’est la raison pour laquelle ce notebook s’exécute depuis le répertoire du lake : c’est là que le kernel détecte le workspace et sa toolchain.

-- TOUTES les importations de la session viennent ici (tête de session) :
-- le kernel lean4-wsl partage UN environnement entre cellules, où `import`
-- n'est légal qu'en tête de session, comme en tête de fichier Lean.
import Hecke.HeckeOperator
import Hecke.SevenPid
import Hecke.ElevenPid
import Hecke.ThirteenPid
import Hecke.FltRoute

-- Les notations du lake (GL, matrices !![...]) puis son namespace :
open scoped MatrixGroups
open ModularForm

#check @ModularForm.heckeMatrix        -- le représentant γ_{p,j} = !![1, j; 0, p]
#check @ModularForm.heckeDiagMatrix    -- le représentant diagonal !![p, 0; 0, 1]
#check @ModularForm.heckeU             -- la partie triangulaire U_p
#check @ModularForm.heckeT             -- l'opérateur de Hecke T_p = U_p + diagonal
#check @ModularForm.coeffHeckeT        -- la formule des coefficients de T_p
#check @ModularForm.coeffHeckeU        -- l'échantillonnage a (n p) de U_p

-- TOUTES les importations de la session viennent ici (tête de session) :

-- le kernel lean4-wsl partage UN environnement entre cellules, où `import`

-- n'est légal qu'en tête de session, comme en tête de fichier Lean.

import Hecke.HeckeOperator

import Hecke.SevenPid

import Hecke.ElevenPid

import Hecke.ThirteenPid

import Hecke.FltRoute

-- Les notations du lake (GL, matrices !![...]) puis son namespace :

open scoped MatrixGroups

open ModularForm

#check @ModularForm.heckeMatrix        -- le représentant γ_{p,j} = !![1, j; 0, p] heckeMatrix : ℕ → ℕ → GL (Fin 2) ℝ

#check @ModularForm.heckeDiagMatrix    -- le représentant diagonal !![p, 0; 0, 1] heckeDiagMatrix : ℕ → GL (Fin 2) ℝ

#check @ModularForm.heckeU             -- la partie triangulaire U_p heckeU : ℤ → ℕ → (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂ

#check @ModularForm.heckeT             -- l'opérateur de Hecke T_p = U_p + diagonal heckeT : ℤ → ℕ → (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂ

#check @ModularForm.coeffHeckeT        -- la formule des coefficients de T_p coeffHeckeT : ℤ → ℕ → (ℕ → ℂ) → ℕ → ℂ

#check @ModularForm.coeffHeckeU        -- l'échantillonnage a (n p) de U_p coeffHeckeU : ℕ → (ℕ → ℂ) → ℕ → ℂ

--% env 0

Raw input

{"cmd": "-- TOUTES les importations de la session viennent ici (t\u00eate de session) :\n-- le kernel lean4-wsl partage UN environnement entre cellules, o\u00f9 `import`\n-- n'est l\u00e9gal qu'en t\u00eate de session, comme en t\u00eate de fichier Lean.\nimport Hecke.HeckeOperator\nimport Hecke.SevenPid\nimport Hecke.ElevenPid\nimport Hecke.ThirteenPid\nimport Hecke.FltRoute\n\n-- Les notations du lake (GL, matrices !![...]) puis son namespace :\nopen scoped MatrixGroups\nopen ModularForm\n\n#check @ModularForm.heckeMatrix        -- le repr\u00e9sentant \u03b3_{p,j} = !![1, j; 0, p]\n#check @ModularForm.heckeDiagMatrix    -- le repr\u00e9sentant diagonal !![p, 0; 0, 1]\n#check @ModularForm.heckeU             -- la partie triangulaire U_p\n#check @ModularForm.heckeT             -- l'op\u00e9rateur de Hecke T_p = U_p + diagonal\n#check @ModularForm.coeffHeckeT        -- la formule des coefficients de T_p\n#check @ModularForm.coeffHeckeU        -- l'\u00e9chantillonnage a (n p) de U_p"}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 14, "column": 0},
   "endPos": {"line": 14, "column": 6},
   "data": "heckeMatrix : ℕ → ℕ → GL (Fin 2) ℝ"},
  {"severity": "info",
   "pos": {"line": 15, "column": 0},
   "endPos": {"line": 15, "column": 6},
   "data": "heckeDiagMatrix : ℕ → GL (Fin 2) ℝ"},
  {"severity": "info",
   "pos": {"line": 16, "column": 0},
   "endPos": {"line": 16, "column": 6},
   "data": "heckeU : ℤ → ℕ → (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂ"},
  {"severity": "info",
   "pos": {"line": 17, "column": 0},
   "endPos": {"line": 17, "column": 6},
   "data": "heckeT : ℤ → ℕ → (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂ"},
  {"severity": "info",
   "pos": {"line": 18, "column": 0},
   "endPos": {"line": 18, "column": 6},
   "data": "coeffHeckeT : ℤ → ℕ → (ℕ → ℂ) → ℕ → ℂ"},
  {"severity": "info",
   "pos": {"line": 19, "column": 0},
   "endPos": {"line": 19, "column": 6},
   "data": "coeffHeckeU : ℕ → (ℕ → ℂ) → ℕ → ℂ"}],
 "env": 0}

Lecture des signatures

Sortie obtenue : six signatures, rendues par le compilateur contre les oleans du lake.

Symbole	Signature	Rôle
`heckeMatrix`	`ℕ → ℕ → GL (Fin 2) ℝ`	le représentant triangulaire $\gamma_{p,j}$
`heckeDiagMatrix`	`ℕ → GL (Fin 2) ℝ`	le représentant diagonal, même déterminant
`heckeU`	`ℤ → ℕ → (ℍ → ℂ) → ℍ → ℂ`	somme des $p$ slashs triangulaires
`heckeT`	`ℤ → ℕ → (ℍ → ℂ) → ℍ → ℂ`	$T_p = U_p + $ slash diagonal
`coeffHeckeT`	`ℤ → ℕ → (ℕ → ℂ) → ℕ → ℂ`	la suite de Fourier de $T_p f$
`coeffHeckeU`	`ℕ → (ℕ → ℂ) → ℕ → ℂ`	l’échantillonnage $a \mapsto a (n\,p)$

Points clés :

Les opérateurs prennent le poids $k : \mathbb{Z}$ en premier argument — c’est lui qui portera le facteur $p^{k-1}$ ;
Ils agissent sur des fonctions arbitraires $\mathbb{H} \to \mathbb{C}$ : aucune modularité n’est exigée à ce stade, $T_p$ est d’abord un endomorphisme d’un espace de fonctions ;
Les opérateurs à coefficients (coeffHeckeT) vivent sur les suites $a : \mathbb{N} \to \mathbb{C}$ — la traduction combinatoire de l’action géométrique.

Note technique : les deux niveaux (fonctions sur $\mathbb{H}$ / suites de Fourier) coexistent dans le même module sans être reliés par un théorème de passage — ce pont (développement en $q$-série) appartient au grain aval du lake.

2. Les représentants $\gamma_{p,j}$ et la partie diagonale

L’opérateur $T_p$ se définit par une somme sur les classes à gauche $\Gamma(1) \backslash \{ M \in M_2(\mathbb{Z}) : \det M = p \}$. Pour $p$ premier, cette orbite admet $p+1$ représentants : les $p$ matrices triangulaires $\gamma_{p,j} = \begin{pmatrix} 1 & j \\ 0 & p \end{pmatrix}$ pour $j = 0, \dots, p-1$ (la partie « $U$ »), plus la matrice diagonale $\begin{pmatrix} p & 0 \\ 0 & 1 \end{pmatrix}$.

Le lake encode la brique commune par upperTriangularGL a b d : la matrice $\begin{pmatrix} a & b \\ 0 & d \end{pmatrix}$ vue dans $GL(2, \mathbb{R})$, avec l’hypothèse a * d ≠ 0 qui garantit l’inversibilité. Les deux familles de représentants en sont des instances :

heckeMatrix p j := upperTriangularGL 1 j p (si $p = 0$, renvoie l’identité — cas dégénéré neutralisé) ;
heckeDiagMatrix p := upperTriangularGL p 0 1.

Les théorèmes val_heckeMatrix et val_heckeDiagMatrix (@[simp]) donnent les valeurs explicites ; det_heckeMatrix et det_heckeDiagMatrix assurent que le déterminant vaut exactement $p$ — et det_heckeMatrix_pos qu’il est positif, la condition qui garantit que les représentants préservent $\mathbb{H}$.

-- Les briques : la matrice triangulaire et ses valeurs explicites.
#check @ModularForm.upperTriangularGL
#check @ModularForm.val_heckeMatrix
#check @ModularForm.val_heckeDiagMatrix

-- Le déterminant des représentants vaut EXACTEMENT p (pas |p|) :
#check @ModularForm.det_heckeMatrix
#check @ModularForm.det_heckeDiagMatrix
#check @ModularForm.det_heckeMatrix_pos

-- Certificat : preuve close, sans axiome au-delà des standards.
#print axioms ModularForm.det_heckeMatrix

-- Les briques : la matrice triangulaire et ses valeurs explicites.

#check @ModularForm.upperTriangularGL upperTriangularGL : (a : ℝ) → ℝ → (d : ℝ) → a * d ≠ 0 → GL (Fin 2) ℝ

#check @ModularForm.val_heckeMatrix @val_heckeMatrix : ∀ {p : ℕ}, p ≠ 0 → ∀ (j : ℕ), ↑(heckeMatrix p j) = !![1, ↑j; 0, ↑p]

#check @ModularForm.val_heckeDiagMatrix @val_heckeDiagMatrix : ∀ {p : ℕ}, p ≠ 0 → ↑(heckeDiagMatrix p) = !![↑p, 0; 0, 1]

-- Le déterminant des représentants vaut EXACTEMENT p (pas |p|) :

#check @ModularForm.det_heckeMatrix @det_heckeMatrix : ∀ {p : ℕ}, p ≠ 0 → ∀ (j : ℕ), ↑(Matrix.GeneralLinearGroup.det (heckeMatrix p j)) = ↑p

#check @ModularForm.det_heckeDiagMatrix @det_heckeDiagMatrix : ∀ {p : ℕ}, p ≠ 0 → ↑(Matrix.GeneralLinearGroup.det (heckeDiagMatrix p)) = ↑p

#check @ModularForm.det_heckeMatrix_pos det_heckeMatrix_pos : ∀ (p j : ℕ), 0 < ↑(Matrix.GeneralLinearGroup.det (heckeMatrix p j))

-- Certificat : preuve close, sans axiome au-delà des standards.

#print axioms ModularForm.det_heckeMatrix 'ModularForm.det_heckeMatrix' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 1

Raw input

{"cmd": "-- Les briques : la matrice triangulaire et ses valeurs explicites.\n#check @ModularForm.upperTriangularGL\n#check @ModularForm.val_heckeMatrix\n#check @ModularForm.val_heckeDiagMatrix\n\n-- Le d\u00e9terminant des repr\u00e9sentants vaut EXACTEMENT p (pas |p|) :\n#check @ModularForm.det_heckeMatrix\n#check @ModularForm.det_heckeDiagMatrix\n#check @ModularForm.det_heckeMatrix_pos\n\n-- Certificat : preuve close, sans axiome au-del\u00e0 des standards.\n#print axioms ModularForm.det_heckeMatrix", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "upperTriangularGL : (a : ℝ) → ℝ → (d : ℝ) → a * d ≠ 0 → GL (Fin 2) ℝ"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@val_heckeMatrix : ∀ {p : ℕ}, p ≠ 0 → ∀ (j : ℕ), ↑(heckeMatrix p j) = !![1, ↑j; 0, ↑p]"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@val_heckeDiagMatrix : ∀ {p : ℕ}, p ≠ 0 → ↑(heckeDiagMatrix p) = !![↑p, 0; 0, 1]"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "@det_heckeMatrix : ∀ {p : ℕ}, p ≠ 0 → ∀ (j : ℕ), ↑(Matrix.GeneralLinearGroup.det (heckeMatrix p j)) = ↑p"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "@det_heckeDiagMatrix : ∀ {p : ℕ}, p ≠ 0 → ↑(Matrix.GeneralLinearGroup.det (heckeDiagMatrix p)) = ↑p"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "det_heckeMatrix_pos : ∀ (p j : ℕ), 0 < ↑(Matrix.GeneralLinearGroup.det (heckeMatrix p j))"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 6},
   "data":
   "'ModularForm.det_heckeMatrix' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 1}

Lecture : valeurs et déterminants

Sortie obtenue : les équations de valeur (val_heckeMatrix hp j : heckeMatrix p j = !![1, j; 0, p]), les déterminants (((heckeMatrix p j).det : ℝ) = p), et le certificat d’axiomes de det_heckeMatrix.

Énoncé	Ce qu’il dit
`val_heckeMatrix`	$\gamma_{p,j}$ est littéralement la matrice $\begin{pmatrix} 1 & j \\ 0 & p \end{pmatrix}$ à coefficients réels
`det_heckeMatrix`	son déterminant vaut $p$ — l’indice de l’opérateur, pas une valeur absolue
`det_heckeMatrix_pos`	déterminant positif y compris pour $p = 0$ (identité) : l’action préserve $\mathbb{H}$

Points clés :

Le déterminant est énoncé dans $\mathbb{R}$ via le coercion ((...).det : ℝ) = p — le $p$ de droite est un naturel coercé, l’égalité est exacte ;
Pour det_heckeMatrix, #print axioms ne liste que les axiomes standards (propext, Classical.choice, Quot.sound selon la sortie ci-dessus) et aucun sorryAx : ce certificat établit que ce théorème interrogé a une preuve close. La propriété globale « zéro sorry » repose séparément sur le scan du source du lake.

Note technique : la positivité du déterminant n’est pas un détail : c’est elle qui distingue les représentants de Hecke des éléments de $GL_2^-(\mathbb{R})$, qui échangeraient les deux demi-plans.

Exercice 1 — lire la valeur d’un représentant

Sur le modèle de val_heckeMatrix, établissez la valeur explicite du représentant $\gamma_{3,2} = \begin{pmatrix} 1 & 2 \\ 0 & 3 \end{pmatrix}$ : l’énoncé compare la coercion de heckeMatrix 3 2 dans Matrix (Fin 2) (Fin 2) ℝ au littéral !![1, 2; 0, 3].

Indice : val_heckeMatrix prend l’hypothèse p ≠ 0 — pour $p = 3$, elle se décharge par decide ; rw ramène ensuite le but à une égalité de littéraux numériques, que rfl referme (explicite : le rfl implicite de rw ne déplie pas assez les coercitions ↑2 contre 2).

-- Exercice 1 : la valeur explicite du représentant γ_{3,2} (déterminant 3).
--
-- Objectif : établir
--   ((ModularForm.heckeMatrix 3 2 : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)
--       = !![(1 : ℝ), 2; 0, 3]
-- TODO étudiant : à compléter (indice dans la cellule précédente).

#check @ModularForm.val_heckeMatrix   -- le lemme à invoquer

-- Exercice 1 : la valeur explicite du représentant γ_{3,2} (déterminant 3).

--

-- Objectif : établir

--   ((ModularForm.heckeMatrix 3 2 : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)

--       = !![(1 : ℝ), 2; 0, 3]

-- TODO étudiant : à compléter (indice dans la cellule précédente).

#check @ModularForm.val_heckeMatrix   -- le lemme à invoquer @val_heckeMatrix : ∀ {p : ℕ}, p ≠ 0 → ∀ (j : ℕ), ↑(heckeMatrix p j) = !![1, ↑j; 0, ↑p]

--% env 2

Raw input

{"cmd": "-- Exercice 1 : la valeur explicite du repr\u00e9sentant \u03b3_{3,2} (d\u00e9terminant 3).\n--\n-- Objectif : \u00e9tablir\n--   ((ModularForm.heckeMatrix 3 2 : GL (Fin 2) \u211d) : Matrix (Fin 2) (Fin 2) \u211d)\n--       = !![(1 : \u211d), 2; 0, 3]\n-- TODO \u00e9tudiant : \u00e0 compl\u00e9ter (indice dans la cellule pr\u00e9c\u00e9dente).\n\n#check @ModularForm.val_heckeMatrix   -- le lemme \u00e0 invoquer", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "@val_heckeMatrix : ∀ {p : ℕ}, p ≠ 0 → ∀ (j : ℕ), ↑(heckeMatrix p j) = !![1, ↑j; 0, ↑p]"}],
 "env": 2}

3. L’action sur le demi-plan supérieur : le slash

Le groupe $GL_2^+(\mathbb{R})$ agit sur $\tau \in \mathbb{H}$ par homographies, et cette action se relève en l’action de slash de poids $k$ sur les fonctions :

\[(f \mid [k]\ \gamma)(\tau) = \det(\gamma)^{k-1} \cdot \sigma(\gamma)\big(c\tau + d\big)^{-k} \cdot f(\gamma \cdot \tau)\]

Le lake décompose cette formule pour chacun des deux représentants :

pour $\gamma_{p,j}$ : le dénominateur $c\tau + d$ vaut $p$ (théorème denom_heckeMatrix), le caractère $\sigma$ est trivial (déterminant positif), et l’action sur $\tau$ est l’homothétie-translation $(\tau + j)/p$ (coe_heckeMatrix_smul) — d’où la lecture $(f \mid [k]\ \gamma_{p,j})(\tau) = p^{-1} f\big((\tau + j)/p\big)$ ;
pour le diagonal : le dénominateur vaut $1$, l’action est la dilatation $p\,\tau$, et le déterminant $p$ porte le facteur $p^{k-1}$ — d’où $(f \mid [k]\ \mathrm{diag})(\tau) = p^{k-1} f(p\,\tau)$.

Les deux théorèmes slash_heckeMatrix_apply et slash_heckeDiagMatrix_apply sont ces lectures démontrées — ce sont eux qui feront le pont entre la définition abstraite de $T_p$ et la formule des coefficients.

-- L'action des représentants sur τ ∈ ℍ :
#check @ModularForm.coe_heckeMatrix_smul       -- γ_{p,j} • τ = (τ + j) / p
#check @ModularForm.coe_heckeDiagMatrix_smul   -- diag • τ = p • τ
#check @ModularForm.denom_heckeMatrix          -- dénominateur p
#check @ModularForm.denom_heckeDiagMatrix      -- dénominateur 1
#check @ModularForm.σ_heckeMatrix              -- caractère σ trivial (det > 0)

-- Les lectures du slash sur chaque famille :
#check @ModularForm.slash_heckeMatrix_apply
#check @ModularForm.slash_heckeDiagMatrix_apply

-- L'action des représentants sur τ ∈ ℍ :

#check @ModularForm.coe_heckeMatrix_smul       -- γ_{p,j} • τ = (τ + j) / p @coe_heckeMatrix_smul : ∀ {p : ℕ}, p ≠ 0 → ∀ (j : ℕ) (τ : UpperHalfPlane), ↑(heckeMatrix p j • τ) = (↑τ + ↑j) / ↑p

#check @ModularForm.coe_heckeDiagMatrix_smul   -- diag • τ = p • τ @coe_heckeDiagMatrix_smul : ∀ {p : ℕ}, p ≠ 0 → ∀ (τ : UpperHalfPlane), ↑(heckeDiagMatrix p • τ) = ↑p * ↑τ

#check @ModularForm.denom_heckeMatrix          -- dénominateur p @denom_heckeMatrix : ∀ {p : ℕ}, p ≠ 0 → ∀ (j : ℕ) (τ : UpperHalfPlane), UpperHalfPlane.denom (heckeMatrix p j) ↑τ = ↑p

#check @ModularForm.denom_heckeDiagMatrix      -- dénominateur 1 @denom_heckeDiagMatrix : ∀ {p : ℕ}, p ≠ 0 → ∀ (τ : UpperHalfPlane), UpperHalfPlane.denom (heckeDiagMatrix p) ↑τ = 1

#check @ModularForm.σ_heckeMatrix              -- caractère σ trivial (det > 0) σ_heckeMatrix : ∀ (p j : ℕ), UpperHalfPlane.σ (heckeMatrix p j) = ContinuousAlgEquiv.refl ℝ ℂ

-- Les lectures du slash sur chaque famille :

#check @ModularForm.slash_heckeMatrix_apply slash_heckeMatrix_apply : ∀ (k : ℤ) {p : ℕ},
  p ≠ 0 →
    ∀ (j : ℕ) (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),
      (f ∣[k] heckeMatrix p j) τ = (↑p)⁻¹ * f (heckeMatrix p j • τ)

#check @ModularForm.slash_heckeDiagMatrix_apply slash_heckeDiagMatrix_apply : ∀ (k : ℤ) {p : ℕ},
  p ≠ 0 →
    ∀ (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),
      (f ∣[k] heckeDiagMatrix p) τ = ↑p ^ (k - 1) * f (heckeDiagMatrix p • τ)

--% env 3

Raw input

{"cmd": "-- L'action des repr\u00e9sentants sur \u03c4 \u2208 \u210d :\n#check @ModularForm.coe_heckeMatrix_smul       -- \u03b3_{p,j} \u2022 \u03c4 = (\u03c4 + j) / p\n#check @ModularForm.coe_heckeDiagMatrix_smul   -- diag \u2022 \u03c4 = p \u2022 \u03c4\n#check @ModularForm.denom_heckeMatrix          -- d\u00e9nominateur p\n#check @ModularForm.denom_heckeDiagMatrix      -- d\u00e9nominateur 1\n#check @ModularForm.\u03c3_heckeMatrix              -- caract\u00e8re \u03c3 trivial (det > 0)\n\n-- Les lectures du slash sur chaque famille :\n#check @ModularForm.slash_heckeMatrix_apply\n#check @ModularForm.slash_heckeDiagMatrix_apply", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@coe_heckeMatrix_smul : ∀ {p : ℕ}, p ≠ 0 → ∀ (j : ℕ) (τ : UpperHalfPlane), ↑(heckeMatrix p j • τ) = (↑τ + ↑j) / ↑p"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@coe_heckeDiagMatrix_smul : ∀ {p : ℕ}, p ≠ 0 → ∀ (τ : UpperHalfPlane), ↑(heckeDiagMatrix p • τ) = ↑p * ↑τ"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@denom_heckeMatrix : ∀ {p : ℕ}, p ≠ 0 → ∀ (j : ℕ) (τ : UpperHalfPlane), UpperHalfPlane.denom (heckeMatrix p j) ↑τ = ↑p"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@denom_heckeDiagMatrix : ∀ {p : ℕ}, p ≠ 0 → ∀ (τ : UpperHalfPlane), UpperHalfPlane.denom (heckeDiagMatrix p) ↑τ = 1"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "σ_heckeMatrix : ∀ (p j : ℕ), UpperHalfPlane.σ (heckeMatrix p j) = ContinuousAlgEquiv.refl ℝ ℂ"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "slash_heckeMatrix_apply : ∀ (k : ℤ) {p : ℕ},\n  p ≠ 0 →\n    ∀ (j : ℕ) (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),\n      (f ∣[k] heckeMatrix p j) τ = (↑p)⁻¹ * f (heckeMatrix p j • τ)"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "slash_heckeDiagMatrix_apply : ∀ (k : ℤ) {p : ℕ},\n  p ≠ 0 →\n    ∀ (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),\n      (f ∣[k] heckeDiagMatrix p) τ = ↑p ^ (k - 1) * f (heckeDiagMatrix p • τ)"}],
 "env": 3}

Lecture : deux comportements opposés du slash

Sortie obtenue : les homothéties $(\gamma_{p,j} \bullet \tau : \mathbb{C}) = (\tau + j)/p$ et $(\mathrm{diag} \bullet \tau : \mathbb{C}) = p \cdot \tau$, plus les deux lectures du slash.

Représentant	Action sur $\tau$	Slash de poids $k$ en $\tau$
$\gamma_{p,j}$ (triangulaire)	$(\tau + j)/p$ — $p$ translatées écrasées vers la pointe	$p^{-1} f\big((\tau+j)/p\big)$
diagonal	$p\,\tau$ — dilatation vers l’intérieur	$p^{k-1} f(p\,\tau)$

Points clés :

La partie $U$ contracte le voisinage de la pointe ($\tau \mapsto (\tau+j)/p$ envoie $\mathbb{H}$ proche de $0$), tandis que le diagonal l’étire ($\tau \mapsto p\tau$) — les deux morceaux de $T_p$ explorent des régions opposées du demi-plan ;
Le facteur de poids se loge entièrement dans le terme diagonal ($p^{k-1}$) : la partie triangulaire ne porte que $p^{-1}$, indépendant de $k$ ;
Ces lectures sont les seuls endroits du module où la formule générale du slash est effectivement calculée — en aval (heckeU_apply, heckeT_apply), tout s’exprime à partir d’elles.

Note technique : $\sigma$ trivial (σ_heckeMatrix) signifie pas de conjugaison supplémentaire — c’est une conséquence directe de la positivité du déterminant vue en section 2.

4. Les opérateurs $U_p$ et $T_p$

Les définitions tombent maintenant naturellement :

\[U_p f = \sum_{j=0}^{p-1} f \mid [k]\ \gamma_{p,j}, \qquad T_p f = U_p f + f \mid [k]\ \begin{pmatrix} p & 0 \\ 0 & 1 \end{pmatrix}\]

Le lake en donne trois niveaux de lecture : la définition (heckeU_def, heckeT_def, par sommes finies sur Finset.range p), la lecture ponctuelle (heckeU_apply, heckeT_apply — la valeur en un $\tau$ fixé) et le cas dégénéré heckeT_zero_left : pour $p = 0$, $T_0 = \mathrm{id}$. La linéarité en $f$ (heckeT_add, heckeT_smul, et leurs versions $U$) fait de chaque $T_p$ un endomorphisme de l’espace des fonctions $\mathbb{H} \to \mathbb{C}$ — le décor minimal pour une théorie spectrale des formes modulaires.

-- Les opérateurs, par leurs définitions et lectures ponctuelles :
#check @ModularForm.heckeU_def
#check @ModularForm.heckeT_def
#check @ModularForm.heckeU_apply
#check @ModularForm.heckeT_apply

-- Cas dégénéré p = 0 : T₀ est l'identité (lemme @[simp]).
#check @ModularForm.heckeT_zero_left

-- Certificat : la lecture ponctuelle de T_p est une preuve close.
#print axioms ModularForm.heckeT_apply

-- Les opérateurs, par leurs définitions et lectures ponctuelles :

#check @ModularForm.heckeU_def heckeU_def : ∀ (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ), heckeU k p f = ∑ j ∈ Finset.range p, f ∣[k] heckeMatrix p j

#check @ModularForm.heckeT_def heckeT_def : ∀ (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ),
  heckeT k p f = ∑ j ∈ Finset.range p, f ∣[k] heckeMatrix p j + f ∣[k] heckeDiagMatrix p

#check @ModularForm.heckeU_apply heckeU_apply : ∀ (k : ℤ) {p : ℕ},
  p ≠ 0 →
    ∀ (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),
      heckeU k p f τ = (↑p)⁻¹ * ∑ j ∈ Finset.range p, f (heckeMatrix p j • τ)

#check @ModularForm.heckeT_apply heckeT_apply : ∀ (k : ℤ) {p : ℕ},
  p ≠ 0 →
    ∀ (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),
      heckeT k p f τ = (↑p)⁻¹ * ∑ j ∈ Finset.range p, f (heckeMatrix p j • τ) + ↑p ^ (k - 1) * f (heckeDiagMatrix p • τ)

-- Cas dégénéré p = 0 : T₀ est l'identité (lemme @[simp]).

#check @ModularForm.heckeT_zero_left heckeT_zero_left : ∀ (k : ℤ) (f : UpperHalfPlane → ℂ), heckeT k 0 f = f

-- Certificat : la lecture ponctuelle de T_p est une preuve close.

#print axioms ModularForm.heckeT_apply 'ModularForm.heckeT_apply' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 4

Raw input

{"cmd": "-- Les op\u00e9rateurs, par leurs d\u00e9finitions et lectures ponctuelles :\n#check @ModularForm.heckeU_def\n#check @ModularForm.heckeT_def\n#check @ModularForm.heckeU_apply\n#check @ModularForm.heckeT_apply\n\n-- Cas d\u00e9g\u00e9n\u00e9r\u00e9 p = 0 : T\u2080 est l'identit\u00e9 (lemme @[simp]).\n#check @ModularForm.heckeT_zero_left\n\n-- Certificat : la lecture ponctuelle de T_p est une preuve close.\n#print axioms ModularForm.heckeT_apply", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "heckeU_def : ∀ (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ), heckeU k p f = ∑ j ∈ Finset.range p, f ∣[k] heckeMatrix p j"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "heckeT_def : ∀ (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ),\n  heckeT k p f = ∑ j ∈ Finset.range p, f ∣[k] heckeMatrix p j + f ∣[k] heckeDiagMatrix p"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "heckeU_apply : ∀ (k : ℤ) {p : ℕ},\n  p ≠ 0 →\n    ∀ (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),\n      heckeU k p f τ = (↑p)⁻¹ * ∑ j ∈ Finset.range p, f (heckeMatrix p j • τ)"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "heckeT_apply : ∀ (k : ℤ) {p : ℕ},\n  p ≠ 0 →\n    ∀ (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),\n      heckeT k p f τ = (↑p)⁻¹ * ∑ j ∈ Finset.range p, f (heckeMatrix p j • τ) + ↑p ^ (k - 1) * f (heckeDiagMatrix p • τ)"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "heckeT_zero_left : ∀ (k : ℤ) (f : UpperHalfPlane → ℂ), heckeT k 0 f = f"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 6},
   "data":
   "'ModularForm.heckeT_apply' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 4}

Lecture : la formule ponctuelle de $T_p$

Sortie obtenue : les définitions par sommes finies, et surtout heckeT_apply :

\[\big(T_p f\big)(\tau) = \frac{1}{p} \sum_{j=0}^{p-1} f\!\left(\frac{\tau + j}{p}\right) + p^{k-1} f(p\,\tau)\]

Terme	Origine géométrique
$p^{-1} \sum_j f\big((\tau+j)/p\big)$	la partie $U$ : $p$ translatées écrasées, facteur $1/p$ du dénominateur
$p^{k-1} f(p\tau)$	le diagonal : dilatation, facteur de poids du déterminant

Points clés :

Cette formule est démontrée, pas posée : heckeT_apply la déduit de la définition par sommes + les lectures du slash de la section 3 — et #print axioms atteste que la preuve est close ;
heckeT_zero_left fait de $p = 0$ un cas exact ($T_0 f = f$, refermé dans le lake par simp [heckeT] : la somme vide et le slash par l’identité restituent $f$) — la définition est robuste au cas dégénéré sans clause ad hoc ;
On voit ici la parenté avec l’opérateur $U_p$ des formes à niveau $p$ : heckeU_apply isole le premier terme — c’est l’opérateur qui, appliqué à une $q$-série, garde les coefficients d’indice multiple de $p$.

Exercice 2 — le cas dégénéré $T_0 = \mathrm{id}$

Prouvez en une seule tactique que $T_0$ est l’identité : l’énoncé heckeT k 0 f = f est exactement le lemme heckeT_zero_left du lake, déjà enregistré comme @[simp].

Indice : après unfolding automatique par simp, la somme sur Finset.range 0 est vide et le slash par l’identité (cas $p = 0$ de heckeDiagMatrix) restitue $f$.

-- Exercice 2 : le cas dégénéré T₀ = id.
--
-- Objectif : établir, pour tout poids k et toute fonction f,
--   ModularForm.heckeT k 0 f = f
-- TODO étudiant : à compléter (une seule tactique suffit).

#check @ModularForm.heckeT_zero_left   -- le lemme disponible

-- Exercice 2 : le cas dégénéré T₀ = id.

--

-- Objectif : établir, pour tout poids k et toute fonction f,

--   ModularForm.heckeT k 0 f = f

-- TODO étudiant : à compléter (une seule tactique suffit).

#check @ModularForm.heckeT_zero_left   -- le lemme disponible heckeT_zero_left : ∀ (k : ℤ) (f : UpperHalfPlane → ℂ), heckeT k 0 f = f

--% env 5

Raw input

{"cmd": "-- Exercice 2 : le cas d\u00e9g\u00e9n\u00e9r\u00e9 T\u2080 = id.\n--\n-- Objectif : \u00e9tablir, pour tout poids k et toute fonction f,\n--   ModularForm.heckeT k 0 f = f\n-- TODO \u00e9tudiant : \u00e0 compl\u00e9ter (une seule tactique suffit).\n\n#check @ModularForm.heckeT_zero_left   -- le lemme disponible", "env": 4}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "heckeT_zero_left : ∀ (k : ℤ) (f : UpperHalfPlane → ℂ), heckeT k 0 f = f"}],
 "env": 5}

Linéarité : des opérateurs, pas des transformations

La section d’après regroupe les théorèmes de linéarité — $T_p$ et $U_p$ commutent avec l’addition (heckeT_add, heckeU_add), la multiplication scalaire (heckeT_smul, heckeU_smul) et par conséquent la soustraction (heckeT_sub) et le passage à l’opposé (heckeT_neg). Techniquement, ces énoncés sont des conséquences de la structure du slash (SlashAction.add_slash, smul_slash) et de la linéarité des sommes finies — mais le lake les énonce et les prouve à la main pour chacun des deux opérateurs.

C’est ce qui autorise, en théorie des formes modulaires, la question spectrale : sur l’espace (de dimension finie) des formes modulaires de poids $k$, les $T_p$ commutent entre eux et diagonalisent simultanément — les valeurs propres $\lambda_p$ relient alors l’analyse (opérateurs) et l’arithmétique (coefficients, section 5).

-- La linéarité de T_p et U_p en l'argument :
#check @ModularForm.heckeT_add
#check @ModularForm.heckeU_add
#check @ModularForm.heckeT_smul
#check @ModularForm.heckeU_smul
#check @ModularForm.heckeT_neg
#check @ModularForm.heckeT_sub

-- La linéarité de T_p et U_p en l'argument :

#check @ModularForm.heckeT_add heckeT_add : ∀ (k : ℤ) (p : ℕ) (f g : UpperHalfPlane → ℂ), heckeT k p (f + g) = heckeT k p f + heckeT k p g

#check @ModularForm.heckeU_add heckeU_add : ∀ (k : ℤ) (p : ℕ) (f g : UpperHalfPlane → ℂ), heckeU k p (f + g) = heckeU k p f + heckeU k p g

#check @ModularForm.heckeT_smul heckeT_smul : ∀ (k : ℤ) (p : ℕ) (c : ℂ) (f : UpperHalfPlane → ℂ), heckeT k p (c • f) = c • heckeT k p f

#check @ModularForm.heckeU_smul heckeU_smul : ∀ (k : ℤ) (p : ℕ) (c : ℂ) (f : UpperHalfPlane → ℂ), heckeU k p (c • f) = c • heckeU k p f

#check @ModularForm.heckeT_neg heckeT_neg : ∀ (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ), heckeT k p (-f) = -heckeT k p f

#check @ModularForm.heckeT_sub heckeT_sub : ∀ (k : ℤ) (p : ℕ) (f g : UpperHalfPlane → ℂ), heckeT k p (f - g) = heckeT k p f - heckeT k p g

--% env 6

Raw input

{"cmd": "-- La lin\u00e9arit\u00e9 de T_p et U_p en l'argument :\n#check @ModularForm.heckeT_add\n#check @ModularForm.heckeU_add\n#check @ModularForm.heckeT_smul\n#check @ModularForm.heckeU_smul\n#check @ModularForm.heckeT_neg\n#check @ModularForm.heckeT_sub", "env": 5}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "heckeT_add : ∀ (k : ℤ) (p : ℕ) (f g : UpperHalfPlane → ℂ), heckeT k p (f + g) = heckeT k p f + heckeT k p g"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "heckeU_add : ∀ (k : ℤ) (p : ℕ) (f g : UpperHalfPlane → ℂ), heckeU k p (f + g) = heckeU k p f + heckeU k p g"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "heckeT_smul : ∀ (k : ℤ) (p : ℕ) (c : ℂ) (f : UpperHalfPlane → ℂ), heckeT k p (c • f) = c • heckeT k p f"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "heckeU_smul : ∀ (k : ℤ) (p : ℕ) (c : ℂ) (f : UpperHalfPlane → ℂ), heckeU k p (c • f) = c • heckeU k p f"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "heckeT_neg : ∀ (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ), heckeT k p (-f) = -heckeT k p f"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "heckeT_sub : ∀ (k : ℤ) (p : ℕ) (f g : UpperHalfPlane → ℂ), heckeT k p (f - g) = heckeT k p f - heckeT k p g"}],
 "env": 6}

Lecture : la structure d’endomorphisme

Sortie obtenue : six égalités fonctionnelles — pour $T_p$ et $U_p$, la compatibilité avec +, •, - (unaire et binaire).

Théorème	Énoncé informel
`heckeT_add` / `heckeU_add`	$T_p(f+g) = T_p f + T_p g$
`heckeT_smul` / `heckeU_smul`	$T_p(c \cdot f) = c \cdot T_p f$
`heckeT_neg`, `heckeT_sub`	conséquences : opposé et différence

Points clés :

La preuve de heckeT_add mélange heckeU_add et SlashAction.add_slash puis referme par abel — un exemple représentatif du style du module : réutiliser les briques Mathlib, ne jamais re-démontrer la structure ;
Ces énoncés portent sur des fonctions arbitraires : aucune régularité ni modularité — la restriction aux formes modulaires (stabilité de $T_p$) est un théorème plus profond, hors périmètre du lake ;
heckeU_smul est prouvé par simp sur la définition — contraste utile avec heckeT_smul (un rw explicite) : même énoncé, poids de preuve différent selon l’opérateur.

5. La formule des coefficients : la combinatoire de $T_p$

Si $f(\tau) = \sum_{n \geq 0} a(n)\, q^n$ (avec $q = e^{2\pi i \tau}$), l’action de $T_p$ sur la suite $a$ se lit termes à termes — c’est le théorème combinatoire du module :

\[\big(T_p f\big)_n = a(np) + \begin{cases} p^{k-1}\, a(n/p) & \text{si } p \mid n \\ 0 & \text{sinon} \end{cases}\]

Le lake encode cette formule par une définition (coeffHeckeT) et deux lectures conditionnelles démontrées (coeffHeckeT_of_dvd, coeffHeckeT_of_not_dvd). La partie $U$ correspond à l’échantillonnage pur coeffHeckeU p a n = a (n * p) — un simple « prélèvement » d’un coefficient sur $p$, sans aucun facteur.

La section Examples du lake (absente du dépôt amont) exécute cette formule sur la suite $a(n) = n$ au poids $k = 12$ — le poids de la forme modulaire discriminant $\Delta$. Les cellules qui suivent les reproduisent en-kernel puis les étendent.

-- La formule des coefficients et ses lectures conditionnelles :
#check @ModularForm.coeffHeckeT_apply
#check @ModularForm.coeffHeckeT_of_dvd      -- p ∣ n : les DEUX termes
#check @ModularForm.coeffHeckeT_of_not_dvd  -- p ∤ n : échantillonnage seul
#check @ModularForm.coeffHeckeU_apply

-- Exemples calculables (section Examples du lake), pour a n = n et k = 12 :
example : coeffHeckeU 2 (fun n => (n : ℂ)) 3 = 6 := rfl

example : coeffHeckeT 12 2 (fun n => (n : ℂ)) 1 = 2 := by
  have h : ¬ (2 : ℕ) ∣ 1 := by decide
  simp only [coeffHeckeT, if_neg h]
  norm_num

example : coeffHeckeT 12 2 (fun n => (n : ℂ)) 2 = 4 + 2 ^ 11 := by
  have h : (2 : ℕ) ∣ 2 := by decide
  simp only [coeffHeckeT, if_pos h]
  norm_num

example : coeffHeckeT 12 3 (fun n => (n : ℂ)) 3 = 9 + 3 ^ 11 := by
  have h : (3 : ℕ) ∣ 3 := by decide
  simp only [coeffHeckeT, if_pos h]
  norm_num

-- La formule des coefficients et ses lectures conditionnelles :

#check @ModularForm.coeffHeckeT_apply coeffHeckeT_apply : ∀ (k : ℤ) (p : ℕ) (a : ℕ → ℂ) (n : ℕ),
  coeffHeckeT k p a n = a (n * p) + if p ∣ n then ↑p ^ (k - 1) * a (n / p) else 0

#check @ModularForm.coeffHeckeT_of_dvd      -- p ∣ n : les DEUX termes coeffHeckeT_of_dvd : ∀ (k : ℤ) {p n : ℕ},
  p ∣ n → ∀ (a : ℕ → ℂ), coeffHeckeT k p a n = a (n * p) + ↑p ^ (k - 1) * a (n / p)

#check @ModularForm.coeffHeckeT_of_not_dvd  -- p ∤ n : échantillonnage seul coeffHeckeT_of_not_dvd : ∀ (k : ℤ) {p n : ℕ}, ¬p ∣ n → ∀ (a : ℕ → ℂ), coeffHeckeT k p a n = a (n * p)

#check @ModularForm.coeffHeckeU_apply coeffHeckeU_apply : ∀ (p : ℕ) (a : ℕ → ℂ) (n : ℕ), coeffHeckeU p a n = a (n * p)

-- Exemples calculables (section Examples du lake), pour a n = n et k = 12 :

example : coeffHeckeU 2 (fun n => (n : ℂ)) 3 = 6 := rfl

example : coeffHeckeT 12 2 (fun n => (n : ℂ)) 1 = 2 := by

  have h : ¬ (2 : ℕ) ∣ 1 := by decide

  simp only [coeffHeckeT, if_neg h]

  norm_num

example : coeffHeckeT 12 2 (fun n => (n : ℂ)) 2 = 4 + 2 ^ 11 := by

  have h : (2 : ℕ) ∣ 2 := by decide

  simp only [coeffHeckeT, if_pos h]

  norm_num

example : coeffHeckeT 12 3 (fun n => (n : ℂ)) 3 = 9 + 3 ^ 11 := by

  have h : (3 : ℕ) ∣ 3 := by decide

  simp only [coeffHeckeT, if_pos h]

  norm_num

--% env 7

Raw input

{"cmd": "-- La formule des coefficients et ses lectures conditionnelles :\n#check @ModularForm.coeffHeckeT_apply\n#check @ModularForm.coeffHeckeT_of_dvd      -- p \u2223 n : les DEUX termes\n#check @ModularForm.coeffHeckeT_of_not_dvd  -- p \u2224 n : \u00e9chantillonnage seul\n#check @ModularForm.coeffHeckeU_apply\n\n-- Exemples calculables (section Examples du lake), pour a n = n et k = 12 :\nexample : coeffHeckeU 2 (fun n => (n : \u2102)) 3 = 6 := rfl\n\nexample : coeffHeckeT 12 2 (fun n => (n : \u2102)) 1 = 2 := by\n  have h : \u00ac (2 : \u2115) \u2223 1 := by decide\n  simp only [coeffHeckeT, if_neg h]\n  norm_num\n\nexample : coeffHeckeT 12 2 (fun n => (n : \u2102)) 2 = 4 + 2 ^ 11 := by\n  have h : (2 : \u2115) \u2223 2 := by decide\n  simp only [coeffHeckeT, if_pos h]\n  norm_num\n\nexample : coeffHeckeT 12 3 (fun n => (n : \u2102)) 3 = 9 + 3 ^ 11 := by\n  have h : (3 : \u2115) \u2223 3 := by decide\n  simp only [coeffHeckeT, if_pos h]\n  norm_num", "env": 6}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "coeffHeckeT_apply : ∀ (k : ℤ) (p : ℕ) (a : ℕ → ℂ) (n : ℕ),\n  coeffHeckeT k p a n = a (n * p) + if p ∣ n then ↑p ^ (k - 1) * a (n / p) else 0"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "coeffHeckeT_of_dvd : ∀ (k : ℤ) {p n : ℕ},\n  p ∣ n → ∀ (a : ℕ → ℂ), coeffHeckeT k p a n = a (n * p) + ↑p ^ (k - 1) * a (n / p)"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "coeffHeckeT_of_not_dvd : ∀ (k : ℤ) {p n : ℕ}, ¬p ∣ n → ∀ (a : ℕ → ℂ), coeffHeckeT k p a n = a (n * p)"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "coeffHeckeU_apply : ∀ (p : ℕ) (a : ℕ → ℂ) (n : ℕ), coeffHeckeU p a n = a (n * p)"}],
 "env": 7}

Lecture : les quatre calculs

Sortie obtenue : les quatre signatures d’en-tête (coeffHeckeT_apply, coeffHeckeT_of_dvd, coeffHeckeT_of_not_dvd, coeffHeckeU_apply) — puis rien : chaque example est une égalité close que Lean valide en silence. Une cellule d’exemples qui échoue produit une erreur ; une cellule qui réussit ne produit que les sorties explicites de ses #check.

Énoncé	Cas	Valeur
`coeffHeckeU 2 a 3 = 6`	échantillonnage	$a(6) = 6$, `rfl` pur
`coeffHeckeT 12 2 a 1 = 2`	$2 \nmid 1$	$a(2) = 2$ seul
`coeffHeckeT 12 2 a 2 = 4 + 2¹¹`	$2 \mid 2$	$a(4) + 2^{11} a(1)$
`coeffHeckeT 12 3 a 3 = 9 + 3¹¹`	$3 \mid 3$	$a(9) + 3^{11} a(1)$

Points clés :

Le premier exemple se referme par rfl : l’échantillonnage est une égalité définitionnelle — le compilateur la voit par simple unfolding, sans tactique ;
Les autres suivent le schéma du lake : décider de la divisibilité (decide), réécrire la conditionnelle (if_pos / if_neg), refermer l’arithmétique (norm_num) ;
Le poids $k = 12$ fait apparaître $2^{11}$ et $3^{11}$ — au poids 12, le facteur diagonal domine largement le terme d’échantillonnage (cf. section suivante).

Note technique : ces example sont anonymes — ils ne déclarent pas de nom dans l’environnement. Pour les citer (ou vérifier leurs axiomes), il faudrait les nommer theorem ; le lake a fait ce choix pour sa section Examples, ce notebook les garde jetables.

L’ordre de grandeur du facteur diagonal

La formule des coefficients fait coexister deux termes d’échelles très différentes : l’échantillonnage $a(np)$ croît linéairement en $p$ (pour $a(n) = n$), quand le facteur diagonal $p^{k-1}$ croît exponentiellement. Au poids $k = 12$, la cellule suivante calcule les valeurs exactes de $p^{11}$ pour $p = 2, 3, 5$, et la valeur $1 + 2^{11}$ — la valeur du second exemple divisible du lake (branche $p \mid n$), prise sur la suite $a \equiv 1$ à $n = 2$ (le lake la démontre : coeffHeckeT 12 2 (fun _ => 1) 2 = 1 + 2 ^ 11 ; la suite constante n’est pas une suite propre de $T_2$ au sens global — c’est la valeur de cet exemple, pas une valeur propre).

-- L'ordre de grandeur du facteur diagonal p^{k-1} au poids k = 12 :
#eval 2 ^ 11      -- facteur diagonal de T₂
#eval 3 ^ 11      -- facteur diagonal de T₃
#eval 5 ^ 11      -- facteur diagonal de T₅
#eval 1 + 2 ^ 11  -- second exemple divisible : suite a ≡ 1, n = 2 (branche 2 ∣ 2)

-- L'ordre de grandeur du facteur diagonal p^{k-1} au poids k = 12 :

#eval 2 ^ 11      -- facteur diagonal de T₂ 2048

#eval 3 ^ 11      -- facteur diagonal de T₃ 177147

#eval 5 ^ 11      -- facteur diagonal de T₅ 48828125

#eval 1 + 2 ^ 11  -- second exemple divisible : suite a ≡ 1, n = 2 (branche 2 ∣ 2) 2049

--% env 8

Raw input

{"cmd": "-- L'ordre de grandeur du facteur diagonal p^{k-1} au poids k = 12 :\n#eval 2 ^ 11      -- facteur diagonal de T\u2082\n#eval 3 ^ 11      -- facteur diagonal de T\u2083\n#eval 5 ^ 11      -- facteur diagonal de T\u2085\n#eval 1 + 2 ^ 11  -- second exemple divisible : suite a \u2261 1, n = 2 (branche 2 \u2223 2)", "env": 7}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 5},
   "data": "2048"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 5},
   "data": "177147"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 5},
   "data": "48828125"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 5},
   "data": "2049"}],
 "env": 8}

Lecture : $p^{k-1}$ écrase l’échantillonnage

Sortie obtenue : quatre naturels calculés par le compilateur — 2048, 177147, 48828125, 2049.

Grandeur	Valeur	Signification
$2^{11}$	2 048	facteur diagonal de $T_2$ au poids 12
$3^{11}$	177 147	facteur diagonal de $T_3$
$5^{11}$	48 828 125	facteur diagonal de $T_5$
$1 + 2^{11}$	2 049	second exemple divisible : suite $a \equiv 1$, $n = 2$ (branche $2 \mid 2$)

Points clés :

Pour la forme discriminant $\Delta(\tau) = \sum \tau(n)\, q^n$ (poids 12, normalisée : $a(1) = 1$), $\Delta$ est forme propre de $T_2$ avec $\lambda_2 = \tau(2) = -24$. La formule à $n = 2$ impose alors $\tau(4) + 2^{11} \cdot a(1) = \lambda_2\, a(2)$, c’est-à-dire $\tau(4) + 2048 = (-24)^2 = 576$, soit $\tau(4) = -1472$ — exactement la valeur de Ramanujan. Le pont « forme propre » n’est pas prouvé dans le lake, mais le calcul colle à la théorie ;
La croissance exponentielle de $p^{k-1}$ est la marque du poids : c’est elle qui empêche les coefficients de Hecke d’être bornés indépendamment de $k$ ;
Ces #eval sont des calculs décidables sur ℕ — à distinguer des example sur ℂ de la section précédente, refermés par preuve et non par évaluation ($\mathbb{C}$ est non calculable en kernel).

Exercice 3 — $T_5$ au poids 12 sur un indice divisible

Étendez le calcul au cas $p = 5$, $n = 10$ (avec $5 \mid 10$) : l’énoncé attendu est $\texttt{coeffHeckeT}\ 12\ 5\ a\ 10 = 50 + 5^{11} \cdot 2$ — c’est-à-dire $a(10 \cdot 5) + 5^{11} a(10/5)$.

Indice : même schéma que les exemples de la section — decide pour $5 \mid 10$, if_pos pour choisir la branche, norm_num pour l’arithmétique.

-- Exercice 3 : T₅ au poids 12 sur la suite a n = n, pour n = 10 (5 ∣ 10).
--
-- Objectif : établir
--   ModularForm.coeffHeckeT 12 5 (fun n => (n : ℂ)) 10 = 50 + 5 ^ 11 * 2
-- TODO étudiant : à compléter (même schéma que les exemples de la section 5).

#check @ModularForm.coeffHeckeT_of_dvd   -- le lemme à invoquer

-- Exercice 3 : T₅ au poids 12 sur la suite a n = n, pour n = 10 (5 ∣ 10).

--

-- Objectif : établir

--   ModularForm.coeffHeckeT 12 5 (fun n => (n : ℂ)) 10 = 50 + 5 ^ 11 * 2

-- TODO étudiant : à compléter (même schéma que les exemples de la section 5).

#check @ModularForm.coeffHeckeT_of_dvd   -- le lemme à invoquer coeffHeckeT_of_dvd : ∀ (k : ℤ) {p n : ℕ},
  p ∣ n → ∀ (a : ℕ → ℂ), coeffHeckeT k p a n = a (n * p) + ↑p ^ (k - 1) * a (n / p)

--% env 9

Raw input

{"cmd": "-- Exercice 3 : T\u2085 au poids 12 sur la suite a n = n, pour n = 10 (5 \u2223 10).\n--\n-- Objectif : \u00e9tablir\n--   ModularForm.coeffHeckeT 12 5 (fun n => (n : \u2102)) 10 = 50 + 5 ^ 11 * 2\n-- TODO \u00e9tudiant : \u00e0 compl\u00e9ter (m\u00eame sch\u00e9ma que les exemples de la section 5).\n\n#check @ModularForm.coeffHeckeT_of_dvd   -- le lemme \u00e0 invoquer", "env": 8}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "coeffHeckeT_of_dvd : ∀ (k : ℤ) {p n : ℕ},\n  p ∣ n → ∀ (a : ℕ → ℂ), coeffHeckeT k p a n = a (n * p) + ↑p ^ (k - 1) * a (n / p)"}],
 "env": 9}

6. La première route : Kummer, ou quand la factorialité remplace la preuve

Le lake porte deux routes vers Fermat, et ce compagnon n’en avait visité qu’une moitié : les opérateurs des sections 2 à 5 sont la mécanique de la route moderne (section 7). Les trois modules SevenPid.lean, ElevenPid.lean et ThirteenPid.lean portent la route historique, celle de Kummer au XIXe siècle.

L’idée de Kummer part de la factorisation dans $\mathbb{Z}[\zeta_p]$ :

\[x^p + y^p = \prod_{j=0}^{p-1} (x + \zeta_p^{\,j}\, y),\]

qui décompose l’équation de Fermat en un produit d’idéaux. Si l’anneau des entiers $\mathcal{O}_K = \mathbb{Z}[\zeta_p]$ du corps cyclotomique $K = \mathbb{Q}(\zeta_p)$ est principal, la factorialité des idéaux se transporte aux éléments et l’argument d’Euclide (descente par divisibilité) se referme — c’est ainsi que Kummer démontre Fermat pour les premiers réguliers. La question devient arithmétique : pour quels premiers $p$ l’anneau $\mathbb{Z}[\zeta_p]$ est-il principal ? Le lake y répond pour les trois premiers difficiles $p = 7$, $11$, $13$ — les cas $p = 3, 5$ étant déjà dans Mathlib (borne de Minkowski trop petite pour laisser passer un idéal non principal).

Le même critère, trois exécutions de difficulté croissante. Les trois modules emploient le critère de Marcus (Number Fields, discussion après le théorème 37) : $\mathcal{O}_K$ est principal dès que tout idéal premier $P$ au-dessus d’un premier $p$ avec $p^f \leq \lfloor M K \rfloor$ ($f$ le degré d’inertie) est principal. Ce qui change d’un module à l’autre, c’est la partie entière de la borne de Minkowski — $4$, puis $58$, puis $307$ — et donc le nombre de premiers à éliminer un à un.

Module	$\lfloor M K \rfloor$	Premiers exigeant un certificat	Moyen
`SevenPid`	$4$	aucun ($2^3 > 4$, $3^6 > 4$)	degrés d’inertie seuls
`ElevenPid`	$58$	$11$ (ramifié), $23$	générateur explicite $\alpha = \zeta^3 + \zeta + 1$
`ThirteenPid`	$< 307$	$3$, $13$, $53$, $79$, $131$, $157$	corps de certificats $\mathbb{F}_{27}$ + quatre tranches

-- Premier maillon : Z[zeta_7] est principal, par élimination pure.
#check @CyclotomicPID.floor_M_seven            -- ⌊M K⌋₊ = 4 : la borne ne laisse passer que p ≤ 4
#check @CyclotomicPID.orderOf_two_zmod_seven   -- ordre de 2 dans (ZMod 7)ˣ : 3
#check @CyclotomicPID.orderOf_three_zmod_seven -- ordre de 3 dans (ZMod 7)ˣ : 6

-- Ces ordres sont des faits décidés par le noyau, pas des hypothèses :
example : (2 : ZMod 7) ^ 3 = 1 := by decide
example : (2 : ZMod 7) ^ 1 ≠ 1 ∧ (2 : ZMod 7) ^ 2 ≠ 1 := by decide
example : (3 : ZMod 7) ^ 6 = 1 := by decide

-- Le bilan : l'anneau des entiers de Q(zeta_7) est principal.
#check @CyclotomicPID.seven_pid
#print axioms CyclotomicPID.seven_pid

-- Premier maillon : Z[zeta_7] est principal, par élimination pure.

#check @CyclotomicPID.floor_M_seven            -- ⌊M K⌋₊ = 4 : la borne ne laisse passer que p ≤ 4 @CyclotomicPID.floor_M_seven : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [IsCyclotomicExtension {7} ℚ K],
  ⌊(4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
        (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|)⌋₊ =
    4

#check @CyclotomicPID.orderOf_two_zmod_seven   -- ordre de 2 dans (ZMod 7)ˣ : 3 CyclotomicPID.orderOf_two_zmod_seven : orderOf ↑2 = 3

#check @CyclotomicPID.orderOf_three_zmod_seven -- ordre de 3 dans (ZMod 7)ˣ : 6 CyclotomicPID.orderOf_three_zmod_seven : orderOf ↑3 = 6

-- Ces ordres sont des faits décidés par le noyau, pas des hypothèses :

example : (2 : ZMod 7) ^ 3 = 1 := by decide

example : (2 : ZMod 7) ^ 1 ≠ 1 ∧ (2 : ZMod 7) ^ 2 ≠ 1 := by decide

example : (3 : ZMod 7) ^ 6 = 1 := by decide

-- Le bilan : l'anneau des entiers de Q(zeta_7) est principal.

#check @CyclotomicPID.seven_pid CyclotomicPID.seven_pid : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [IsCyclotomicExtension {7} ℚ K],
  IsPrincipalIdealRing (NumberField.RingOfIntegers K)

#print axioms CyclotomicPID.seven_pid 'CyclotomicPID.seven_pid' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 10

Raw input

{"cmd": "-- Premier maillon : Z[zeta_7] est principal, par \u00e9limination pure.\n#check @CyclotomicPID.floor_M_seven            -- \u230aM K\u230b\u208a = 4 : la borne ne laisse passer que p \u2264 4\n#check @CyclotomicPID.orderOf_two_zmod_seven   -- ordre de 2 dans (ZMod 7)\u02e3 : 3\n#check @CyclotomicPID.orderOf_three_zmod_seven -- ordre de 3 dans (ZMod 7)\u02e3 : 6\n\n-- Ces ordres sont des faits d\u00e9cid\u00e9s par le noyau, pas des hypoth\u00e8ses :\nexample : (2 : ZMod 7) ^ 3 = 1 := by decide\nexample : (2 : ZMod 7) ^ 1 \u2260 1 \u2227 (2 : ZMod 7) ^ 2 \u2260 1 := by decide\nexample : (3 : ZMod 7) ^ 6 = 1 := by decide\n\n-- Le bilan : l'anneau des entiers de Q(zeta_7) est principal.\n#check @CyclotomicPID.seven_pid\n#print axioms CyclotomicPID.seven_pid", "env": 9}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@CyclotomicPID.floor_M_seven : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]\n  [IsCyclotomicExtension {7} ℚ K],\n  ⌊(4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *\n        (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|)⌋₊ =\n    4"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data": "CyclotomicPID.orderOf_two_zmod_seven : orderOf ↑2 = 3"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data": "CyclotomicPID.orderOf_three_zmod_seven : orderOf ↑3 = 6"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 6},
   "data":
   "CyclotomicPID.seven_pid : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [IsCyclotomicExtension {7} ℚ K],\n  IsPrincipalIdealRing (NumberField.RingOfIntegers K)"},
  {"severity": "info",
   "pos": {"line": 13, "column": 0},
   "endPos": {"line": 13, "column": 6},
   "data":
   "'CyclotomicPID.seven_pid' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 10}

Lecture : une élimination complète, sans un seul générateur

Sortie obtenue : la borne de Minkowski à valeur exacte 4, les deux ordres dans $(\mathbb{Z}/7\mathbb{Z})^\times$, trois égalités décidées par le noyau, puis le théorème seven_pid et son certificat d’axiomes.

Fait	Rôle dans la preuve
$\lfloor M K \rfloor = 4$	le critère de Marcus ne regarde que $p \in \{1, \ldots, 4\}$
$2$ d’ordre $3$	degré d’inertie $f = 3$ au-dessus de $2$ : $2^3 = 8 > 4$
$3$ d’ordre $6$	degré d’inertie $f = 6$ au-dessus de $3$ : $3^6 > 4$

Points clés : 1. Le degré d’inertie d’un premier au-dessus de $q$ dans $\mathbb{Q}(\zeta_m)$ ($q \nmid m$) est l’ordre de $q$ dans $(\mathbb{Z}/m\mathbb{Z})^\times$ : c’est le pont orderOf_two_zmod_seven ↔︎ inertiaDeg_eq_of_not_dvd ; 2. $1$ et $4$ ne sont pas premiers : l’intervalle est épuisé, la preuve tient en une page ; 3. les trois example ... := by decide sont le noyau qui calcule dans $\mathbb{Z}/7\mathbb{Z}$ : le fait $2^3 = 1$ avec $2^1, 2^2 \neq 1$ est l’ordre 3 rendu mécanique, et le #print axioms ne montre que les axiomes standards — la factorialité de $\mathbb{Z}[\zeta_7]$ est une preuve close, du critère de Marcus à l’encadrement de $\pi$ à 20 décimales (floor_minkowskiBound_seven dans le module).

-- Deuxième maillon : la borne monte à 58, et un premier résiste — 23.
#check @CyclotomicPID.M11                                  -- ⌊M K⌋₊ = 58
#check @CyclotomicPID.not_pow_orderOf_le                   -- l'éliminateur générique par degré d'inertie

-- Le générateur explicite au-dessus de 23 : α = ζ³ + ζ + 1, avec α · β = 23.
#check @CyclotomicPID.isPrincipal_of_liesOver_twentythree

#check @CyclotomicPID.eleven_pid
#print axioms CyclotomicPID.eleven_pid

-- Deuxième maillon : la borne monte à 58, et un premier résiste — 23.

#check @CyclotomicPID.M11                                  -- ⌊M K⌋₊ = 58 @CyclotomicPID.M11 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] [hK : IsCyclotomicExtension {11} ℚ K],
  ⌊(4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
        (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|)⌋₊ =
    58

#check @CyclotomicPID.not_pow_orderOf_le                   -- l'éliminateur générique par degré d'inertie @CyclotomicPID.not_pow_orderOf_le : ∀ {a : ZMod 11} {p B : ℕ} (k : ℕ),
  a ^ 10 = 1 → 0 < p → B < p ^ (k + 1) → (∀ i ∈ Finset.Icc 1 k, a ^ i ≠ 1) → ¬p ^ orderOf a ≤ B

-- Le générateur explicite au-dessus de 23 : α = ζ³ + ζ + 1, avec α · β = 23.

#check @CyclotomicPID.isPrincipal_of_liesOver_twentythree @CyclotomicPID.isPrincipal_of_liesOver_twentythree : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {11} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP : P.IsPrime]
  [hP23 : P.LiesOver (Ideal.span {23})], Submodule.IsPrincipal P

#check @CyclotomicPID.eleven_pid CyclotomicPID.eleven_pid : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {11} ℚ K], IsPrincipalIdealRing (NumberField.RingOfIntegers K)

#print axioms CyclotomicPID.eleven_pid 'CyclotomicPID.eleven_pid' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 11

Raw input

{"cmd": "-- Deuxi\u00e8me maillon : la borne monte \u00e0 58, et un premier r\u00e9siste \u2014 23.\n#check @CyclotomicPID.M11                                  -- \u230aM K\u230b\u208a = 58\n#check @CyclotomicPID.not_pow_orderOf_le                   -- l'\u00e9liminateur g\u00e9n\u00e9rique par degr\u00e9 d'inertie\n\n-- Le g\u00e9n\u00e9rateur explicite au-dessus de 23 : \u03b1 = \u03b6\u00b3 + \u03b6 + 1, avec \u03b1 \u00b7 \u03b2 = 23.\n#check @CyclotomicPID.isPrincipal_of_liesOver_twentythree\n\n#check @CyclotomicPID.eleven_pid\n#print axioms CyclotomicPID.eleven_pid", "env": 10}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@CyclotomicPID.M11 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] [hK : IsCyclotomicExtension {11} ℚ K],\n  ⌊(4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *\n        (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|)⌋₊ =\n    58"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@CyclotomicPID.not_pow_orderOf_le : ∀ {a : ZMod 11} {p B : ℕ} (k : ℕ),\n  a ^ 10 = 1 → 0 < p → B < p ^ (k + 1) → (∀ i ∈ Finset.Icc 1 k, a ^ i ≠ 1) → ¬p ^ orderOf a ≤ B"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "@CyclotomicPID.isPrincipal_of_liesOver_twentythree : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]\n  [hK : IsCyclotomicExtension {11} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP : P.IsPrime]\n  [hP23 : P.LiesOver (Ideal.span {23})], Submodule.IsPrincipal P"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "CyclotomicPID.eleven_pid : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]\n  [hK : IsCyclotomicExtension {11} ℚ K], IsPrincipalIdealRing (NumberField.RingOfIntegers K)"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "'CyclotomicPID.eleven_pid' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 11}

Lecture : le générateur explicite au-dessus de 23

Sortie obtenue : la borne M11 à 58, le lemme générique not_pow_orderOf_le, le théorème isPrincipal_of_liesOver_twentythree, puis le bilan eleven_pid.

Ce qui rend $p = 11$ plus difficile que $p = 7$ : cette fois, un premier échappe à l’élimination par degré d’inertie. Le premier $23$ vérifie $23^1 \leq 58$ (inertie totale, $f = 1$), donc le critère de Marcus exige de lui un générateur. Le module en exhibe un, calculé :

le morphisme $\varphi : \mathbb{Z}[\zeta_{11}] \to \mathbb{Z}/23\mathbb{Z}$ envoyant $\zeta_{11} \mapsto 4$ a pour noyau l’idéal engendré par $\alpha = \zeta^3 + \zeta + 1$ ;
deux identités vérifiées par linear_combination contre la relation cyclotomique : $\alpha \cdot \beta = 23$ et $\alpha \cdot \gamma = \zeta - 4$, avec $\beta$ et $\gamma$ des polynômes explicites en $\zeta$ de degré $\leq 9$ à coefficients entiers ;
un argument galoisien transporte ce générateur à tout idéal au-dessus de $23$.

Point clé : l’élimination générique not_pow_orderOf_le — si $a$ est d’ordre $> k$ dans $(\mathbb{Z}/11\mathbb{Z})^\times$, alors $p^{\mathrm{ord}(a)} > B$ pour toute borne $B < p^{k+1}$ — est ce qui permet d’écarter les autres premiers une tactique chacun, au lieu d’un lemme par premier : c’est la différence entre le cas $p = 7$ (deux ordres suffisent) et le cas $p = 11$ (une quinzaine de premiers à passer au crible).

Exercice 4 — l’ordre de 2 dans $(\mathbb{Z}/11\mathbb{Z})^\times$

Le lemme not_pow_orderOf_le élimine les premiers de $\mathbb{Q}(\zeta_{11})$ par les ordres dans $(\mathbb{Z}/11\mathbb{Z})^\times$. Établissez le premier d’entre eux :

\[\mathrm{ord}(2) = 10 \quad \text{dans } (\mathbb{Z}/11\mathbb{Z})^\times\]

autrement dit : 2 est une racine primitive modulo 11. Les deux égalités décidées de la cellule ci-dessous donnent l’ancrage numérique ($2^5 \equiv -1 \neq 1$ et $2^{10} = 1$) ; le gabarit de preuve est orderOf_two_zmod_seven : orderOf_eq_iff, puis interval_cases sur les exposants intermédiaires, chaque cas refermé par decide.

-- Exercice 4 : l'ordre de 2 dans (ZMod 11)ˣ.
--
-- Objectif : établir
--   orderOf ((2 : ℕ) : ZMod 11) = 10
-- TODO étudiant : à compléter (gabarit : orderOf_two_zmod_seven).

example : (2 : ZMod 11) ^ 5 ≠ 1 := by decide   -- le noyau décide l'ancrage : 2⁵ ≡ -1
example : (2 : ZMod 11) ^ 10 = 1 := by decide  -- et 2¹⁰ retombe sur 1
#check @CyclotomicPID.orderOf_two_zmod_seven   -- le schéma à transposer de 7 vers 11

-- Exercice 4 : l'ordre de 2 dans (ZMod 11)ˣ.

--

-- Objectif : établir

--   orderOf ((2 : ℕ) : ZMod 11) = 10

-- TODO étudiant : à compléter (gabarit : orderOf_two_zmod_seven).

example : (2 : ZMod 11) ^ 5 ≠ 1 := by decide   -- le noyau décide l'ancrage : 2⁵ ≡ -1

example : (2 : ZMod 11) ^ 10 = 1 := by decide  -- et 2¹⁰ retombe sur 1

#check @CyclotomicPID.orderOf_two_zmod_seven   -- le schéma à transposer de 7 vers 11 CyclotomicPID.orderOf_two_zmod_seven : orderOf ↑2 = 3

--% env 12

Raw input

{"cmd": "-- Exercice 4 : l'ordre de 2 dans (ZMod 11)\u02e3.\n--\n-- Objectif : \u00e9tablir\n--   orderOf ((2 : \u2115) : ZMod 11) = 10\n-- TODO \u00e9tudiant : \u00e0 compl\u00e9ter (gabarit : orderOf_two_zmod_seven).\n\nexample : (2 : ZMod 11) ^ 5 \u2260 1 := by decide   -- le noyau d\u00e9cide l'ancrage : 2\u2075 \u2261 -1\nexample : (2 : ZMod 11) ^ 10 = 1 := by decide  -- et 2\u00b9\u2070 retombe sur 1\n#check @CyclotomicPID.orderOf_two_zmod_seven   -- le sch\u00e9ma \u00e0 transposer de 7 vers 11", "env": 11}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data": "CyclotomicPID.orderOf_two_zmod_seven : orderOf ↑2 = 3"}],
 "env": 12}

Troisième maillon : $p = 13$ et le corps de certificats $\mathbb{F}_{27}$

La borne monte encore — l’élimination passe par un corps fini.

-- Troisième maillon : Z[zeta_13]. Ici le corps de certificats est construit.
#check @CyclotomicPID.M3dS11.g3_irreducible                -- X³ - X - 1 irréductible sur 𝔽₃
#check @CyclotomicPID.M3dS11.F27_charP                      -- F₂₇ = AdjoinRoot g3 : caractéristique 3
#check @CyclotomicPID.M3dS11.isPrincipal_of_liesOver_three  -- générateur : image galoisienne de 1 + ζ - ζ³

-- La borne monte encore, et l'élimination se fait en quatre tranches :
#check @CyclotomicPID.M3aS12.M13        -- ⌊M K⌋₊ < 307
#check @CyclotomicPID.M3aS12.dispatchA  -- tranche {2, …, 80}
#check @CyclotomicPID.M3aS12.dispatchB  -- tranche {81, …, 160}
#check @CyclotomicPID.M3aS12.dispatchC  -- tranche {161, …, 240}
#check @CyclotomicPID.M3aS12.dispatchD  -- tranche {241, …, 306}

#check @CyclotomicPID.M3aS12.thirteen_pid
#print axioms CyclotomicPID.M3aS12.thirteen_pid

Lecture : le corps de certificats $\mathbb{F}_{27}$ et les quatre tranches

Sortie obtenue : l’irréductibilité de $X^3 - X - 1$ sur $\mathbb{F}_3$, la caractéristique du corps $\mathbb{F}_{27}$ construit comme AdjoinRoot g3, la principauté au-dessus de 3, la borne $M13 < 307$, les quatre dispatch, puis le bilan thirteen_pid.

La nouveauté de $p = 13$ tient en deux gestes :

Un corps de certificats. Pour prouver que les idéaux au-dessus de $3$ sont principaux, la preuve construit $\mathbb{F}_{27} = \mathbb{F}_3[X]/(X^3 - X - 1)$ — un objet défini dans le module (g3, F27, F27_charP) — et vérifie que l’image de $\zeta_{13}$ dans ce corps engendre le noyau du morphisme de réduction, avec pour générateur d’idéal l’image galoisienne de $1 + \zeta - \zeta^3$. Le certificat n’est plus une identité entre polynômes en $\zeta$ : c’est un corps fini construit pour l’occasion ;
Quatre tranches d’interval_cases. Avec $\lfloor M K \rfloor < 307$, le nombre de premiers à écarter dépasse la centaine : les lemmes dispatchA à dispatchD partitionnent $\{2, \ldots, 306\}$ en quatre tranches, et dans chacune, seuls quelques premiers ($3$, $13$, $53$, $79$ pour la première ; $131$, $157$ pour la deuxième ; etc.) exigent un certificat de principauté — tous les autres tombent par degré d’inertie.

Point clé : l’escalade $4 \to 58 \to 307$ n’est pas un artefact d’implémentation — elle mesure la croissance du discriminant $p^{p-2}$ ($7^5 = 16807$, $11^9 \approx 2{,}4 \cdot 10^9$, $13^{11} \approx 1{,}8 \cdot 10^{12}$), et c’est exactement pourquoi la méthode s’essouffle : au-delà de $p = 19$, le nombre de certificats exigés dépasse ce qu’une preuve lisible peut contenir (the proof is more and more involved, dit le dépôt amont).

Exercice 5 — $\mathbb{F}_{27}$ : la relation fondamentale du générateur

Le corps de certificats construit ci-dessus est $\mathbb{F}_{27} = \mathbb{F}_3[\theta]$ où $\theta$ est la classe de $X$ modulo $X^3 - X - 1$. Établissez la relation fondamentale que toute la section M3dS11 exploite :

\[\theta^3 = \theta + 1\]

Une seule tactique suffit : l’énoncé F27_root donne $\theta^3 - \theta - 1 = 0$, et le but est une combinaison linéaire de cette égalité (tactique linear_combination, croisée au passage dans la section 6 sur les identités $\alpha \cdot \beta = 23$).

-- Exercice 5 : θ³ = θ + 1 dans F₂₇ = 𝔽₃[X]/(X³ - X - 1).
--
-- Objectif : établir
--   (AdjoinRoot.root CyclotomicPID.M3dS11.g3) ^ 3
--     = (AdjoinRoot.root CyclotomicPID.M3dS11.g3) + 1
-- TODO étudiant : à compléter (une seule tactique — la relation F27_root).

#check @CyclotomicPID.M3dS11.F27_root   -- θ³ - θ - 1 = 0 : l'égalité à réarranger

-- Exercice 5 : θ³ = θ + 1 dans F₂₇ = 𝔽₃[X]/(X³ - X - 1).

--

-- Objectif : établir

--   (AdjoinRoot.root CyclotomicPID.M3dS11.g3) ^ 3

--     = (AdjoinRoot.root CyclotomicPID.M3dS11.g3) + 1

-- TODO étudiant : à compléter (une seule tactique — la relation F27_root).

#check @CyclotomicPID.M3dS11.F27_root   -- θ³ - θ - 1 = 0 : l'égalité à réarranger CyclotomicPID.M3dS11.F27_root : AdjoinRoot.root CyclotomicPID.M3dS11.g3 ^ 3 - AdjoinRoot.root CyclotomicPID.M3dS11.g3 -
    1 =
  0

--% env 14

Raw input

{"cmd": "-- Exercice 5 : \u03b8\u00b3 = \u03b8 + 1 dans F\u2082\u2087 = \ud835\udd3d\u2083[X]/(X\u00b3 - X - 1).\n--\n-- Objectif : \u00e9tablir\n--   (AdjoinRoot.root CyclotomicPID.M3dS11.g3) ^ 3\n--     = (AdjoinRoot.root CyclotomicPID.M3dS11.g3) + 1\n-- TODO \u00e9tudiant : \u00e0 compl\u00e9ter (une seule tactique \u2014 la relation F27_root).\n\n#check @CyclotomicPID.M3dS11.F27_root   -- \u03b8\u00b3 - \u03b8 - 1 = 0 : l'\u00e9galit\u00e9 \u00e0 r\u00e9arranger", "env": 13}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "CyclotomicPID.M3dS11.F27_root : AdjoinRoot.root CyclotomicPID.M3dS11.g3 ^ 3 - AdjoinRoot.root CyclotomicPID.M3dS11.g3 -\n    1 =\n  0"}],
 "env": 14}

7. La seconde route : la courbe de Frey meurt dans $S_2(\Gamma_0(2)) = 0$

Pour $p = 37$, la factorisation s’enlise — la route moderne change d’objet.

-- Arithmétique de Frey : le carré d'un impair est 1 modulo 8, et cela contraint a ≡ c.
#check @FltRoute.sq_odd_eq_one_mod_eight     -- (2k+1)² ≡ 1 [MOD 8]
#check @FltRoute.odd_pow_congr_self_mod_eight -- x, p impairs ⟹ x ^ p ≡ x [MOD 8]
#check @FltRoute.frey_congr_mod_eight        -- a^p + b^p = c^p, b pair ⟹ a ≡ c [MOD 8]

-- La courbe de Frey, comme WeierstrassCurve ℚ construite littéralement :
#check @FltRoute.freyCurve

-- L'indice de Γ₀(2) dans SL₂(ℤ), par énumération des colonnes non nulles de (ZMod 2)² :
#check @FltRoute.firstColMod2               -- la classe à gauche ↦ sa première colonne modulo 2
#check @FltRoute.gamma0_two_index_eq_three  -- [SL₂(ℤ) : Γ₀(2)] = 3

-- Arithmétique de Frey : le carré d'un impair est 1 modulo 8, et cela contraint a ≡ c.

#check @FltRoute.sq_odd_eq_one_mod_eight     -- (2k+1)² ≡ 1 [MOD 8] @FltRoute.sq_odd_eq_one_mod_eight : ∀ {k : ℕ}, (2 * k + 1) ^ 2 ≡ 1 [MOD 8]

#check @FltRoute.odd_pow_congr_self_mod_eight -- x, p impairs ⟹ x ^ p ≡ x [MOD 8] @FltRoute.odd_pow_congr_self_mod_eight : ∀ {x p : ℕ}, x % 2 = 1 → p % 2 = 1 → x ^ p ≡ x [MOD 8]

#check @FltRoute.frey_congr_mod_eight        -- a^p + b^p = c^p, b pair ⟹ a ≡ c [MOD 8] @FltRoute.frey_congr_mod_eight : ∀ {a b c p : ℕ},
  5 ≤ p → p % 2 = 1 → a % 2 = 1 → b % 2 = 0 → c % 2 = 1 → a ^ p + b ^ p = c ^ p → a ≡ c [MOD 8]

-- La courbe de Frey, comme WeierstrassCurve ℚ construite littéralement :

#check @FltRoute.freyCurve FltRoute.freyCurve : ℕ → ℕ → ℕ → WeierstrassCurve ℚ

-- L'indice de Γ₀(2) dans SL₂(ℤ), par énumération des colonnes non nulles de (ZMod 2)² :

#check @FltRoute.firstColMod2               -- la classe à gauche ↦ sa première colonne modulo 2 FltRoute.firstColMod2 : SL(2, ℤ) → ZMod 2 × ZMod 2

#check @FltRoute.gamma0_two_index_eq_three  -- [SL₂(ℤ) : Γ₀(2)] = 3 FltRoute.gamma0_two_index_eq_three : (CongruenceSubgroup.Gamma0 2).index = 3

--% env 15

Raw input

{"cmd": "-- Arithm\u00e9tique de Frey : le carr\u00e9 d'un impair est 1 modulo 8, et cela contraint a \u2261 c.\n#check @FltRoute.sq_odd_eq_one_mod_eight     -- (2k+1)\u00b2 \u2261 1 [MOD 8]\n#check @FltRoute.odd_pow_congr_self_mod_eight -- x, p impairs \u27f9 x ^ p \u2261 x [MOD 8]\n#check @FltRoute.frey_congr_mod_eight        -- a^p + b^p = c^p, b pair \u27f9 a \u2261 c [MOD 8]\n\n-- La courbe de Frey, comme WeierstrassCurve \u211a construite litt\u00e9ralement :\n#check @FltRoute.freyCurve\n\n-- L'indice de \u0393\u2080(2) dans SL\u2082(\u2124), par \u00e9num\u00e9ration des colonnes non nulles de (ZMod 2)\u00b2 :\n#check @FltRoute.firstColMod2               -- la classe \u00e0 gauche \u21a6 sa premi\u00e8re colonne modulo 2\n#check @FltRoute.gamma0_two_index_eq_three  -- [SL\u2082(\u2124) : \u0393\u2080(2)] = 3", "env": 14}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@FltRoute.sq_odd_eq_one_mod_eight : ∀ {k : ℕ}, (2 * k + 1) ^ 2 ≡ 1 [MOD 8]"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@FltRoute.odd_pow_congr_self_mod_eight : ∀ {x p : ℕ}, x % 2 = 1 → p % 2 = 1 → x ^ p ≡ x [MOD 8]"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@FltRoute.frey_congr_mod_eight : ∀ {a b c p : ℕ},\n  5 ≤ p → p % 2 = 1 → a % 2 = 1 → b % 2 = 0 → c % 2 = 1 → a ^ p + b ^ p = c ^ p → a ≡ c [MOD 8]"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data": "FltRoute.freyCurve : ℕ → ℕ → ℕ → WeierstrassCurve ℚ"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data": "FltRoute.firstColMod2 : SL(2, ℤ) → ZMod 2 × ZMod 2"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 6},
   "data":
   "FltRoute.gamma0_two_index_eq_three : (CongruenceSubgroup.Gamma0 2).index = 3"}],
 "env": 15}

Lecture : trois classes, et le raccord avec les représentants de la section 2

Sortie obtenue : la congruence des impairs, sa montée à toute puissance impaire, la normalisation de Frey, la courbe, l’application firstColMod2 et l’indice 3.

Le lien avec le début du notebook est littéral : $\Gamma_0(N)$ est le sous-groupe de $SL_2(\mathbb{Z})$ des matrices $\begin{pmatrix} a & b \\ c & d \end{pmatrix}$ avec $N \mid c$ — le groupe qui classe les formes de niveau $N$, celui sur lequel les opérateurs $T_p$ des sections 2 à 5 sont construits. Le module prouve $[SL_2(\mathbb{Z}) : \Gamma_0(2)] = 3$ par une bijection explicite (cosetToProj) : chaque classe à gauche s’envoie sur la première colonne modulo 2 de ses éléments, une colonne non nulle de $(\mathbb{Z}/2\mathbb{Z})^2$ — et il y en a exactement trois : $(1,0)$, $(0,1)$, $(1,1)$, la colonne $(1,0)$ étant $\Gamma_0(2)$ lui-même ($c \equiv 0$).

Pourquoi cet indice compte : c’est lui qui, dans l’astuce de la norme (voir la percée, ci-dessous), fait passer le poids 2 sur $\Gamma_0(2)$ au poids $2 \times 3 = 6$ sur $SL_2(\mathbb{Z})$. Et pourquoi la congruence de Frey compte : c’est elle ($a \equiv c \pmod 8$) qui, dans la preuve complète, interdit à la courbe d’être dans le « package » exclu par l’étape 2 — le module en prouve la partie arithmétique, l’étape de Tate reste admise.

Exercice 6 — Frey : le cube d’un impair modulo 8

La normalisation de Frey repose sur la chaîne « le carré d’un impair est 1 modulo 8, donc toute puissance impaire d’un impair est congrue à l’impair lui-même » (odd_pow_congr_self_mod_eight). Établissez le premier maillon au cube :

\[(2k+1)^3 \equiv 2k+1 \pmod 8 \qquad \text{pour tout } k \in \mathbb{N}\]

Indication : $(2k+1)^3 = (2k+1)^2 \cdot (2k+1)$ — composer la congruence sq_odd_eq_one_mod_eight avec la réflexivité, par Nat.ModEq.mul.

-- Exercice 6 : le cube d'un impair est congru à l'impair modulo 8.
--
-- Objectif : établir, pour tout k : ℕ,
--   (2 * k + 1) ^ 3 ≡ 2 * k + 1 [MOD 8]
-- TODO étudiant : à compléter (composer le carré et la réflexivité).

#check @FltRoute.sq_odd_eq_one_mod_eight  -- la brique : (2k+1)² ≡ 1 [MOD 8]

-- Exercice 6 : le cube d'un impair est congru à l'impair modulo 8.

--

-- Objectif : établir, pour tout k : ℕ,

--   (2 * k + 1) ^ 3 ≡ 2 * k + 1 [MOD 8]

-- TODO étudiant : à compléter (composer le carré et la réflexivité).

#check @FltRoute.sq_odd_eq_one_mod_eight  -- la brique : (2k+1)² ≡ 1 [MOD 8] @FltRoute.sq_odd_eq_one_mod_eight : ∀ {k : ℕ}, (2 * k + 1) ^ 2 ≡ 1 [MOD 8]

--% env 16

Raw input

{"cmd": "-- Exercice 6 : le cube d'un impair est congru \u00e0 l'impair modulo 8.\n--\n-- Objectif : \u00e9tablir, pour tout k : \u2115,\n--   (2 * k + 1) ^ 3 \u2261 2 * k + 1 [MOD 8]\n-- TODO \u00e9tudiant : \u00e0 compl\u00e9ter (composer le carr\u00e9 et la r\u00e9flexivit\u00e9).\n\n#check @FltRoute.sq_odd_eq_one_mod_eight  -- la brique : (2k+1)\u00b2 \u2261 1 [MOD 8]", "env": 15}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "@FltRoute.sq_odd_eq_one_mod_eight : ∀ {k : ℕ}, (2 * k + 1) ^ 2 ≡ 1 [MOD 8]"}],
 "env": 16}

La percée : la norme relève le poids 2 au poids 6

Une forme fantôme fait mourir la courbe de Frey.

-- La percée : la norme d'une cusp form de poids k sur 𝒢 ⊆ ℋ est une cusp form
-- de poids k × [ℋ : 𝒢] sur ℋ — et la norme ne s'annule que si f s'annule.
#check @FltRoute.CuspForm.norm
#check @FltRoute.CuspForm.norm_eq_zero_iff

-- Mathlib sait que le poids 6 en niveau 1 est sous le seuil (poids < 12 ⟹ rang nul) :
#check @FltRoute.s6_levelOne_eq_zero

-- Alors S₂(Γ₀(2)) = 0 : la norme relève 2 → 2 × 3 = 6, et le poids 6 meurt en niveau 1.
#check @FltRoute.s2_gamma0_2_eq_zero
#check @FltRoute.no_weight2_level2_cusp_form

-- Le bilan : étapes 2-5 en hypothèses, la contradiction en preuve close.
#check @FltRoute.flt_of_full_route
#print axioms FltRoute.s2_gamma0_2_eq_zero
#print axioms FltRoute.flt_of_full_route

-- La percée : la norme d'une cusp form de poids k sur 𝒢 ⊆ ℋ est une cusp form

-- de poids k × [ℋ : 𝒢] sur ℋ — et la norme ne s'annule que si f s'annule.

#check @FltRoute.CuspForm.norm @FltRoute.CuspForm.norm : {𝒢 : Subgroup (GL (Fin 2) ℝ)} →
  (ℋ : Subgroup (GL (Fin 2) ℝ)) →
    {F : Type u_1} →
      F →
        [inst : FunLike F UpperHalfPlane ℂ] →
          {k : ℤ} →
            [𝒢.IsFiniteRelIndex ℋ] →
              [ℋ.HasDetPlusMinusOne] → [CuspFormClass F 𝒢 k] → CuspForm ℋ (k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ)))

#check @FltRoute.CuspForm.norm_eq_zero_iff @FltRoute.CuspForm.norm_eq_zero_iff : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1}
  (f : F) [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : ℋ.HasDetPlusMinusOne]
  [inst_3 : CuspFormClass F 𝒢 k], FltRoute.CuspForm.norm ℋ f = 0 ↔ ⇑f = 0

-- Mathlib sait que le poids 6 en niveau 1 est sous le seuil (poids < 12 ⟹ rang nul) :

#check @FltRoute.s6_levelOne_eq_zero FltRoute.s6_levelOne_eq_zero : ∀
  (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 6), f = 0

-- Alors S₂(Γ₀(2)) = 0 : la norme relève 2 → 2 × 3 = 6, et le poids 6 meurt en niveau 1.

#check @FltRoute.s2_gamma0_2_eq_zero FltRoute.s2_gamma0_2_eq_zero : ∀
  (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 2)) 2), f = 0

#check @FltRoute.no_weight2_level2_cusp_form FltRoute.no_weight2_level2_cusp_form : ¬∃ f, f ≠ 0

-- Le bilan : étapes 2-5 en hypothèses, la contradiction en preuve close.

#check @FltRoute.flt_of_full_route @FltRoute.flt_of_full_route : ∀ {p a b c : ℕ},
  5 ≤ p → 0 < a → 0 < b → 0 < c → (a ^ p + b ^ p = c ^ p → ∃ f, f ≠ 0) → a ^ p + b ^ p ≠ c ^ p

#print axioms FltRoute.s2_gamma0_2_eq_zero 'FltRoute.s2_gamma0_2_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms FltRoute.flt_of_full_route 'FltRoute.flt_of_full_route' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 17

Raw input

{"cmd": "-- La perc\u00e9e : la norme d'une cusp form de poids k sur \ud835\udca2 \u2286 \u210b est une cusp form\n-- de poids k \u00d7 [\u210b : \ud835\udca2] sur \u210b \u2014 et la norme ne s'annule que si f s'annule.\n#check @FltRoute.CuspForm.norm\n#check @FltRoute.CuspForm.norm_eq_zero_iff\n\n-- Mathlib sait que le poids 6 en niveau 1 est sous le seuil (poids < 12 \u27f9 rang nul) :\n#check @FltRoute.s6_levelOne_eq_zero\n\n-- Alors S\u2082(\u0393\u2080(2)) = 0 : la norme rel\u00e8ve 2 \u2192 2 \u00d7 3 = 6, et le poids 6 meurt en niveau 1.\n#check @FltRoute.s2_gamma0_2_eq_zero\n#check @FltRoute.no_weight2_level2_cusp_form\n\n-- Le bilan : \u00e9tapes 2-5 en hypoth\u00e8ses, la contradiction en preuve close.\n#check @FltRoute.flt_of_full_route\n#print axioms FltRoute.s2_gamma0_2_eq_zero\n#print axioms FltRoute.flt_of_full_route", "env": 16}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@FltRoute.CuspForm.norm : {𝒢 : Subgroup (GL (Fin 2) ℝ)} →\n  (ℋ : Subgroup (GL (Fin 2) ℝ)) →\n    {F : Type u_1} →\n      F →\n        [inst : FunLike F UpperHalfPlane ℂ] →\n          {k : ℤ} →\n            [𝒢.IsFiniteRelIndex ℋ] →\n              [ℋ.HasDetPlusMinusOne] → [CuspFormClass F 𝒢 k] → CuspForm ℋ (k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ)))"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@FltRoute.CuspForm.norm_eq_zero_iff : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1}\n  (f : F) [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : ℋ.HasDetPlusMinusOne]\n  [inst_3 : CuspFormClass F 𝒢 k], FltRoute.CuspForm.norm ℋ f = 0 ↔ ⇑f = 0"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "FltRoute.s6_levelOne_eq_zero : ∀\n  (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 6), f = 0"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "FltRoute.s2_gamma0_2_eq_zero : ∀\n  (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 2)) 2), f = 0"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 6},
   "data": "FltRoute.no_weight2_level2_cusp_form : ¬∃ f, f ≠ 0"},
  {"severity": "info",
   "pos": {"line": 14, "column": 0},
   "endPos": {"line": 14, "column": 6},
   "data":
   "@FltRoute.flt_of_full_route : ∀ {p a b c : ℕ},\n  5 ≤ p → 0 < a → 0 < b → 0 < c → (a ^ p + b ^ p = c ^ p → ∃ f, f ≠ 0) → a ^ p + b ^ p ≠ c ^ p"},
  {"severity": "info",
   "pos": {"line": 15, "column": 0},
   "endPos": {"line": 15, "column": 6},
   "data":
   "'FltRoute.s2_gamma0_2_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 16, "column": 0},
   "endPos": {"line": 16, "column": 6},
   "data":
   "'FltRoute.flt_of_full_route' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 17}

Lecture : la boucle est bouclée — l’espace où vit $T_p$ est nul

Sortie obtenue : la norme cuspidale et son critère d’annulation, le seuil de Mathlib pour le poids 6 en niveau 1, la nullité $S_2(\Gamma_0(2)) = 0$, puis le bilan flt_of_full_route — avec ses deux certificats d’axiomes (axiomes standards uniquement).

L’argument tient en trois lignes, et chacune est un théorème du module :

Norme. Pour $f$ cuspidale de poids 2 sur $\Gamma_0(2)$, la norme $N(f) = \prod_{\bar{g}} f \mid [\bar{g}]$ (produit sur les 3 classes) est cuspidale de poids $2 \times 3 = 6$ sur $SL_2(\mathbb{Z})$ — et $N(f) = 0 \iff f = 0$ (norm_eq_zero_iff) ;
Seuil. Mathlib (CuspForm.rank_eq_zero_of_weight_lt_twelve) sait que l’espace des cusp forms de niveau 1 s’annule en poids $< 12$ : le poids 6 est vide (s6_levelOne_eq_zero) ;
Conclusion. $N(f)$ vit dans un espace nul donc $N(f) = 0$ donc $f = 0$ : $S_2(\Gamma_0(2)) = 0$.

Le raccord avec les sections 2 à 5, enfin littéral : les opérateurs $T_p$ agissent sur des espaces de formes de niveau $N$ — et le théorème ci-dessus dit que pour $N = 2$, poids 2, l’espace lui-même est nul : il n’y a rien à diagonaliser, aucune valeur propre, aucune suite de coefficients. C’est cette vacuité que la route de Frey exploite : le contre-exemple supposé fabrique (via les étapes admises 2 à 5) une forme non nulle dans un espace nul — contradiction. Les #print axioms montrent que les deux théorèmes pivots sont des preuves closes, sans sorryAx : l’étape 6 de Fermat est mécaniquement vérifiée, du comptage des colonnes à la formule des dimensions.

Synthèse : la carte de la seconde route

La route moderne — Frey (1984), Ribet (1986), Wiles (1995) — renverse le sens de circulation : au lieu de factoriser l’équation, elle fabrique un objet géométrique à partir d’un contre-exemple supposé et montre que cet objet ne peut pas exister. Le module FltRoute.lean en cartographie les six étapes, et la section vient d’en exécuter les maillons prouvables :

#	Étape	Statut dans le module
1	Fermat : $a^p + b^p \neq c^p$ pour $3 \leq p$	énoncée (bilan sous hypothèses admises)
2	la courbe de Frey est « hors package » (Tate)	admise (la courbe, elle, est construite)
3	Mazur–Frey : semi-stabilité, représentation galoisienne	admise (l’arithmétique de normalisation est prouvée)
4	modularité des courbes semi-stables (Wiles)	admise
5	abaissement du niveau vers $N = 2$ (Ribet)	admise (l’indice $[SL_2(\mathbb{Z}) : \Gamma_0(2)] = 3$ est prouvé)
6	$S_2(\Gamma_0(2)) = 0$	PROUVÉE

La logique du bilan : si les étapes 2 à 5 livrent, à partir d’un contre-exemple de Fermat, une forme modulaire cuspidale non nulle de poids 2 sur $\Gamma_0(2)$, l’étape 6 — prouvée dans le module, exécutée ci-dessus — la tue. Les maillons prouvables depuis Mathlib seule viennent d’être exécutés : l’arithmétique de Frey, la courbe elle-même, l’indice de $\Gamma_0(2)$, puis la percée $S_2(\Gamma_0(2)) = 0$. Le reste de la route (Tate, Mazur–Frey, Wiles, Ribet) reste hors de portée d’une formalisation depuis Mathlib seule — c’est le plafond honnête de ce lake, détaillé dans la section suivante.

8. Transparence axiomatique, i18n et limites

Le lake revendique une propriété forte : zéro sorry — propriété établie en amont par le scan du source et le build du lake, déjà validés. Ce notebook la corrobore par échantillonnage : chaque #print axioms exécuté au fil des sections certifie le théorème interrogé, et chacun est revenu avec la seule liste des axiomes standards du raisonnement classique (extensionnalité propositionnelle, choix, quotients — la liste exacte est dans les sorties). Un sorry — même transitif, caché dans une dépendance — apparaîtrait comme sorryAx dans la liste du théorème qui en dépend : son absence sur les théorèmes échantillonnés atteste que ces preuves-là sont closes.

Convention i18n : chaque module français a son miroir HeckeOperator_en.lean (docstrings anglaises, énoncés byte-identiques, namespaces distincts — EPIC #4980). Ce notebook visite le module FR ; les énoncés cités existent à l’identique côté EN.

Limites du périmètre (assumées par le lake, grain aval) :

le produit de Petersson et l’orthogonalité des opérateurs de Hecke ne sont pas formalisés ;
les cusp forms ne sont pas construites dans HeckeOperator : le pont « $T_p f$ a pour coefficients coeffHeckeT k p a » reste un encodage parallèle, pas un théorème de passage. Le module FltRoute (section 7) utilise bien les CuspForm de Mathlib et démontre la vacuité $S_2(\Gamma_0(2)) = 0$, mais la stabilité de l’espace des formes par $T_p$ et la théorie spectrale restent hors du lake ;
sur la route FLT, les étapes 2 à 5 (Tate, Mazur–Frey, Wiles, Ribet) sont des hypothèses de flt_of_full_route, pas des preuves : le lake vérifie mécaniquement la dernière étape seule.

-- Transparence axiomatique finale : trois théorèmes représentatifs du lake.
#check @ModularForm.slash_heckeMatrix_apply   -- la brique analytique
#check @ModularForm.coeffHeckeT_of_dvd        -- la brique combinatoire
#check @ModularForm.heckeT_smul               -- la brique structurelle

#print axioms ModularForm.slash_heckeMatrix_apply
#print axioms ModularForm.coeffHeckeT_of_dvd
#print axioms ModularForm.heckeT_smul

-- Transparence axiomatique finale : trois théorèmes représentatifs du lake.

#check @ModularForm.slash_heckeMatrix_apply   -- la brique analytique slash_heckeMatrix_apply : ∀ (k : ℤ) {p : ℕ},
  p ≠ 0 →
    ∀ (j : ℕ) (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),
      (f ∣[k] heckeMatrix p j) τ = (↑p)⁻¹ * f (heckeMatrix p j • τ)

#check @ModularForm.coeffHeckeT_of_dvd        -- la brique combinatoire coeffHeckeT_of_dvd : ∀ (k : ℤ) {p n : ℕ},
  p ∣ n → ∀ (a : ℕ → ℂ), coeffHeckeT k p a n = a (n * p) + ↑p ^ (k - 1) * a (n / p)

#check @ModularForm.heckeT_smul               -- la brique structurelle heckeT_smul : ∀ (k : ℤ) (p : ℕ) (c : ℂ) (f : UpperHalfPlane → ℂ), heckeT k p (c • f) = c • heckeT k p f

#print axioms ModularForm.slash_heckeMatrix_apply 'ModularForm.slash_heckeMatrix_apply' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms ModularForm.coeffHeckeT_of_dvd 'ModularForm.coeffHeckeT_of_dvd' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms ModularForm.heckeT_smul 'ModularForm.heckeT_smul' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 18

Raw input

{"cmd": "-- Transparence axiomatique finale : trois th\u00e9or\u00e8mes repr\u00e9sentatifs du lake.\n#check @ModularForm.slash_heckeMatrix_apply   -- la brique analytique\n#check @ModularForm.coeffHeckeT_of_dvd        -- la brique combinatoire\n#check @ModularForm.heckeT_smul               -- la brique structurelle\n\n#print axioms ModularForm.slash_heckeMatrix_apply\n#print axioms ModularForm.coeffHeckeT_of_dvd\n#print axioms ModularForm.heckeT_smul", "env": 17}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "slash_heckeMatrix_apply : ∀ (k : ℤ) {p : ℕ},\n  p ≠ 0 →\n    ∀ (j : ℕ) (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),\n      (f ∣[k] heckeMatrix p j) τ = (↑p)⁻¹ * f (heckeMatrix p j • τ)"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "coeffHeckeT_of_dvd : ∀ (k : ℤ) {p n : ℕ},\n  p ∣ n → ∀ (a : ℕ → ℂ), coeffHeckeT k p a n = a (n * p) + ↑p ^ (k - 1) * a (n / p)"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "heckeT_smul : ∀ (k : ℤ) (p : ℕ) (c : ℂ) (f : UpperHalfPlane → ℂ), heckeT k p (c • f) = c • heckeT k p f"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "'ModularForm.slash_heckeMatrix_apply' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "'ModularForm.coeffHeckeT_of_dvd' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "'ModularForm.heckeT_smul' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 18}

Lecture : trois briques, trois certificats

Sortie obtenue : les signatures de trois théorèmes représentatifs — l’analyse (slash_heckeMatrix_apply), la combinatoire (coeffHeckeT_of_dvd), la structure (heckeT_smul) — et leurs listes d’axiomes, toutes identiques et sans sorryAx.

Théorème	Famille	Axiomes
`slash_heckeMatrix_apply`	analyse sur $\mathbb{H}$	standards uniquement
`coeffHeckeT_of_dvd`	coefficients	standards uniquement
`heckeT_smul`	linéarité	standards uniquement

Point clé : ces trois certificats cohérents couvrent des théorèmes de familles différentes et établissent que ces preuves échantillonnées ne dépendent ni d’un axiome exotique ni de sorryAx. Ils ne constituent pas un audit exhaustif du module ; l’absence globale de sorry est établie séparément par le scan du source du lake.

Conclusion

Ce compagnon a fait exécuter par le compilateur les cinq modules du lake hecke_lean. D’abord les trois familles d’énoncés des opérateurs : les représentants $\gamma_{p,j}$ et diagonaux (valeurs, déterminants, positivité), l’action de slash décomposée (homothéties écrasées contre dilatation), les opérateurs $U_p$ et $T_p$ (définitions, lecture ponctuelle, linéarité) et la formule des coefficients — avec ses exemples calculables reproduits en-kernel et étendus (exercice 3). Puis les deux routes vers Fermat : la route cyclotomique de Kummer ($\mathbb{Z}[\zeta_p]$ principal pour $p = 7, 11, 13$, de l’élimination pure au corps de certificats $\mathbb{F}_{27}$) et la route moderne (courbe de Frey, indice de $\Gamma_0(2)$, vacuité $S_2(\Gamma_0(2)) = 0$ et bilan sous hypothèses admises). Tous les #print axioms sont revenus identiques : ils certifient les théorèmes échantillonnés ; l’absence globale de sorry est celle du scan du source et du build du lake, déjà validés en amont.

Ce que le notebook a montré

Niveau	Symbole	Preuve vue
Géométrie	`val_heckeMatrix`, `det_heckeMatrix`	équations de valeur, déterminant exact
Analyse	`slash_heckeMatrix_apply`, `heckeT_apply`	le slash calculé sur chaque représentant
Combinatoire	`coeffHeckeT_of_dvd/_of_not_dvd`	$a(np) + p^{k-1} a(n/p)$
Structure	`heckeT_add`, `heckeT_smul`	endomorphismes de l’espace des fonctions
Arithmétique	`floor_M_seven`, `M11`, `M13`, `seven_pid`	la chaîne Minkowski → Marcus → PID
Géométrie des classes	`gamma0_two_index_eq_three`	$[SL_2(\mathbb{Z}) : \Gamma_0(2)] = 3$ par colonnes
Percée	`s2_gamma0_2_eq_zero`, `flt_of_full_route`	la norme tue l’espace, la route tue Fermat

Trois takeaways

Le #check est un typage : il valide la signature du théorème contre les oleans du lake — ce que vous voyez est ce qui est prouvé ;
Le #print axioms est un certificat (par théorème) : l’absence de sorryAx est la vérification mécanique que ce théorème-là a une preuve close ;
Le rfl/norm_num sur exemples est un oracle : la formule des coefficients se calcule réellement (échantillonnage rfl, branches decide + if_pos/if_neg + norm_num) — la théorie ne reste pas symbolique.

Pour aller plus loin

Grain aval du lake : produit de Petersson, cusp forms, pont $q$-série (suivre le README du lake) ;
La source amont : le dépôt anthropics/fermats-last-theorem, fichier Definitions/Def_ModularForm_HeckeOperator.lean — attribution Apache-2.0 complète dans hecke_lean/NOTICE.md ;
Références théoriques : Diamond & Shurman, A First Course in Modular Forms (ch. 5) ; Apostol, Modular Functions and Dirichlet Series in Number Theory (ch. 6) ; pour la perspective computationnelle sur les coefficients, le cours de Don Zagier sur les formes modulaires et la fonction τ de Ramanujan.

Exercices — progression conseillée

Sans dévoiler les preuves, voici le chemin de chacun :

Exercice 1 (représentants) : décharger l’hypothèse $p \neq 0$ pour $p = 3$ par décision, invoquer l’équation de valeur, puis refermer l’égalité de littéraux — attention aux coercitions $\uparrow 2$ contre $2$, la réflexion doit être explicite ;
Exercice 2 (cas dégénéré) : le lemme voulu est déjà enregistré pour la simplification automatique — une seule tactique referme le but ;
Exercice 3 (coefficients) : trancher $5 \mid 10$ par décision, choisir la bonne branche de la conditionnelle, normaliser l’arithmétique — les exemples de la section 5 donnent le gabarit ;
Exercice 4 (ordres) : transposer le gabarit orderOf_eq_iff + interval_cases + decide de 7 vers 11 — les deux example décidés de la cellule donnent l’ancrage numérique ;
Exercice 5 ($\mathbb{F}_{27}$) : une seule tactique — réarranger F27_root par linear_combination ;
Exercice 6 (Frey) : composer le carré d’un impair avec la réflexivité par Nat.ModEq.mul.

Retour au sommet

Représentant	Action sur \(\tau\)	Slash de poids \(k\) en \(\tau\)
\(\gamma_{p,j}\) (triangulaire)	\((\tau + j)/p\) — \(p\) translatées écrasées vers la pointe	\(p^{-1} f\big((\tau+j)/p\big)\)
diagonal	\(p\,\tau\) — dilatation vers l’intérieur	\(p^{k-1} f(p\,\tau)\)

Grandeur	Valeur	Signification
\(2^{11}\)	2 048	facteur diagonal de \(T_2\) au poids 12
\(3^{11}\)	177 147	facteur diagonal de \(T_3\)
\(5^{11}\)	48 828 125	facteur diagonal de \(T_5\)
\(1 + 2^{11}\)	2 049	second exemple divisible : suite \(a \equiv 1\), \(n = 2\) (branche \(2 \mid 2\))

Module	\(\lfloor M K \rfloor\)	Premiers exigeant un certificat	Moyen
`SevenPid`	\(4\)	aucun (\(2^3 > 4\), \(3^6 > 4\))	degrés d’inertie seuls
`ElevenPid`	\(58\)	\(11\) (ramifié), \(23\)	générateur explicite \(\alpha = \zeta^3 + \zeta + 1\)
`ThirteenPid`	\(< 307\)	\(3\), \(13\), \(53\), \(79\), \(131\), \(157\)	corps de certificats \(\mathbb{F}_{27}\) + quatre tranches

Fait	Rôle dans la preuve
\(\lfloor M K \rfloor = 4\)	le critère de Marcus ne regarde que \(p \in \{1, \ldots, 4\}\)
\(2\) d’ordre \(3\)	degré d’inertie \(f = 3\) au-dessus de \(2\) : \(2^3 = 8 > 4\)
\(3\) d’ordre \(6\)	degré d’inertie \(f = 6\) au-dessus de \(3\) : \(3^6 > 4\)

Pourquoi ce lake dans CoursIA

Pourquoi ce compagnon

Plan du notebook

Conventions du notebook

Substance formelle

Prérequis

Durée estimée

1. Le lake hecke_lean : un port pédagogique, trois familles d’énoncés

Lecture des signatures

2. Les représentants \(\gamma_{p,j}\) et la partie diagonale

Lecture : valeurs et déterminants

Exercice 1 — lire la valeur d’un représentant

3. L’action sur le demi-plan supérieur : le slash

Lecture : deux comportements opposés du slash

4. Les opérateurs \(U_p\) et \(T_p\)

Lecture : la formule ponctuelle de \(T_p\)

Exercice 2 — le cas dégénéré \(T_0 = \mathrm{id}\)

Linéarité : des opérateurs, pas des transformations

Lecture : la structure d’endomorphisme

5. La formule des coefficients : la combinatoire de \(T_p\)

Lecture : les quatre calculs

L’ordre de grandeur du facteur diagonal

Lecture : \(p^{k-1}\) écrase l’échantillonnage

Exercice 3 — \(T_5\) au poids 12 sur un indice divisible

6. La première route : Kummer, ou quand la factorialité remplace la preuve

Lecture : une élimination complète, sans un seul générateur

Lecture : le générateur explicite au-dessus de 23

Exercice 4 — l’ordre de 2 dans \((\mathbb{Z}/11\mathbb{Z})^\times\)

Troisième maillon : \(p = 13\) et le corps de certificats \(\mathbb{F}_{27}\)

Lecture : le corps de certificats \(\mathbb{F}_{27}\) et les quatre tranches

Exercice 5 — \(\mathbb{F}_{27}\) : la relation fondamentale du générateur

7. La seconde route : la courbe de Frey meurt dans \(S_2(\Gamma_0(2)) = 0\)

Lecture : trois classes, et le raccord avec les représentants de la section 2

Exercice 6 — Frey : le cube d’un impair modulo 8

La percée : la norme relève le poids 2 au poids 6

Lecture : la boucle est bouclée — l’espace où vit \(T_p\) est nul

Synthèse : la carte de la seconde route

8. Transparence axiomatique, i18n et limites

Lecture : trois briques, trois certificats

Conclusion

Ce que le notebook a montré

Trois takeaways

Pour aller plus loin

Exercices — progression conseillée

1. Le lake `hecke_lean` : un port pédagogique, trois familles d’énoncés