rename(lean,#17545): descente MIMO -- 21c/21/21b -> MIMO/MIMO-0N-*

MyIA.AI.Notebooks/GameTheory/GameTheory-16d-Echange-de-Reins-Lean-Python.ipynb

@@ -567,7 +567,7 @@
     "\n",
     "**Cohabitation pattern Lean/Python** : le notebook Python peut **lire** les sources Lean (regex balanced, cf lecon c.437-L1) et **citer** les theoremes, sans executer `lake env lean`. Le kernel Python suffit pour cette verification structurelle. La verification formelle (lake build) releve du notebook Lean side track `GameTheory-15b-Lean-CooperativeGames-Lean.ipynb`.\n",
     "\n",
-    "C'est le pattern transversal documente dans `GameTheory-15d-Mobius-Coalitions-Lean-Python.ipynb` (c.438) — la localisation par ancetres et le `raise` si introuvable y sont deja en place — et `Lean-21c-Descente-Budget.ipynb` (c.437). JAMAIS de simulation jouet - ou bien le vrai outil est invoque, ou bien l'absence est documentee.\n"
+    "C'est le pattern transversal documente dans `GameTheory-15d-Mobius-Coalitions-Lean-Python.ipynb` (c.438) — la localisation par ancetres et le `raise` si introuvable y sont deja en place — et `MIMO-01-Descente-Budget-Lean-Python.ipynb` (c.437). JAMAIS de simulation jouet - ou bien le vrai outil est invoque, ou bien l'absence est documentee.\n"
    ]
   },
   {

MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03b-PatternDatabases.ipynb

@@ -976,7 +976,7 @@
     "\n",
     "> **Quotienter / fibrer** — changer l'échelle de description en projetant l'état sur un quotient. **Loi** : la règle de chaîne $H(X) = H(\\pi(X)) + H(X \\mid \\pi(X))$. **Témoin** : $I(X_i ; X_j \\mid Q)$ sur un quotient commun $Q$. **Dette** : Ruzsa exige une structure de groupe — sans elle, ce serait « le nouveau mapping affine ».\n",
     "\n",
-    "**Position dans la table.** Première attestation : [Lean-21b](../../SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb) (PR [#12252](https://github.com/jsboige/CoursIA/pull/12252), primitives PFR). Candidate non-indépendante : Infer-20 (PR [#12277](https://github.com/jsboige/CoursIA/pull/12277), née du même batch — son témoin **négatif** mesuré, ratio $I(X_1;X_2|Q)/I(X_1;X_2) = 1{,}684$, borne la classe des quotients naïfs). Cette section est la **seconde attestation, sur un substrat indépendant** (Search/Python), avec le cas **positif** que la table attend : un quotient commun sous lequel l'interaction disparaît **exactement**.\n",
+    "**Position dans la table.** Première attestation : [Lean-21b](../../SymbolicAI/Lean/MIMO/MIMO-03-Converse-Native-Lean.ipynb) (PR [#12252](https://github.com/jsboige/CoursIA/pull/12252), primitives PFR). Candidate non-indépendante : Infer-20 (PR [#12277](https://github.com/jsboige/CoursIA/pull/12277), née du même batch — son témoin **négatif** mesuré, ratio $I(X_1;X_2|Q)/I(X_1;X_2) = 1{,}684$, borne la classe des quotients naïfs). Cette section est la **seconde attestation, sur un substrat indépendant** (Search/Python), avec le cas **positif** que la table attend : un quotient commun sous lequel l'interaction disparaît **exactement**.\n",
     "\n",
     "**Les trois personnages :**\n",
     "\n",

MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb

@@ -21,7 +21,7 @@
     "\n",
     "| Notebook précédent | Notebook suivant |\n",
     "|---|---|\n",
-    "| [ANALYSE-04 - PFR Primitives](ANALYSE-04-PFR-Primitives-Python.ipynb) | [Lean-21 - MIMO Detection Flips](../Lean-21-MIMO-Detection-Flips.ipynb) |\n",
+    "| [ANALYSE-04 - PFR Primitives](ANALYSE-04-PFR-Primitives-Python.ipynb) | [Lean-21 - MIMO Detection Flips](../MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb) |\n",
     "\n",
     "***\n",
     "\n",

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

@@ -19,6 +19,6 @@ La série principale garde son tutoriel (numéros 1 à 14) ; le présent dossier
 
 **Prérequis d'entrée** : le tutoriel de la série principale (numéros 1 à 6, tactiques et Mathlib). Le point d'entrée réel documenté du carnet 01 est [Search-03e-AStar-Optimality](../../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) (heuristique A*, companion `search_lean`) — voir sa cellule d'ouverture.
 
-**Marches nommées, à écrire** (règle 5 de la gradation) : entropie de Shannon avant ANALYSE-03, inégalités de concentration avant le converse MIMO ([Lean-21b](../Lean-21b-MIMO-Converse-Native.ipynb)). Elles vivront dans ce dossier ou la série principale selon la décision de renumérotation.
+**Marches nommées, à écrire** (règle 5 de la gradation) : entropie de Shannon avant ANALYSE-03, inégalités de concentration avant le converse MIMO ([Lean-21b](../MIMO/MIMO-03-Converse-Native-Lean.ipynb)). Elles vivront dans ce dossier ou la série principale selon la décision de renumérotation.
 
 **Marches franchissables** : depuis la série principale, le tutoriel (1-14) suffit pour ANALYSE-01. ANALYSE-02 suppose la lecture d'un lac externe ; ANALYSE-03/04 supposent l'entropie de Shannon (marche nommée ci-dessus) ; ANALYSE-05 ne suppose rien au-delà du tutoriel : son lac est local, posé à côté du carnet.

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-Capstone-Digestions-Tao-Python.ipynb

@@ -22,7 +22,7 @@
     "\n",
     "| Notebook précédent | Notebook suivant |\n",
     "|---|---|\n",
-    "| [Lean-17c - Knots Companion Formel](KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb) | [ANALYSE-01 - Sendov](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb) pour entrer dans la sous-série, ou [Lean-21 - MIMO Detection Flips](Lean-21-MIMO-Detection-Flips.ipynb) pour poursuivre le parcours principal |\n",
+    "| [Lean-17c - Knots Companion Formel](KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb) | [ANALYSE-01 - Sendov](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb) pour entrer dans la sous-série, ou [Lean-21 - MIMO Detection Flips](MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb) pour poursuivre le parcours principal |\n",
     "\n",
     "***\n",
     "\n",
@@ -686,7 +686,7 @@
     "3. **Une marche montée.** La règle de chaîne et la distance de Ruzsa, calculées sur F₂³, suffisent pour lire l'énoncé entropique de PFR : une distance nulle est une structure, et une petite distance est une structure approchée.\n",
     "4. **Une surface mesurée, avec ses défauts.** Les titres, les exercices d'ANALYSE-04 et le nom du dossier sont suivis dans [#18408](https://github.com/jsboige/CoursIA/issues/18408).\n",
     "\n",
-    "**Suite.** Entrer par [ANALYSE-01](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb), ou poursuivre le parcours principal avec [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb). Ce dernier reprend les deux registres de la sous-série : des illustrations numériques, puis des `#check` réels sur un lac compilé. Les primitives entropiques de PFR ont aussi vocation à être greffées dans la série ICT ([#18405](https://github.com/jsboige/CoursIA/issues/18405))."
+    "**Suite.** Entrer par [ANALYSE-01](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb), ou poursuivre le parcours principal avec [Lean-21](MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb). Ce dernier reprend les deux registres de la sous-série : des illustrations numériques, puis des `#check` réels sur un lac compilé. Les primitives entropiques de PFR ont aussi vocation à être greffées dans la série ICT ([#18405](https://github.com/jsboige/CoursIA/issues/18405))."
    ]
   }
  ],

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb

@@ -18,7 +18,7 @@
     "\n",
     "**Série** : SymbolicAI / Lean — Théorie des groupes sporadiques et problème inverse de Galois\n",
     "\n",
-    "**Navigation** : [<< Lean-21 MIMO](Lean-21-MIMO-Detection-Flips.ipynb) | [Index](README.md)\n",
+    "**Navigation** : [<< Lean-21 MIMO](MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb) | [Index](README.md)\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",

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

@@ -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)](Lean-21-MIMO-Detection-Flips.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)](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)`."
    ]
   }
  ],

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-29-Hecke-Operators-Native.ipynb

@@ -28,7 +28,7 @@
     "\n",
     "**L'enjeu de ce que le lake porte.** Les opérateurs de Hecke ne sont pas un objet d'exposition : ils sont la charnière par laquelle une forme modulaire devient une **suite de nombres comparable à autre chose**. Une forme propre normalisée — un vecteur propre commun de tous les $T_p$ — a ses coefficients de Fourier $a(p)$ égaux à ses valeurs propres, et c'est cette suite que le théorème de modularité apparie aux comptages de points $\\#E(\\mathbb{F}_p)$ d'une courbe elliptique sur $\\mathbb{Q}$. La chaîne courbe de Frey $\\rightarrow$ abaissement du niveau $\\rightarrow$ modularité, qui clôt le dernier théorème de Fermat, passe donc par la relation $a(np) + p^{k-1} a(n/p)$ — celle que `coeffHeckeT` porte ici, et que la section 5 fait calculer. Le dépôt amont dont ce lake est un port, `anthropics/fermats-last-theorem`, est un chantier de formalisation de cette chaîne. **Le lake en formalise les opérateurs, pas la preuve** : c'est un fragment de fondation, et la section 8 en prouve la dernière étape — $S_2(\\Gamma_0(2)) = 0$ — pendant que la section 9 mesure exactement ce que le lake démontre et ce qu'il suppose.\n",
     "\n",
-    "**Pourquoi ce module parmi environ 15 000 théorèmes du corpus FLT.** Son choix n'est pas justifié par le seul fait qu'un énoncé non trivial puisse être soumis au noyau Lean — cet argument vaudrait pour n'importe quel module du corpus. Hecke prolonge deux objets déjà enseignés dans CoursIA. D'abord, [Lean-12](Lean-12-Sensitivity-Theorem.ipynb) et son [compagnon Lean-12b](Lean-12b-Lean-Sensitivity-Theorem.ipynb) introduisent les fonctions sur l'hypercube et le lake [`sensitivity_lean`](sensitivity_lean/) ; son module [`Sensitivity/Fourier.lean`](sensitivity_lean/Sensitivity/Fourier.lean) représente une fonction par une famille de coefficients de Walsh, établit leur orthogonalité puis une reconstruction par somme finie. Ensuite, ce même lake formalise dans [`Sensitivity/Operator.lean`](sensitivity_lean/Sensitivity/Operator.lean) un opérateur linéaire $f_n$ et la relation $f_n^2=n\\,\\mathrm{Id}$, tandis que [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb), son [compagnon Lean-21b](Lean-21b-MIMO-Converse-Native.ipynb) et le lake [`mimo_lean`](mimo_lean/) manipulent matrices, applications linéaires, actions scalaires et sommes finies. Le passage pédagogique devient alors lisible : **fonction décrite par des coefficients** $\\rightarrow$ **opérateur additif et homogène agissant sur une fonction** $\\rightarrow$ **transformation arithmétique explicite de ses coefficients**. Hecke est le fragment du corpus FLT où ces deux fils déjà familiers se rencontrent dans un nouvel objet : les formes modulaires sur le demi-plan supérieur, leurs slash actions et la formule de `coeffHeckeT`.\n",
+    "**Pourquoi ce module parmi environ 15 000 théorèmes du corpus FLT.** Son choix n'est pas justifié par le seul fait qu'un énoncé non trivial puisse être soumis au noyau Lean — cet argument vaudrait pour n'importe quel module du corpus. Hecke prolonge deux objets déjà enseignés dans CoursIA. D'abord, [Lean-12](Lean-12-Sensitivity-Theorem.ipynb) et son [compagnon Lean-12b](Lean-12b-Lean-Sensitivity-Theorem.ipynb) introduisent les fonctions sur l'hypercube et le lake [`sensitivity_lean`](sensitivity_lean/) ; son module [`Sensitivity/Fourier.lean`](sensitivity_lean/Sensitivity/Fourier.lean) représente une fonction par une famille de coefficients de Walsh, établit leur orthogonalité puis une reconstruction par somme finie. Ensuite, ce même lake formalise dans [`Sensitivity/Operator.lean`](sensitivity_lean/Sensitivity/Operator.lean) un opérateur linéaire $f_n$ et la relation $f_n^2=n\\,\\mathrm{Id}$, tandis que [Lean-21](MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb), son [compagnon Lean-21b](MIMO/MIMO-03-Converse-Native-Lean.ipynb) et le lake [`mimo_lean`](mimo_lean/) manipulent matrices, applications linéaires, actions scalaires et sommes finies. Le passage pédagogique devient alors lisible : **fonction décrite par des coefficients** $\\rightarrow$ **opérateur additif et homogène agissant sur une fonction** $\\rightarrow$ **transformation arithmétique explicite de ses coefficients**. Hecke est le fragment du corpus FLT où ces deux fils déjà familiers se rencontrent dans un nouvel objet : les formes modulaires sur le demi-plan supérieur, leurs slash actions et la formule de `coeffHeckeT`.\n",
     "\n",
     "**Raccord conceptuel, dépendance réelle.** Ce passage est une analogie structurante, pas une identification mathématique : les coefficients de Fourier booléens de `Sensitivity/Fourier.lean` décrivent une fonction sur un hypercube fini à l'aide des caractères de Walsh ; les coefficients $a(n)$ manipulés ici sont ceux d'une $q$-expansion de forme modulaire. De même, `sensitivity_lean` et `mimo_lean` préparent la lecture des matrices, sommes finies, actions scalaires, additivité et homogénéité, mais **ne sont pas des dépendances Lean** de ce notebook. La cellule d'import charge réellement `Hecke.HeckeOperator`, et ce module importe directement `Mathlib.NumberTheory.ModularForms.SlashActions`. Aucun lien historique ou formel particulier avec Galois, Belyi ou la théorie de l'information n'est revendiqué à partir de cette seule proximité de vocabulaire.\n",
     "\n",

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb → MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-01-Descente-Budget-Lean-Python.ipynb

@@ -14,9 +14,9 @@
     "tags": []
    },
    "source": [
-    "# Lean-21c : Le budget de descente - quand la decroissance borne le nombre de flips\n",
+    "# MIMO-01 : Le budget de descente - quand la decroissance borne le nombre de flips\n",
     "\n",
-    "**Navigation** : [Index](README.md) | [Lean-21b (MIMO Converse) <<](Lean-21b-MIMO-Converse-Native.ipynb) | [Lean-22 (Galois) >>](Lean-22-Galois-Probleme-Inverse-M23.ipynb)\n",
+    "**Navigation** : [Index](README.md) | [<< Lean-20 (Capstone Tao)](../Lean-20-Capstone-Digestions-Tao-Python.ipynb) | [MIMO-02 (Detection Flips) >>](MIMO-02-Detection-Flips-Lean-Python.ipynb)\n",
     "\n",
     "Ce notebook presente le lake **`mimo_lean`** sur un theoreme sous-estime : `descent_target_before_ceiling` (fichier `Descent.lean`). Sous trois hypotheses tres explicites - *decroissance stricte du cout*, *confinement dans une barriere*, *absence de point bloquant hors cible* - toute trajectoire terminale **atteint sa cible avant un plafond `M_N` de flips**. Ce n'est pas un theoreme d'optimalite ; c'est une **garantie de terminaison**.\n",
     "\n",
@@ -2120,10 +2120,10 @@
     "- **D. Papailiopoulos** (2026) - *Detection MIMO by coordinate flips : Proposition 9.1* (papier source des theoremes `Descent.lean`).\n",
     "- **`Descent.lean`** (`MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/`) - la formalisation : `Run` (inductif sur List sigma), `lastState`, lemmes 1-3 (`run_tail_cost_lt`, `run_nodup`, `run_length_le_cost`), `descent_flips_le_barrier`, `descent_target_before_ceiling`. Aucun `sorry`, aucun `axiom NAME := ...` global, aucun `native_decide`.\n",
     "- **`lean4-wsl` kernel** - Repare c.380, valide c.426, reutilise pour ce notebook (le pattern << lecture directe des sources >> permet l'execution Python portable sans `lake env lean`).\n",
-    "- **Notebooks Lean associes** : `[Lean-24 (Calibration)](Lean-24-Calibration-Native-Companion.ipynb)`, `[Lean-23 (ERC-20)](Lean-23-ERC20-Invariant-Companion.ipynb)`, `[Lean-22 (Galois)](Lean-22-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-21 (MIMO)](Lean-21-MIMO-Detection-Flips.ipynb)`, `[Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb)`.\n",
+    "- **Notebooks Lean associes** : `[Lean-24 (Calibration)](../Lean-24-Calibration-Native-Companion.ipynb)`, `[Lean-23 (ERC-20)](../Lean-23-ERC20-Invariant-Companion.ipynb)`, `[Lean-22 (Galois)](../Lean-22-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-21 (MIMO)](MIMO-02-Detection-Flips-Lean-Python.ipynb)`, `[Lean-20 (PFR)](../ANALYSE/ANALYSE-03-PFR-Lean.ipynb)`.\n",
     "- **EPIC #4980** - convention i18n Lean (lac `mimo_lean` est FR-only ; un sibling pair `_en.lean` est une suite a explorer mais hors scope de ce notebook).\n",
     "- **Regle C.1** - pas d'erreur volontaire dans les cellules d'exercice (stub `pass` ou `print(\"Exercice a completer\")`).\n",
-    "- **Regle C.7 (count_code_sorry)** - l'instrument canonique `scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`), jamais `grep -c sorry`. Cf [anti-regression.md](../../../.claude/rules/anti-regression.md)."
+    "- **Regle C.7 (count_code_sorry)** - l'instrument canonique `scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`), jamais `grep -c sorry`. Cf [anti-regression.md](../../../../.claude/rules/anti-regression.md)."
    ]
   }
  ],
@@ -2151,13 +2151,13 @@
    "end_time": "2026-10-08T19:43:36.553099+00:00",
    "environment_variables": {},
    "exception": null,
-   "input_path": "Lean-21c-Descente-Budget.ipynb",
-   "output_path": "Lean-21c-Descente-Budget.ipynb",
+   "input_path": "MIMO-01-Descente-Budget-Lean-Python.ipynb",
+   "output_path": "MIMO-01-Descente-Budget-Lean-Python.ipynb",
    "parameters": {},
    "start_time": "2026-10-08T19:43:32.305668+00:00",
    "version": "2.7.0"
   }
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}