diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/kls_lean/KLS/Defs.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/kls_lean/KLS/Defs.lean
index ae4eea9aa54..ef961947b6a 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/kls_lean/KLS/Defs.lean
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/kls_lean/KLS/Defs.lean
@@ -69,8 +69,11 @@ def IsLogConcaveOnRR (f : ℝ → ℝ) : Prop :=
   ConvexOn ℝ (univ : Set ℝ) fun t => -Real.log (f t)
 
 /-- Convexité de `t ↦ t²/2` sur `ℝ`. L'identité clef sous `a + b = 1` :
-`a x² + b y² − (a x + b y)² = a b (x − y)² ≥ 0`. Aucun lemme de convexité du
-carré n'existe au pin (audit du 2026-10-07) — la preuve est autonome. -/
+`a x² + b y² − (a x + b y)² = a b (x − y)² ≥ 0`. Mathlib porte la convexité
+du carré au pin du lake (`520045ab14`) : `Even.convexOn_pow`
+(`Mathlib.Analysis.Convex.Mul:161`) et `convexOn_univ_norm`
+(`Mathlib.Analysis.Normed.Module.Convex:53`). La preuve reste autonome pour
+exposer l'identité scalaire clef, non par absence de lemme. -/
 theorem convexOn_half_sq : ConvexOn ℝ (univ : Set ℝ) fun t => (1 / 2) * t ^ 2 :=
   ⟨convex_univ, by
     intros
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/riemann200_lean/Riemann200/LiminfForme.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/riemann200_lean/Riemann200/LiminfForme.lean
index 37befc4ba85..e6ad1ce7f7c 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/riemann200_lean/Riemann200/LiminfForme.lean
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/riemann200_lean/Riemann200/LiminfForme.lean
@@ -18,9 +18,16 @@ dans le carnet R-12.
 
 ## Grounding mesuré (convention de la série)
 
-- Mathlib **ne porte pas** la fonction ζ ni ses zéros (v4.33.0, greppé au
-  grain 1) : le théorème A lui-même est hors de portée formelle ici, et
-  ce module ne le prétend pas.
+- Mathlib **porte** la fonction ζ et un début de zérologie formelle au pin
+  du lake (`db584cd6d4`) : `def riemannZeta`, sa dérivabilité hors de `s = 1`
+  et l'équation fonctionnelle (`Mathlib.NumberTheory.LSeries.RiemannZeta`) ;
+  les zéros triviaux, et l'ensemble `riemannZetaZeros` fermé, discret,
+  d'intersection finie avec tout compact
+  (`Mathlib.NumberTheory.LSeries.ZetaZeros`).
+- Le **théorème A** d'Alpöge–Furman, lui, reste hors de portée formelle ici :
+  Mathlib n'énonce pas la proportion de zéros simples sur la droite critique
+  (l'hypothèse de Riemann n'y figure que comme `Prop`,
+  `def RiemannHypothesis`), et ce module ne le prétend pas.
 - Mathlib **porte** : `Filter.liminf` et ses caractérisations
   (`Mathlib.Order.LiminfLimsup` — `le_liminf_iff`, `eventually_lt_of_lt_liminf`,
   dont les hypothèses de bornitude sont celles que ce module expose telles
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/riemann200_lean/Riemann200/Memoire1859.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/riemann200_lean/Riemann200/Memoire1859.lean
index 0900ce82684..031374588ef 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/riemann200_lean/Riemann200/Memoire1859.lean
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/riemann200_lean/Riemann200/Memoire1859.lean
@@ -16,14 +16,29 @@ d'Euler (1737) dont le mémoire hérite.
 
 ## Grounding mesuré (convention de la série)
 
-- Mathlib **ne porte pas** la fonction ζ ni la ligne critique : aucun
-  `RiemannZeta` dans l'arbre (v4.33.0, greppé au grain).
-- Mathlib **porte** : les p-séries et le test de condensation
+Mesuré au pin Mathlib du lake (`db584cd6d4`, greppé dans
+`.lake/packages/mathlib`) :
+
+- Mathlib **porte** la fonction ζ, son prolongement et son équation
+  fonctionnelle : `def riemannZeta := hurwitzZetaEven 0`
+  (`Mathlib.NumberTheory.LSeries.RiemannZeta:121`),
+  `differentiableAt_riemannZeta` hors de `s = 1` (l.139) et
+  `riemannZeta_one_sub` (l.178), qui énonce
+  `ζ(1 − s) = 2 · (2π)^(−s) · Γ(s) · cos(πs/2) · ζ(s)`.
+- Mathlib **porte** un début de zérologie : les zéros triviaux
+  (`riemannZeta_neg_two_mul_nat_add_one`, l.173) et l'ensemble
+  `riemannZetaZeros`, fermé, discret, d'intersection finie avec tout compact
+  (`Mathlib.NumberTheory.LSeries.ZetaZeros`, l.35-66). Elle **énonce**
+  l'hypothèse de Riemann (`def RiemannHypothesis`, l.185) sans la prouver :
+  la localisation des zéros sur la droite critique reste ouverte.
+- Mathlib **porte** aussi : les p-séries et le test de condensation
   (`Mathlib.Analysis.PSeries`) ; la divergence de la somme des inverses des
   premiers (`Mathlib.NumberTheory.SumPrimeReciprocals`).
-- Le prolongement, l'équation fonctionnelle et les zéros restent hors
-  Mathlib : ce sont les carnets R-01/R-02 de la série qui les rendent
-  **calculables** (`mpmath.zetazero`), pas formels.
+- Ce que ce module apporte n'est donc pas l'existence formelle de ζ : c'est
+  le **fil du mémoire** — le pôle en `s = 1`, le fait d'Euler de 1737, et
+  leurs ré-exports commentés. Les carnets R-01/R-02 rendent les zéros
+  **calculables** (`mpmath.zetazero`) ; ils ne sont pas seuls à les rendre
+  formels.
 -/
 
 import Mathlib.Analysis.PSeries