diff --git a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb b/MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb
similarity index 99%
rename from MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb
rename to MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb
index a1d49860a9..a9dd334b69 100644
--- a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb
+++ b/MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb
@@ -14,13 +14,13 @@
     "tags": []
    },
    "source": [
-    "# Search-09d — Discrépance combinatoire : la couche formelle (Komlós, Bansal–Jiang 2025)\n",
+    "# Discrepancy-02 — Discrépance combinatoire : la couche formelle (Komlós, Bansal–Jiang 2025)\n",
     "\n",
-    "> **Partie 1 — Fondations · compagnon formel de [Search-09c](Search-09c-CombinatorialDiscrepancy.ipynb)**\n",
+    "> **Deuxième marche de la sous-série `Discrepancy/`** (issue #17816, arbitrage Search #17802) — compagnon formel de [Search-09c](../Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb)\n",
     "\n",
     "Le lake [`discrepancy_lean`](../discrepancy_lean/README.md) formalise la **discrépance combinatoire** :\n",
     "colorer en `±1` les éléments d'un système d'ensembles de degré `≤ k` en minimisant la pire somme\n",
-    "colorée `‖Ax‖∞`. [Search-09c](Search-09c-CombinatorialDiscrepancy.ipynb) a exploré ce territoire en\n",
+    "colorée `‖Ax‖∞`. [Search-09c](../Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb) a exploré ce territoire en\n",
     "**Python numérique** — tirages aléatoires, arrondi flottant de Beck–Fiala, oracle exact CP-SAT. Ce\n",
     "compagnon exécute la couche **formelle** : les énoncés exacts du lake, intégrés au noyau Lean 4.\n",
     "\n",
@@ -2487,7 +2487,7 @@
     "**calculée par énumération exhaustive dans le noyau** (`1/5` puis `1`), les théorèmes P0 relus\n",
     "avec leur témoin, et la machinerie prouvée interrogée boute par boute. Relié au corpus :\n",
     "\n",
-    "- [Search-09c](Search-09c-CombinatorialDiscrepancy.ipynb) mesure les **mêmes objets en numérique**\n",
+    "- [Search-09c](../Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb) mesure les **mêmes objets en numérique**\n",
     "  (numpy, arrondi Beck–Fiala, oracle CP-SAT) — la discrépance exacte qu'il approche par solver,\n",
     "  ce compagnon l'énumère in-kernel sur des petits témoins, et sa borne `2k − 1` est maintenant\n",
     "  le théorème exécuté de la section 6 ;\n",
diff --git a/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md b/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md
index dd73ed9614..8e98ecaa6c 100644
--- a/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md
+++ b/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md
@@ -14,8 +14,8 @@ hors `_en` ; bascule #11688 — historiquement `standalone-tactic` ; les mention
 | Lake | Toolchain | sorry (production) | Modules | Notebook câblé | Classe | Suivi |
 |------|-----------|--------------------:|--------:|---------------:|--------|-------|
 | `search_lean` | v4.33.0 | 0 | 5 | 1¹ | PEDA/REF | #4048, #4038, #3801 |
-| `discrepancy_lean` | v4.33.0 | 0 | 8 | 0² | PEDA/REF | #12823 |
-| **Total** | — | **0** | **13** | **1** | — | — |
+| `discrepancy_lean` | v4.33.0 | 0 | 8 | 1² | PEDA/REF | #12823 |
+| **Total** | — | **0** | **13** | **2** | — | — |
 
 ¹ Notebook câblé : **Search-03e-AStar-Optimality.ipynb**
 (`Search/Part1-Foundations/`, descente tranche 1 #13662 depuis
@@ -25,9 +25,16 @@ A* vs BFS sur terrain pondéré — convention sibling-lake). Répond aussi au p
 problème non-trivial (heuristique discriminante), pas un graphe à coût uniforme où A*
 dégénère en BFS.
 
-² Notebook compagnon prévu : `Search-15-CombinatorialDiscrepancy` (livrable A de
-[#12823](https://github.com/jsboige/CoursIA/issues/12823)) — Beck–Fiala 2k−1 implémenté +
-CP-SAT en oracle exact. Pas encore câblé.
+² Notebook câblé : **Discrepancy-02-Komlos-Lean.ipynb** (`Search/Discrepancy/`, kernel
+`lean4-wsl`, descendu le 2026-10-04 de l'ancien chemin
+`Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb` par #19151) — `#check` des
+énoncés du lake (Komlós, Beck–Fiala, régimes Bansal–Jiang 2025) et
+témoins coloriés ±1 énumérés exhaustivement sur des instances jouet.
+
+Le livrable A de [#12823](https://github.com/jsboige/CoursIA/issues/12823) (Beck–Fiala 2k−1
+implémenté + CP-SAT en oracle exact) est livré en **Discrepancy-01-BeckFiala-Lean-Python.ipynb**
+(kernel `python3`) : c'est un **pont Python vers le lake**, sans Lean au runtime — il ne compte
+donc pas dans la colonne *Notebook câblé*, qui mesure l'invocation effective du lake.
 
 ---
 
diff --git a/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md b/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md
index 331a79f0ea..97ab966aa2 100644
--- a/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md
+++ b/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md
@@ -63,7 +63,7 @@ Cette partie est l'alphabet de toute la série : la formalisation en espace d'é
 | 9 (.NET) | [Search-09-LinearProgramming (C#)](Search-09-LinearProgramming-CSharp.ipynb) | .NET (C#) | **Jumeau .NET** : programmation linéaire avec Google OrTools (`LinearSolver`, solveurs GLOP/CBC) — problème de production, diet problem, analyse de sensibilité et dualité (shadow prices), PLNE (sac à dos binaire), exercices (set cover, optimisation multi-objectif) — port C# fidèle du notebook Python (PuLP) — parité #4956 | ~1h |
 | 9b | [Search-09b-SpuriousMinima](Search-09b-SpuriousMinima.ipynb) | Python 3 | Relaxation SDP de MaxCut (Goemans–Williamson, résolue exactement par cvxpy/CLARABEL) **et sa factorisation de Burer–Monteiro** $Y = XX^T$ : recensement borné des minima fallacieux par rang (40 départs × 3 instances C6/K8/G10, graines fixes, référence brute-force $2^{n-1}$) — à $r=1$ le paysage dégénère en MaxCut discret (40/40 fallacieux), les pièges se raréfient aux rangs intermédiaires, et **aucun piège à/au-dessus du seuil** $r(r+1)/2 > m$ (Burer–Monteiro 2005, Barvinok–Pataki) — le point d'arrivée « certification » du fil paysages (suite directe de Search-9, écho de MGS-15) | ~1h15 |
 | 9c | [Search-09c-CombinatorialDiscrepancy](Search-09c-CombinatorialDiscrepancy.ipynb) | Python 3 | Discrépance combinatoire (Beck–Fiala 1981, frontière 2025 Bansal–Jiang arXiv:2508.03961) : colorier ±1 sans déséquilibrer, borne inf √k (Chernoff), arrondi flottant 2k−1 implémenté, CP-SAT en oracle exact — fil relaxation/arrondi/optimisation combinatoire (accrétion de Search-9) | ~45min |
-| 9d | [Search-09d-Lean-Discrepancy-Komlos](Search-09d-Lean-Discrepancy-Komlos.ipynb) | lean4-wsl | **Compagnon formel de Search-09c** : le lake [`discrepancy_lean`](../discrepancy_lean/README.md) exécuté depuis le kernel Lean 4 — `#check` des conjectures (Komlós ∃C universel, Beck–Fiala 2k−1, régimes Bansal–Jiang 2025), témoins coloriés ±1 énumérés exhaustivement sur des instances jouet (Hadamard ½n en particulier), exercices ancrés sur les énoncés du lake | ~45min |
+| 9d | [Discrepancy-02-Komlos-Lean](../Discrepancy/Discrepancy-02-Komlos-Lean.html) | lean4-wsl | **Compagnon formel de Search-09c** : le lake [`discrepancy_lean`](../discrepancy_lean/README.md) exécuté depuis le kernel Lean 4 — `#check` des conjectures (Komlós ∃C universel, Beck–Fiala 2k−1, régimes Bansal–Jiang 2025), témoins coloriés ±1 énumérés exhaustivement sur des instances jouet (Hadamard ½n en particulier), exercices ancrés sur les énoncés du lake | ~45min |
 | 10 | [Search-10-SymbolicAutomata](Search-10-SymbolicAutomata.html) | Python 3 | Automates finis (DFA/NFA) avec automata-lib, prédicats Z3, automates symboliques | ~2h |
 | 10 (.NET) | [Search-10-SymbolicAutomata (C#)](Search-10-SymbolicAutomata-CSharp.ipynb) | .NET (C#) | **Jumeau .NET** (tranches 1+2) : automates finis classiques (DFA/NFA hand-rolled, opérations ensemblistes par produit cartésien) **+** automates symboliques avec `Microsoft.Z3` (NuGet 4.12.2) — classe `SymbolicAutomaton` (transitions = prédicats Z3, décision via solveur SMT), intervalle [10,100], parité, multiples de 5, opérations symboliques (union/intersection/complément via `MkAnd`/`MkOr`/`MkNot` vérifiées exactes) — port C# fidèle §1-4 — parité #4956 | ~1h30 |
 | 11 | [Search-11-Metaheuristics](Search-11-Metaheuristics.html) | Python 3 | PSO, ABC, SA, BRO avec MEALPy, benchmark comparatif de métaheuristiques | ~1h30 |
@@ -87,7 +87,7 @@ Les trois premiers notebooks forment le socle commun — on y apprend à poser u
 - **Recherche dans les jeux** : Search-3 puis Search-6 (AdversarialSearch) puis Search-7 (MCTS)
 - **Couverture exacte** : Search-2 puis Search-8 (DancingLinks)
 - **Boîte à outils de graphes** : Search-2 puis Search-2b (NetworkX, ou son jumeau C#) puis Search-2c (QuikGraph)
-- **Indépendants** : Search-9 (LinearProgramming, algèbre linéaire requise), Search-09b (SpuriousMinima, sa suite semidéfinie : Search-9 recommandé au préalable), Search-09c (CombinatorialDiscrepancy, relaxation/arrondi — écho du fil optimisation) suivi de son compagnon formel Search-09d (Lean, kernel `lean4-wsl` : Search-09c recommandé au préalable), Search-11c (Empirical-Algorithm-Selection, distillation benchmark cross-paradigmes : aucun prérequis, écho App-14), Search-12a (Composer-Regards, lecture avant/arrière d'un même terrain : Search-3 recommandé au préalable, op 12 du chantier ICT #12204), Search-13a (Traverser-Murs-Certifies, chemin minimal certifié à travers une bande de cellules coûteuses : Search-2 recommandé au préalable, op 13 du chantier ICT #12204), Search-03f (Reparer-Localement-Sous-Garantie, repair incrémental LPA\* avec garantie d'optimalité transportée : Search-3 recommandé au préalable, op 6 du chantier ICT #12204) et Search-10 (SymbolicAutomata, liens avec SymbolicAI/SMT/Z3-Linq2Z3)
+- **Indépendants** : Search-9 (LinearProgramming, algèbre linéaire requise), Search-09b (SpuriousMinima, sa suite semidéfinie : Search-9 recommandé au préalable), Search-09c (CombinatorialDiscrepancy, relaxation/arrondi — écho du fil optimisation) suivi de son compagnon formel Discrepancy-02 (Lean, kernel `lean4-wsl` : Search-09c recommandé au préalable), Search-11c (Empirical-Algorithm-Selection, distillation benchmark cross-paradigmes : aucun prérequis, écho App-14), Search-12a (Composer-Regards, lecture avant/arrière d'un même terrain : Search-3 recommandé au préalable, op 12 du chantier ICT #12204), Search-13a (Traverser-Murs-Certifies, chemin minimal certifié à travers une bande de cellules coûteuses : Search-2 recommandé au préalable, op 13 du chantier ICT #12204), Search-03f (Reparer-Localement-Sous-Garantie, repair incrémental LPA\* avec garantie d'optimalité transportée : Search-3 recommandé au préalable, op 6 du chantier ICT #12204) et Search-10 (SymbolicAutomata, liens avec SymbolicAI/SMT/Z3-Linq2Z3)
 
 ```mermaid
 flowchart LR
@@ -117,7 +117,7 @@ Les fondamentaux de cette partie (formalisation, backtracking, heuristiques) son
 | `z3-solver` | Search-10 (Symbolic Automata), Search-11c (SMT) |
 | OpenSpiel | Search-7 (MCTS) : requiert WSL ou Linux |
 | `cvxpy` | Search-09b (relaxation SDP, solveur CLARABEL embarqué) |
-| Kernel `lean4-wsl` | Search-09d : kernel Jupyter Lean 4 + miroir local du lake [`discrepancy_lean`](../discrepancy_lean/README.md) (Mathlib 4 via les packages du dépôt) — cf. [`docs/reference/wsl-kernels-detail.md`](../../../docs/reference/wsl-kernels-detail.md) |
+| Kernel `lean4-wsl` | Discrepancy-02 : kernel Jupyter Lean 4 + miroir local du lake [`discrepancy_lean`](../discrepancy_lean/README.md) (Mathlib 4 via les packages du dépôt) — cf. [`docs/reference/wsl-kernels-detail.md`](../../../docs/reference/wsl-kernels-detail.md) |
 | `QuikGraph 2.5.0` (NuGet) | Search-2c (parité C#) : nécessite .NET Interactive, installable via `dotnet tool install --global Microsoft.dotnet-interactive` |
 
 Pour le setup complet, voir le [README de la série Search](../README.md).
@@ -147,7 +147,7 @@ Couverture par notebook des sources fondatrices mobilisées dans cette partie :
 | Search-5 (GeneticAlgorithms) | Holland, J. H. (1975) — *Adaptation in Natural and Artificial Systems*. University of Michigan Press. Origine des algorithmes génétiques. |
 | Search-7 (MCTS) | Browne, C. B., Powley, E., et al. (2012) — « A Survey of Monte Carlo Tree Search Methods », *IEEE Trans. on Computational Intelligence and AI in Games* 4(1). |
 | Search-8 (DancingLinks) | Knuth, D. E. (2000) — « Dancing Links », dans *Millennial Perspectives in Computer Science* (Springer). |
-| Search-09d (conjecture de Komlós) | Matoušek, J. (1999) — *Geometric Discrepancy: An Illustrated Guide*, Springer. Contexte classique de la conjecture de Komlós (disc ≤ C pour colonnes unitaires) ; les énoncés `KomlosConjecture` / `BansalJiangLargeDegree` / `KomlosBansalJiangWeak` formalisés dans [`discrepancy_lean/Komlos.lean`](../discrepancy_lean/Discrepancy/Komlos.lean) suivent les régimes de Bansal & Jiang (2025, arXiv:2508.03961 — cf. Search-09c). |
+| Discrepancy-02 (conjecture de Komlós) | Matoušek, J. (1999) — *Geometric Discrepancy: An Illustrated Guide*, Springer. Contexte classique de la conjecture de Komlós (disc ≤ C pour colonnes unitaires) ; les énoncés `KomlosConjecture` / `BansalJiangLargeDegree` / `KomlosBansalJiangWeak` formalisés dans [`discrepancy_lean/Komlos.lean`](../discrepancy_lean/Discrepancy/Komlos.lean) suivent les régimes de Bansal & Jiang (2025, arXiv:2508.03961 — cf. Search-09c). |
 | Search-11 (Metaheuristics) | Kennedy, J., & Eberhart, R. (1995) — « Particle Swarm Optimization », *Proc. IEEE Int. Conf. on Neural Networks*. Origine du PSO. |
 
 ## FAQ
diff --git a/MyIA.AI.Notebooks/Search/README.md b/MyIA.AI.Notebooks/Search/README.md
index 6bc27f10fb..1fd8e08a80 100644
--- a/MyIA.AI.Notebooks/Search/README.md
+++ b/MyIA.AI.Notebooks/Search/README.md
@@ -215,7 +215,8 @@ Cette série est née **Python d'abord** pour son cœur pédagogique (recherche,
 
 | Sous-série | Cœur pédagogique | Langage | Correspondance dans l'autre langage |
 |-----------|-----------|---------|-------------------------------------|
-| [Part1-Foundations](Part1-Foundations/) | 24 (Search-1 à Search-11, Search-2b, Search-2c, Search-03b à Search-03e, Search-09b à Search-09d, Search-11c, Search-11d, Search-12a, Search-13a) | Python (22) + Lean (Search-09d) + C# natif (Search-2c QuikGraph) | **15 jumeaux C#** (Search-1 à 11, 2b, 03b/03c/03d) + déclinaison deep-dive **Search-11b** (Métaheuristiques, 4 volets) |
+| [Part1-Foundations](Part1-Foundations/) | 23 (Search-1 à Search-11, Search-2b, Search-2c, Search-03b à Search-03e, Search-09b à Search-09c, Search-11c, Search-11d, Search-12a, Search-13a) | Python (22) + C# natif (Search-2c QuikGraph) | **15 jumeaux C#** (Search-1 à 11, 2b, 03b/03c/03d) + déclinaison deep-dive **Search-11b** (Métaheuristiques, 4 volets) |
+| [Discrepancy](Discrepancy/) | 2 (Discrepancy-01 Beck–Fiala, Discrepancy-02 Komlós) | Python + Lean 4 (kernel `lean4-wsl`) | Compagnons formels du lake [`discrepancy_lean`](discrepancy_lean/README.md) |
 | [Part2-CSP](Part2-CSP/) | 9 (CSP-1 à CSP-9) | Python + .NET | **9 binômes complets** — marathon achevé, voir [bilan final](#marathon-epic-4956) |
 | [Part4-Metaheuristics](Part4-Metaheuristics/) | 35 (25 à la racine + 10 dans `MGS-vs-mealpy/`) | C# / .NET (natif) | Prolonge Search-5 / Search-11 (Python) sous l'angle ingénierie |
 | [Applications](Applications/) | 20 cas cœur (App-1 à App-20), 57 notebooks actuels | Python + .NET | **20 binômes complets** + compagnons et audits App-21 à App-31 |
@@ -320,7 +321,7 @@ Search/
 ├── README.md                              # Ce fichier
 ├── requirements.txt                       # Dependances Python
 ├── search_helpers.py                      # Utilitaires partages
-├── Part1-Foundations/                     # Search Fondamental (43 notebooks : 22 Python + 1 Lean + 20 C# — 15 jumeaux directs -Csharp Search-1..11/2b/03b..03d + Search-2c QuikGraph natif + déclinaison Métaheuristiques Search-11b en 4 volets + Search-09b/09c/09d discrépance + Search-03e optimalité A* + Search-11c/11d sélection empirique & descente sous budget + Search-12a Composer-Regards + Search-13a Traverser-Murs-Certifies)
+├── Part1-Foundations/                     # Search Fondamental — jumeaux directs -Csharp Search-1..11/2b/03b..03d + Search-2c QuikGraph natif + déclinaison Métaheuristiques Search-11b en 4 volets + Search-09b/09c discrépance + Search-03e optimalité A* + Search-11c/11d sélection empirique & descente sous budget + Search-12a Composer-Regards + Search-13a Traverser-Murs-Certifies
 │   ├── Search-01-StateSpace.ipynb
 │   ├── Search-02-Uninformed.ipynb
 │   ├── Search-02b-NetworkX.ipynb
@@ -335,7 +336,6 @@ Search/
 │   ├── Search-09-LinearProgramming.ipynb
 │   ├── Search-09b-SpuriousMinima.ipynb
 │   ├── Search-09c-CombinatorialDiscrepancy.ipynb
-│   ├── Search-09d-Lean-Discrepancy-Komlos.ipynb   # Compagnon formel : lake discrepancy_lean via kernel lean4-wsl (#13868)
 │   ├── Search-10-SymbolicAutomata.ipynb
 │   ├── Search-11-Metaheuristics.ipynb
 │   ├── Search-11c-Empirical-Algorithm-Selection.ipynb
@@ -345,6 +345,9 @@ Search/
 │   ├── Search-03d-WeightedAstar.ipynb
 │   ├── Search-12a-Composer-Regards.ipynb       # Composer des regards : play forward x coplay backward, corridor optimal f*=g+d (op 12 #12204)
 │   └── Search-13a-Traverser-Murs-Certifies.ipynb   # Traverser un mur : chemin minimal certifié (potentiels, 0-1 BFS, flot max/coupure min) sur pavage hexagonal (op 13 #12204)
+├── Discrepancy/                           # Sous-série formelle (ouverte par #17816, arbitrage Search #17802) : compagnons Lean du lake discrepancy_lean
+│   ├── Discrepancy-01-BeckFiala-Lean-Python.ipynb   # Beck–Fiala : pont Python vers le lake, sans Lean au runtime
+│   └── Discrepancy-02-Komlos-Lean.ipynb             # Compagnon formel : lake discrepancy_lean via kernel lean4-wsl (#13868)
 │
 ├── Part2-CSP/                             # Programmation par Contraintes (18 notebooks : 9 Python + 9 jumeaux C#)
 │   ├── CSP-1-Fundamentals.ipynb
diff --git a/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md b/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
index 44cae539fc..780e4920e4 100644
--- a/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
+++ b/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
@@ -153,7 +153,7 @@ branche, jamais `main`. Issue de suivi : #17845.
 | **k2** | **Lemme 1.4** — induction simultanée sur `n` et `d` (la noix de cette voie) | fini + induction | k1 |
 | **k3** | Lemme 4.1 — densité-tente, FTC sur segments, Cauchy–Schwarz `L²`, `TV ≤ ‖v‖₂/√12` | analyse | `norm_image_sub_le` (re-vérifier au pin) |
 | **k4** | Lemme 1.5 — discrétisation sur la grille, cas rationnel | fini | k3 |
-| **k5** | Assemblage Thm 1.2 sur `ℚ` (témoin `36`) + corollaires (`KomlosBansalJiangWeak`, Beck–Fiala régulier `72√k`) + notebooks `Search-09c`/`Search-09d` (ligne « course aux bornes » du 22/09/2026) | assemblage | k2, k4 |
+| **k5** | Assemblage Thm 1.2 sur `ℚ` (témoin `36`) + corollaires (`KomlosBansalJiangWeak`, Beck–Fiala régulier `72√k`) + notebooks `Search-09c`/`Discrepancy-02` (ligne « course aux bornes » du 22/09/2026) | assemblage | k2, k4 |
 
 **Deux routes, non exclusives** — à trancher au premier cycle d'implémentation :
 
diff --git a/MyIA.AI.Notebooks/Search/index.qmd b/MyIA.AI.Notebooks/Search/index.qmd
index adc4d9ca51..f120c8e84b 100644
--- a/MyIA.AI.Notebooks/Search/index.qmd
+++ b/MyIA.AI.Notebooks/Search/index.qmd
@@ -72,6 +72,17 @@ discrimine, pas un cas dégénéré où A\* ≡ BFS). Le companion de la série
   [#13662](https://github.com/jsboige/CoursIA/issues/13662) depuis
   `SymbolicAI/Lean/`.
 
+Le second lake de la série, [`discrepancy_lean`](discrepancy_lean/FORMAL_STATUS.md), formalise
+la **discrépance combinatoire** (distillation Bansal–Jiang 2025, arXiv:2508.03961) : colorations
+`±1` de systèmes d'ensembles de degré `≤ k`, borne de Beck–Fiala assemblée, borne inférieure
+d'Erdős–Spencer à constante explicite. Ses companions :
+
+- [Discrepancy-02-Komlos-Lean](Discrepancy/Discrepancy-02-Komlos-Lean.ipynb)
+  — compagnon formel, kernel `lean4-wsl` : `#check` des énoncés du lake et témoins
+  coloriés ±1 énumérés exhaustivement sur des instances jouet ;
+- [Discrepancy-01-BeckFiala-Lean-Python](Discrepancy/Discrepancy-01-BeckFiala-Lean-Python.ipynb)
+  — pont Python vers le même lake (CP-SAT en oracle exact), sans Lean au runtime.
+
 ## Démarrage rapide
 
 ```bash
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb
index 34a7a9ebec..964c13d944 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb
@@ -1876,7 +1876,7 @@
     "\n",
     "1. **Formaliser un énoncé** : le dépôt [Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) fournit des conjectures en Lean, mais leur présence dans le benchmark ne signifie pas qu'elles sont prouvées. Sa documentation avertit aussi qu'une formalisation peut perdre une nuance de l'énoncé source.\n",
     "2. **Chercher une preuve** : Tsoukalas et al., *Advancing Mathematics Research with AI-Driven Formal Proof Search* ([arXiv:2605.22763v1](https://arxiv.org/abs/2605.22763v1)), rapportent 9 résolutions sur 353 problèmes ouverts tentés. Ce résultat expérimental ne justifie ni une extrapolation à tous les problèmes, ni l'attribution de numéros précis à d'autres systèmes sans source primaire.\n",
-    "3. **Vérifier ce que le dépôt prouve réellement** : CoursIA contient `erdos_spencer_lb_explicit`, une borne inférieure d'Erdős–Spencer formalisée dans `discrepancy_lean` et exécutée dans [Search-09d](../../Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb). La couche Python pédagogique correspondante se trouve dans [Search-09c](../../Search/Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb).\n",
+    "3. **Vérifier ce que le dépôt prouve réellement** : CoursIA contient `erdos_spencer_lb_explicit`, une borne inférieure d'Erdős–Spencer formalisée dans `discrepancy_lean` et exécutée dans [Discrepancy-02](../../Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb). La couche Python pédagogique correspondante se trouve dans [Search-09c](../../Search/Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb).\n",
     "\n",
     "[Lean-10](Lean-10-LeanDojo.ipynb) présente déjà Formal Conjectures comme cible de traçage LeanDojo. La cellule de code de cette section construit donc un **registre de niveaux de preuve**, et non une liste de résolutions supposées."
    ]
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-08-Agentic-Proving-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-08-Agentic-Proving-Python.ipynb
index 2c19b086ee..787ef3fb77 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-08-Agentic-Proving-Python.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-08-Agentic-Proving-Python.ipynb
@@ -1524,7 +1524,7 @@
     "\n",
     "Nous testons ici l'orchestration sur des **identités arithmétiques élémentaires**. Ce smoke test vérifie la circulation entre recherche, génération et vérification simulée ; il ne mesure pas la capacité à résoudre des problèmes d'Erdős ou de niveau IMO.\n",
     "\n",
-    "Pour passer à un corpus de recherche, il faut distinguer les [énoncés formalisés de Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) des résultats effectivement prouvés. [Lean-10](Lean-10-LeanDojo.ipynb) montre comment tracer ce corpus. Dans CoursIA, [Search-09d](../../Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb) exécute le résultat `erdos_spencer_lb_explicit` réellement présent dans `discrepancy_lean`."
+    "Pour passer à un corpus de recherche, il faut distinguer les [énoncés formalisés de Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) des résultats effectivement prouvés. [Lean-10](Lean-10-LeanDojo.ipynb) montre comment tracer ce corpus. Dans CoursIA, [Discrepancy-02](../../Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb) exécute le résultat `erdos_spencer_lb_explicit` réellement présent dans `discrepancy_lean`."
    ]
   },
   {
@@ -2573,7 +2573,7 @@
     "|--------|-----------|------------------|\n",
     "| Énoncés | [Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) et [Lean-10](Lean-10-LeanDojo.ipynb) | Corpus Lean pour la recherche, pas collection de preuves acquises |\n",
     "| Étude empirique | [Tsoukalas et al. (2026)](https://arxiv.org/abs/2605.22763v1) | Succès rapportés sur un corpus tenté, avec coûts, variance et biais de sélection |\n",
-    "| Preuve dans CoursIA | [Search-09d](../../Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb) | `erdos_spencer_lb_explicit`, borne formelle inspectable dans `discrepancy_lean` |\n",
+    "| Preuve dans CoursIA | [Discrepancy-02](../../Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb) | `erdos_spencer_lb_explicit`, borne formelle inspectable dans `discrepancy_lean` |\n",
     "\n",
     "Le gain scientifique vient donc de la chaîne complète : **digérer l'énoncé, vérifier sa formalisation, chercher une preuve, faire contrôler la preuve par Lean, puis soumettre l'interprétation mathématique à la revue humaine**.\n",
     "\n",
diff --git a/_quarto.yml b/_quarto.yml
index 733ab83c3f..cf57a711df 100644
--- a/_quarto.yml
+++ b/_quarto.yml
@@ -1715,7 +1715,7 @@ project:
     - "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09-LinearProgramming.ipynb"
     - "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09b-SpuriousMinima.ipynb"
     - "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb"
-    - "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb"
+    - "MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb"
     - "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-10-SymbolicAutomata-CSharp.ipynb"
     - "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-10-SymbolicAutomata.ipynb"
     - "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-11-Metaheuristics-CSharp.ipynb"
diff --git a/docs/curriculum/aima-walk.md b/docs/curriculum/aima-walk.md
index 7786de036c..d75d7bdebc 100644
--- a/docs/curriculum/aima-walk.md
+++ b/docs/curriculum/aima-walk.md
@@ -137,7 +137,7 @@ métaheuristiques composées) — l'épilogue le nomme.
 ### Épilogue — Où le corpus dépasse AIMA, ~45 min
 
 25. **`IIT/IIT-01-IntroToPyPhi.ipynb`** (45 min) — théorie de l'information intégrée :
-    hors AIMA, propre au dépôt. Prolongements nommés : `Search-09d-Lean-Discrepancy-Komlos`
+    hors AIMA, propre au dépôt. Prolongements nommés : `Discrepancy-02-Komlos-Lean`
     (recherche **formelle**, compagnon Lean de la phase 2), la série IIT complète (59
     notebooks de la famille la plus dense du dépôt, cf `docs/curriculum/recherche.md`).
 
diff --git a/docs/curriculum/ia-classique.md b/docs/curriculum/ia-classique.md
index 16a9118323..8bea669b34 100644
--- a/docs/curriculum/ia-classique.md
+++ b/docs/curriculum/ia-classique.md
@@ -123,7 +123,7 @@ Algorithmes de recherche classique, satisfaction de contraintes (CSP), résoluti
 | 29 | [Search-09-LinearProgramming : Programmation Lineaire et…](../../MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09-LinearProgramming.ipynb) | BETA | Oui |
 | 30 | [Search-09b : Minima fallacieux — le paysage de la…](../../MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09b-SpuriousMinima.ipynb) | BETA | Oui |
 | 31 | [Search-09c — Discrépance combinatoire : colorier ±1…](../../MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb) | BETA | Oui |
-| 32 | [Search-09d — Discrépance combinatoire : la couche…](../../MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb) | BETA | Oui |
+| 32 | [Discrepancy-02 — Discrépance combinatoire : la couche…](../../MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb) | BETA | Oui |
 | 33 | [Search-10 (C#) : Automates Finis Classiques — jumeau…](../../MyIA.AI.Notebooks/Search/Part1-Foundations/Search-10-SymbolicAutomata-CSharp.ipynb) | BETA | Oui |
 | 34 | [Search-10 : Automates Symboliques avec Z3](../../MyIA.AI.Notebooks/Search/Part1-Foundations/Search-10-SymbolicAutomata.ipynb) | BETA | Oui |
 | 35 | [Search-11 (C#) : Métaheuristiques — Optimisation par…](../../MyIA.AI.Notebooks/Search/Part1-Foundations/Search-11-Metaheuristics-CSharp.ipynb) | BETA | Oui |
diff --git a/docs/reference/rename-ledger.tsv b/docs/reference/rename-ledger.tsv
index 4d9ebd836b..c63b909973 100644
--- a/docs/reference/rename-ledger.tsv
+++ b/docs/reference/rename-ledger.tsv
@@ -225,5 +225,6 @@ MyIA.AI.Notebooks/SymbolicAI/SmartContracts/06-Real-World/SC-25-Mainnet-Deploy.i
 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
 ancien	nouveau	date	lane
-MyIA.AI.Notebooks/IIT/ICT-Series/ICT-42-Crosscoder-Distillation-Python.ipynb	MyIA.AI.Notebooks/IIT/ICT-Series/ICT-41b-Crosscoder-Distillation-Python.ipynb	2026-10-03	myia-po-2027:CoursIA
-MyIA.AI.Notebooks/IIT/ICT-Series/ICT-45-InoculationBifurcation-9B-Python.ipynb	MyIA.AI.Notebooks/IIT/ICT-Series/ICT-42b-InoculationBifurcation-9B-Python.ipynb	2026-10-04	myia-po-2023:CoursIA
+MyIA.AI.Notebooks/IIT/ICT-Series/ICT-42-Crosscoder-Distillation-Python.ipynb	MyIA.AI.Notebooks/IIT/ICT-Series/ICT-41b-Crosscoder-Distillation-Python.ipynb	2026-10-03	myia-po-2027:CoursIA
+MyIA.AI.Notebooks/IIT/ICT-Series/ICT-45-InoculationBifurcation-9B-Python.ipynb	MyIA.AI.Notebooks/IIT/ICT-Series/ICT-42b-InoculationBifurcation-9B-Python.ipynb	2026-10-04	myia-po-2023:CoursIA
+MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb	MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb	2026-10-04	myia-po-2027:CoursIA