myia-ai-01 · Oct 5, 2026 · Oct 4, 2026 · Oct 4, 2026 · Oct 4, 2026 · Oct 4, 2026
diff --git a/.../Search-09d-Lean-Discrepancy-Komlos.ipynb → ...crepancy/Discrepancy-02-Komlos-Lean.ipynb b/.../Search-09d-Lean-Discrepancy-Komlos.ipynb → ...crepancy/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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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