Rename(#17545): T2 GALOIS - descente de l'ilot (carnet 22 + lake galois_lean)

.github/workflows/lean-galois.yml

@@ -1,6 +1,6 @@
 name: Lean Galois CI
 
-# CI for galois_lean (SymbolicAI/Lean/galois_lean).
+# CI for galois_lean (SymbolicAI/Lean/GALOIS/galois_lean).
 # Inverse Galois problem / M23 — proof layer for the Lean-19 notebook.
 # Rule lean-merge-discipline: lake build SUCCESS local OBLIGATOIRE avant merge.
 #
@@ -19,10 +19,10 @@ on:
   push:
     branches: [main]
     paths:
-      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/**.lean'
-      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/lakefile.lean'
-      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/lakefile.toml'
-      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/lean-toolchain'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/**.lean'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/lakefile.lean'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/lakefile.toml'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/lean-toolchain'
       - '.github/workflows/lean-galois.yml'
       - '.github/workflows/lean-axiom.yml'
       - '.github/workflows/lean-build.yml'
@@ -33,10 +33,10 @@ on:
   pull_request:
     types: [opened, synchronize, edited, reopened]
     paths:
-      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/**.lean'
-      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/lakefile.lean'
-      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/lakefile.toml'
-      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/lean-toolchain'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/**.lean'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/lakefile.lean'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/lakefile.toml'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/lean-toolchain'
       # The gate must run on the PR that introduces or changes it (cf #8712).
       - '.github/workflows/lean-galois.yml'
       - '.github/workflows/lean-axiom.yml'
@@ -56,7 +56,7 @@ jobs:
   ci:
     uses: jsboige/CoursIA/.github/workflows/lean-build.yml@main
     with:
-      project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean
+      project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean
       display-name: galois_lean
       sorry-baseline: "0"
       sorry-filter-mode: real
@@ -87,7 +87,7 @@ jobs:
     needs: ci  # c.306 parity with knot_lean (#14922) -- serialize the two compiles; ordering edge only, no measured clone-halving (c.329, ai-01 re-review #15150)
     uses: ./.github/workflows/lean-axiom.yml
     with:
-      project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean
+      project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean
       display-name: galois_lean
       target-modules: "*"
       allow-axioms: ""

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb → MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/GALOIS-01-Probleme-Inverse-M23-Python.ipynb

@@ -14,11 +14,11 @@
     "tags": []
    },
    "source": [
-    "# Lean-22 : Le problème inverse de Galois — M₂₃ refermé le 9 août 2026\n",
+    "# GALOIS-01 : Le problème inverse de Galois — M₂₃ refermé le 9 août 2026\n",
     "\n",
     "**Série** : SymbolicAI / Lean — Théorie des groupes sporadiques et problème inverse de Galois\n",
     "\n",
-    "**Navigation** : [<< MIMO-04 Capstone](MIMO/MIMO-04-Capstone-Digestion-Python.ipynb) | [Index](README.md)\n",
+    "**Navigation** : [<< MIMO-04 Capstone](../MIMO/MIMO-04-Capstone-Digestion-Python.ipynb) | [Index](README.md) | [Lean-23 (ERC-20) >>](../Lean-23-ERC20-Invariant-Companion.ipynb)\n",
     "\n",
     "**Kernel** : Python 3 (vérifications exécutables sympy + extraction Steiner) + Lean 4 via WSL\n",
     "(`galois_lean`, source de vérité formelle — sections 3 et 4)\n",
@@ -552,7 +552,7 @@
     "4. **Spécialisation** (irréductibilité de Hilbert) : de ℚ(t) vers le ℚ du polynôme f₁.\n",
     "\n",
     "Le dépôt porte déjà le socle géométrique de cette chaîne dans\n",
-    "[`grothendieck_lean`](grothendieck_lean/README.md) : sites, faisceaux,\n",
+    "[`grothendieck_lean`](../grothendieck_lean/README.md) : sites, faisceaux,\n",
     "cohomologie — mais **pas** le π₁ étale ni l'existence de Riemann. La phrase qui doit rester\n",
     "noir sur blanc : **« M₂₃ est un groupe de Galois sur ℚ » n'est PAS formalisé dans ce dépôt** —\n",
     "il est prouvé dans le préprint, et vérifié computationnellement ci-dessous au niveau du\n",
@@ -1610,7 +1610,7 @@
    "end_time": "2026-09-20T02:00:08.303200+00:00",
    "environment_variables": {},
    "exception": null,
-   "input_path": "Lean-22-Galois-Probleme-Inverse-M23.ipynb",
+   "input_path": "GALOIS-01-Probleme-Inverse-M23-Python.ipynb",
    "output_path": "16581_pm_output2.ipynb",
    "parameters": {},
    "start_time": "2026-09-20T01:53:28.665774+00:00",

MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/README.md

@@ -0,0 +1,15 @@
+# GALOIS — le problème inverse de Galois, M₂₃ refermé
+
+Sous-série de la série [Lean](../README.md) — **îlot à une entrée** de la gradation #17545 (décision du 24/09, note de conception c.6408913452) : le problème inverse de Galois descend ici avec son lac [`galois_lean`](galois_lean/README.md). Pas de capstone dédié (décision du 11/10 : le capstone reste MIMO-only) — l'îlot se réduit à son carnet et à son lac, le lac y est exposé en entier (sections 3-4 et annexes A-B du carnet).
+
+L'ancien identifiant de série (`Lean-22` → `GALOIS-01`) est consigné dans `docs/reference/rename-ledger.tsv`.
+
+**Escalier depuis la série principale** : l'entrée se fait depuis [MIMO-04 — Capstone](../MIMO/MIMO-04-Capstone-Digestion-Python.ipynb), sortie de la sous-série MIMO ; l'îlot se referme sur GALOIS-01 et le parcours principal reprend à [Lean-23 (ERC-20)](../Lean-23-ERC20-Invariant-Companion.ipynb).
+
+| Carnet | Contenu | Durée |
+|---|---|---|
+| [GALOIS-01-Probleme-Inverse-M23-Python](GALOIS-01-Probleme-Inverse-M23-Python.ipynb) | Le problème inverse de Galois refermé (arXiv:2608.08538, 9 août 2026) : M₂₃ prouvé simple d'ordre 10 200 960 **à l'écran** (`card_M23`/`simple_M23` exécutés, `#print axioms` = liste blanche), design de Witt S(4,7,23) vérifié des deux côtés (253 heptades), polynôme f₁ de degré 23 manipulé pour de vrai (empreinte, irréductibilité, discriminant 383 chiffres, Frobenius mod p) — les deux énoncés distingués : prouvé vs cité | 45 min |
+
+**Prérequis d'entrée** : Python 3 (NumPy, sympy). Le lac `galois_lean` est résolu par `find_lean_project` — le lac est frère du carnet dans l'îlot, aucune configuration manuelle.
+
+**Statut du lac** : `galois_lean` est **sorry-free** (mode `real` : 0 `sorry` tactique, 0 `native_decide`, 0 `axiom` déclaré) — preuve M₂₃ *vendored* Apache-2.0 depuis [`KitaKen1/finite-simple-groups-lean`](https://github.com/KitaKen1/finite-simple-groups-lean), axiomes `{propext, Classical.choice, Quot.sound}` (whitelist §B), gardé par la CI `lean-galois.yml`. Détail : [`galois_lean/README.md`](galois_lean/README.md).

MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/README.md → MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/README.md

@@ -1,6 +1,6 @@
 # Problème inverse de Galois — M₂₃ groupe de Galois sur ℚ
 
-Lake `galois_lean` : couche de preuve pour le notebook **[Lean-22](../Lean-22-Galois-Probleme-Inverse-M23.ipynb)** (problème inverse de Galois), autour du groupe sporadique de Mathieu M₂₃.
+Lake `galois_lean` : couche de preuve pour le notebook **[Lean-22](../GALOIS-01-Probleme-Inverse-M23-Python.ipynb)** (problème inverse de Galois), autour du groupe sporadique de Mathieu M₂₃.
 
 ## Contexte
 
@@ -38,6 +38,6 @@ Per `sota-not-workaround` : refaire une échelle de petits groupes à côté d'u
 
 ## Voir aussi
 
-- [Lean-15-Grothendieck-Tribute](../Lean-15-Grothendieck-Tribute.ipynb) — hommage comparable (prouve ce qu'il annonce)
+- [Lean-15-Grothendieck-Tribute](../../Lean-15-Grothendieck-Tribute.ipynb) — hommage comparable (prouve ce qu'il annonce)
 - `grothendieck_lean` — angle SGA1 (π₁ étale, existence de Riemann) pour le chaînon-pont vers la réalisation galoisienne
 - EPIC i18n #4980 : siblings `_en` à venir

MyIA.AI.Notebooks/SymbolicAI/Lean/LEAN_INVENTORY.md

@@ -217,8 +217,8 @@ pour l'identification `23T5 = M23` que la couche proof-assistant ne reproduit pa
   tactique, 0 `native_decide`, 0 `axiom` déclaré. `Sporadic.card_M23` et
   `Sporadic.simple_M23` prouvés par chaîne de stabilisateurs à certificats
   (Schreier–Sims matérialisé).
-- **Notebook câblé** : 1 notebook (Lean-22-Galois-Probleme-Inverse-M23).
-- **Suivi** : préprint #2608.08538 (cf. `galois_lean/README.md`).
+- **Notebook câblé** : GALOIS/GALOIS-01-Probleme-Inverse-M23-Python.
+- **Suivi** : préprint #2608.08538 (cf. `GALOIS/galois_lean/README.md`).
 - **i18n** : EN-sibling à venir (EPIC #4980).
 - **Caveat build** : `lakefile.toml` utilise la forme **bare** + agrégateur racine (la
   forme `globs = #[Galois.*]` déclenche un quirk trace *job-computation* sous lake

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb

@@ -1652,7 +1652,7 @@
     "\n",
     "Le théorème structurel est de Grothendieck (SGA 7) : la monodromie d'une famille lisse au-dessus d'un disque épointé est **quasi-unipotente** — un certain pouvoir de la transformation est unipotent, autrement dit toutes ses valeurs propres sont des racines de l'unité. C'est un résultat de finitude remarquable : quelle que soit la famille, la boucle ne peut engendrer qu'une torsion d'ordre fini ou quasi fini. Deligne en a fait l'arme centrale de *Weil II* (1980) : c'est en contrôlant la monodromie ℓ-adique qu'il porte l'analogie de Riemann sur les corps finis. Le polynôme d'Alexander du trèfle est précisément le polynôme caractéristique de cette action.\n",
     "\n",
-    "**État mesuré (18/10/2026)** : la série Lean manipule la monodromie sans jamais l'introduire — 4 occurrences d'usage ([Lean-22](Lean-22-Galois-Probleme-Inverse-M23.ipynb) ×1, [Lean-28](Lean-28-Complex-Structure-S6.ipynb) ×2 — le triangle (3,4,∞) « fournit les monodromies » qui donnent la présentation de π₁ — et [Riemann200/README](Riemann200/README.md) ×1), zéro définition. Mathlib 4 ne formalise pas davantage la quasi-unipotence : du hors-scope cohérent avec la table ci-dessus. La première marche — groupe fondamental d'un plan épointé, action de monodromie d'un exemple explicite, quasi-unipotence calculée — est ouverte en grain dédié : [#21308](https://github.com/jsboige/CoursIA/issues/21308).\n"
+    "**État mesuré (18/10/2026)** : la série Lean manipule la monodromie sans jamais l'introduire — 4 occurrences d'usage ([Lean-22](GALOIS/GALOIS-01-Probleme-Inverse-M23-Python.ipynb) ×1, [Lean-28](Lean-28-Complex-Structure-S6.ipynb) ×2 — le triangle (3,4,∞) « fournit les monodromies » qui donnent la présentation de π₁ — et [Riemann200/README](Riemann200/README.md) ×1), zéro définition. Mathlib 4 ne formalise pas davantage la quasi-unipotence : du hors-scope cohérent avec la table ci-dessus. La première marche — groupe fondamental d'un plan épointé, action de monodromie d'un exemple explicite, quasi-unipotence calculée — est ouverte en grain dédié : [#21308](https://github.com/jsboige/CoursIA/issues/21308).\n"
    ]
   },
   {

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb

@@ -16,7 +16,7 @@
    "source": [
     "# Lean-23 : ERC-20 sous Lean 4 — l'invariant de conservation prouvé\n",
     "\n",
-    "**Navigation** : [Index](README.md) | [Lean-22 (Galois) <<](Lean-22-Galois-Probleme-Inverse-M23.ipynb) | [SC-7 SmartContract (Solidity ERC-20) >>](../SmartContracts/02-Solidity-Advanced/SC-07-Token-Standards-Python.ipynb)\n",
+    "**Navigation** : [Index](README.md) | [Lean-22 (Galois) <<](GALOIS/GALOIS-01-Probleme-Inverse-M23-Python.ipynb) | [SC-7 SmartContract (Solidity ERC-20) >>](../SmartContracts/02-Solidity-Advanced/SC-07-Token-Standards-Python.ipynb)\n",
     "\n",
     "Ce notebook presente le lake **`erc20_lean`** de ce dépot (issue #4047, livrable phase 1) : le port formel de l'**invariant de conservation d'un jeton ERC-20** en Lean 4 avec Mathlib. La propriété foncière d'un jeton fongible — aucun token ne peut être créé ou détruit par un `transfer` (seuls `mint`/`burn` le font, symétriquement sur l'offre) — est ici prouvée **mécaniquement** sur une machine à états finie de **trois transitions gardées**.\n",
     "\n",
@@ -948,7 +948,7 @@
     "- **Lake `erc20_lean`** (`MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean/`) — la version Lean 4 + Mathlib : `ERC20/State.lean` (modèle), `ERC20/Ops.lean` (transitions), `ERC20/Invariant.lean` (préservation).\n",
     "- **EPIC #4980** — convention i18n Lean (aggrégateur bilingue inline FR-EN dans `ERC20.lean`, sibling pair dans `ERC20_en.lean`).\n",
     "- **Rule C.6** (mandat user 2026-08-19) — préférence pour un compagnon kernel `lean4-wsl` à côté du notebook Python ; le pattern actuel (subprocess `lake env lean`) reste mergeable, le kernel Lean natif est une suite à explorer.\n",
-    "- Notebooks associés : `[Lean-22 (Galois)](Lean-22-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-21 (MIMO)](MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb)`, `[Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb)`, `[Lean-13 (Kochen-Specker)](Lean-13-Kochen-Specker.ipynb)`, `[A* Optimalite (Search-03e)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb)`."
+    "- Notebooks associés : `[Lean-22 (Galois)](GALOIS/GALOIS-01-Probleme-Inverse-M23-Python.ipynb)`, `[Lean-21 (MIMO)](MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb)`, `[Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb)`, `[Lean-13 (Kochen-Specker)](Lean-13-Kochen-Specker.ipynb)`, `[A* Optimalite (Search-03e)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb)`."
    ]
   }
  ],