Docs(search,#20975): tranche serie Search -- compteurs de prose resorbes

MyIA.AI.Notebooks/Search/Part1-Foundations/README.md

@@ -77,7 +77,7 @@ Cette partie est l'alphabet de toute la série : la formalisation en espace d'é
 | 11d | [Search-11d-Descente-Sous-Budget](Search-11d-Descente-Sous-Budget.ipynb) | Python 3 | Variante de Search-11 et Search-11c : la loi derrière les descentes sous budget (op 11 du chantier ICT, [#12204](https://github.com/jsboige/CoursIA/issues/12204)). Les hypothèses de `SymbolicAI/Lean/mimo_lean/Descent.lean` sont exercées au runtime : décroissance stricte et confinement vérifiés à chaque mouvement accepté, plafond d'évaluations vérifié à chaque exécution, sans violation sur des graines fixes. L'hypothèse `hnostall` (un mouvement améliorant existe toujours hors de la cible) y est réfutée : à budget généreux, tous les blocages sont des optima locaux hors cible. La courbe qualité-budget plafonne ensuite, car les arrêts restants sont des blocages et non des interruptions. Bibliothèque standard seule, trois exercices (restarts, barrière, voisinage 2-flip) | ~45 min |
 | 12 | [Search-12-BranchAndBound-Borne-LP-Python](Search-12-BranchAndBound-Borne-LP-Python.ipynb) | Python 3 | **Pourquoi la recherche arborescente fonctionne, et quand sa borne s'effondre** : le sac à dos 0-1 comme terrain à deux algorithmes exacts de nature opposée — la DP pseudo-polynomiale en la **capacité** (`O(n·W)`, une passe numpy par objet) et le **branch-and-bound** gouverné par la borne de relaxation continue, arbitrés par `scipy.optimize.milp` (HiGHS) qui sert de juge indépendant. Trois mesures, aucune supposée : les trois méthodes exactes concordent 9/9 et le glouton de ratio reste strictement sous l'optimum 3/9 ; à `n` et famille fixes, une capacité ×100 fait passer la DP de la fraction de milliseconde à quelques millisecondes tandis que le B&B reste **exactement à 113 nœuds** ; et sur des instances **fortement corrélées** (`v = w + 10`) le nombre de nœuds est **multiplié par six** (113 → 682) alors que l'écart de borne, lui, **diminue** (0,50 % → 0,16 %) — une borne plus serrée en valeur n'élague pas mieux. Complète Search-9 (formulation PuLP/CBC) en montrant le mécanisme plutôt que l'appel ; figure des deux axes de coût, trois exercices (reconstruire la solution, borne plus serrée et nœuds, frontière DP/B&B) | ~45 min |
 | 12a | [Search-12a-Composer-Regards](Search-12a-Composer-Regards.ipynb) | Python 3 | **Composer des regards** (op 12 du chantier ICT, [#12204](https://github.com/jsboige/CoursIA/issues/12204)) : play forward (`g`, Dijkstra depuis le départ) × coplay backward (`d`, Dijkstra depuis l'arrivée) sur un gridworld pondéré 10×14 déterministe — corridor optimal isolé par `f* = g + d` (19/140 nœuds), associativité de la composition à relais (toujours vraie comme opérateur), exactitude conditionnelle (écart 0 sur route, +2 hors route : inégalité triangulaire), **paire de lectures incompatibles exhibée** (coût × pas : divergence dès le pas 1, route à +32 de coût ; A* 24 vs 75 expansions) — 2e attestation directe, substrat indépendant de GT-21 (#12245) | ~1h |
-| 13a | [Search-13a-Traverser-Murs-Certifies](Search-13a-Traverser-Murs-Certifies.ipynb) | Python 3 | **Traverser un mur** (op 13 du chantier ICT, [#12204](https://github.com/jsboige/CoursIA/issues/12204)) : pavage hexagonal de 61 salles (coordonnées axiales), deux chambres séparées par une double chaîne de murs (8+9 cellules de coût 3 contre sol à 1) fermant l'anneau de bout en bout, six swaps générateurs (les six directions hexagonales) — chemin minimal **certifié** par quatre organes indépendants (Dijkstra L=12, audit de potentiels : 312 arêtes, 0 violation, égalités serrées le long du chemin ; 0-1 BFS : épaisseur m_path=2 ; flot max Edmonds-Karp par nœuds fendus : largeur m=8 = coupure minimale, certificat de coupe par BFS) — distinction **épaisseur** (murs sur un chemin) vs **largeur** (murs à démolir, Menger), test négatif de l'opération : percement Δ=−2 et certificat rejeté (pas un morphisme) contre swap silencieux de feuille Δ=0 et certificat préservé (morphisme), balayage du coût c_w qui bascule le point de passage (3 → 2 murs franchis) — 2e attestation directe, substrat indépendant de GT-24 (#12364) | ~1h |
+| 13a | [Search-13a-Traverser-Murs-Certifies](Search-13a-Traverser-Murs-Certifies.ipynb) | Python 3 | **Traverser un mur** (op 13 du chantier ICT, [#12204](https://github.com/jsboige/CoursIA/issues/12204)) : pavage hexagonal de 61 salles (coordonnées axiales), deux chambres séparées par une double chaîne de murs (cellules de coût 3 contre sol à 1) fermant l'anneau de bout en bout, six swaps générateurs (les six directions hexagonales) — chemin minimal **certifié** par quatre organes indépendants (Dijkstra L=12, audit de potentiels : 312 arêtes, 0 violation, égalités serrées le long du chemin ; 0-1 BFS : épaisseur m_path=2 ; flot max Edmonds-Karp par nœuds fendus : largeur m=8 = coupure minimale, certificat de coupe par BFS) — distinction **épaisseur** (murs sur un chemin) vs **largeur** (murs à démolir, Menger), test négatif de l'opération : percement Δ=−2 et certificat rejeté (pas un morphisme) contre swap silencieux de feuille Δ=0 et certificat préservé (morphisme), balayage du coût c_w qui bascule le point de passage (3 → 2 murs franchis) — 2e attestation directe, substrat indépendant de GT-24 (#12364) | ~1h |
 
 ### Accrétions avancées de Search-3 (ex-Partie 3)
 

MyIA.AI.Notebooks/Search/README.md

@@ -77,7 +77,7 @@ flowchart LR
 
 ### Side-track avancé : métaheuristiques composables (Part 4, C# .NET 9)
 
-En parallèle du parcours Python, la [Partie 4 — MetaGeneticSharp](Part4-Metaheuristics/README.md) propose un **side-track .NET 9** de 22 notebooks (MGS-1 à MGS-19 plus la trilogie MGS-7b/7c/7d de projection N-D des paysages) qui **reconstruit et compose** les métaheuristiques au-dessus de GeneticSharp plutôt que d'importer une boîte noire. Il prolonge Search-5 (GeneticAlgorithms) et Search-11 (Métaheuristiques) et se lit en quatre temps : **MGS-1 à 7** bâtissent le moteur et la grammaire de composition (jusqu'au TSP) ; **MGS-7b, MGS-8 à 14** visualisent les paysages de fitness (MGS-7b projette les benchmarks en dimension N≥5) et mesurent la robustesse aux biais des bancs CEC (décalage, rotation, synergie d'îles) ; **MGS-15 à 18** referment la série sur l'analyse quantitative de paysage et la méta-stratégie (No-Free-Lunch, contrôle de paramètres) ; **MGS-19** démonte le recuit simulé pour éprouver l'opérateur de Metropolis seul. Optionnel pour qui vise le cœur Python, central pour qui veut *construire* ses métaheuristiques en .NET.
+En parallèle du parcours Python, la [Partie 4 — MetaGeneticSharp](Part4-Metaheuristics/README.md) propose un **side-track .NET 9** (MGS-1 à MGS-19 plus la trilogie MGS-7b/7c/7d de projection N-D des paysages) qui **reconstruit et compose** les métaheuristiques au-dessus de GeneticSharp plutôt que d'importer une boîte noire. Il prolonge Search-5 (GeneticAlgorithms) et Search-11 (Métaheuristiques) et se lit en quatre temps : **MGS-1 à 7** bâtissent le moteur et la grammaire de composition (jusqu'au TSP) ; **MGS-7b, MGS-8 à 14** visualisent les paysages de fitness (MGS-7b projette les benchmarks en dimension N≥5) et mesurent la robustesse aux biais des bancs CEC (décalage, rotation, synergie d'îles) ; **MGS-15 à 18** referment la série sur l'analyse quantitative de paysage et la méta-stratégie (No-Free-Lunch, contrôle de paramètres) ; **MGS-19** démonte le recuit simulé pour éprouver l'opérateur de Metropolis seul. Optionnel pour qui vise le cœur Python, central pour qui veut *construire* ses métaheuristiques en .NET.
 
 ## Ce que chaque notebook apporte
 
@@ -361,7 +361,7 @@ Search/
 │   ├── 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)
 │
-├── Part2-CSP/                             # Programmation par Contraintes (18 notebooks : 9 Python + 9 jumeaux C#)
+├── Part2-CSP/                             # Programmation par Contraintes (Python + jumeaux C#, marathon #4956 achevé)
 │   ├── CSP-1-Fundamentals.ipynb
 │   ├── CSP-2-Consistency.ipynb
 │   ├── CSP-3-Advanced.ipynb
@@ -400,7 +400,7 @@ Search/
 ├── Part5-Frontieres/                     # Partie 5 — frontières : audits de garanties et distillations de preprints (Frontieres-01..10, carte #19253)
 │
 ├── MetaGeneticSharp/                      # Sous-module : metaheuristiques composables sur GeneticSharp (jsboige/MetaGeneticSharp)
-├── Part4-Metaheuristics/                  # Partie 4 (35 notebooks C# .NET 9 : 25 à la racine + 10 sous MGS-vs-mealpy/) ; consomme le sous-module MetaGeneticSharp
+├── Part4-Metaheuristics/                  # Partie 4 (C# .NET 9, volumes portés par le catalogue) ; consomme le sous-module MetaGeneticSharp
 │
 └── _archive/                               # Notebooks racine archivés (C209 tranche 8/8 #5081) — voir _archive/README.md
     ├── README.md
@@ -482,9 +482,9 @@ Audit **disque ↔ CATALOG-STATUS ↔ prose** vérifié firsthand via `git ls-fi
 
 | Sous-série | Fichiers `.ipynb` gît-tracked | Langages | Algorithmes représentatifs |
 | --- | --- | --- | --- |
-| **Part 1 — Fondements** (`Part1-Foundations/`) | **43** (**23 notebooks Python + Lean** : Search-1 → Search-11, Search-2b, Search-03b/03c/03d/03e (ex-Partie 3 + optimalité A*), Search-09b, Search-09c, Search-11c, Search-11d, Search-12a (Composer-Regards, op 12 #12204), Search-13a (Traverser-Murs-Certifies, op 13 #12204) + **compagnon Lean Search-09d** (kernel `lean4-wsl`, lake `discrepancy_lean`) + **20 C#** : jumeaux `-Csharp` (Search-1 à 11, 2b et 03b/03c/03d) + Search-2c QuikGraph natif + déclinaison deep-dive **Search-11b Métaheuristiques en 4 volets** C# natif, marathon #4956) | Python + Lean 4 + .NET (C#) | StateSpace, BFS/DFS/UCS/IDDFS, A*, Local Search (SA/Tabu), GA, Minimax/Alpha-Beta, MCTS, DLX, LP, Symbolic Automata, métaheuristiques (PSO/ABC/BRO + 160+ MEALPy), NetworkX, QuikGraph, Pattern Databases, Limited Discrepancy Search, Weighted A*, minima fallacieux SDP (Burer–Monteiro), discrépance combinatoire (Beck–Fiala, Bansal–Jiang 2025) et sa formalisation Lean 4 (conjecture de Komlós), sélection empirique d'algorithme, descente gloutonne sous plafond d'évaluations (loi `Descent.lean`) |
+| **Part 1 — Fondements** (`Part1-Foundations/`) | **43** (**Python + Lean** : Search-1 → Search-11, Search-2b, Search-03b/03c/03d/03e (ex-Partie 3 + optimalité A*), Search-09b, Search-09c, Search-11c, Search-11d, Search-12a (Composer-Regards, op 12 #12204), Search-13a (Traverser-Murs-Certifies, op 13 #12204) + **compagnon Lean Search-09d** (kernel `lean4-wsl`, lake `discrepancy_lean`) + **20 C#** : jumeaux `-Csharp` (Search-1 à 11, 2b et 03b/03c/03d) + Search-2c QuikGraph natif + déclinaison deep-dive **Search-11b Métaheuristiques en 4 volets** C# natif, marathon #4956) | Python + Lean 4 + .NET (C#) | StateSpace, BFS/DFS/UCS/IDDFS, A*, Local Search (SA/Tabu), GA, Minimax/Alpha-Beta, MCTS, DLX, LP, Symbolic Automata, métaheuristiques (PSO/ABC/BRO + 160+ MEALPy), NetworkX, QuikGraph, Pattern Databases, Limited Discrepancy Search, Weighted A*, minima fallacieux SDP (Burer–Monteiro), discrépance combinatoire (Beck–Fiala, Bansal–Jiang 2025) et sa formalisation Lean 4 (conjecture de Komlós), sélection empirique d'algorithme, descente gloutonne sous plafond d'évaluations (loi `Descent.lean`) |
 | **Part 2 — Programmation par Contraintes** (`Part2-CSP/`) | **18** (9 Python : CSP-1 → CSP-9 + **9 jumeaux C#**, marathon #4956 achevé) | Python + .NET (C#) | CSP Fundamentals (backtracking), AC-3/FC/MAC, CSP Advanced (AllDifferent/Cumulative/Circuit), Scheduling (Job-Shop/RCPSP/Nurse), Optimization (Bin Packing/Knapsack), Hybridization (LCG/CP+SAT/CP+ML/LLM+CSP), Soft, Temporal (Allen's Interval Algebra), Distributed (Yokoo 1992) |
-| **Part 4 — Métaheuristiques composables** (`Part4-Metaheuristics/`, C# .NET 9, MetaGeneticSharp) | **35** (MGS-1 → MGS-31 : cœur MGS-1..19, **trilogie MGS-7b/7c/7d** de projection N-D des paysages, MGS-17b sélection empirique, **MGS-21** représentation vs algorithme ; le **volet comparatif vs MEALPY** (10 notebooks MGS-22..31) vit dans la sous-série [`Part4-Metaheuristics/MGS-vs-mealpy/`](Part4-Metaheuristics/MGS-vs-mealpy/README.md) — duels PSO/DE/SA/WOA/EO/FBI/BBPSO/GA/ScatterSearch vs Mealpy + synthèse croisée ; tous C# .NET au-dessus de GeneticSharp vendored) | C# / .NET | Composition, Eukaryote, Islands, Compound Metaheuristics, TSP, projection N-D des paysages, Landscape Explorer, Center Bias, Island Synergy, Axis Alignment, Landscape Debias, Island Synergy Found, Landscape Analysis (FDC), Algorithm Selection (No-Free-Lunch), Parameter Control, CEC Banc, Metropolis Reinsertion, représentation vs algorithme, [campagne comparative MGS vs mealpy](Part4-Metaheuristics/MGS-vs-mealpy/README.md) |
+| **Part 4 — Métaheuristiques composables** (`Part4-Metaheuristics/`, C# .NET 9, MetaGeneticSharp) | **35** (MGS-1 → MGS-31 : cœur MGS-1..19, **trilogie MGS-7b/7c/7d** de projection N-D des paysages, MGS-17b sélection empirique, **MGS-21** représentation vs algorithme ; le **volet comparatif vs MEALPY** (MGS-22..31) vit dans la sous-série [`Part4-Metaheuristics/MGS-vs-mealpy/`](Part4-Metaheuristics/MGS-vs-mealpy/README.md) — duels PSO/DE/SA/WOA/EO/FBI/BBPSO/GA/ScatterSearch vs Mealpy + synthèse croisée ; tous C# .NET au-dessus de GeneticSharp vendored) | C# / .NET | Composition, Eukaryote, Islands, Compound Metaheuristics, TSP, projection N-D des paysages, Landscape Explorer, Center Bias, Island Synergy, Axis Alignment, Landscape Debias, Island Synergy Found, Landscape Analysis (FDC), Algorithm Selection (No-Free-Lunch), Parameter Control, CEC Banc, Metropolis Reinsertion, représentation vs algorithme, [campagne comparative MGS vs mealpy](Part4-Metaheuristics/MGS-vs-mealpy/README.md) |
 | **Partie 3 — Cas pratiques** (`Part3-Cas-pratiques/`) | **57** (37 Python + 20 C# — **20 binômes Python ⇄ C#** App-1 à App-20, plus compagnons statistical-validity, jumeaux Python et notebooks d'audit App-23 à App-31) | 37 Python + 20 C# | N-Queens, Graph Coloring, Nurse/Job-Shop/Timetabling Scheduling, Minesweeper, Wordle, MiniZinc, Picross (speedup mesuré 17.4x sur 10x10), Sports/Crossword/WFC CSP, SudokuBenchmark, Portfolio/TSP/VRP/Hyperparameter Tuning, Edge Detection, ConnectFour (Minimax/MCTS), Covering Arrays, Algorithm Selection |
 | **_archive** (`_archive/`) | **2** (CSPs_Intro, Exploration_non_informée_et_informée_intro, historiques pré-tranche 8/8 #5081) | Python | Notebooks historiques, remplacés par Part2-CSP/CSP-1-Fundamentals et Part1-Foundations/Search-{2,3} |
 | **Total** | **153** (43 + 18 + 35 + 57 = 153 pédagogiques, Search-09d inclus + 2 archive = 155) | Python + Lean 4 + C# | 4 piliers + archive, voir « Structure des fichiers » pour l'arborescence complète |

MyIA.AI.Notebooks/Search/search_lean/README.md

@@ -157,7 +157,7 @@ consistante : la frontière de `f` ne recule jamais, donc **aucun nœud n'est ja
 ré-expansé** — par contraste avec une heuristique admissible (mais non consistante) qui
 garantit l'optimalité (phase 1) mais autorise des ré-expansions.
 
-**Preuve** (0 `sorry`, axiomes `[propext, Classical.choice, Quot.sound]`, 1 ligne) :
+**Preuve** (0 `sorry`, axiomes `[propext, Classical.choice, Quot.sound]`) :
 `g n' + h n' = g n + edge n n' + h n' ≥ g n + h n` par consistance
 (`h n ≤ edge n n' + h n'`), donc `linarith` après réécriture de `g n'`.