diff --git a/MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk_en.lean b/MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk_en.lean
index 78ddb2de9e6..06227c2fc2e 100644
--- a/MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk_en.lean
+++ b/MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk_en.lean
@@ -24,11 +24,12 @@ import Mathlib.Topology.Basic
   EN historique pré-Option A à recover, fichier FR-first depuis origin).
 
   Namespace sibling : `RepeatedGames_en` (the FR canonical stays
-  `RepeatedGames`). Shared types `PrisonersDilemma`, `PDAction` (defined in
-  `Stage.lean` under `namespace RepeatedGames`) are re-exposed via
-  `open RepeatedGames` so the EN sibling resolves them as FR `GrimTrigger_en`
-  does. Field projections `g.P`/`g.R`/`g.S`/`g.T` are structure-field access
-  (not namespace dot-notation), hence safe under the open.
+  `RepeatedGames`). Shared types `PrisonersDilemma`, `PDAction` are defined
+  in `Stage_en.lean` under `namespace RepeatedGames_en` and consumed via
+  `import RepeatedGames.Stage_en`; every higher-level EN sibling of this
+  series resolves them through `open RepeatedGames_en`. Field
+  projections `g.P`/`g.R`/`g.S`/`g.T` are structure-field access
+  (not namespace dot-notation), hence unaffected by the open.
 
   See #4980. Part of #4208 (axe E).
 -/
diff --git a/MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Stage_en.lean b/MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Stage_en.lean
index 32630f506f3..4ccd2880af9 100644
--- a/MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Stage_en.lean
+++ b/MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Stage_en.lean
@@ -16,11 +16,16 @@ import Mathlib.Tactic
   Namespace: `RepeatedGames_en` (anti-collision with `RepeatedGames` of
   the FR canonical `Stage.lean`). External access:
   `RepeatedGames_en.PDAction`, `RepeatedGames_en.PrisonersDilemma`, etc.
-  No external module imports this EN sibling; the FR-canonical modules
-  (Discounting, GrimTrigger, Folk) reference `RepeatedGames.PrisonersDilemma`
-  via `open RepeatedGames` (the FR namespace), and the higher-level EN
-  siblings (Discounting_en, GrimTrigger_en) likewise reference the FR
-  base types. This Stage_en is the autonomous EN mirror of the foundation.
+  Import rule for this series: every higher-level EN module imports
+  `RepeatedGames.Stage_en` and works inside `namespace RepeatedGames_en`,
+  resolving the base types through `open RepeatedGames_en`, never through
+  the FR namespace. The current roster of those modules is the
+  `## Structure` section of `RepeatedGames_en.lean`; it is deliberately not
+  restated here, so adding a sibling means updating one place, not two.
+  The FR-canonical modules (Discounting, GrimTrigger, Folk) stay inside
+  `namespace RepeatedGames` and reference the base types directly, and no
+  FR module crosses into the EN namespace. This Stage_en is the autonomous
+  EN mirror of the foundation.
 
   Methodological note: manual translation of the FR canonical (no historical
   pre-Option-A EN source to recover; FR-first file since origin).