diff --git a/.claude/rules/pr-review-discipline.md b/.claude/rules/pr-review-discipline.md
index 8dc216430e..3bfb51ba13 100644
--- a/.claude/rules/pr-review-discipline.md
+++ b/.claude/rules/pr-review-discipline.md
@@ -75,7 +75,7 @@ Single-seed ou single-fold = **CHANGES_REQUESTED** sauf flag explicite `[POC]` d
 
 7. **PRs notebook : lire le check-run ADVISORY `Output-collapse ratchet (base vs PR, advisory)`** (organe `scripts/notebook_tools/check_output_collapse.py`, enregistré `blocking=False` dans `scripts/ci/fast_lane_registry.py`, #15327). Conclusion neutre par design — le signal vit dans le détail du check-run. Un finding `SIGNATURE` (sortie base substantielle remplacée par « `Execution sautee (API non configuree)` » et consœurs) = **re-exécution sans les clés → `CHANGES_REQUESTED`** : les cellules se sont « exécutées avec succès » en dégradation gracieuse (`if api_ok:`), c'est le contournement de C.2 par la porte de secours. Contre-exemple mesuré (fondateur) : #15209, `Lean-7b-Examples.ipynb` `6b327a9bf` → `56d98429a` — 11 → 11 cellules, 0 erreur, `execution_count` réels partout, et **10637 → 2985** caractères de sortie (cellules `2195 → 147`, `2568 → 38`, `2074 → 42`) : tous les organes verts, la perte réelle. Un finding `MAGNITUDE` (perte d'un ordre de grandeur par cellule, non couvert par les exemptions automatiques contenu-déplacé/purge-diagnostic) exige une **justification dans le body** (allègement déclaré, au même titre que les autres ratchets) — sans elle : `CHANGES_REQUESTED`.
 
-8. **PRs notebook : lire le check-run ADVISORY `Source-collapse ratchet (base vs PR, advisory)`** (organe `scripts/notebook_tools/check_source_collapse.py`, enregistré `blocking=False` dans `scripts/ci/fast_lane_registry.py`, #15901). Le point 7 mesure la perte de **sortie**, celui-ci la perte de **source** : les deux sont indépendantes, et c'est tout l'intérêt. Contre-exemple mesuré (fondateur) : #15862, `GameTheory-06e-Open-Source-Game-Theory.ipynb` `244c7c54f032` → `7a355873de32`, cellule `c989_independent_v2` **8425 → 5309** caractères de source (-37.0 %, 3116 perdus) — une table déclarative et un `assert` avaient disparu, aucun organe rouge, parce qu'une table supprimée et un `assert` reduit ne produisent **aucune sortie** : la perte est invisible par construction aux ratchets de sortie. Un finding `MAGNITUDE` exige une **justification dans le body** (allègement déclaré) — sans elle : `CHANGES_REQUESTED`. Les exemptions automatiques (contenu déplacé vers une AUTRE cellule du **même** notebook, purge de texte de diagnostic type `CS####`/`warning`) blanchissent le signal : leur silence n'est **pas** un acquittement, et un `exempt-moved` qui ne déplace que quelques lignes doit être recontrôlé à l'œil. Le **même** check-run porte depuis #16110 le **second mécanisme** de la famille, pris par l'autre bout : la source survit en volume et perd sa **forme**. Un finding `STRUCTURE` signale `emptied` (la cellule avait des instructions, elle n'en a plus) et/ou `orphan-output` (elle porte une sortie qu'aucune instruction ne peut avoir produite) : le code est parti, la preuve d'exécution est restée → **restaurer la source ou retirer la sortie**, sinon `CHANGES_REQUESTED`. Contre-exemple mesuré (fondateur) : #16097, `Lean-18-Sendov-Complex-Analysis.ipynb` cellule `40cb37d5`, **1132 → 1728** caractères (la cellule **grossit** : la même écriture qui a retiré les `\n` a ajouté une note de récupération) et `ast.parse(...).body` **10 → 0** — tout le code replié en un seul commentaire. Le ratchet de volume ne pouvait pas le voir (le gate s'arrête avant tout plancher quand la tête est plus longue) et `notebook-cell-source-parses` non plus (une cellule intégralement commentée se **parse proprement**) : `orphan-output` ne consulte que la cellule, il n'y a aucune exemption qui le blanchisse.
+8. **PRs notebook : lire le check-run ADVISORY `Source-collapse ratchet (base vs PR, advisory)`** (organe `scripts/notebook_tools/check_source_collapse.py`, enregistré `blocking=False` dans `scripts/ci/fast_lane_registry.py`, #15901). Le point 7 mesure la perte de **sortie**, celui-ci la perte de **source** : les deux sont indépendantes, et c'est tout l'intérêt. Contre-exemple mesuré (fondateur) : #15862, `GameTheory-06e-Open-Source-Game-Theory.ipynb` `244c7c54f032` → `7a355873de32`, cellule `c989_independent_v2` **8425 → 5309** caractères de source (-37.0 %, 3116 perdus) — une table déclarative et un `assert` avaient disparu, aucun organe rouge, parce qu'une table supprimée et un `assert` reduit ne produisent **aucune sortie** : la perte est invisible par construction aux ratchets de sortie. Un finding `MAGNITUDE` exige une **justification dans le body** (allègement déclaré) — sans elle : `CHANGES_REQUESTED`. Les exemptions automatiques (contenu déplacé vers une AUTRE cellule du **même** notebook, purge de texte de diagnostic type `CS####`/`warning`) blanchissent le signal : leur silence n'est **pas** un acquittement, et un `exempt-moved` qui ne déplace que quelques lignes doit être recontrôlé à l'œil. Le **même** check-run porte depuis #16110 le **second mécanisme** de la famille, pris par l'autre bout : la source survit en volume et perd sa **forme**. Un finding `STRUCTURE` signale `emptied` (la cellule avait des instructions, elle n'en a plus) et/ou `orphan-output` (elle porte une sortie qu'aucune instruction ne peut avoir produite) : le code est parti, la preuve d'exécution est restée → **restaurer la source ou retirer la sortie**, sinon `CHANGES_REQUESTED`. Contre-exemple mesuré (fondateur) : #16097, `ANALYSE-01-Sendov-Lean-Python.ipynb` cellule `40cb37d5`, **1132 → 1728** caractères (la cellule **grossit** : la même écriture qui a retiré les `\n` a ajouté une note de récupération) et `ast.parse(...).body` **10 → 0** — tout le code replié en un seul commentaire. Le ratchet de volume ne pouvait pas le voir (le gate s'arrête avant tout plancher quand la tête est plus longue) et `notebook-cell-source-parses` non plus (une cellule intégralement commentée se **parse proprement**) : `orphan-output` ne consulte que la cellule, il n'y a aucune exemption qui le blanchisse.
 
 **Advisory `.NET execution_count` ≠ outputs vides autorisés (#5214).** L'advisory autorise à sauter la ré-exécution **CI** (pas de kernel .NET en CI), **pas** à committer des sorties vides : `.NET Interactive` s'exécute **localement** sur chaque worker → une cellule .NET committée **DOIT** porter `execution_count != null`. `validate_pr_notebooks.py` FAIL sur `.NET` + `null`, et ne tolère `null` que là où l'exécution locale est aussi impossible (QC Cloud, Lean). Verdict attendu dans le body : `EXEC_PROVED` vs `STRUCTURAL_ONLY` (refus).
 
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb
similarity index 99%
rename from MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.ipynb
rename to MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb
index 3ab7549a8f..252f9d9525 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb
@@ -26,7 +26,7 @@
     "\n",
     "| Notebook precedent | Notebook suivant |\n",
     "|---|---|\n",
-    "| [A* Optimalite (Search-03e)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | [Lean-19 - Analysis-I Tao Workflow](Lean-19-Analysis-I-Tao-Workflow.ipynb) |\n",
+    "| [A* Optimalite (Search-03e)](../../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | [Lean-19 - Analysis-I Tao Workflow](ANALYSE-02-Tao-Lean-Python.ipynb) |\n",
     "\n",
     "***\n",
     "\n",
@@ -1360,8 +1360,8 @@
    "end_time": "2026-09-14T09:43:28.570564+00:00",
    "environment_variables": {},
    "exception": null,
-   "input_path": "Lean-18-Sendov-Complex-Analysis.ipynb",
-   "output_path": "Lean-18-Sendov-Complex-Analysis.ipynb",
+   "input_path": "ANALYSE-01-Sendov-Lean-Python.ipynb",
+   "output_path": "ANALYSE-01-Sendov-Lean-Python.ipynb",
    "parameters": {},
    "start_time": "2026-09-14T09:43:09.504617+00:00",
    "version": "2.6.0"
@@ -1369,4 +1369,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
\ No newline at end of file
+}
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Analysis-I-Tao-Workflow.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb
similarity index 99%
rename from MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Analysis-I-Tao-Workflow.ipynb
rename to MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb
index 7464eca6b0..0ba8f4861c 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Analysis-I-Tao-Workflow.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb
@@ -25,7 +25,7 @@
     "\n",
     "| Notebook precedent | Notebook suivant |\n",
     "|---|---|\n",
-    "| [Lean-18 - Sendov Complex Analysis](Lean-18-Sendov-Complex-Analysis.ipynb) | [Lean-20 - PFR Entropy Method](Lean-20-PFR-Entropy-Method.ipynb) |\n",
+    "| [Lean-18 - Sendov Complex Analysis](ANALYSE-01-Sendov-Lean-Python.ipynb) | [Lean-20 - PFR Entropy Method](ANALYSE-03-PFR-Lean.ipynb) |\n",
     "\n",
     "***\n",
     "\n",
@@ -37,7 +37,7 @@
     "\n",
     "- Notre serie Lean a deja couvert Sendov (Lean-18 : digestion par Tao de la preuve de L. Mazur, analyse complexe, 1 grain = 1 théorème). Pour ce 2e grain — cette fois une oeuvre propre de Tao — on prend du recul : ce n'est plus *un* théorème mais *un manuel entier* (11 chapitres, 109 fichiers, 44 297 LOC, 2079 `sorry` deliberes par l'auteur comme exercices au lecteur).\n",
     "- **Substance nouvelle** : Lean-19 est le premier grain de notre serie qui est *Lean-meta* (recit methodologique) plutot que *Lean-content* (preuve formelle). C'est ce qu'on appelle dans le jargon de la preuve agentique un *process notebook* — un notebook qui decrit un processus de preuve, pas une preuve.\n",
-    "- **Méthode nouvelle** : comparaison directe avec notre cluster — en realite TROIS méthodes : Tao a la main (seul, 2 ans, 5-15 commits/jour), Tao + grosse machinerie (Sendov digere en 2 jours, cf. [Lean-18](Lean-18-Sendov-Complex-Analysis.ipynb)), et notre cluster (4 workers + 1 coordinateur, ~2 PRs/h, petits increments sur des problemes varies). Quels sont les tradeoffs ?\n",
+    "- **Méthode nouvelle** : comparaison directe avec notre cluster — en realite TROIS méthodes : Tao a la main (seul, 2 ans, 5-15 commits/jour), Tao + grosse machinerie (Sendov digere en 2 jours, cf. [Lean-18](ANALYSE-01-Sendov-Lean-Python.ipynb)), et notre cluster (4 workers + 1 coordinateur, ~2 PRs/h, petits increments sur des problemes varies). Quels sont les tradeoffs ?\n",
     "- **Apport a Mathlib** : Tao n'utilise presque pas Mathlib dans les chapitres 2-5 (auto-contenu, axiomes Peano, construction de Cauchy des réels), puis transitionne progressivement vers Mathlib a partir du chapitre 6. C'est une approche pedagogique rare — la plupart des projets partent de Mathlib.\n",
     "\n",
     "**Note methodologique** : conformement a la convention de notre serie (cf. Lean-12 Sensitivity, Lean-17 Knots, Lean-18 Sendov), ce notebook utilise un **kernel Python 3**, pas Lean 4. Les enonces Lean sont presentes sous forme pedagogique (pseudo-Lean), et les preuves sont illustrees en Python. Le **vrai code Lean** est disponible dans le lac source : `git clone https://github.com/teorth/analysis && cd analysis && lake build`."
@@ -535,7 +535,7 @@
     "\n",
     "| | Méthode 1 — Humain a la main, longue haleine | Méthode 2 — Single-agent + grosse machinerie | Méthode 3 — Cluster distribue |\n",
     "|---|---|---|---|\n",
-    "| **Exemple** | Tao, *Analysis I* (ce manuel) | Tao digerant la preuve Sendov de L. Mazur ([Lean-18](Lean-18-Sendov-Complex-Analysis.ipynb)) | CoursIA (ce depot) |\n",
+    "| **Exemple** | Tao, *Analysis I* (ce manuel) | Tao digerant la preuve Sendov de L. Mazur ([Lean-18](ANALYSE-01-Sendov-Lean-Python.ipynb)) | CoursIA (ce depot) |\n",
     "| **Duree** | 2 ans, continuite | 2 jours, sprint intensif | continue, sans terme |\n",
     "| **Machinerie** | Lean 4 + Mathlib, en grande partie a la main | Claude Opus 5 en co-pilote (14,9k LOC en 2 jours) | 4-5 workers + coordinateur + harnais de regles |\n",
     "| **Objet** | UN projet profond tenu longtemps : manuel complet, 11 chapitres | UN théorème SOTA digere en entier | problemes varies ; les 2 travaux presentes ici (Lean-18, Lean-19) sont des petites noix typiques |\n",
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-PFR-Entropy-Method.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-03-PFR-Lean.ipynb
similarity index 99%
rename from MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-PFR-Entropy-Method.ipynb
rename to MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-03-PFR-Lean.ipynb
index 1b1d5c0336..ba1c9eefe5 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-PFR-Entropy-Method.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-03-PFR-Lean.ipynb
@@ -29,7 +29,7 @@
     "\n",
     "| Notebook précédent | Notebook suivant |\n",
     "|---|---|\n",
-    "| [Lean-19 - Analysis-I Tao Workflow](Lean-19-Analysis-I-Tao-Workflow.ipynb) | [Lean-21 - MIMO Detection Flips](Lean-21-MIMO-Detection-Flips.ipynb) |\n",
+    "| [Lean-19 - Analysis-I Tao Workflow](ANALYSE-02-Tao-Lean-Python.ipynb) | [Lean-21 - MIMO Detection Flips](../Lean-21-MIMO-Detection-Flips.ipynb) |\n",
     "\n",
     "***\n",
     "\n",
@@ -1384,13 +1384,13 @@
    "source": [
     "## 7. Pont vers la série ICT — l'entropie comme monnaie commune\n",
     "\n",
-    "La série [ICT](../../IIT/ICT-Series/) (information et calcul) manipule l'entropie dans des contextes très différents de la combinatoire additive. PFR s'y rattache directement :\n",
+    "La série [ICT](../../../IIT/ICT-Series/) (information et calcul) manipule l'entropie dans des contextes très différents de la combinatoire additive. PFR s'y rattache directement :\n",
     "\n",
     "| Notebook ICT | Rôle de l'entropie | Lien avec PFR |\n",
     "|---|---|---|\n",
-    "| [ICT-16 — MDL](../../IIT/ICT-Series/ICT-16-MDLTwoPartCode.ipynb) | longueur de code minimale = entropie | `binEntropy` est la longueur du code optimal d'un bit biaisé (section 5) |\n",
-    "| [ICT-17 — Epsilon-machine](../../IIT/ICT-Series/ICT-17-EpsilonMachine.ipynb) | entropie des états causaux, complexité statistique | « structure = compressibilité » : mesurer l'entropie pour révéler la machine cachée |\n",
-    "| [ICT-14 — Free energy](../../IIT/ICT-Series/ICT-14-FreeEnergySurprise.ipynb) | surprise, bornes informationnelles | l'information comme borne sur le comportement d'un système |\n",
+    "| [ICT-16 — MDL](../../../IIT/ICT-Series/ICT-16-MDLTwoPartCode.ipynb) | longueur de code minimale = entropie | `binEntropy` est la longueur du code optimal d'un bit biaisé (section 5) |\n",
+    "| [ICT-17 — Epsilon-machine](../../../IIT/ICT-Series/ICT-17-EpsilonMachine.ipynb) | entropie des états causaux, complexité statistique | « structure = compressibilité » : mesurer l'entropie pour révéler la machine cachée |\n",
+    "| [ICT-14 — Free energy](../../../IIT/ICT-Series/ICT-14-FreeEnergySurprise.ipynb) | surprise, bornes informationnelles | l'information comme borne sur le comportement d'un système |\n",
     "\n",
     "Le slogan commun : **l'information mesure la structure**. En ICT, une faible complexité statistique révèle une machine à états petite ; en théorie additive, une **petite duplication** (peu d'entropie dans X + X′) force une **structure algébrique** — le sous-espace H de la conjecture de Marton. PFR est un théorème de « compression ⟹ structure », et il est prouvé par la théorie de l'information elle-même."
    ]
@@ -1498,7 +1498,7 @@
     "\n",
     "**Dette 3 -- Generalisation aux structures non-polynomiales.** PFR polynomial dit : si la pluie sur les `n` degres est `1/n^(1+δ)`, alors structure. La generalisation aux structures non-polynomiales (pluie exponentielle, melange Markov, chaines de Markov) reste conjecturale. Le travail de Gowers 2016 sur la *Normalised Fourier Analysis* n'aborde pas la generalisation.\n",
     "\n",
-    "**Dette 4 -- Pont vers la serie ICT non formalise.** La section 7 evoque le pont « entropie comme monnaie commune » avec la serie [ICT](../../IIT/ICT-Series/), mais le pont formel entre `PFR.ForMathlib.Entropy.Basic` et `InformationFlow.lean` (ICT) n'est pas etabli. Une issue de suivi pourrait nommer ce deficit dans l'EPIC #13106 (tranche D, hors cette PR).\n",
+    "**Dette 4 -- Pont vers la serie ICT non formalise.** La section 7 evoque le pont « entropie comme monnaie commune » avec la serie [ICT](../../../IIT/ICT-Series/), mais le pont formel entre `PFR.ForMathlib.Entropy.Basic` et `InformationFlow.lean` (ICT) n'est pas etabli. Une issue de suivi pourrait nommer ce deficit dans l'EPIC #13106 (tranche D, hors cette PR).\n",
     "\n",
     "**Statut au 2026-09** : ces quatre dettes sont *documentees*, pas *resolues*. Elles relevent d'un travail ulterieur, pas d'un fix de fond dans ce notebook. La mention explicite sert deux fins : (a) empecher un lecteur de croire la preuve close sur les points quantitatifs ; (b) ouvrir la voie a un futur grain qui attaquerait l'une des quatre."
    ]
@@ -1517,7 +1517,9 @@
     "tags": []
    },
    "source": [
-    "## 9. Exercices\n\nTrois exercices pour s'approprier les briques. Chaque cellule code est un point de départ **exécutable** : elle charge l'énoncé-cible (`#check`) ou un calcul d'amorce (`#eval`), et laisse le raisonnement en `TODO`. Le kernel persiste d'une cellule à l'autre : les définitions du Code 2.1 (`addBit`, `sumset`) restent disponibles."
+    "## 9. Exercices\n",
+    "\n",
+    "Trois exercices pour s'approprier les briques. Chaque cellule code est un point de départ **exécutable** : elle charge l'énoncé-cible (`#check`) ou un calcul d'amorce (`#eval`), et laisse le raisonnement en `TODO`. Le kernel persiste d'une cellule à l'autre : les définitions du Code 2.1 (`addBit`, `sumset`) restent disponibles."
    ]
   },
   {
@@ -1786,7 +1788,7 @@
     "2. Le cas d'égalité est caractérisé par `binEntropy_eq_log_two` : H₂(p) = log 2 ⟺ p = 1/2.\n",
     "3. Avec `binEntropy_eq_zero` : H₂(p) = 0 ⟺ p ∈ {0, 1} — une pièce parfaitement déterminée n'a aucune incertitude.\n",
     "\n",
-    "**Conclusion attendue** : le bit le plus imprévisible possible est un bit **équilibré** — pont direct vers [ICT-16](../../IIT/ICT-Series/ICT-16-MDLTwoPartCode.ipynb) : le code le plus court pour un bit est celui d'une pièce honnête."
+    "**Conclusion attendue** : le bit le plus imprévisible possible est un bit **équilibré** — pont direct vers [ICT-16](../../../IIT/ICT-Series/ICT-16-MDLTwoPartCode.ipynb) : le code le plus court pour un bit est celui d'une pièce honnête."
    ]
   },
   {
@@ -1912,7 +1914,7 @@
     "\n",
     "### 10.3 Ce qui reste ouvert\n",
     "\n",
-    "L'exposant continue de baisser (12 → 11,123 → 11 → 9) ; l'extension aux groupes de torsion bornée avance dans le lac ; et la version entropique elle-même (`entropic_PFR_conjecture`) reste un bel objet d'étude — la constante 11 y est-elle optimale ? Autant de grains futurs pour cette série — et côté [ICT](../../IIT/ICT-Series/), l'entropie y reviendra sous toutes ses formes."
+    "L'exposant continue de baisser (12 → 11,123 → 11 → 9) ; l'extension aux groupes de torsion bornée avance dans le lac ; et la version entropique elle-même (`entropic_PFR_conjecture`) reste un bel objet d'étude — la constante 11 y est-elle optimale ? Autant de grains futurs pour cette série — et côté [ICT](../../../IIT/ICT-Series/), l'entropie y reviendra sous toutes ses formes."
    ]
   }
  ],
@@ -1932,4 +1934,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
\ No newline at end of file
+}
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20b-PFR-Primitives-Transportables.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb
similarity index 99%
rename from MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20b-PFR-Primitives-Transportables.ipynb
rename to MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb
index a5d127b736..48de54cbc3 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20b-PFR-Primitives-Transportables.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb
@@ -17,7 +17,7 @@
     "# Lean-20b : Trois primitives de PFR, et l'endroit exact où elles cessent de valoir\n",
     "\n",
     "**Série** : SymbolicAI / Lean — Digestions de résultats profonds, companion de Lean-20\n",
-    "**Source** : Lean-20-PFR-Entropy-Method.ipynb (digestion PFR par Gowers-Green-Manners-Tao, 2023)\n",
+    "**Source** : ANALYSE-03-PFR-Lean.ipynb (digestion PFR par Gowers-Green-Manners-Tao, 2023)\n",
     "**Lac source** : https://github.com/teorth/pfr (formalisation collaborative Lean 4)\n",
     "**Kernel** : `lean4-wsl` — le notebook conceptuel Python illustre les primitives, les preuves formelles restent dans Lean-20\n",
     "\n",
@@ -25,7 +25,7 @@
     "\n",
     "| Notebook précédent | Notebook suivant |\n",
     "|---|---|\n",
-    "| [Lean-20 - PFR Entropy Method](Lean-20-PFR-Entropy-Method.ipynb) | [Lean-21 - MIMO Detection Flips](Lean-21-MIMO-Detection-Flips.ipynb) |\n",
+    "| [Lean-20 - PFR Entropy Method](ANALYSE-03-PFR-Lean.ipynb) | [Lean-21 - MIMO Detection Flips](../Lean-21-MIMO-Detection-Flips.ipynb) |\n",
     "\n",
     "***\n",
     "\n",
@@ -991,14 +991,14 @@
    "end_time": "2026-09-02T21:29:17.311787",
    "environment_variables": {},
    "exception": null,
-   "input_path": "Lean-20b-PFR-Primitives-Transportables.ipynb",
-   "output_path": "Lean-20b-PFR-Primitives-Transportables.ipynb",
+   "input_path": "ANALYSE-04-PFR-Primitives-Python.ipynb",
+   "output_path": "ANALYSE-04-PFR-Primitives-Python.ipynb",
    "parameters": {},
    "start_time": "2026-09-02T21:29:13.778559",
    "version": "2.6.0"
   },
   "references": [
-   "Lean-20-PFR-Entropy-Method.ipynb (companion upstream)",
+   "ANALYSE-03-PFR-Lean.ipynb (companion upstream)",
    "Gowers, Green, Manners, Tao (novembre 2023) — On a conjecture of Marton",
    "https://github.com/teorth/pfr — formalisation collaborative Lean 4"
   ],
@@ -1006,4 +1006,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
\ No newline at end of file
+}
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md
new file mode 100644
index 0000000000..598cf562f6
--- /dev/null
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md
@@ -0,0 +1,18 @@
+# ANALYSE — formalisations d'analyse, digérées
+
+Sous-série de la série [Lean](../README.md) (décision de gradation #17545, 24/09) : les formalisations de recherche en analyse — Sendov, *Analysis I* de Tao, PFR — descendent ici avec un arc interne **Licence → Recherche** : chaque carnet part d'un énoncé lisible et finit sur le lac réel cité par ses déclarations.
+
+La série principale garde son tutoriel (numéros 1 à 14) ; le présent dossier porte l'arc d'analyse. Les numéros de la table ci-dessous renvoient à l'ancien identifiant de série (`Lean-18` → `ANALYSE-01`, etc. — table de correspondance dans `docs/reference/rename-ledger.tsv`).
+
+| Carnet | Contenu | Durée |
+|---|---|---|
+| [ANALYSE-01-Sendov-Lean-Python](ANALYSE-01-Sendov-Lean-Python.ipynb) | La conjecture de Sendov (preuve L. Mazur 2026, digestion et formalisation T. Tao) : pour un polynôme dont tous les zéros sont dans le disque unité, chaque zéro a un point critique à distance ≤ 1 — énoncé, illustrations numériques des cas, contexte de la preuve | 45 min |
+| [ANALYSE-02-Tao-Lean-Python](ANALYSE-02-Tao-Lean-Python.ipynb) | Le manuel *Analysis I* de T. Tao en lac Lean 4 (`teorth/analysis`) : architecture du lac, philosophie d'auto-contenance vs Mathlib, cinq lemmes emblématiques parmi 44k LOC, méta-récit single-agent vs cluster distribué | 40 min |
+| [ANALYSE-03-PFR-Lean](ANALYSE-03-PFR-Lean.ipynb) | La conjecture PFR (polynomial Freiman–Ruzsa, ZMod 2) : méthode entropique de la preuve `teorth/pfr` — énoncé combinatoire, illustrations cosets dans F₂³, `#check` réels et axiomes du lac compilé | 45 min |
+| [ANALYSE-04-PFR-Primitives-Python](ANALYSE-04-PFR-Primitives-Python.ipynb) | Trois primitives de PFR, et l'endroit exact où elles cessent de valoir — companion de digestion de ANALYSE-03 : ce qui se transporte hors du cadre d'origine (#12214) | 30 min |
+
+**Prérequis d'entrée** : le tutoriel de la série principale (numéros 1 à 6, tactiques et Mathlib). Le point d'entrée réel documenté du carnet 01 est [Search-03e-AStar-Optimality](../../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) (heuristique A*, companion `search_lean`) — voir sa cellule d'ouverture.
+
+**Marches nommées, à écrire** (règle 5 de la gradation) : entropie de Shannon avant ANALYSE-03, inégalités de concentration avant le converse MIMO ([Lean-21b](../Lean-21b-MIMO-Converse-Native.ipynb)). Elles vivront dans ce dossier ou la série principale selon la décision de renumérotation.
+
+**Marches franchissables** : depuis la série principale, le tutoriel (1-14) suffit pour ANALYSE-01. ANALYSE-02 suppose la lecture d'un lac externe ; ANALYSE-03/04 supposent l'entropie de Shannon (marche nommée ci-dessus).
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb
index 0ca0afe9e1..a5fd6f945c 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb
@@ -16,7 +16,7 @@
    "source": [
     "# Lean-21 : Detection MIMO par flips -- le seuil 2 log N sous preuve Lean\n",
     "\n",
-    "**Navigation** : [Index](README.md) | [Lean-20 (PFR)](Lean-20-PFR-Entropy-Method.ipynb) | [Lean-22 (Galois) >>](Lean-22-Galois-Probleme-Inverse-M23.ipynb)\n",
+    "**Navigation** : [Index](README.md) | [Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb) | [Lean-22 (Galois) >>](Lean-22-Galois-Probleme-Inverse-M23.ipynb)\n",
     "\n",
     "Ce notebook presente le lake **`mimo_lean`** de ce depot (issue #10984) : le port\n",
     "formel de l'algorithme de detection MIMO par flips de coordonnées de\n",
@@ -39,7 +39,7 @@
     "`M·ε·φ(2) ≥ 2·log N − log log N`, `P(erreur ML) ≥ 1 − exp(−(2·log N − log log N))`\n",
     "(issues #11673, #11709).\n",
     "\n",
-    "Comme dans [Lean-20](Lean-20-PFR-Entropy-Method.ipynb), nous procedons en deux\n",
+    "Comme dans [Lean-20](ANALYSE/ANALYSE-03-PFR-Lean.ipynb), nous procedons en deux\n",
     "registres : des **illustrations numeriques** (Python) qui montrent les phenomenes,\n",
     "puis des **`#check` reels** executes par `lake env lean` sur le lac compile --\n",
     "les enonces affiches sont ceux que le compilateur Lean 4 a verifies, pas des\n",
@@ -1965,7 +1965,7 @@
     "- **YuanheZ/lean-stat-learning-theory** (ICML 2026, Apache 2.0) :\n",
     "  Hanson-Wright, mesures gaussiennes -- dependance externe de la Phase 3b.\n",
     "- **Mathlib 4** : `MeasureTheory`, `ProbabilityTheory`, espaces de Hilbert.\n",
-    "- Notebooks associes : [Lean-20 (PFR)](Lean-20-PFR-Entropy-Method.ipynb),\n",
+    "- Notebooks associes : [Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb),\n",
     "  [A* Optimalite (Search-03e)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb),\n",
     "  [Lean-6 (Mathlib)](Lean-6-Mathlib-Essentials.ipynb)."
    ]
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb
index dfb96fa239..1719146deb 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb
@@ -1535,7 +1535,7 @@
     "- **D. Papailiopoulos** (2026) - *Detection MIMO by coordinate flips : Proposition 9.1* (papier source des theoremes `Descent.lean`).\n",
     "- **`Descent.lean`** (`MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/`) - la formalisation : `Run` (inductif sur List sigma), `lastState`, lemmes 1-3 (`run_tail_cost_lt`, `run_nodup`, `run_length_le_cost`), `descent_flips_le_barrier`, `descent_target_before_ceiling`. Aucun `sorry`, aucun `axiom NAME := ...` global, aucun `native_decide`.\n",
     "- **`lean4-wsl` kernel** - Repare c.380, valide c.426, reutilise pour ce notebook (le pattern << lecture directe des sources >> permet l'execution Python portable sans `lake env lean`).\n",
-    "- **Notebooks Lean associes** : `[Lean-24 (Calibration)](Lean-24-Calibration-Native-Companion.ipynb)`, `[Lean-23 (ERC-20)](Lean-23-ERC20-Invariant-Companion.ipynb)`, `[Lean-22 (Galois)](Lean-22-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-21 (MIMO)](Lean-21-MIMO-Detection-Flips.ipynb)`, `[Lean-20 (PFR)](Lean-20-PFR-Entropy-Method.ipynb)`.\n",
+    "- **Notebooks Lean associes** : `[Lean-24 (Calibration)](Lean-24-Calibration-Native-Companion.ipynb)`, `[Lean-23 (ERC-20)](Lean-23-ERC20-Invariant-Companion.ipynb)`, `[Lean-22 (Galois)](Lean-22-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-21 (MIMO)](Lean-21-MIMO-Detection-Flips.ipynb)`, `[Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb)`.\n",
     "- **EPIC #4980** - convention i18n Lean (lac `mimo_lean` est FR-only ; un sibling pair `_en.lean` est une suite a explorer mais hors scope de ce notebook).\n",
     "- **Regle C.1** - pas d'erreur volontaire dans les cellules d'exercice (stub `pass` ou `print(\"Exercice a completer\")`).\n",
     "- **Regle C.7 (count_code_sorry)** - l'instrument canonique `scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`), jamais `grep -c sorry`. Cf [anti-regression.md](../../../.claude/rules/anti-regression.md)."
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb
index a88d992b36..ca15b2a15f 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb
@@ -1379,7 +1379,7 @@
     "- **Lake `erc20_lean`** (`MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean/`) — la version Lean 4 + Mathlib : `ERC20/State.lean` (modèle), `ERC20/Ops.lean` (transitions), `ERC20/Invariant.lean` (préservation).\n",
     "- **EPIC #4980** — convention i18n Lean (aggrégateur bilingue inline FR-EN dans `ERC20.lean`, sibling pair dans `ERC20_en.lean`).\n",
     "- **Rule C.6** (mandat user 2026-08-19) — préférence pour un compagnon kernel `lean4-wsl` à côté du notebook Python ; le pattern actuel (subprocess `lake env lean`) reste mergeable, le kernel Lean natif est une suite à explorer.\n",
-    "- Notebooks associés : `[Lean-22 (Galois)](Lean-22-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-21 (MIMO)](Lean-21-MIMO-Detection-Flips.ipynb)`, `[Lean-20 (PFR)](Lean-20-PFR-Entropy-Method.ipynb)`, `[Lean-13 (Kochen-Specker)](Lean-13-Kochen-Specker.ipynb)`, `[A* Optimalite (Search-03e)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb)`."
+    "- Notebooks associés : `[Lean-22 (Galois)](Lean-22-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-21 (MIMO)](Lean-21-MIMO-Detection-Flips.ipynb)`, `[Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb)`, `[Lean-13 (Kochen-Specker)](Lean-13-Kochen-Specker.ipynb)`, `[A* Optimalite (Search-03e)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb)`."
    ]
   }
  ],
@@ -1404,4 +1404,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
\ No newline at end of file
+}
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb
index e3acb2085d..c833f331e1 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb
@@ -7,7 +7,7 @@
    "source": [
     "# Lean-28 : Le problème de Hopf sur S⁶ — digestion d'une preuve constructive mécanisée\n",
     "\n",
-    "**Série** : [SymbolicAI / Lean](README.md) — digestions de résultats profonds (cf. [Lean-18 Sendov](Lean-18-Sendov-Complex-Analysis.ipynb), [Lean-19 Analysis I](Lean-19-Analysis-I-Tao-Workflow.ipynb), [Lean-20 PFR](Lean-20-PFR-Entropy-Method.ipynb)) · **Issue** : #13353 · **Epic** : #13105\n",
+    "**Série** : [SymbolicAI / Lean](README.md) — digestions de résultats profonds (cf. [Lean-18 Sendov](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb), [Lean-19 Analysis I](ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb), [Lean-20 PFR](ANALYSE/ANALYSE-03-PFR-Lean.ipynb)) · **Issue** : #13353 · **Epic** : #13105\n",
     "\n",
     "Ce notebook digère un résultat récent et spectaculaire : la construction d'une **structure de variété complexe intégrable** sur la sphère S⁶ — le *problème de Hopf*, ouvert depuis les années 1950. Il s'appuie sur un couple de ressources complémentaires :\n",
     "\n",
@@ -868,7 +868,7 @@
     "\n",
     "### 6.2 Perspective\n",
     "\n",
-    "Ce cas illustre la doctrine de l'Epic #13105 : la digestion d'un résultat profond n'est ni un import ni un récit — c'est l'articulation *énoncé → construction → certificat → attribution*. Le contraste avec [Lean-20 (PFR)](Lean-20-PFR-Entropy-Method.ipynb) est instructif : là, un lac communautaire court et fini ; ici, un monolithe single-file de 248 818 lignes — deux régimes de la formalisation contemporaine, et deux façons de l'enseigner.\n",
+    "Ce cas illustre la doctrine de l'Epic #13105 : la digestion d'un résultat profond n'est ni un import ni un récit — c'est l'articulation *énoncé → construction → certificat → attribution*. Le contraste avec [Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb) est instructif : là, un lac communautaire court et fini ; ici, un monolithe single-file — deux régimes de la formalisation contemporaine, et deux façons de l'enseigner.\n",
     "\n",
     "*Note d'exécution* : les cellules des sections 1 et 3 consomment le checkout piné et les logs réels de la reproduction locale (WSL, ext4 natif) via `scripts/notebook_tools/hopf_s6_reproduction.py` ; la figure 2.4 et les calculs 2.1–2.3 sont autonomes (fractions/entiers exacts)."
    ]
@@ -895,4 +895,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}
\ No newline at end of file
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md
index 6efe966ecc..e3c2e4e241 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md
@@ -142,10 +142,10 @@ Tous les notebooks incluent une **barre de navigation** en haut et en bas permet
 
 | # | Notebook | Contenu | Durée |
 |---|----------|---------|-------|
-| 18 | [Lean-18-Sendov-Complex-Analysis](Lean-18-Sendov-Complex-Analysis.ipynb) | La conjecture de Sendov (preuve L. Mazur 2026, digestion et formalisation T. Tao) : pour un polynôme dont tous les zéros sont dans le disque unité, chaque zéro a un point critique à distance ≤ 1 — énoncé, illustrations numériques des cas, contexte de la preuve | 45 min |
-| 19 | [Lean-19-Analysis-I-Tao-Workflow](Lean-19-Analysis-I-Tao-Workflow.ipynb) | Le manuel *Analysis I* de T. Tao en lac Lean 4 (`teorth/analysis`) : architecture du lac, philosophie d'auto-contenance vs Mathlib, cinq lemmes emblématiques parmi 44k LOC, méta-récit single-agent vs cluster distribué | 40 min |
-| 20 | [Lean-20-PFR-Entropy-Method](Lean-20-PFR-Entropy-Method.ipynb) | La conjecture PFR (polynomial Freiman–Ruzsa, ZMod 2) : méthode entropique de la preuve `teorth/pfr` — énoncé combinatoire, illustrations cosets dans F₂³, `#check` réels et axiomes du lac compilé | 45 min |
-| 20b | [Lean-20b-PFR-Primitives-Transportables](Lean-20b-PFR-Primitives-Transportables.ipynb) | Trois primitives de PFR, et l'endroit exact où elles cessent de valoir — companion de digestion de Lean-20 : ce qui se transporte hors du cadre d'origine (#12214) | 30 min |
+| 18 | [ANALYSE-01-Sendov-Lean-Python](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb) | Ouverture de la sous-série [ANALYSE](ANALYSE/README.md) (dossier `ANALYSE/`, gradation #17545) — la conjecture de Sendov (preuve L. Mazur 2026, digestion et formalisation T. Tao) : pour un polynôme dont tous les zéros sont dans le disque unité, chaque zéro a un point critique à distance ≤ 1 — énoncé, illustrations numériques des cas, contexte de la preuve | 45 min |
+| 19 | [ANALYSE-02-Tao-Lean-Python](ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb) | Le manuel *Analysis I* de T. Tao en lac Lean 4 (`teorth/analysis`) : architecture du lac, philosophie d'auto-contenance vs Mathlib, cinq lemmes emblématiques parmi 44k LOC, méta-récit single-agent vs cluster distribué | 40 min |
+| 20 | [ANALYSE-03-PFR-Lean](ANALYSE/ANALYSE-03-PFR-Lean.ipynb) | La conjecture PFR (polynomial Freiman–Ruzsa, ZMod 2) : méthode entropique de la preuve `teorth/pfr` — énoncé combinatoire, illustrations cosets dans F₂³, `#check` réels et axiomes du lac compilé | 45 min |
+| 20b | [ANALYSE-04-PFR-Primitives-Python](ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb) | Trois primitives de PFR, et l'endroit exact où elles cessent de valoir — companion de digestion de ANALYSE-03 : ce qui se transporte hors du cadre d'origine (#12214) | 30 min |
 | 21 | [Lean-21-MIMO-Detection-Flips](Lean-21-MIMO-Detection-Flips.ipynb) | Détection MIMO par flips de coordonnées (Papailiopoulos 2026) : le seuil 2·log N — descente simulée et comptage de flips, probabilité d'échappement du bruit (Monte-Carlo vs `e^{−np}`), `#check` réels des quatre phases et du converse complet `ml_error_prob_ge_threshold` (P(erreur ML) ≥ 1 − e^{−(2·log N − log log N)}) du companion `mimo_lean` (sorry-free, lake externe SLT pour Hanson–Wright) | 45 min |
 | 21b | [Lean-21b-MIMO-Converse-Native](Lean-21b-MIMO-Converse-Native.ipynb) | Compagnon **natif** (kernel `lean4-wsl`) du lac `mimo_lean` : le lac importé et exécuté dans un kernel Lean 4 réel — la frontière SLT exhibée par `#check` (ce qui est prouvé vs emprunté à `YuanheZ/lean-stat-learning-theory`), les six déclarations de `NormTails` (concentration de Lipschitz gaussienne), les seize briques du converse Hanson–Wright (dont `hanson_wright_noise` et la queue chi-carré `chisq_norm_concentration`), les treize du pont ML (`Bridge`), `#print axioms` sur les théorèmes clés — uniquement les axiomes standards, zéro `sorry` | 40 min |
 | 21c | [Lean-21c-Descente-Budget](Lean-21c-Descente-Budget.ipynb) | Le budget de descente : quand la décroissance borne le nombre de flips — l'analyse qui fonde le seuil 2·log N de la détection MIMO (#12219) | 35 min |
@@ -463,10 +463,6 @@ Lean/
 ├── Lean-17b-Knots-Invariants-Companion.ipynb # Python kernel - invariants de nœuds (PD-codes, Reidemeister, Fox tricolorability), compagnon knot_lean
 ├── Lean-17c-Knots-Companion-Formel.ipynb # Python kernel - companion formel knot_lean (modules non cités par 17b, murs R2/R3, miroir i18n)
 ├── Search-03e-AStar-Optimality.ipynb # Python kernel - optimalité de A* sous heuristique admissible (companion search_lean, 0 sorry)
-├── Lean-18-Sendov-Complex-Analysis.ipynb # Python kernel - conjecture de Sendov (preuve Mazur 2026, digestion et formalisation Tao)
-├── Lean-19-Analysis-I-Tao-Workflow.ipynb # Python kernel - le lac Analysis I de Tao (architecture, 5 lemmes emblématiques)
-├── Lean-20-PFR-Entropy-Method.ipynb # Python kernel - conjecture PFR (méthode entropique, #check réels du lac compilé)
-├── Lean-20b-PFR-Primitives-Transportables.ipynb # Python kernel - trois primitives de PFR et leurs limites de transport (#12214)
 ├── Lean-21-MIMO-Detection-Flips.ipynb # Python kernel - détection MIMO par flips (seuil 2·log N, companion mimo_lean)
 ├── Lean-21b-MIMO-Converse-Native.ipynb # Lean4 (WSL) kernel - converse MIMO natif (NormTails, Hanson-Wright, #print axioms)
 ├── Lean-21c-Descente-Budget.ipynb # Python kernel - budget de descente (décroissance borne les flips, #12219)
@@ -490,6 +486,7 @@ Lean/
 ├── lean_runner.py                  # Module Python multi-backend
 ├── README.md
 ├── .env.example
+├── ANALYSE/                       # Sous-série des formalisations d'analyse (Sendov, Tao Analysis I, PFR ×2 — gradation #17545) : [README](ANALYSE/README.md)
 ├── sensitivity_lean/               # Théorème de sensibilité (Huang 2019, companion Lean-12/12b) - 0 sorry 0 axiome, Lake build natif (jonction Mathlib)
 ├── finiteness_lean/                # Finitude des dérivées de Brzozowski (companion Lean-14) - 0 sorry, Lake build
 ├── conway_lean/                    # Conway tribute workspace (0 sorry, Lake build)
diff --git a/_quarto.yml b/_quarto.yml
index 7ea0bc057b..58b42986be 100644
--- a/_quarto.yml
+++ b/_quarto.yml
@@ -1098,9 +1098,9 @@ project:
     - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17a-Knots-Conway-Proofs.ipynb"
     - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17b-Knots-Invariants-Companion.ipynb"
     - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17c-Knots-Companion-Formel.ipynb"
-    - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.ipynb"
-    - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-PFR-Entropy-Method.ipynb"
-    - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20b-PFR-Primitives-Transportables.ipynb"
+    - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb"
+    - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-03-PFR-Lean.ipynb"
+    - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb"
     - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb"
     - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb"
     - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb"
diff --git a/docs/curriculum/ia-symbolique.md b/docs/curriculum/ia-symbolique.md
index 1fcbe7ad47..369d61f0fb 100644
--- a/docs/curriculum/ia-symbolique.md
+++ b/docs/curriculum/ia-symbolique.md
@@ -110,11 +110,11 @@ Preuves formelles en Lean 4, logique probabiliste avec Tweety, web sémantique,
 | 24 | [Lean 17a — Conway, les Nœuds et la Preuve de Piccirillo](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17a-Knots-Conway-Proofs.ipynb) | BETA | Non |
 | 25 | [Lean 17b — Invariants de Nœuds : Calcul et Vérification](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17b-Knots-Invariants-Companion.ipynb) | BETA | Non |
 | 26 | [Lean 17c — Le lake knot_lean par ses déclarations…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17c-Knots-Companion-Formel.ipynb) | BETA | Non |
-| 27 | [Lean-18 : La Conjecture de Sendov (preuve L. Mazur,…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.ipynb) | BETA | Non |
-| 28 | [Lean-19 : Le manuel *Analysis I* de T. Tao en Lean 4…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Analysis-I-Tao-Workflow.ipynb) | BETA | Non |
+| 27 | [ANALYSE-01 — La Conjecture de Sendov (preuve L. Mazur,…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb) | BETA | Non |
+| 28 | [ANALYSE-02 — Le manuel *Analysis I* de T. Tao en Lean 4…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb) | BETA | Non |
 | 29 | [Lean 2 - Types Dependants et Calcul des Constructions](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-2-Dependent-Types.ipynb) | BETA | Non |
-| 30 | [Lean-20 : La conjecture de Freiman-Ruzsa polynomiale…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-PFR-Entropy-Method.ipynb) | BETA | Non |
-| 31 | [Lean-20b : Trois primitives de PFR, et l'endroit exact…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20b-PFR-Primitives-Transportables.ipynb) | BETA | Non |
+| 30 | [ANALYSE-03 — La conjecture de Freiman-Ruzsa polynomiale…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-03-PFR-Lean.ipynb) | BETA | Non |
+| 31 | [ANALYSE-04 — Trois primitives de PFR, et l'endroit exact…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb) | BETA | Non |
 | 32 | [Lean-21 : Detection MIMO par flips -- le seuil 2 log N…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb) | BETA | Non |
 | 33 | [Lean-21b : le lake mimo_lean par ses énoncés —…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb) | BETA | Non |
 | 34 | [Lean-21c : Le budget de descente - quand la…](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb) | BETA | Non |
diff --git a/docs/grothendieckian-lens.md b/docs/grothendieckian-lens.md
index 2227b3ca5d..df918eee78 100644
--- a/docs/grothendieckian-lens.md
+++ b/docs/grothendieckian-lens.md
@@ -94,7 +94,7 @@ Entre les séries d'enseignement elles-mêmes, de nouvelles tresses se sont nou
 
 Au-dessus des deux versants veillent les grands noms, chacun avec son Epic. Mais un nom n'entre pas dans le dépôt parce qu'on le cite : il y entre quand une série exécute ce qu'il a pensé. Serre y est entré par des diptyques où le même énoncé est calculé en Python et démontré en Lean ([Serre 100](../MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/README.md)), et par une carte qui rattache sa moitié du pont à la formalisation de Grothendieck ([`SerreMap.lean`](../MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/SerreMap.lean)). Tegmark, par une boucle en trois temps : le cours d'apprentissage automatique exécute les diagrammes de phase du *grokking* ([2.9c](../MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9c-Grokking-Diagrammes-Phases.ipynb)), un lake démontre les lois conservées qu'on en extrait ([`Grokking.lean`](../MyIA.AI.Notebooks/ML/learning_theory_lean/EffectiveTheory/Grokking.lean)), et ICT mesure la géométrie des concepts appris ([ICT-41](../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-41-SAE-GeometrieFeatures.ipynb)).
 
-Schmidhuber a un organe dans ICT ([`ict/beauty.py`](../MyIA.AI.Notebooks/IIT/ICT-Series/ict/beauty.py)) et un verdict exécuté : « le compression-progress de Schmidhuber tient » ([ICT-17b](../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-17b-Grokking-CompressionProgress.ipynb)). Aaronson a fait de l'écart entre permanent et déterminant un compte d'opérations, avec l'algorithme de Ryser déjà présent dans le Sudoku ([Complexity-05](../MyIA.AI.Notebooks/Complexity/Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb)). Pearl a trouvé sa démonstration par la machine : deux modèles causaux qui produisent les mêmes données et prédisent des interventions opposées ([CausalBridges-01-Do-Calculus](../MyIA.AI.Notebooks/Probas/DecisionTheory/Causal-Bridges/CausalBridges-01-Do-Calculus.ipynb)). Tao a digéré et formalisé une preuve récente de la conjecture de Sendov ([Lean-18](../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.ipynb)). D'autres attendent : Russell, cité partout, n'habite qu'un notebook, le jeu de l'interrupteur ([GameTheory-15](../MyIA.AI.Notebooks/GameTheory/GameTheory-15-CooperativeGames.ipynb)). Les Epics le mesurent elles-mêmes : plusieurs de ces noms *hantent* encore le dépôt plus qu'ils ne l'*habitent*, et c'est en les faisant habiter que naissent les ponts.
+Schmidhuber a un organe dans ICT ([`ict/beauty.py`](../MyIA.AI.Notebooks/IIT/ICT-Series/ict/beauty.py)) et un verdict exécuté : « le compression-progress de Schmidhuber tient » ([ICT-17b](../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-17b-Grokking-CompressionProgress.ipynb)). Aaronson a fait de l'écart entre permanent et déterminant un compte d'opérations, avec l'algorithme de Ryser déjà présent dans le Sudoku ([Complexity-05](../MyIA.AI.Notebooks/Complexity/Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb)). Pearl a trouvé sa démonstration par la machine : deux modèles causaux qui produisent les mêmes données et prédisent des interventions opposées ([CausalBridges-01-Do-Calculus](../MyIA.AI.Notebooks/Probas/DecisionTheory/Causal-Bridges/CausalBridges-01-Do-Calculus.ipynb)). Tao a digéré et formalisé une preuve récente de la conjecture de Sendov ([Lean-18](../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb)). D'autres attendent : Russell, cité partout, n'habite qu'un notebook, le jeu de l'interrupteur ([GameTheory-15](../MyIA.AI.Notebooks/GameTheory/GameTheory-15-CooperativeGames.ipynb)). Les Epics le mesurent elles-mêmes : plusieurs de ces noms *hantent* encore le dépôt plus qu'ils ne l'*habitent*, et c'est en les faisant habiter que naissent les ponts.
 
 Prenons de la hauteur. Le dépôt est un site, au sens du deuxième mouvement : les séries en sont les ouverts, les ponts les recouvrements, et l'accord sur les recouvrements la condition de recollement. Là où deux séries s'accordent — Tweety et Lean sur le même syllogisme, Infer.NET et PyMC sur la même valeur d'information — une connaissance plus globale apparaît. Là où elles divergent, ou ne se ressemblent que par la structure — la percolation et l'adoption collective, la preuve de HashLife et le saut qu'elle ne couvrait pas —, l'écart n'est pas un échec : c'est une obstruction, et elle montre où travailler. C'est une image, de grade C, et elle se déclare comme telle. Mais elle dit juste : la mer ne monte plus autour d'une seule noix, elle monte entre les séries.
 
diff --git a/docs/notebook-metadata/production-scope.md b/docs/notebook-metadata/production-scope.md
index 4df73b1070..1c9b9c7ea4 100644
--- a/docs/notebook-metadata/production-scope.md
+++ b/docs/notebook-metadata/production-scope.md
@@ -315,9 +315,9 @@ l'Epic) ; un dossier de revue est alors préparé (T2).*
 - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17a-Knots-Conway-Proofs.ipynb`
 - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17b-Knots-Invariants-Companion.ipynb`
 - [ ] `MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb`
-- [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.ipynb`
-- [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Analysis-I-Tao-Workflow.ipynb`
-- [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-PFR-Entropy-Method.ipynb`
+- [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb`
+- [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb`
+- [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-03-PFR-Lean.ipynb`
 - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb`
 <!-- MyIA.AI.Notebooks/SymbolicAI/SemanticWeb -->
 
diff --git a/docs/reference/rename-ledger.tsv b/docs/reference/rename-ledger.tsv
index 6cdc0e04b8..4688d3e41a 100644
--- a/docs/reference/rename-ledger.tsv
+++ b/docs/reference/rename-ledger.tsv
@@ -29,4 +29,8 @@ MyIA.AI.Notebooks/SymbolicAI/SmartContracts/06-Real-World/SC-24-Testnet-Deploy.i
 MyIA.AI.Notebooks/SymbolicAI/SmartContracts/06-Real-World/SC-25-Mainnet-Deploy.ipynb	MyIA.AI.Notebooks/SymbolicAI/SmartContracts/06-Real-World/SC-25-Mainnet-Deploy-Python.ipynb	2026-09-25	myia-po-2025:CoursIA
 MyIA.AI.Notebooks/SymbolicAI/SmartContracts/06-Real-World/SC-26-Final-Project.ipynb	MyIA.AI.Notebooks/SymbolicAI/SmartContracts/06-Real-World/SC-26-Final-Project-Python.ipynb	2026-09-25	myia-po-2025:CoursIA
 MyIA.AI.Notebooks/SymbolicAI/SmartContracts/06-Real-World/SC-27-Dette-Irreversibilite.ipynb	MyIA.AI.Notebooks/SymbolicAI/SmartContracts/06-Real-World/SC-27-Dette-Irreversibilite-Python.ipynb	2026-09-25	myia-po-2025:CoursIA
+MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.ipynb	MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb	2026-09-27	myia-po-2026:CoursIA
+MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Analysis-I-Tao-Workflow.ipynb	MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb	2026-09-27	myia-po-2026:CoursIA
+MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-PFR-Entropy-Method.ipynb	MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-03-PFR-Lean.ipynb	2026-09-27	myia-po-2026:CoursIA
+MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20b-PFR-Primitives-Transportables.ipynb	MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb	2026-09-27	myia-po-2026:CoursIA
 MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb	MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb	2026-09-28	myia-po-2023:CoursIA
diff --git a/scripts/notebook_tools/check_source_collapse.py b/scripts/notebook_tools/check_source_collapse.py
index 6b7001b919..54ed34ffdb 100644
--- a/scripts/notebook_tools/check_source_collapse.py
+++ b/scripts/notebook_tools/check_source_collapse.py
@@ -56,7 +56,7 @@
 A THIRD mechanism, same family, is the SOURCE-side counterpart taken by the
 other end (issue #16110): the source SURVIVES in volume and loses its
 STRUCTURE. Founding case, measured firsthand on PR #16097 (head
-``1209b5357``, cell ``40cb37d5`` of ``Lean-18-Sendov-Complex-Analysis.ipynb``,
+``1209b5357``, cell ``40cb37d5`` of ``ANALYSE-01-Sendov-Lean-Python.ipynb``,
 base ``origin/main``): every newline of the cell was stripped at write time,
 so the 44 source items joined into ONE line whose first character is ``#`` --
 the whole code becomes a comment. The cell kept its 312-character stream
@@ -279,7 +279,7 @@
 SELF_TEST_16110_BASE = "7cc2fb2d203f"  # merge-base(main, #16097)
 SELF_TEST_16110_HEAD = "1209b5357"
 SELF_TEST_16110_NOTEBOOK = (
-    "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.ipynb")
+    "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb")
 SELF_TEST_16110_CELL = "40cb37d5"
 
 
diff --git a/scripts/notebook_tools/pedagogy_density_baseline.json b/scripts/notebook_tools/pedagogy_density_baseline.json
index f7c27b4bc7..5f267e587f 100644
--- a/scripts/notebook_tools/pedagogy_density_baseline.json
+++ b/scripts/notebook_tools/pedagogy_density_baseline.json
@@ -633,7 +633,7 @@
     "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16f-Conway-Free-Will-Theorem.ipynb": 1581.429,
     "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17a-Knots-Conway-Proofs.ipynb": 2833.333,
     "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17b-Knots-Invariants-Companion.ipynb": 922.056,
-    "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.ipynb": 2357.333,
+    "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb": 2357.333,
     "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-2-Dependent-Types.ipynb": 1619.5,
     "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-3-Propositions-Proofs.ipynb": 2118.12,
     "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-4-Quantifiers.ipynb": 2100.96,
diff --git a/scripts/tests/baseline_nb_nav_chain.json b/scripts/tests/baseline_nb_nav_chain.json
index ddd3e41aee..425f13dccd 100644
--- a/scripts/tests/baseline_nb_nav_chain.json
+++ b/scripts/tests/baseline_nb_nav_chain.json
@@ -60,21 +60,6 @@
       "notebook": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API",
       "series": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API"
     },
-    {
-      "kind": "orphan_entry",
-      "notebook": "MyIA.AI.Notebooks/Complexity/Complexity-04-OnlineAlgorithms-Python.ipynb",
-      "series": "MyIA.AI.Notebooks/Complexity"
-    },
-    {
-      "kind": "orphan_entry",
-      "notebook": "MyIA.AI.Notebooks/Complexity/Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb",
-      "series": "MyIA.AI.Notebooks/Complexity"
-    },
-    {
-      "kind": "orphan_entry",
-      "notebook": "MyIA.AI.Notebooks/Complexity/Complexity-06-Aaronson-Dequantification-Stabilizer.ipynb",
-      "series": "MyIA.AI.Notebooks/Complexity"
-    },
     {
       "kind": "orphan_entry",
       "notebook": "MyIA.AI.Notebooks/GameTheory/GameTheory-02-NormalForm-Part2-Python.ipynb",
@@ -785,11 +770,6 @@
       "notebook": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.12-Donnees-Desequilibrees.ipynb",
       "series": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours"
     },
-    {
-      "kind": "orphan_entry",
-      "notebook": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.14b-XAI-Shap-Attribution-Causal-Bridge.ipynb",
-      "series": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours"
-    },
     {
       "kind": "orphan_entry",
       "notebook": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.3d-Modele-Gaussien-LDA-QDA.ipynb",
@@ -1820,11 +1800,6 @@
       "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17c-Knots-Companion-Formel.ipynb",
       "series": "MyIA.AI.Notebooks/SymbolicAI/Lean"
     },
-    {
-      "kind": "orphan_entry",
-      "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20b-PFR-Primitives-Transportables.ipynb",
-      "series": "MyIA.AI.Notebooks/SymbolicAI/Lean"
-    },
     {
       "kind": "orphan_entry",
       "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb",
@@ -2207,6 +2182,10 @@
     }
   ],
   "wrapped": [
+    {
+      "series": "MyIA.AI.Notebooks/Complexity",
+      "notebooks": 9
+    },
     {
       "series": "MyIA.AI.Notebooks/GenAI/00-GenAI-Environment",
       "notebooks": 6
@@ -2227,6 +2206,10 @@
       "series": "MyIA.AI.Notebooks/GenAI/Image/03-Orchestration",
       "notebooks": 4
     },
+    {
+      "series": "MyIA.AI.Notebooks/GenAI/Texte",
+      "notebooks": 31
+    },
     {
       "series": "MyIA.AI.Notebooks/GenAI/Vibe-Coding/Claude-Code/notebooks",
       "notebooks": 5