Add: lake riemann200_lean — module Memoire1859 (critère 2 de #20403)

[jsboige]

Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: LIGHT/ledger #20696

Ce que fait cette PR

Crée le lake compagnon riemann200_lean/ — critère d'acceptation 2 de l'EPIC #20403 (« au moins 1 module riemann200_lean/ avec lake build SUCCESS et distinct_code_sorry 0 »), résiduel réel de l'EPIC après la livraison des dix carnets R-01→R-10 (critère 1).

Premier module : Riemann200/Memoire1859.lean — le mémoire de novembre 1859 face à Mathlib.

Contenu du module

• pole_en_s_un — le pôle en s = 1 : la série harmonique diverge (not_summable_one_div_natCast, voie p-séries), l'obstacle qui force le prolongement analytique du mémoire.
• euler_inverses_premiers — Euler 1737, la moitié arithmétique du produit eulérien : la somme des inverses des premiers diverge (not_summable_one_div_on_primes).
• harmonique_partielle_ge_un — corollaire maison (preuve par Finset.sum_le_sum_of_subset_of_nonneg sur le singleton {0}) : chaque somme partielle atteint au moins 1.

Grounding mesuré (convention de la série, docstring du module)

• Mathlib ne porte pas ζ ni la ligne critique : aucun RiemannZeta dans l'arbre (greppé, v4.33.0 / db584cd6d46c).
• Mathlib porte : p-séries + condensation (Mathlib.Analysis.PSeries), divergence des inverses des premiers (Mathlib.NumberTheory.SumPrimeReciprocals).
• Prolongement, équation fonctionnelle, zéros : hors Mathlib — les carnets R-01/R-02 les rendent calculables (mpmath.zetazero), pas formels.

Validation

lake build          # SUCCESS — « Build completed successfully (2356 jobs) » (v4.33.0, pin mathlib db584cd6d46c — mêmes pins que serre100_lean/hecke_lean)
python scripts/lean/count_code_sorry.py --json   # riemann200_lean : files 3, distinct_code_sorry 0, vacuous []

• Docstrings françaises (convention i18n du dépôt) ; agrégateur racine FR-only by design (pattern i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980, rollout DRAINED).
• lean-toolchain : leanprover/lean4:v4.33.0 (même toolchain que le pin mathlib ; sans ce fichier, elan résout la toolchain par défaut de la machine → mismatch de version sur les deps, mesuré : Qq.Delab en Unknown identifier delabLevel).

See #20403 — critère 2 rempli ; l'EPIC reste ouverte (digestion des 9 PRs carnets, liens croisés).

🤖 Generated with Claude Code

[clusterManager-Myia]

[Hermes] VERDICT: LGTM — lake Lean neuf, lecture intégrale des 68 lignes de Riemann200/Memoire1859.lean au head 17caa7bd.

Vérifications exécutées :

1. Contenu du module lu en entier : 2 ré-exports commentés de Mathlib (pole_en_s_un = Real.not_summable_one_div_natCast ; euler_inverses_premiers = not_summable_one_div_on_primes) + 1 preuve maison harmonique_partielle_ge_un (calc : singleton {0} ⊆ Finset.range(N+1), terme n=0 → 1/1 = 1, sum_le_sum_of_subset_of_nonneg + positivity) — la preuve est correcte et c'est un vrai corollaire, pas un habillage.
2. 0 sorry/admit/native_decide dans le code (les seuls hits du diff sont de la prose README citant le compteur).
3. Pins vérifiés par fetch direct : lake-manifest.json de riemann200_lean porte mathlib rev db584cd6d46c… — identique à serre100_lean au même ref, conformément au claim « mêmes pins » du body ; lean-toolchain v4.33.0 cohérent avec le pin.
4. Grounding honnête : la docstring assume que Mathlib ne porte ni ζ ni la ligne critique (aucun RiemannZeta), et que le module ne couvre que le premier chapitre du mémoire — pas de surenchère.
5. README : la ligne du lake passe du futur (« vivra… à créer ») au présent avec lien réel — pas un total-count, #17633 respecté.
6. Sécurité : 0 hit sur le diff (HF_TOKEN/API_KEY/BEARER/PASSWORD/SECRET/TOKEN=).

Note : je n'ai pas rejoué lake build localement (pas d'environnement Lean sur ce siège) — la validation repose sur les claims du body (2356 jobs SUCCESS) + pins cohérents + CI repo. Si un organe lean de la CI échoue sur ce head, ce point est le seul à re-vérifier.

— Hermes (myia-ai-01) [review bot]

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #20698 (Add: lake riemann200_lean — module Memoire1859 (critère 2 de #20403)) 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.

• fort -- Add(notebook-python,#20403): Riemann200 R-04 -- l'integrale de Riemann (sommes de Darboux) #20460 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/README.md (issues communes : EPIC: Riemann 200 — distillations exécutables des thèmes de Bernhard Riemann #20403)
• fort -- Add(notebook-python,#20403): Riemann200 R-01 -- le memoire de 1859, zeta et l'hypothese #20531 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/README.md (issues communes : EPIC: Riemann 200 — distillations exécutables des thèmes de Bernhard Riemann #20403)
• fort -- feat(notebooks,#20403): Riemann200 R-02 -- la formule explicite, la musique des premiers #20533 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/README.md (issues communes : EPIC: Riemann 200 — distillations exécutables des thèmes de Bernhard Riemann #20403)
• fort -- Add(notebook-python,#20403): Riemann200 R-05 -- la sphere de Riemann et les transformations de Mobius #20601 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/README.md (issues communes : EPIC: Riemann 200 — distillations exécutables des thèmes de Bernhard Riemann #20403)
• fort -- Add(notebook-python,#20403): Riemann200 R-06 -- surfaces de Riemann, monodromie mesurée #20616 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/README.md (issues communes : EPIC: Riemann 200 — distillations exécutables des thèmes de Bernhard Riemann #20403)
• fort -- Add(notebook-python,#20403): Riemann200 R-09 -- Riemann-Lebesgue et Fourier, phenomene de Gibbs mesure #20648 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/README.md (issues communes : EPIC: Riemann 200 — distillations exécutables des thèmes de Bernhard Riemann #20403)
• fort -- Add(riemann200,#20403): R-07 geometrie riemannienne -- habilitation 1854 (metrique, distance, courbure) #20654 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/README.md (issues communes : EPIC: Riemann 200 — distillations exécutables des thèmes de Bernhard Riemann #20403)
• fort -- Add(riemann200,#20403): R-10 le memoire de 1860 -- invariants de Riemann et ondes de choc #20694 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/README.md (issues communes : EPIC: Riemann 200 — distillations exécutables des thèmes de Bernhard Riemann #20403)