feat(lean,#14784): hecke_lean — opérateurs de Hecke classiques (port FLT, premier lake 4.33)

[jsboige]

Grain: MED/lean -- lane myia-po-2026:CoursIA -- prev: MED/tooling #14763

Résumé

Nouveau lake autonome hecke_lean : opérateurs de Hecke classiques T_p/U_p sur le demi-plan supérieur — représentants heckeMatrix/heckeDiagMatrix, linéarité complète, formule des coefficients coeffHeckeT (cas p ∣ n / p ∤ n), exemples calculables ajoutés (poids 12, p ∈ {2,3}). Port pédagogique de anthropics/fermats-last-theorem (Def_ModularForm_HeckeOperator.lean @ aa2d8b34692b) : énoncés/preuves repris tels quels, docstrings FR + sibling EN (ModularForm_en, parité des corps vérifiée modulo namespace), attribution Apache-2.0 dans NOTICE.md.

Premier lake CoursIA sur Lean v4.33.0 + Mathlib db584cd6 (ancre #14773) — autonome, sans dépendance à la migration galois_lean. Un seul import Mathlib ciblé, aucun import monolithique FLT.

Preuves (critère B — PR Lean)

1. lake build SUCCESS local (WSL) : Build completed successfully (2290 jobs) — les DEUX agrégateurs racines compilés (glob .one \Hecke`` ajouté : plus strict que sensitivity_lean, dont la racine FR reste non-compilée — leçon Lean i18n #4980 : les modules root <Lib>_en.lean aggregators ne sont pas batis par lake build (orphan glob coverage) #6585 appliquée aux deux racines).
2. grep -c sorry = 0/0/0/0 sur les 4 fichiers .lean (Hecke/HeckeOperator{,_en}.lean, Hecke{,_en}.lean). Aucun native_decide.
3. Proof-integrity (critère B.3) — #print axioms local (WSL, post-build) :
   • ModularForm.heckeT → [propext, Classical.choice, Quot.sound]
   • ModularForm.coeffHeckeT → [propext, Classical.choice, Quot.sound]
   • ModularForm_en.heckeT / ModularForm_en.coeffHeckeT → identiques (parité byte des preuves)
   • Conforme à l'ancre de l'issue (« axiomes de heckeT et coeffHeckeT : [propext, Classical.choice, Quot.sound] »). La CI lean-hecke.yml (jobs ci lean-build + proof-integrity lean-axiom, sorry-baseline 0, fail-on-sorry) re-joue build + axioms sur chaque PR touchant le lake.
4. Pas de refactor du prover ; création pure (13 fichiers, +998/−2, dont 11 fichiers lake + workflow CI + ligne LEAN_INVENTORY.md).

Choix d'implémentation

• Fix in-flight sur les exemples : première rédaction rw [coeffHeckeT_of_dvd (by decide)] rejetée par Lean (métavariables — le by decide s'élaborait avant unification) ; réécrit en have h : … := by decide concret avant simp only [coeffHeckeT, if_pos/if_neg h] — déterministe, buildé.
• Parité FR/EN vérifiée programmatiquement : strip docstrings/comments → diff = lignes namespace/end uniquement (suffixe _en légitime).
• Globs racines : .submodules \Hecke` + `.one `Hecke` + `Hecke_en`— la racine FR n'était pas dans l'ensemble de build du pattern sensitivity (vérifié :Hecke.olean` absent avant l'ajout).

Acceptance #14784 (8/8)

• emplacement/lake autonome sans diluer le bundle Galois M23
• cible Lean/Mathlib cohérente avec feat(lean): migrer les 27 lakes first-party vers Lean/Mathlib 4.33 #14773 (v4.33.0 + db584cd6)
• imports ciblés, sans import monolithique FLT
• siblings FR/EN conformes
• lake build complet SUCCESS
• aucun nouveau sorry, sorryAx ou native_decide
• proof-integrity ciblée verte
• attribution Apache-2.0/NOTICE préservée

Closes #14784

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2026:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-05) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=11 cap=12)
• GENRE-RUN : run consecutif d'un genre LIGHT (voir signals.runs dans le log du job)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[clusterManager-Myia]

[NanoClaw] structural review — #14803 (lake hecke_lean : opérateurs de Hecke T_p/U_p, #14784)

Verdict : FAVORABLE — création pure (+998/−2, 13 fichiers, aucun code existant touché), premier lake CoursIA sur Lean 4.33.0 + Mathlib db584cd6 (ancre #14773), autonome vis-à-vis de galois_lean comme exigé par l'issue.

Vérifié firsthand ce tour (head 9d003dbe) :

• Le port est fidèle à l'amont : Def_ModularForm_HeckeOperator.lean @ aa2d8b3469 existe dans anthropics/fermats-last-theorem (9 724 o) et le head du fichier correspond exactement — mêmes imports (SlashActions seul), même namespace, mêmes upperTriangularGL/heckeMatrix/heckeDiagMatrix avec preuves identiques. Le claim « énoncés/preuves repris tels quels » est exact, et NOTICE.md préserve Apache-2.0 avec commit amont cité.
• La math est saine (module lu en entier, 329 lignes) : déterminants exacts (det γ_{p,j} = p via 1·p − j·0), cas dégénérés p = 0 neutralisés partout (identité), lecture des slash correcte (p⁻¹ pour γ_{p,j} car p^(k−1)/p^k ; p^(k−1) pour le diagonal car denom = 1), linéarité complète (add/smul/neg/sub pour U et T), et coeffHeckeT = a(n·p) + [p∣n] p^(k−1) a(n/p) est la formule standard. Les 6 exemples calculables recalculés à la main : a 6 = 6, a 2 = 2 (2∤1), 4 + 2¹¹ (2∣2), a 6 = 6 (2∤3), 9 + 3¹¹ (3∣3), 1 + 2¹¹ (a≡1) — tous justes.
• 0 sorry / axiom / admit / native_decide sur HeckeOperator.lean ET le mirror _en (grep direct), racines = imports simples. Axiomes du body ([propext, Classical.choice, Quot.sound] sur heckeT/coeffHeckeT FR+EN) = les 3 standard, conformes à l'ancre de l'issue — re-joués par la CI.
• Mirror FR/EN structurellement fidèle : 39/39 noms de déclarations identiques (diff = docstrings/namespace), cohérent avec le claim « parité des corps modulo namespace », et i18n sibling drift vert au head.
• CI au head : 28 checks, 0 failure — Lean CI (hecke_lean) et Proof integrity (hecke_lean) success (build + axioms re-joués, fail-on-sorry), PR gate, Always-on guards, Gitleaks verts. Leçon #6585 appliquée : les DEUX racines (Hecke/Hecke_en) couvertes par le glob .one et compilées — plus strict que sensitivity_lean.

Observations :

1. Le pont géométrie → coefficients est documenté, pas prouvé : coeffHeckeT transcrit la formule combinatoire, mais aucun théorème ne relie l'action de heckeT sur les fonctions aux coefficients de Fourier (le vrai théorème exigerait la théorie des q-expansions). Le header du module dit la formule « formalisée par coeffHeckeT » — c'est une def parallèle, comme dans l'amont FLT. Acceptable pour une première tranche (le docstring du module annonce Petersson/cusp forms hors périmètre), mais le lecteur pédagogique peut croire le pont prouvé — une phrase « la liaison T_p f ↔ coefficients sera prouvée au grain aval » lèverait l'ambiguïté.
2. p premier implicite : la décomposition en p représentants + diagonal n'est la décomposition classique de Γ(1)\M₂(ℤ) que pour p premier ; les defs sont typées p : ℕ quelconque et restent formellement correctes, le docstring dit « usuellement premier » — fine, mais un grain aval sur p composé (opérateurs T_n généraux) devra revisiter ces defs.
3. Le docstring du dernier example parle de « valeur propre du terme constant » — c'est une lecture de coefficient (pour a≡1), pas une valeur propre au sens fonction propre ; demi-ligne de vocabulaire à affiner si le grain aval touche cette section.

— structural review (HeckeOperator.lean lu en entier FR + greppé EN ; amont FLT fetché et comparé ; axioms, CI et NOTICE vérifiés en direct au head).

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #14803 (feat(lean,#14784): hecke_lean — opérateurs de Hecke classiques (port FLT, premier lake 4.33)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- feat(lean,#2874): preuves kernel conway+KT — maison-mère du split 4 unités (#15434 ✓, #15440, #15460 ✓, #15583) #14821 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/LEAN_INVENTORY.md