myia-ai-01 · Nov 5, 2026 · Nov 3, 2026 · Nov 3, 2026 · Nov 3, 2026 · Nov 4, 2026
diff --git a/.github/workflows/lean-derived-pages-gate.yml b/.github/workflows/lean-derived-pages-gate.yml
@@ -0,0 +1,116 @@
+name: Lean derived pages gate
+
+# Purpose
+# -------
+# BLOQUING gate, portee par le garde `scripts/lean/check_lean_derived_pages.py` :
+# les pages derivees de l'arbre Lean (`docs/reference/lean-theorem-duplicates.md`,
+# `docs/reference/lean-material-map.md`) sont **regenerees**, jamais ecrites a la
+# main. Ce garde verifie que la page **commitee** suit l'arbre **de la revision
+# testee**, et nomme la commande qui la regenere.
+#
+# Pourquoi une porte dediee, et non le test global
+# --------------------------------------------------
+# Le job `Scripts Tests (CPU)` execute tous les tests de `scripts/`, donc le
+# test de derive de `lean-theorem-duplicates.md` rendait ROUGE **toute PR de la
+# flotte** qui touche `scripts/` -- mesure du 2026-11-03 : 22 PRs de la lane
+# `myia-ai-01:CoursIA-2` bloquees le meme jour, sans qu'aucune n'ait touche
+# l'arbre Lean. La derive, elle, est legitime : l'arbre bouge, la page doit
+# suivre. C'est la **portee** du predicat qui etait fausse -- une porte qui
+# accuse une PR d'un defaut qu'elle ne peut pas causer.
+#
+# Ce garde porte le predicat la ou il est causable : il ne se declenche que
+# sur les PRs qui touchent l'arbre Lean, les generateurs, ou les pages.
+#
+# Paths watched
+# -------------
+#   - **/*.lean                    (l'arbre Lean lui-meme, lakefiles inclus)
+#   - **/lakefile.toml             (les lacs declares hors `.lean`)
+#   - scripts/lean/lean_*.py      (les generateurs, proprietaires des pages)
+#   - scripts/lean/check_lean_derived_pages.py (ce garde)
+#   - docs/reference/lean-*.md    (les pages derivees)
+#   - .github/workflows/**         (la carte du materiel lit la couverture CI)
+#
+# Le declencheur est un `pull_request` ordinaire : la porte ne fait que LIRE
+# (elle appelle les generateurs en `--check`), elle n'ecrit rien et ne
+# demande aucun droit.
+
+on:
+  pull_request:
+    paths:
+      - '**/*.lean'
+      - '**/lakefile.toml'
+      - 'scripts/lean/lean_*.py'
+      - 'scripts/lean/check_lean_derived_pages.py'
+      - 'docs/reference/lean-*.md'
+      - '.github/workflows/**'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: lean-derived-pages-gate-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  derived-pages:
+    name: "Lean derived pages gate (#24183, #23097)"
+    runs-on: ${{ (github.event.pull_request.head.repo.full_name == github.repository && vars.CI_OVERFLOW_LOCAL == 'true') && fromJSON('["self-hosted","coursia-ephemeral","coursia-linux"]') || 'ubuntu-latest' }}
+    timeout-minutes: 20
+
+    steps:
+      - name: Checkout PR
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+          filter: blob:none
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.11'
+
+      - name: Check the derived pages against the Lean tree
+        # Le verdict porte sur la REVISION TESTEE : le checkout d'un evenement
+        # `pull_request` materialise la ref de merge, c'est-a-dire l'etat que
+        # `main` aura apres le merge de cette PR. C'est exactement l'etat que
+        # la page doit decrire.
+        run: |
+          set +e
+          python scripts/lean/check_lean_derived_pages.py --json \
+              > lean_derived_pages.json 2>lean_derived_pages_stderr.log
+          EXIT=$?
+          set -e
+          # En mode `--json`, le garde ecrit le JSON **pure** sur stdout et la
+          # ligne de verdict (`VERDICT: ...`) sur stderr : le rapport reste
+          # donc parsable, et le verdict reste lisible dans le journal.
+          if [ -s lean_derived_pages_stderr.log ]; then
+            echo "Derived-pages tool output (stderr):"
+            cat lean_derived_pages_stderr.log
+          fi
+          if ! python3 -c "import json; json.load(open('lean_derived_pages.json'))" 2>/dev/null; then
+            echo "::error title=Lean derived pages report unparseable::The JSON report could not be parsed. Tool exit was $EXIT."
+            tail -c 400 lean_derived_pages.json || true
+            cat lean_derived_pages_stderr.log 2>/dev/null || true
+            exit 1
+          fi
+          python3 - <<'PY'
+          import json
+          import sys
+
+          data = json.load(open("lean_derived_pages.json"))
+          pages = data.get("pages") or []
+          drifted = [p for p in pages if p.get("drifted")]
+
+          if not drifted:
+              print("::notice title=Lean derived pages::%d page(s) derivee(s) conforme(s) a l'arbre Lean." % len(pages))
+              sys.exit(0)
+
+          print("::error title=Lean derived pages divergeantes::%d page(s) derivee(s) ne suivent plus l'arbre Lean de cette revision." % len(drifted))
+          for p in drifted:
+              print("- %s" % p.get("page"))
+              if p.get("detail"):
+                  print("  %s" % p["detail"])
+              print("  geste : python %s --write" % p.get("generator"))
+          sys.exit(1)
+          PY
diff --git a/docs/reference/lean-material-map.md b/docs/reference/lean-material-map.md
@@ -10,8 +10,8 @@ Cette page est regeneree par `scripts/lean/lean_material_map.py`. Une table reco
 
 | Lac | Modules | Miroirs | CI | Gate axiomes | Naissance |
 |---|---|---|---|---|---|
-| `MyIA.AI.Notebooks/SymbolicAI/Lean/GROTH/grothendieck_lean` | 100 | 98 | declare | couverte | 2026-05-31 |
-| `MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean` | 57 | 41 | declare | couverte | 2026-11-02 |
+| `MyIA.AI.Notebooks/SymbolicAI/Lean/GROTH/grothendieck_lean` | 100 | 98 | declare | couverte | 2026-11-04 |
+| `MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean` | 57 | 41 | declare | couverte | 2026-11-04 |
 | `MyIA.AI.Notebooks/GameTheory/game_theory_lean` | 39 | 25 | declare | couverte | 2026-07-10 |
 | `MyIA.AI.Notebooks/Search/discrepancy_lean` | 33 | 25 | declare | couverte | 2026-08-25 |
 | `MyIA.AI.Notebooks/ML/learning_theory_lean` | 32 | 30 | declare | couverte | 2026-06-25 |

diff --git a/docs/reference/lean-theorem-duplicates.md b/docs/reference/lean-theorem-duplicates.md
@@ -34,22 +34,22 @@ Ces paires partagent un terme rare mais ne decrivent pas clairement le meme resu
 | `jumpCapturedF_reconstruction_of_spaceship_mod` | `MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean` | `reconstruction` | `MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean` | 0.03 | `reconstruction` |
 | `jumpCapturedF_reconstruction_of_static_frame` | `MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean` | `reconstruction` | `MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean` | 0.04 | `reconstruction` |
 
-Detail des paires (fichier et ligne) :
-
-- **1.00** -- `arrow` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Arrow.lean:696) et `arrow_impossibility` (MyIA.AI.Notebooks/GameTheory/lean_game_defs/SocialChoice.lean:899) -- nom 1.00 / docstring 0.27 / enonce 0.08 / termes arrow
-- **1.00** -- `sen_impossibility` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Sen.lean:77) et `sen_impossibility` (MyIA.AI.Notebooks/GameTheory/lean_game_defs/SocialChoice.lean:996) -- nom 1.00 / docstring 0.29 / enonce 0.09 / termes sen
-- **1.00** -- `fairBot_fairBot_cooperation` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/FairBot.lean:205) et `fairBot_self_cooperation` (MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean:97) -- nom 1.00 / docstring 0.09 / enonce 0.00 / termes cooperation
-- **1.00** -- `fairBot_fairBot_cooperation` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/FairBot.lean:205) et `fairBot_mutual_cooperation` (MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean:105) -- nom 1.00 / docstring 0.09 / enonce 0.00 / termes cooperation
-- **1.00** -- `fairBot_fairBot_cooperation` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/FairBot.lean:205) et `pa_fairBot_self_cooperation` (MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean:175) -- nom 1.00 / docstring 0.09 / enonce 0.00 / termes cooperation
-- **1.00** -- `fairBot_fairBot_cooperation` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/FairBot.lean:205) et `standard_fairBot_pair_cooperation` (MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean:218) -- nom 1.00 / docstring 0.10 / enonce 0.00 / termes cooperation
-- **1.00** -- `one_sub_pow_le_exp` (MyIA.AI.Notebooks/ML/learning_theory_lean/PacLearning/PacFiniteBound.lean:116) et `one_sub_pow_le_exp_mul` (MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/Converse.lean:179) -- nom 1.00 / docstring 0.00 / enonce 0.33 / termes exp, le, one, sub
-- **1.00** -- `Canonical.filter` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/GridCanonical.lean:239) et `countP_length_filter` (MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/ArcPartition.lean:842) -- nom 1.00 / docstring 0.11 / enonce 0.22 / termes filter
-- **1.00** -- `jumpCapturedF_reconstruction_of_still_life` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean:1216) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean:105) -- nom 1.00 / docstring 0.03 / enonce 0.00 / termes reconstruction
-- **1.00** -- `jumpCapturedF_reconstruction_of_period` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean:1589) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean:105) -- nom 1.00 / docstring 0.03 / enonce 0.00 / termes reconstruction
-- **1.00** -- `jumpCapturedF_reconstruction_of_period_mod` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean:1669) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean:105) -- nom 1.00 / docstring 0.03 / enonce 0.00 / termes reconstruction
-- **1.00** -- `jumpCapturedF_reconstruction_of_spaceship` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean:2509) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean:105) -- nom 1.00 / docstring 0.03 / enonce 0.00 / termes reconstruction
-- **1.00** -- `jumpCapturedF_reconstruction_of_spaceship_mod` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean:2689) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean:105) -- nom 1.00 / docstring 0.03 / enonce 0.00 / termes reconstruction
-- **1.00** -- `jumpCapturedF_reconstruction_of_static_frame` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean:4137) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean:105) -- nom 1.00 / docstring 0.04 / enonce 0.00 / termes reconstruction
+Detail des paires (fichier et declaration) :
+
+- **1.00** -- `arrow` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Arrow.lean) et `arrow_impossibility` (MyIA.AI.Notebooks/GameTheory/lean_game_defs/SocialChoice.lean) -- nom 1.00 / docstring 0.27 / enonce 0.08 / termes arrow
+- **1.00** -- `sen_impossibility` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Sen.lean) et `sen_impossibility` (MyIA.AI.Notebooks/GameTheory/lean_game_defs/SocialChoice.lean) -- nom 1.00 / docstring 0.29 / enonce 0.09 / termes sen
+- **1.00** -- `fairBot_fairBot_cooperation` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/FairBot.lean) et `fairBot_self_cooperation` (MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean) -- nom 1.00 / docstring 0.09 / enonce 0.00 / termes cooperation
+- **1.00** -- `fairBot_fairBot_cooperation` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/FairBot.lean) et `fairBot_mutual_cooperation` (MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean) -- nom 1.00 / docstring 0.09 / enonce 0.00 / termes cooperation
+- **1.00** -- `fairBot_fairBot_cooperation` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/FairBot.lean) et `pa_fairBot_self_cooperation` (MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean) -- nom 1.00 / docstring 0.09 / enonce 0.00 / termes cooperation
+- **1.00** -- `fairBot_fairBot_cooperation` (MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/FairBot.lean) et `standard_fairBot_pair_cooperation` (MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean) -- nom 1.00 / docstring 0.10 / enonce 0.00 / termes cooperation
+- **1.00** -- `one_sub_pow_le_exp` (MyIA.AI.Notebooks/ML/learning_theory_lean/PacLearning/PacFiniteBound.lean) et `one_sub_pow_le_exp_mul` (MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/Converse.lean) -- nom 1.00 / docstring 0.00 / enonce 0.33 / termes exp, le, one, sub
+- **1.00** -- `Canonical.filter` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/GridCanonical.lean) et `countP_length_filter` (MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/ArcPartition.lean) -- nom 1.00 / docstring 0.11 / enonce 0.22 / termes filter
+- **1.00** -- `jumpCapturedF_reconstruction_of_still_life` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean) -- nom 1.00 / docstring 0.03 / enonce 0.00 / termes reconstruction
+- **1.00** -- `jumpCapturedF_reconstruction_of_period` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean) -- nom 1.00 / docstring 0.03 / enonce 0.00 / termes reconstruction
+- **1.00** -- `jumpCapturedF_reconstruction_of_period_mod` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean) -- nom 1.00 / docstring 0.03 / enonce 0.00 / termes reconstruction
+- **1.00** -- `jumpCapturedF_reconstruction_of_spaceship` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean) -- nom 1.00 / docstring 0.03 / enonce 0.00 / termes reconstruction
+- **1.00** -- `jumpCapturedF_reconstruction_of_spaceship_mod` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean) -- nom 1.00 / docstring 0.03 / enonce 0.00 / termes reconstruction
+- **1.00** -- `jumpCapturedF_reconstruction_of_static_frame` (MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/HashlifeMarginFragment.lean) et `reconstruction` (MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Fourier.lean) -- nom 1.00 / docstring 0.04 / enonce 0.00 / termes reconstruction
 
 ## Methode