myia-ai-01 · Oct 2, 2026 · Oct 1, 2026 · Oct 1, 2026 · Oct 1, 2026 · Oct 1, 2026
diff --git a/MyIA.AI.Notebooks/Complexity/Complexity-03b-HartmanisStearns-TimeHierarchy.ipynb b/MyIA.AI.Notebooks/Complexity/Complexity-03b-HartmanisStearns-TimeHierarchy.ipynb
@@ -1131,7 +1131,7 @@
     "  contrôle des armements. Ce travail devint un chapitre du livre d'Aumann et Maschler (1995,\n",
     "  prix Lanchester), dont la page de titre porte *« with the collaboration of Richard E.\n",
     "  Stearns »* ; il appelait l'épisode *« the story of how I almost won the Lanchester\n",
-    "  Prize »*. Le dépôt possède [`repeated_games_lean`](../GameTheory/repeated_games_lean/)\n",
+    "  Prize »*. Le dépôt possède [`game_theory_lean/RepeatedGames`](../GameTheory/game_theory_lean/RepeatedGames/)\n",
     "  (lake complet) et l'écho coopératif dans\n",
     "  [ICT-13 — Axelrod](../IIT/ICT-Series/ICT-13-AxelrodStrategicMorphodynamics.ipynb).\n",
     "\n",

diff --git a/MyIA.AI.Notebooks/GameTheory/GameTheory-06b-Lean-RepeatedGames-Lean-Python.ipynb b/MyIA.AI.Notebooks/GameTheory/GameTheory-06b-Lean-RepeatedGames-Lean-Python.ipynb
@@ -48,7 +48,7 @@
     "théorie du 6c. Aucune cellule ne « recopie » une preuve : le fichier Lean **est** la\n",
     "source formelle ; ici on apprend où elle vit et ce qu'elle dit exactement.\n",
     "\n",
-    "**Repère d'orientation** : si vous explorez le disque, le répertoire `repeated_games_lean/` du dossier GameTheory est une **coquille archive** — depuis la PR #6146 (EPIC #4365 Phase-4), les quatre modules sources (`Stage`, `Discounting`, `GrimTrigger`, `Folk`) sont absorbés byte-identique dans `game_theory_lean/RepeatedGames/`, home canonique (`@[default_target]` du lakefile de `game_theory_lean`). C'est ce home canonique que ce notebook lit."
+    "**Repère d'orientation** : si vous explorez le disque, le répertoire `repeated_games_lean/` du dossier GameTheory a été retiré du disque (coquille archive, #4362) — depuis la PR #6146 (EPIC #4365 Phase-4), les quatre modules sources (`Stage`, `Discounting`, `GrimTrigger`, `Folk`) sont absorbés byte-identique dans `game_theory_lean/RepeatedGames/`, home canonique (`@[default_target]` du lakefile de `game_theory_lean`). C'est ce home canonique que ce notebook lit."
    ]
   },
   {

diff --git a/MyIA.AI.Notebooks/GameTheory/GameTheory-06c-RepeatedGames-FolkTheorem-CSharp.ipynb b/MyIA.AI.Notebooks/GameTheory/GameTheory-06c-RepeatedGames-FolkTheorem-CSharp.ipynb
@@ -1954,7 +1954,7 @@
     "\n",
     "- [GameTheory-06-EvolutionTrust-Python (C#)](GameTheory-06-EvolutionTrust-CSharp.ipynb) : l'évolution de la confiance dans les jeux répétés simulés.\n",
     "- [GameTheory-07-ExtensiveForm-Python (C#)](GameTheory-07-ExtensiveForm-CSharp.ipynb) : forme extensive et sous-game-perfection.\n",
-    "- Le port Lean ([`game_theory_lean/RepeatedGames/`](game_theory_lean/RepeatedGames/), lake bilingue FR/EN, home canonique depuis #6146, l'ancien standalone `repeated_games_lean/` est une coquille archive) formalise ces résultats dans le calcul des constructions inductives.\n",
+    "- Le port Lean ([`game_theory_lean/RepeatedGames/`](game_theory_lean/RepeatedGames/), lake bilingue FR/EN, home canonique depuis #6146, l'ancien standalone `repeated_games_lean/` a été retiré du disque) formalise ces résultats dans le calcul des constructions inductives.\n",
     "\n",
     "***\n",
     "\n",

diff --git a/MyIA.AI.Notebooks/GameTheory/LEAN_INVENTORY.md b/MyIA.AI.Notebooks/GameTheory/LEAN_INVENTORY.md
@@ -28,7 +28,7 @@ module-set réel du disque (issue #13138). Ligne `conway_cgt_lean` re-synchronis
 |-----------|---------|
 | ~~`cooperative_games_lean`~~ | **Supprimé** (rm #6587) → [`game_theory_lean/CooperativeGames/`](game_theory_lean/CooperativeGames/) |
 | ~~`social_choice_lean`~~ | Absorbé (#6058, 2026-07-11) → [`game_theory_lean/SocialChoice/`](game_theory_lean/SocialChoice/) — ne subsistent que 4 markdown tombstone |
-| ~~`repeated_games_lean`~~ | Absorbé (#6146) → [`game_theory_lean/RepeatedGames/`](game_theory_lean/RepeatedGames/) — coquille archive conservée (lakefile neutralisé) |
+| ~~`repeated_games_lean`~~ | Absorbé (#6146) → [`game_theory_lean/RepeatedGames/`](game_theory_lean/RepeatedGames/) — coquille retirée du disque (#4362) |
 
 Note : `SymbolicAI/Lean/examples/llm_assisted_proof.lean` (2 sorry) est un exemple pédagogique, pas du code de production. `asymmetric_information_lean` porte 2 *naive* sorry (prose/docstrings) pour 0 vrai sorry de code.
 
@@ -276,8 +276,8 @@ Folk (`folk_theorem_discounted`) porte 1 sorry stretch, toléré au titre de #48
 |---------|----------|-----------|
 | game_theory_lean | COMPLET | 1 sorry (stretch Folk, toléré #4880). StableMarriage : anciens énoncés faux réfutés, `exists_isManOptimal` honnête prouvé ; Lattice fermé. A absorbé `stable_marriage_lean/` + `cooperative_games_lean/` + `social_choice_lean/` + `repeated_games_lean/` (EPIC #4365). |
 | ~~cooperative_games_lean~~ | **Supprimé** (rm #6587) | Absorbé byte-identique dans `game_theory_lean/CooperativeGames/`. |
-| ~~social_choice_lean~~ | **Absorbé** (#6058) | 7 modules → `game_theory_lean/SocialChoice/` ; docs tombstone uniquement. |
-| ~~repeated_games_lean~~ | **Absorbé** (#6146) | 4 modules → `game_theory_lean/RepeatedGames/` ; coquille archive. |
+| ~~social_choice_lean~~ | **Absorbé** (#6058) | → `game_theory_lean/SocialChoice/` ; docs tombstone uniquement. |
+| ~~repeated_games_lean~~ | **Absorbé** (#6146) | → `game_theory_lean/RepeatedGames/` ; coquille retirée du disque (#4362). |
 | lean_game_defs / _ext | COMPLET | 0 sorry, sans Mathlib. |
 | minimax_lean | COMPLET | 0 sorry ; application de Sion prouvée. |
 | assignment_lean | COMPLET | 0 sorry (#12598). |

diff --git a/MyIA.AI.Notebooks/GameTheory/README.md b/MyIA.AI.Notebooks/GameTheory/README.md
@@ -562,7 +562,7 @@ La série aligne simulation numérique et preuve formelle : les notebooks motive
 | `asymmetric_information_lean` | Akerlof (seuil de pooling exact), Spence, Rothschild-Stiglitz, Wilson-Miyazaki | 17b, 17c, 17d |
 | `social_choice_lean_peters` | Lake de référence externe (D. Peters, MIT) : Gibbard-Satterthwaite, Split Cycle et d'autres règles | SocialChoice 01b, 07 |
 
-Les anciens lakes autonomes du choix social, des jeux coopératifs, du mariage stable et des jeux répétés ont été absorbés dans `game_theory_lean` (#4365) ; `social_choice_lean/` et `repeated_games_lean/` ne restent que comme coquilles documentaires. Au niveau du dépôt, voir le [hub SymbolicAI/Lean](../SymbolicAI/Lean/README.md) et la feuille de route Lean ([#4038](https://github.com/jsboige/CoursIA/issues/4038)).
+Les anciens lakes autonomes du choix social, des jeux coopératifs, du mariage stable et des jeux répétés ont été absorbés dans `game_theory_lean` (#4365). `repeated_games_lean/` a été retirée du disque (coquille sans module, #4362) ; `social_choice_lean/` ne reste que comme coquille documentaire. Au niveau du dépôt, voir le [hub SymbolicAI/Lean](../SymbolicAI/Lean/README.md) et la feuille de route Lean ([#4038](https://github.com/jsboige/CoursIA/issues/4038)).
 
 ### Liens avec les autres séries
 
@@ -591,7 +591,7 @@ GameTheory/
 ├── game_theory_lean/              # lake multi-module (voir Formalisations Lean)
 ├── minimax_lean/  assignment_lean/  asymmetric_information_lean/  conway_cgt_lean/
 ├── lean_game_defs/  lean_game_defs_ext/  social_choice_lean_peters/
-├── repeated_games_lean/  social_choice_lean/     # coquilles documentaires (absorbées)
+├── social_choice_lean/                          # coquille documentaire (absorbée)
 ├── LEAN_INVENTORY.md              # inventaire des lakes
 ├── install_wsl_kernel.md          # installation des kernels WSL
 └── requirements.txt

diff --git a/MyIA.AI.Notebooks/GameTheory/SocialChoice/01-Arrow-Impossibility-Theorem-Csharp.ipynb b/MyIA.AI.Notebooks/GameTheory/SocialChoice/01-Arrow-Impossibility-Theorem-Csharp.ipynb
@@ -54,7 +54,7 @@
     ">\n",
     "> Richard E. Stearns (1936–2026), co-lauréat du prix Turing 1993 pour avoir fondé la théorie de la complexité computationnelle (Hartmanis & Stearns, 1965), a **commencé par le théorème d'Arrow** : son tout premier article, écrit comme étudiant de dernière année à Carleton College, portait sur le paradoxe d'Arrow et a été publié dans *The American Mathematical Monthly* en 1959. Sa thèse de Princeton, dirigée par Harold W. Kuhn (co-éponyme de l'algorithme Kuhn–Munkres, célébré dans cette même série GameTheory), portait sur les jeux coopératifs à trois joueurs sans paiements transférables.\n",
     ">\n",
-    "> L'homme qui a donné son nom à la complexité a donc commencé par l'impossibilité de l'agrégation — le théorème que ce notebook démontre. Autre résonance inattendue : ses travaux sur les jeux répétés à information incomplète (contrôle des armements, chapitre du livre d'Aumann & Maschler 1995), racontés dans le README de [`repeated_games_lean/`](../repeated_games_lean/README.md). Hommage complet — hiérarchie de Hartmanis–Stearns, série `Complexity/` : issue [#15949](https://github.com/jsboige/CoursIA/issues/15949).\n",
+    "> L'homme qui a donné son nom à la complexité a donc commencé par l'impossibilité de l'agrégation — le théorème que ce notebook démontre. Autre résonance inattendue : ses travaux sur les jeux répétés à information incomplète (contrôle des armements, chapitre du livre d'Aumann & Maschler 1995), racontés dans le README de [`game_theory_lean/`](../game_theory_lean/README.md). Hommage complet — hiérarchie de Hartmanis–Stearns, série `Complexity/` : issue [#15949](https://github.com/jsboige/CoursIA/issues/15949).\n",
     ">\n",
     "> *Sources : [CACM, In Memoriam Richard E. Stearns](https://cacm.acm.org/news/in-memoriam-richard-e-stearns-1936-2026/) (Spafford & Garfinkel, 03/09/2026) ; [blog Computational Complexity](https://blog.computationalcomplexity.org/2026/09/richard-stearns-1936-2026.html) (Gasarch, 04/09/2026) ; [transcript du prix Turing ACM](https://amturing.acm.org/pdf/StearnsTuringTranscript.pdf).*"
    ]

diff --git a/MyIA.AI.Notebooks/GameTheory/SocialChoice/01-Arrow-Impossibility-Theorem.ipynb b/MyIA.AI.Notebooks/GameTheory/SocialChoice/01-Arrow-Impossibility-Theorem.ipynb
@@ -82,7 +82,7 @@
     ">\n",
     "> Richard E. Stearns (1936–2026), co-lauréat du prix Turing 1993 pour avoir fondé la théorie de la complexité computationnelle (Hartmanis & Stearns, 1965), a **commencé par le théorème d'Arrow** : son tout premier article, écrit comme étudiant de dernière année à Carleton College, portait sur le paradoxe d'Arrow et a été publié dans *The American Mathematical Monthly* en 1959. Sa thèse de Princeton, dirigée par Harold W. Kuhn (co-éponyme de l'algorithme Kuhn–Munkres, célébré dans cette même série GameTheory), portait sur les jeux coopératifs à trois joueurs sans paiements transférables.\n",
     ">\n",
-    "> L'homme qui a donné son nom à la complexité a donc commencé par l'impossibilité de l'agrégation — le théorème que ce notebook démontre. Autre résonance inattendue : ses travaux sur les jeux répétés à information incomplète (contrôle des armements, chapitre du livre d'Aumann & Maschler 1995), racontés dans le README de [`repeated_games_lean/`](../repeated_games_lean/README.md). Hommage complet — hiérarchie de Hartmanis–Stearns, série `Complexity/` : issue [#15949](https://github.com/jsboige/CoursIA/issues/15949).\n",
+    "> L'homme qui a donné son nom à la complexité a donc commencé par l'impossibilité de l'agrégation — le théorème que ce notebook démontre. Autre résonance inattendue : ses travaux sur les jeux répétés à information incomplète (contrôle des armements, chapitre du livre d'Aumann & Maschler 1995), racontés dans le README de [`game_theory_lean/`](../game_theory_lean/README.md). Hommage complet — hiérarchie de Hartmanis–Stearns, série `Complexity/` : issue [#15949](https://github.com/jsboige/CoursIA/issues/15949).\n",
     ">\n",
     "> *Sources : [CACM, In Memoriam Richard E. Stearns](https://cacm.acm.org/news/in-memoriam-richard-e-stearns-1936-2026/) (Spafford & Garfinkel, 03/09/2026) ; [blog Computational Complexity](https://blog.computationalcomplexity.org/2026/09/richard-stearns-1936-2026.html) (Gasarch, 04/09/2026) ; [transcript du prix Turing ACM](https://amturing.acm.org/pdf/StearnsTuringTranscript.pdf).*"
    ]

diff --git a/MyIA.AI.Notebooks/GameTheory/repeated_games_lean/README.en.md b/MyIA.AI.Notebooks/GameTheory/repeated_games_lean/README.en.md