From 8c5573668507dc17fc08cb983c8cf8a8de4a556e Mon Sep 17 00:00:00 2001
From: jsboige <jsboige@gmail.com>
Date: Sun, 4 Oct 2026 22:53:52 +0200
Subject: [PATCH 1/6] rename(#16231): git mv purs (1 notebooks)

Table : issue:17802#5984216914, pilotee par rename_notebooks.py.
---
 .../Discrepancy-02-Komlos-Lean.ipynb}                             | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename MyIA.AI.Notebooks/Search/{Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb => Discrepancy/Discrepancy-02-Komlos-Lean.ipynb} (100%)

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 100%
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

From ea0362c56b2ca62ce1bf193ca37a30444c46a2f4 Mon Sep 17 00:00:00 2001
From: jsboige <jsboige@gmail.com>
Date: Sun, 4 Oct 2026 22:54:30 +0200
Subject: [PATCH 2/6] rename(#16231): referents reecrits par surface (7
 fichiers)

Cellules de code citees : jamais reecrites (re-execution C.2 due).
Sorties commitees : jamais touchees.
---
 MyIA.AI.Notebooks/Search/Part1-Foundations/README.md          | 2 +-
 MyIA.AI.Notebooks/Search/README.md                            | 2 +-
 .../SymbolicAI/Lean/Lean-08-Agentic-Proving-Python.ipynb      | 4 ++--
 _quarto.yml                                                   | 2 +-
 docs/curriculum/aima-walk.md                                  | 2 +-
 docs/curriculum/ia-classique.md                               | 2 +-
 docs/reference/rename-ledger.tsv                              | 1 +
 scripts/tests/baseline_nb_nav_chain.json                      | 2 +-
 8 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md b/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md
index 36b9bec60a..2020d8d5cc 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-02-Komlos-Lean.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 |
 | 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 |
diff --git a/MyIA.AI.Notebooks/Search/README.md b/MyIA.AI.Notebooks/Search/README.md
index 6bc27f10fb..7fc196221f 100644
--- a/MyIA.AI.Notebooks/Search/README.md
+++ b/MyIA.AI.Notebooks/Search/README.md
@@ -335,7 +335,7 @@ 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)
+│   ├── Discrepancy-02-Komlos-Lean.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
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..6b1c655c9c 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, [Search-09d](../../Search/Part1-Foundations/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 | [Search-09d](../../Search/Part1-Foundations/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 2ac63adcbf..84d6fb2ca3 100644
--- a/_quarto.yml
+++ b/_quarto.yml
@@ -1716,7 +1716,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..0a69dec98f 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 | [Search-09d — 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 0b7acb1758..477ad7ca4f 100644
--- a/docs/reference/rename-ledger.tsv
+++ b/docs/reference/rename-ledger.tsv
@@ -226,3 +226,4 @@ MyIA.AI.Notebooks/SymbolicAI/SmartContracts/06-Real-World/SC-26-Final-Project.ip
 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/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
diff --git a/scripts/tests/baseline_nb_nav_chain.json b/scripts/tests/baseline_nb_nav_chain.json
index 8e442cbd8c..11cc008527 100644
--- a/scripts/tests/baseline_nb_nav_chain.json
+++ b/scripts/tests/baseline_nb_nav_chain.json
@@ -1867,7 +1867,7 @@
     },
     {
       "kind": "unreachable",
-      "notebook": "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb",
+      "notebook": "MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb",
       "series": "MyIA.AI.Notebooks/Search/Part1-Foundations"
     },
     {

From 2d0ec03d584c6141f70d9151bcbecf9270795d28 Mon Sep 17 00:00:00 2001
From: jsboige <jsboige@gmail.com>
Date: Sun, 4 Oct 2026 23:14:10 +0200
Subject: [PATCH 3/6] fix(search,#17802): liens relatifs casses par la descente
 de 09d -- prefixe recalcule

L'organe de renommage reecrit le basename d'un lien relatif mais jamais son
prefixe de repertoire : `../../Search/Part1-Foundations/<nom>` pointait donc
encore l'ancien dossier apres le deplacement vers `Search/Discrepancy/`.

Repares : 6 liens casses releves par navlinks, dont 3 dans le notebook deplace
(liens vers `Search-09c`, meme dossier avant le move) que la CI n'avait pas
signales, et 2 dans Lean-08 (HREF_MISSING du garde enrich-quality). Le titre H1
et le fil d'Ariane du notebook deplace suivent la convention du pilote
`Discrepancy-01`.

Aucune cellule de code, aucune sortie, aucun execution_count modifie (garde
I1/I2/I3 de l'organe canonique, verifiee avant ecriture).

See #17802

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
---
 .../Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb   | 8 ++++----
 MyIA.AI.Notebooks/Search/Part1-Foundations/README.md      | 2 +-
 .../SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb        | 2 +-
 .../SymbolicAI/Lean/Lean-08-Agentic-Proving-Python.ipynb  | 4 ++--
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb b/MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb
index a1d49860a9..a9dd334b69 100644
--- a/MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.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/Part1-Foundations/README.md b/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md
index 2020d8d5cc..ffcfc160db 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 | [Discrepancy-02-Komlos-Lean](Discrepancy-02-Komlos-Lean.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.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 |
 | 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 |
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 6b1c655c9c..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/Discrepancy-02-Komlos-Lean.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/Discrepancy-02-Komlos-Lean.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",

From d809ec0e5e79637e832352a4688e00436e07b468 Mon Sep 17 00:00:00 2001
From: jsboige <jsboige@gmail.com>
Date: Sun, 4 Oct 2026 23:55:52 +0200
Subject: [PATCH 4/6] Docs(Search): completer les referents du renommage
 Search-09d -> Discrepancy-02

Le renommage avait suivi le nom de fichier sans le dossier : le carnet restait
liste sous Part1-Foundations/ et la sous-serie Discrepancy/ n'avait aucun noeud
dans l'arbre, alors que le dossier porte deux carnets depuis #17816.

- arbre : noeud Discrepancy/ (01 Beck-Fiala, 02 Komlos) ; le commentaire du
  noeud Part1-Foundations perd son compte et la mention 09d ;
- table Couverture actuelle : ligne Discrepancy/ ajoutee, ligne Part1 corrigee
  (23, sans le compagnon Lean qui a change de dossier) ;
- Part1-Foundations/README.md : trois references de nom (prerequis, table des
  kernels, bibliographie) ;
- discrepancy_lean/FORMAL_STATUS.md k5 et libelle du curriculum ;
- baseline nav-chain : l'entree unreachable de Discrepancy-02 est retiree, elle
  portait une serie devenue fausse et le finding ne se produit plus.

See #17802, See #17816

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
---
 MyIA.AI.Notebooks/Search/Part1-Foundations/README.md     | 6 +++---
 MyIA.AI.Notebooks/Search/README.md                       | 9 ++++++---
 .../Search/discrepancy_lean/FORMAL_STATUS.md             | 2 +-
 docs/curriculum/ia-classique.md                          | 2 +-
 scripts/tests/baseline_nb_nav_chain.json                 | 5 -----
 5 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md b/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md
index ffcfc160db..fdbe4797f0 100644
--- a/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md
+++ b/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md
@@ -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 7fc196221f..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
-│   ├── Discrepancy-02-Komlos-Lean.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 a395fb1d66..e07da4d885 100644
--- a/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
+++ b/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
@@ -152,7 +152,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/docs/curriculum/ia-classique.md b/docs/curriculum/ia-classique.md
index 0a69dec98f..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/Discrepancy/Discrepancy-02-Komlos-Lean.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/scripts/tests/baseline_nb_nav_chain.json b/scripts/tests/baseline_nb_nav_chain.json
index 11cc008527..f27eda092f 100644
--- a/scripts/tests/baseline_nb_nav_chain.json
+++ b/scripts/tests/baseline_nb_nav_chain.json
@@ -1865,11 +1865,6 @@
       "notebook": "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb",
       "series": "MyIA.AI.Notebooks/Search/Part1-Foundations"
     },
-    {
-      "kind": "unreachable",
-      "notebook": "MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb",
-      "series": "MyIA.AI.Notebooks/Search/Part1-Foundations"
-    },
     {
       "kind": "unreachable",
       "notebook": "MyIA.AI.Notebooks/Search/Part2-CSP/CSP-8-Temporal-CSharp.ipynb",

From 13ffb2173653651fdefcd12eaf19938f0e6594db Mon Sep 17 00:00:00 2001
From: jsboige <jsboige@gmail.com>
Date: Mon, 5 Oct 2026 00:10:03 +0200
Subject: [PATCH 5/6] docs(search,#17802): completer les referents de la
 descente 09d -- inventaire Lean et index
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Deux surfaces ne connaissaient pas encore la descente de Search-09d vers
Search/Discrepancy/ :

- LEAN_INVENTORY.md declarait `discrepancy_lean` sans notebook cable
  (« compagnon prevu : Search-15-CombinatorialDiscrepancy ... Pas encore
  cable »). Mesure : Discrepancy-02-Komlos-Lean tourne sur `lean4-wsl` avec
  27 `#check` sur les enonces du lake -- il est cable. La ligne passe a 1² et
  le Total a 2. Le livrable A de #12823 est livre en Discrepancy-01, kernel
  `python3`, pont Python vers le lake sans Lean au runtime : il ne compte donc
  pas dans cette colonne, qui mesure l'invocation effective du lake.
- index.qmd ne documentait que `search_lean`. La section « Companion formel »
  nomme desormais `discrepancy_lean` et ses deux carnets.

Residuel nomme, non traite ici : Lean-07b-Examples-Python.ipynb cellule 30
imprime encore l'ancien libelle (`Search-09d-Lean-Discrepancy-Komlos.ipynb`).
Le corriger demande une re-execution, et l'executeur de cellule unique
(scripts/notebook_tools/exec_single_cell.py) retire par conception les blocs
`metadata.papermill` herites (#12722) -- soit 387 lignes sur ce carnet, sans
rapport avec ce renommage. Mesure : 1134 des 1485 carnets committes portent
ces blocs, c'est la convention dominante du depot. Le sujet part donc en PR
dediee plutot que d'entrer ici.

Guards : prose-counts rc=0 ; navlinks 0 lien casse (1472 carnets) ;
nav-chain --check rc=0 (0 NEW vs baseline).

See #17802

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
---
 MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md | 17 ++++++++++++-----
 MyIA.AI.Notebooks/Search/index.qmd         | 11 +++++++++++
 2 files changed, 23 insertions(+), 5 deletions(-)

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/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

From 5cc849e71aee1afe5b3a73204301e8991d8426da Mon Sep 17 00:00:00 2001
From: jsboige <jsboige@gmail.com>
Date: Mon, 5 Oct 2026 03:09:33 +0200
Subject: [PATCH 6/6] fix(search,#17802): lien README vers le rendu .html de
 Discrepancy-02

`Audit README -> .ipynb links` signalait une NOUVELLE violation sur cette PR :

  STALE_LINK Search/Part1-Foundations/README.md ->
    ../Discrepancy/Discrepancy-02-Komlos-Lean.ipynb

Le carnet deplace est desormais dans la render-list (`_quarto.yml`), donc le
lien brut `.ipynb` 404 sur Pages -- la ligne doit pointer le rendu `.html`,
comme les autres lignes rendues du meme tableau (Search-05-CSharp, Search-10,
Search-11). Le lien precedent (ancien chemin `Search-09d-...`) n'etait pas
dans la render-list : le deplacement a cree la violation, pas le style de lien.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
---
 MyIA.AI.Notebooks/Search/Part1-Foundations/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md b/MyIA.AI.Notebooks/Search/Part1-Foundations/README.md
index fdbe4797f0..8c276048c8 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 | [Discrepancy-02-Komlos-Lean](../Discrepancy/Discrepancy-02-Komlos-Lean.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 |