fix(gametheory,#15615): reparer la couche de renvois cassee par la renum #15586

MyIA.AI.Notebooks/GameTheory/GameTheory-02b-Lean-Definitions.ipynb

@@ -51,7 +51,7 @@
     "\n",
     "### Prerequis\n",
     "\n",
-    "- Avoir complete les notebooks Python 1-4 (concepts de base)\n",
+    "- Avoir complete les notebooks Python 01-02 (concepts de base)\n",
     "- Notions de base en Lean 4 (serie SymbolicAI/Lean recommandee)\n",
     "- Kernel Lean 4 (WSL) installe (voir `scripts/README.md`)\n",
     "\n",
@@ -4752,7 +4752,7 @@
     "\n",
     "***\n",
     "\n",
-    "**Navigation** : [<- GameTheory-17-MultiAgent-RL](GameTheory-17-MultiAgent-RL.ipynb) | [Index](GameTheory-01-Setup.ipynb) | [GameTheory-04b-Lean-NashExistence ->](GameTheory-04b-Lean-NashExistence.ipynb)"
+    "**Navigation** : [<- GameTheory-02-NormalForm (palier parent)](GameTheory-02-NormalForm.ipynb) | [Index](README.md) | [GameTheory-04b-Lean-NashExistence ->](GameTheory-04b-Lean-NashExistence.ipynb)"
    ]
   },
   {

MyIA.AI.Notebooks/GameTheory/GameTheory-03a-Chemins-de-Swaps.ipynb

@@ -23,7 +23,7 @@
     "1. **Le générateur propose** — un parcours en largeur (BFS) explore l'espace niveau par niveau et produit un plus court chemin candidat.\n",
     "2. **Le certificat garantit** — un module compagnon en Lean (`game_theory_lean/Swaps/Basic.lean`, écrit pour ce grain) certifie qu'un chemin proposé est bien formé et mène bien de l'arrivée au départ ; sur le cas témoin Dilemme → Chicken, il certifie aussi qu'aucun chemin plus court n'existe. Le générateur Python et le vérificateur Lean restent deux artefacts distincts,chacun à sa place.\n",
     "\n",
-    "**Prérequis** : GameTheory-3 (générateurs $R_{12}/R_{23}/R_{34}/C_{12}/C_{23}/C_{34}$), GameTheory-3b (codimension, murs, facettes), GameTheory-21 (deux espèces de flèches). Toutes les mesures de ce notebook sont calculées sur l'espace complet des 576 jeux stricts — le quotient par renommage des stratégies (144 classes) est une dette rapportée, jamais affirmée ici."
+    "**Prérequis** : GameTheory-3 (générateurs $R_{12}/R_{23}/R_{34}/C_{12}/C_{23}/C_{34}$), GameTheory-3b (codimension, murs, facettes), GameTheory-03h (deux espèces de flèches). Toutes les mesures de ce notebook sont calculées sur l'espace complet des 576 jeux stricts — le quotient par renommage des stratégies (144 classes) est une dette rapportée, jamais affirmée ici."
    ]
   },
   {
@@ -641,7 +641,7 @@
    "source": [
     "### Interprétation : le théorème établi par énumération\n",
     "\n",
-    "**La décomposition vaut pour chacune des 331 776 paires.** Comme le théorème de la condition de transformation dans GT-21 (vérifié sur les 3 456 paires jeu-générateur), l'énoncé est ici *établi par énumération exhaustive* : l'espace est fini, la vérification est complète, et le résultat se lit sur la sortie. La preuve conceptuelle — indépendance des deux côtés, graphe de Cayley de $S_4$, produit cartésien — est **rapportée en dette** (§Sources) : nous n'en livrons pas la démonstration générale, seulement l'évidence exhaustive sur cet espace.\n",
+    "**La décomposition vaut pour chacune des 331 776 paires.** Comme le théorème de la condition de transformation dans GT-3h (vérifié sur les 3 456 paires jeu-générateur), l'énoncé est ici *établi par énumération exhaustive* : l'espace est fini, la vérification est complète, et le résultat se lit sur la sortie. La preuve conceptuelle — indépendance des deux côtés, graphe de Cayley de $S_4$, produit cartésien — est **rapportée en dette** (§Sources) : nous n'en livrons pas la démonstration générale, seulement l'évidence exhaustive sur cet espace.\n",
     "\n",
     "Trois corollaires immédiats, tous mesurés :\n",
     "\n",
@@ -1226,7 +1226,7 @@
     "\n",
     "**Module compagnon** : `game_theory_lean/Swaps/Basic.lean` (ce grain) — pur core Lean, sans Mathlib, sans `sorry` ; `lake build Swaps` sans dépendance.\n",
     "\n",
-    "**Encodages** : identiques à GameTheory-3 et GT-21 (tables de rangs 1-4, cellules dans l'ordre haut-gauche, haut-droit, bas-gauche, bas-droit)."
+    "**Encodages** : identiques à GameTheory-3 et GT-3h (tables de rangs 1-4, cellules dans l'ordre haut-gauche, haut-droit, bas-gauche, bas-droit)."
    ]
   }
  ],

MyIA.AI.Notebooks/GameTheory/GameTheory-03g-Derivation-Quotient.ipynb

@@ -27,7 +27,7 @@
     "\n",
     "Et il établit honnêtement la frontière : **aucune** des notions naturelles testées ici (classes de meilleures réponses, signatures d'équilibres, orbites, arêtes) ne produit 37. La dérivation du tore exige la construction du livre (un complexe de dimension 2, pas un simple comptage) : ce point précis reste une dette ouverte, documentée en section 6.\n",
     "\n",
-    "**Prérequis** : GameTheory-03 (l'univers des 576), GameTheory-03a (les swaps comme générateurs). Voir aussi GameTheory-21 pour le versant morphismes."
+    "**Prérequis** : GameTheory-03 (l'univers des 576), GameTheory-03a (les swaps comme générateurs). Voir aussi GameTheory-03h pour le versant morphismes."
    ]
   },
   {
@@ -872,7 +872,7 @@
     "- Robinson, D. & Goforth, D. (2005). *The Topology of the 2×2 Games*. Routledge — source du 144 et du tore ; le 144 est ici **dérivé**, le tore reste **rapporté**.\n",
     "- Rapoport, A. & Guyer, M. (1966). A taxonomy of 2x2 games. *General Systems* 11 — le 78 historique, retrouvé par le calcul (section 4).\n",
     "- EPIC #12207, section 3 (dettes de vérification) — le présent notebook paie les items dérivables sans le texte source et délimite le reste.\n",
-    "- Les swaps adjacents comme générateurs : GameTheory-03a ; le versant morphismes : GameTheory-21 ; les murs et chambres : GameTheory-03b."
+    "- Les swaps adjacents comme générateurs : GameTheory-03a ; le versant morphismes : GameTheory-03h ; les murs et chambres : GameTheory-03b."
    ]
   }
  ],

MyIA.AI.Notebooks/GameTheory/GameTheory-04b-Lean-NashExistence.ipynb

@@ -24,7 +24,7 @@
     "\n",
     "**Kernel** : Lean 4 (WSL)\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "## Introduction\n",
     "\n",
@@ -43,13 +43,13 @@
     "\n",
     "### Prerequis\n",
     "\n",
-    "- Avoir complète le notebook 17 (définitions de base)\n",
+    "- Avoir complète le notebook GameTheory-02b-Lean-Definitions (définitions de base)\n",
     "- Notions de topologie (continuite, compacite, convexite)\n",
     "- Familiarite avec les tactiques Lean\n",
     "\n",
     "### Duree estimee : 55 minutes\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "## Plan de ce Notebook\n",
     "\n",
@@ -431,7 +431,7 @@
     "\n",
     "**L'importance de la convexite** : La convexite du simplexe est l'une des trois hypotheses fondamentales du theoreme de Brouwer (compact, convexe, non vide). Sans convexite, le theoreme ne s'applique pas et l'existence de Nash n'est pas garantie.\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "<a id=\"2-brouwer\"></a>\n",
     "## 2. Theoreme du Point Fixe de Brouwer\n",
@@ -742,12 +742,12 @@
     "\n",
     "L'axiome `brouwer_product` affirme que toute fonction continue du produit vers lui-même admet un point fixe. C'est ce résultat qui sera applique a la fonction de meilleure reponse perturbee pour prouver l'existence de Nash.\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "<a id=\"3-définitions\"></a>\n",
     "## 3. Definitions de Jeu\n",
     "\n",
-    "Rappel des définitions du notebook 17, adaptees pour la preuve d'existence. Nous définissons succèssivement :\n",
+    "Rappel des définitions du notebook GameTheory-02b-Lean-Definitions, adaptees pour la preuve d'existence. Nous définissons succèssivement :\n",
     "- La structure de jeu fini (`FiniteGame`)\n",
     "- Les profils de stratégies mixtes (`MixedProfile`, `MixedProfileSimple`)\n",
     "- Le gain espere (`expectedPayoff2x2`)\n",
@@ -1587,7 +1587,7 @@
     "\n",
     "Cette fonction est la brique de base pour définir l'équilibre de Nash : un profil est Nash si aucun joueur ne peut améliorér son gain espere par deviation unilaterale.\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "<a id=\"4-nash\"></a>\n",
     "## 4. Meilleure Reponse et Equilibre de Nash\n",
@@ -2397,7 +2397,7 @@
     "\n",
     "> **Note** : Dans cette cellule, `perturbedBR` renvoie $\\sigma$ (placeholder). L'implementation complète calcule le regret pour chaque action et realloue les probabilités en consequence.\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "<a id=\"5-structure\"></a>\n",
     "## 5. Structure de la Preuve d'Existence\n",
@@ -3416,7 +3416,7 @@
     "\n",
     "Chaque correction utilise le pattern classique : **unfold** pour deployer les définitions, **have** pour les résultats intermediaires, **exact** pour conclure.\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "### Correction Exemple guide 1"
    ]
@@ -3628,7 +3628,7 @@
     "\n",
     "> **Note sur les axiomes** : Les trois axiomes `float_nonneg_mul`, `float_nonneg_add` et `float_one_sub_nonneg` sont des proprietes **vraies sur les réels** mais non decidables sur `Float` en Lean 4. Dans une formalisation complète avec Mathlib, ces résultats decouleraient de l'arithmetique sur `Real`.\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "### Correction Exemple guide 2"
    ]
@@ -3834,7 +3834,7 @@
     "\n",
     "> **Note technique** : L'axiome `float_pennies_sum_zero` est nécessaire car Lean 4 ne peut pas reduire automatiquement les expressions arithmetiques sur `Float`. Sur les réels formels (`Rat` ou `Real` de Mathlib), `ring` ou `omega` resoudraient ce calcul.\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "### Correction Exemple guide 3"
    ]
@@ -4010,7 +4010,7 @@
     "\n",
     "C'est précisément parce que les simplexes sont **compacts** (fermes et bornes dans $\\mathbb{R}^n$) que Brouwer s'applique, garantissant l'existence d'un équilibre de Nash.\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "<a id=\"8-resume\"></a>\n",
     "## 8. Resume\n",
@@ -4047,7 +4047,7 @@
     "- [harfe/fixed-point-theorems-lean4](https://github.com/harfe/fixed-point-theorems-lean4) - Brouwer + Kakutani\n",
     "- Companion Python : [GameTheory-04c-NashExistence-Python](GameTheory-04c-NashExistence-Python.ipynb) pour illustrations numériques\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "**Navigation** : [<< 4-NashEquilibrium (track principal)](GameTheory-04-NashEquilibrium.ipynb) | [Index](README.md) | [4c-NashExistence-Python >>](GameTheory-04c-NashExistence-Python.ipynb)"
    ]

MyIA.AI.Notebooks/GameTheory/GameTheory-19-Abstraction-a-Dette.ipynb

@@ -7,7 +7,7 @@
    "source": [
     "# GameTheory-19 : L'abstraction a dette mesurable\n",
     "\n",
-    "**Navigation** : [<< 17-MultiAgent-RL](GameTheory-17-MultiAgent-RL.ipynb) | [Index](README.md) | [03h-Deux-Especes-de-Fleches >>](GameTheory-03h-Deux-Especes-de-Fleches.ipynb)\n",
+    "**Navigation** : [<< 18b-Casser-la-Composition](GameTheory-18b-Casser-la-Composition.ipynb) | [Index](README.md) | [20-Chemin-Minimal-Robinson-Goforth >>](GameTheory-20-Chemin-Minimal-Robinson-Goforth.ipynb)\n",
     "\n",
     "## Le retournement\n",
     "\n",

MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb

@@ -14,11 +14,11 @@
     "tags": []
    },
    "source": [
-    "# GameTheory 27b — Le lake `assignment_lean` par son certificat (compagnon natif)\n",
+    "# GameTheory 23b — Le lake `assignment_lean` par son certificat (compagnon natif)\n",
     "\n",
     "**Navigation** : [<< 27-Munkres-Assignment (track principal)](GameTheory-23-Munkres-Assignment.ipynb) | [Index](README.md) | [`assignment_lean/`](assignment_lean/)\n",
     "\n",
-    "**Autruche pédagogique** : le notebook [GT-23](GameTheory-23-Munkres-Assignment.ipynb) *implémente* la méthode hongroise en Python (labels, arbre hongrois, `scipy.optimize.linear_sum_assignment`) et vérifie son triple test **numériquement**. Ce compagnon 27b exécute le **lake Lean `assignment_lean`** sous kernel natif `lean4-wsl` : les mêmes énoncés — dualité faible, certificat à gap nul, invariant de sortie, resserrement hongrois — deviennent des théorèmes **prouvés par le noyau**, et nous terminons sur une preuve complète qu'une affectation concrète 3×3 est optimale, sans énumérer les factorielles.\n",
+    "**Autruche pédagogique** : le notebook [GT-23](GameTheory-23-Munkres-Assignment.ipynb) *implémente* la méthode hongroise en Python (labels, arbre hongrois, `scipy.optimize.linear_sum_assignment`) et vérifie son triple test **numériquement**. Ce compagnon 23b exécute le **lake Lean `assignment_lean`** sous kernel natif `lean4-wsl` : les mêmes énoncés — dualité faible, certificat à gap nul, invariant de sortie, resserrement hongrois — deviennent des théorèmes **prouvés par le noyau**, et nous terminons sur une preuve complète qu'une affectation concrète 3×3 est optimale, sans énumérer les factorielles.\n",
     "\n",
     "Hommage : James R. Munkres (1930–2026), co-éponyme de l'algorithme de Kuhn-Munkres (Kuhn 1955 ; Munkres 1957) — le récit historique est dans le [GT-23](GameTheory-23-Munkres-Assignment.ipynb)."
    ]
@@ -1811,7 +1811,7 @@
     "***\n",
     "## Conclusion\n",
     "\n",
-    "Le lake `assignment_lean` donne au triple test de GT-23 son statut logique complet : la **dualité faible** fixe le plancher, le **gap nul** le certificat, l'**invariant de sortie** la garantie de terminaison correcte, le **resserrement** la sûreté de chaque étape. Là où `scipy.optimize.linear_sum_assignment` rend une affectation, le lake rend une **preuve vérifiée par le noyau** — et le compagnon 27b est le lieu où ces preuves s'exécutent et se lisent.\n",
+    "Le lake `assignment_lean` donne au triple test de GT-23 son statut logique complet : la **dualité faible** fixe le plancher, le **gap nul** le certificat, l'**invariant de sortie** la garantie de terminaison correcte, le **resserrement** la sûreté de chaque étape. Là où `scipy.optimize.linear_sum_assignment` rend une affectation, le lake rend une **preuve vérifiée par le noyau** — et le compagnon 23b est le lieu où ces preuves s'exécutent et se lisent.\n",
     "\n",
     "Ce qui reste délibérément hors scope du lake (cf son README) : la preuve de **terminaison** et la complexité $O(n^3)$ (Edmonds-Karp/Tomizawa), et le pont **Shapley-Shubik** (cœur du jeu d'affectation = solutions duales optimales), traité numériquement dans GT-23 section 5.\n",
     "\n",

MyIA.AI.Notebooks/GameTheory/index.qmd

@@ -4,22 +4,22 @@ subtitle: "Série pédagogique niveau 2 — Nash, Lemke-Howson, Folk, Shapley, A
 description: "Série GameTheory du dépôt CoursIA — équilibre de Nash, théorème minimax, dynamiques d'apprentissage, jeux coopératifs (Shapley, Core), mécanismes (VCG, Gale-Shapley), choix social (Arrow), formalisation Lean 4."
 listing:
   - id: phase1
-    contents: "GameTheory-1-Setup.ipynb"
+    contents: "GameTheory-01-Setup.ipynb"
     type: grid
     sort: "filename"
     page-size: 24
   - id: phase1-notebooks
-    contents: "GameTheory-[2-6]-*.ipynb"
+    contents: "GameTheory-0[2-6]-*.ipynb"
     type: grid
     sort: "filename"
     page-size: 24
   - id: phase2
-    contents: "GameTheory-7-*.ipynb"
+    contents: "GameTheory-07-*.ipynb"
     type: grid
     sort: "filename"
     page-size: 24
   - id: phase2-notebooks
-    contents: "GameTheory-[89]-*.ipynb"
+    contents: "GameTheory-0[89]-*.ipynb"
     type: grid
     sort: "filename"
     page-size: 24
@@ -48,7 +48,7 @@ listing:
 
 ## Vue d'ensemble
 
-La série GameTheory comporte **27 notebooks racine + 4 SocialChoice** répartis en **3 phases** thématiques et une **sous-série SocialChoice** dédiée. Chaque notebook principal (Python/.NET) est exécuté et commité avec ses sorties (règle C.2). Les side tracks Lean 4 (`*-Lean-*`) requièrent WSL + elan ; les side tracks Python (`*-Python`) ajoutent des approfondissements.
+La série GameTheory comporte **96 notebooks racine + 8 SocialChoice** répartis en **3 phases** thématiques et une **sous-série SocialChoice** dédiée. Chaque notebook principal (Python/.NET) est exécuté et commité avec ses sorties (règle C.2). Les side tracks Lean 4 (`*-Lean-*`) requièrent WSL + elan ; les side tracks Python (`*-Python`) ajoutent des approfondissements.
 
 | Phase | Notebooks | Focus pédagogique |
 |-------|-----------|-------------------|