fix(ml,#17692): 2.9e-MIPS -- la Conclusion realignee sur le paragraphe 4 execute

MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9e-MIPS-Extraction-Programme.ipynb

@@ -2161,24 +2161,25 @@
     "| La machinerie d'extraction est correcte | les 24 assignations essayées, **ripple-carry adder** retrouvé, vérifié 4096/4096 |\n",
     "| La taille minimale explique la tâche | `prev2` : $n_{\\min} = 3 = k+1$ (Table 2 du papier) |\n",
     "| Un mode d'échec est structurel | `sum_last5` : sortie entière (6 valeurs) → chemin booléen fermé |\n",
+    "| **La chaîne Jordan → Toeplitz → de-bias est reproduite** | banc affine : 7 états, 0 conflit · réseau entraîné : one-hot à l'identique, 5 conflits à $\\epsilon = 0{,}1$ |\n",
     "\n",
     "### Les trois idées à retenir\n",
     "\n",
     "1. **La lisibilité se construit, elle ne se constate pas.** Les poids d'un réseau entraîné ne sont pas un texte. Il faut choisir une base (normalisateurs), un encodage (autoencodeur), une famille de formules (régression) — et chaque choix est un levier sur ce qu'on peut lire.\n",
-    "2. **Un réseau exact peut être illisible.** Le nôtre additionne parfaitement et ne se lit pas : il transporte l'historique entier au lieu de la seule retenue. La difficulté de MIPS n'est pas la lecture, c'est la **représentation** — ce que le papier traite par son AutoML de simplicité et sa chaîne de normalisateurs, et qui reste ici mesuré mais non reproduit.\n",
+    "2. **Un réseau exact peut être illisible.** Le nôtre additionne parfaitement et ne se lit pas : il transporte l'historique entier au lieu de la seule retenue. La difficulté de MIPS n'est pas la lecture, c'est la **représentation** — ce que le papier traite par son AutoML de simplicité et sa chaîne de normalisateurs, dont la chaîne est désormais **reproduite et mesurée** au §4. La reproduire ne suffit pas : elle aligne le lattice du réseau entraîné sans lui rendre l'affinité qui lui manque.\n",
     "3. **Un programme extrait se prouve.** Le livrable n'est pas une explication plausible, c'est un programme exécutable vérifié sur toutes les entrées. C'est la différence entre raconter une histoire et établir un fait.\n",
     "\n",
     "### Ce que ce notebook ne fait pas — et pourquoi\n",
     "\n",
     "Trois périmètres sont laissés de côté, nommés ici plutôt que passés sous silence :\n",
     "\n",
-    "1. **La chaîne complète des normalisateurs** (Jordan → Toeplitz → de-bias). Le §4 en mesure la nécessité et n'en implémente qu'un sur cinq (le blanchiment). C'est le principal écart avec le papier, et le §3 en donne la raison : sans état minimal à aligner, il n'y a pas de lattice à redresser. Les deux mécanismes vont ensemble — c'est le chaînon à refermer en premier.\n",
+    "1. **Le passage du réseau entraîné à une machine à états minimale.** La chaîne Jordan → Toeplitz → de-bias n'est plus le manque : elle est **implémentée et exécutée** au §4, et ses deux régimes sont mesurés. Sur un banc exactement affine, elle referme la boucle du réseau au programme — $W$ devient le bloc nilpotent du registre à décalage, et la machine quantifiée tient en 7 états sans conflit. Sur le réseau entraîné, elle aligne la géométrie (colonne génératrice one-hot à l'identique, $\\|MB - BM\\| = 0$) mais laisse 5 conflits à $\\epsilon = 0{,}1$ — le prix du résidu affine de 28,7 % mesuré en §4. Ce qui reste hors périmètre est donc **l'application de la chaîne au réseau du §3 jusqu'à la machine minimale** : les normalisateurs alignent le lattice, ils ne fabriquent pas l'affinité que le réseau n'a pas.\n",
     "2. **La tâche « Newton »** (loi de Newton avec ressort / champ magnétique), proposée par l'issue d'origine. Elle produit une sortie **continue**, donc elle relève de l'autoencodeur **entier** (App. A/B) que notre essai de lattice finder n'a pas su faire fonctionner faute de structure affine (§4). Le §7 montre exactement ce mode d'échec sur `sum_last5`, et l'exercice 1 est le point d'entrée pour le reprendre.\n",
     "3. **La vérification formelle** du programme extrait : le papier la fait en Dafny (App. F.1). Ici la vérification est **exhaustive sur les 4096 entrées** — plus faible qu'une preuve, plus forte qu'un échantillon. C'est le pont vers T10 qui reste à construire.\n",
     "\n",
     "> **Pistes pour la suite :**\n",
     "\n",
-    "- **Reproduire la chaîne complète** (Jordan → Toeplitz → de-bias → quantification des poids) pour transformer le réseau du §3 en machine à états minimale, et refermer le maillon manquant.\n",
+    "- **Refermer le maillon restant** : la chaîne est reproduite au §4 ; ce qui manque n'est plus la normalisation mais un état **exactement affine** — ou une quantification des poids — pour que la machine à états minimale se ferme sur le réseau du §3 comme elle se ferme sur le banc de contrôle.\n",
     "- **Reprendre l'autoencodeur entier** (App. A/B) : notre essai de lattice finder a échoué faute de structure affine, ce qui est cohérent avec le §4 et demande la normalisation complète.\n",
     "- Le papier ([arXiv:2402.05110](https://arxiv.org/abs/2402.05110)) et son code : `ejmichaud/neural-verification`.\n",
     "- La suite de l'arc : la vérification formelle du programme extrait (App. F.1 du papier, en Dafny) rejoint la sous-série Lean du dépôt — le pont **extraire → prouver**.\n",