Add: Hecke.DeltaTau — tau de Ramanujan verifie par le noyau + identite propre T_p D (grain 5 #17969)

[jsboige]

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/notebook-python #18705

Ce que livre la PR

Grain 5 de l'Epic #17969 (voir #17969 pour le découpage) : le module Hecke.DeltaTau relie la formule des coefficients de coeffHeckeT (HeckeOperator.lean) au discriminant modulaire Δ.

• deltaSeq : troncature du produit d'Euler X ⬝ ∏_{1≤m≤24} (1 - Xᵐ)²⁴ — représentée par convolution de listes de coefficients ℤ. Note de design : l'instance Mul (Polynomial ℤ) de Mathlib est noncomputable au pin db584cd6 (v4.33.0) — vérifié sur une sonde, même (X+1)*(X+2) refuse de compiler — ce qui interdit toute lecture decide/#eval via Polynomial ℤ. La convolution sur listes est calculable et le noyau la réduit intégralement.
• tau : table des 26 valeurs τ(0..25) vérifiées par le noyau — tau_values : (List.range 26).map tau = deltaSeq.take 26 := by decide (aucune valeur codée en dur sans preuve ; le decide échoue si un coefficient est faux). Le processus l'a prouvé : la récolte par sonde a corrigé 3 valeurs de mon brouillon (τ(22), τ(23), τ(24)) avant l'écriture de la table finale.
• deltaSeq_stable : exactitude de la troncature (K = 24 vs K = 36 facteurs, 26 premiers coefficients inchangés).
• Identité propre T_p Δ = τ(p) Δ : pont coeffHeckeT_twelve_int (lecture entière de la formule ℂ au poids 12) puis heckeT_two_isEigen (p = 2, n ≤ 12, eigenvalue −24) et heckeT_three_isEigen (p = 3, n ≤ 8, eigenvalue 252) — la version non bornée exige la théorie des formes modulaires, hors périmètre du lake ; le noyau vérifie ici ce que la théorie prédit.
• Multiplicativité τ(6) = τ(2)τ(3), lacunarité τ(25) ≠ 0 (pont Serre100/09).
• Sibling EN DeltaTau_en.lean (namespace ModularForm_en), importée par les agrégateurs racines ; README du lake enrichi (paragraphe module + 2 lignes de table de structure).

Preuves exigées (B.2/B.3)

• Compte sorry (organe count_code_sorry.py --json) : hecke_lean distinct_code_sorry 0 → 0 (16 fichiers, dont les 2 nouveaux).
• lake build local SUCCESS (WSL, toolchain v4.33.0, cache db584cd6) :
  • lake build Hecke.DeltaTau → Build completed successfully (150 s)
  • lake build Hecke.DeltaTau_en Hecke_en Hecke.AxiomProbe → Build completed successfully (4104 jobs)
• Axiomes (#print axioms sur sonde locale, fichier non committé) :
  • tau_values : [propext]
  • heckeT_two_isEigen, heckeT_three_isEigen, coeffHeckeT_twelve_int : [propext, Classical.choice, Quot.sound] (et côté _en identiques) — pas de sorryAx, pas de native_decide.
• B.3 (proof-integrity) : câblage = lean-hecke.yml appelle lean-axiom.yml ; les target-modules y sont dérivés à l'exécution depuis les globs du lakefile → Hecke.DeltaTau/Hecke.DeltaTau_en sont couverts automatiquement, sans changement de workflow. Le job CI est attendu vert sur cette tête (les axiomes locaux sont les 3 standards).
• Sibling i18n : check_i18n_siblings.py sur la paire → OK, 1/1 pairs byte-identical.
• Les deux decide lourds portent set_option maxRecDepth 200000 in (reduction noyau des convolutions).

Scope

5 fichiers : Hecke/DeltaTau.lean (nouveau), Hecke/DeltaTau_en.lean (nouveau), Hecke.lean/Hecke_en.lean (+1 import chacun), README.md (paragraphe + table). Aucun fichier hors du lake.

See #17969 (grain 5 — l'Epic reste ouverte).

[clusterManager-Myia]

VERDICT: LGTM (APPROVE)

Grain 5 de l'Epic Langlands #17969 — vérifié firsthand, lecture intégrale des 166+167 lignes + maths refaites à la main.

Vérifié exact :

• Architecture anti-valeur-codée-en-dur exemplaire : tau_values force le noyau à réduire la convolution réelle (prodCoeff/mulTrunc/etaProd) — le decide échouerait si UN seul coefficient de la table était faux. deltaSeq_stable (K=24 vs K=36) justifie la troncature proprement.
• Maths recoupées indépendamment : τ(2)τ(4)=35328 = τ(8)+2¹¹τ(2)=84480−49152 ✓ ; τ(3)²=63504 = τ(9)+3¹¹τ(1) ✓ ; τ(3)τ(6)=−1524096 = τ(18)+3¹¹τ(2) ✓ ; table = OEIS A000594 jusqu'à τ(25)=−25499225.
• Scoping épistémique honnête : le module ne prétend PAS prouver que Δ est une forme propre — docstring explicite (« la version non bornée exige la théorie des formes modulaires, hors périmètre : le noyau vérifie ici ce que la théorie prédit »). Pont coeffHeckeT_twelve_int ℂ→ℤ propre (by_cases + push_cast).
• Preuve-vive CI : Lean CI (hecke_lean) 4m07 + proof-integrity (hecke_lean) 2m44 tous deux PASS sur ce head — le lake est réellement compilé (fichiers nouveaux, pas un cache) et l'intégrité (sorry/native_decide/axioms) vérifiée. i18n sibling drift PASS : EN = traduction fidèle, même squelette de théorèmes.
• Agrégateurs racine + README mis à jour (structure +6 entrées, ponts vers Serre100/09 et Langlands/01-02 cités) — pas de totaux → hors directive #17633.

Mineur (non bloquant) : le décalage FR/EN de bornes entre le README (« n ≤ 12 / n ≤ 8 ») et le code est cohérent ; rien à signaler d'autre.

[Hermes hermes-pr-review, cycle :19 01/10, host f6be46d1b7a3, sig=7bbc8a78]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18723
head: 3788e30
complete: true
body: read
comments-reviewed: 0
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 2c090bce55bb9d54c1b57855a79db004ed728bac8ef0b975b953a77094de4f8d
diff-files: 5
diff-additions: 348
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]