diff --git a/MyIA.AI.Notebooks/GameTheory/conway_cgt_lean/README.en.md b/MyIA.AI.Notebooks/GameTheory/conway_cgt_lean/README.en.md
index dd52ecef0dc..f749ff3732e 100644
--- a/MyIA.AI.Notebooks/GameTheory/conway_cgt_lean/README.en.md
+++ b/MyIA.AI.Notebooks/GameTheory/conway_cgt_lean/README.en.md
@@ -65,7 +65,7 @@ The file imports the upstream modules and exhibits their key results:
 | Games | `PGame` (basic) | `IGame` (concrete) + `Game` (quotient) |
 | Surreals | Basic/Dyadic/Mul | + Division, Hahn series, Birthday, Pow |
 | Nimbers | Basic/Field | + Nat, SimplestExtension |
-| Games lib | 8 modules | 15+ modules (Impartial, Loopy, Specific…) |
+| Games lib | CGT modules | upstream modules (Impartial, Loopy, Specific…) |
 
 ## Modules
 
diff --git a/MyIA.AI.Notebooks/GameTheory/lean_game_defs/README.en.md b/MyIA.AI.Notebooks/GameTheory/lean_game_defs/README.en.md
index dbcde07b561..40520109872 100644
--- a/MyIA.AI.Notebooks/GameTheory/lean_game_defs/README.en.md
+++ b/MyIA.AI.Notebooks/GameTheory/lean_game_defs/README.en.md
@@ -5,7 +5,7 @@ Shared Lean 4 type definitions used by multiple GameTheory Lean projects. A **se
 ## Status
 
 - **Type:** Standalone Lake project (`lakefile.toml`, `lean-toolchain` pinned `v4.32.1`, `lake-manifest.json`)
-- **Files:** 12 `.lean` (6 FR + 6 `_en` siblings, EPIC #4980 Pattern A)
+- **Files:** see catalogue (FR + `_en` siblings, EPIC #4980 Pattern A)
 - **`sorry` count:** 0 (definitions only, no proofs)
 - **Mathlib dependency:** None — all files use core Lean 4 only
 - **Buildable in isolation:** Yes — `lake build` (harness added by #2752, ai-01 review)
@@ -15,10 +15,10 @@ Shared Lean 4 type definitions used by multiple GameTheory Lean projects. A **se
 
 ## Files
 
-- [Basic.lean](Basic.lean) — 107 lines. `NormalFormGame`, `FiniteGame`, `Game2x2` structures + expected payoffs. Source: `GameTheory-16-Lean-Definitions.ipynb`.
-- [Nash.lean](Nash.lean) — 139 lines. Best response, pure/mixed Nash equilibrium, strict dominance. Source: `GameTheory-16-Lean-Definitions.ipynb`.
-- [Combinatorial.lean](Combinatorial.lean) — 113 lines. `GameTree`, minimax evaluation, win/loss determination. Source: `GameTheory-18-Lean-CombinatorialGames.ipynb`.
-- [SocialChoice.lean](SocialChoice.lean) — 126 lines. `Preference`, `StrictPref`, Arrow's axioms (statements). Source: `GameTheory-19-Lean-SocialChoice.ipynb`.
+- [Basic.lean](Basic.lean) — see catalogue. `NormalFormGame`, `FiniteGame`, `Game2x2` structures + expected payoffs. Source: `GameTheory-16-Lean-Definitions.ipynb`.
+- [Nash.lean](Nash.lean) — see catalogue. Best response, pure/mixed Nash equilibrium, strict dominance. Source: `GameTheory-16-Lean-Definitions.ipynb`.
+- [Combinatorial.lean](Combinatorial.lean) — see catalogue. `GameTree`, minimax evaluation, win/loss determination. Source: `GameTheory-18-Lean-CombinatorialGames.ipynb`.
+- [SocialChoice.lean](SocialChoice.lean) — see catalogue. `Preference`, `StrictPref`, Arrow's axioms (statements). Source: `GameTheory-19-Lean-SocialChoice.ipynb`.
 - [Bayesian.lean](Bayesian.lean) — Bayesian games with incomplete information: `BayesianGame`, `TypeStrategy`, `BayesianNashEquilibrium`, `InformationSet`, `SignalingGame`, `FirstPriceAuction`, Kuhn poker definitions. Source: `GameTheory-11-BayesianGames-Python.ipynb`, `GameTheory-13-ImperfectInfo-CFR-Python.ipynb`.
 - [Regret.lean](Regret.lean) — Regret minimization and CFR: `CumulativeRegret`, `regretMatchingStrategy`, `CounterfactualRegret`, `CFRState`, `FictitiousPlayState`. Source: `GameTheory-13-ImperfectInfo-CFR-Python.ipynb`, `GameTheory-17-MultiAgent-RL-Python.ipynb`.
 
@@ -64,7 +64,7 @@ track: shared Lean 4 type definitions (no proofs, 0 `sorry`) used by the teachin
 notebooks and copied by adjacent Lake projects. It has been a standalone Lake
 project since #2752 — `lakefile.toml`, pinned `lean-toolchain`, dedicated CI — with
 no Mathlib dependency; every file is core Lean 4 only, and `lake build` checks the
-whole set (12 modules, FR + `_en` siblings).
+whole set (FR + `_en` siblings).
 
 ### What it provides