fix(lean,#16979): REPAIR-3 morphologique map REACCENT (0 donne + 4 prouve fautifs)

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-25-Coherence-et-Temoin.ipynb

@@ -43,15 +43,7 @@
     "tags": []
    },
    "source": [
-    "## Les deux théorèmes, là où ils vivent\n",
-    "\n",
-    "| Fait | Énoncé | Où |\n",
-    "|---|---|---|\n",
-    "| Incohérence ⟹ Dutch Book | si $q(A)+q(B) \\neq q(A\\cap B)+q(A\\cup B)$, des mises sur les quatre tickets $(A, B, A\\cap B, A\\cup B)$ rapportent un gain **strictement positif dans chaque état** | `decision_theory_lean/Coherence/DutchBook.lean:64` — `non_additive_implies_dutch_book`, constructif |\n",
-    "| Cohérence ⟹ additivité | si aucun Dutch Book n'existe sur les quatre tickets, alors l'inclusion–exclusion tient | `Coherence/DutchBook.lean:94` — `coherent_on_implies_additive` (contraposée du premier) |\n",
-    "| Stabilité affine vNM | si $u$ représente $P$, toute $a\\cdot u+b$ ($a>0$) représente aussi $P$ | `Utility/Representation.lean:163` — `affine_rep_is_rep` |\n",
-    "\n",
-    "Le gain du livret de quatre tickets y est défini (`Coherence/DutchBook.lean:42`, `ieGain`) comme $s_A(\\mathbb{1}_A - q_A) + s_B(\\mathbb{1}_B - q_B) + s_{AB}(\\mathbb{1}_{A\\cap B} - q_{AB}) + s_{AU}(\\mathbb{1}_{A\\cup B} - q_{AU})$ — une mise $s$ **positive achète** le ticket (on paie $s\\cdot q$, on reçoit $s$ si l'événement se produit), une mise **négative le vend**. Le miroir Python ci-dessous reprend cette définition **mot pour mot**, en arithmétique exacte (`fractions.Fraction`) : ce que le lake prouvé pour tout $\\Omega$ fini, le notebook le **mesure** sur une instance — certificat sur l'énoncé, mesure sur l'instance, la dette de dérivation reste explicite."
+    "## Les deux théorèmes, là où ils vivent\n\n| Fait | Énoncé | Où |\n|---|---|---|\n| Incohérence ⟹ Dutch Book | si $q(A)+q(B) \\neq q(A\\cap B)+q(A\\cup B)$, des mises sur les quatre tickets $(A, B, A\\cap B, A\\cup B)$ rapportent un gain **strictement positif dans chaque état** | `decision_theory_lean/Coherence/DutchBook.lean:64` — `non_additive_implies_dutch_book`, constructif |\n| Cohérence ⟹ additivité | si aucun Dutch Book n'existe sur les quatre tickets, alors l'inclusion–exclusion tient | `Coherence/DutchBook.lean:94` — `coherent_on_implies_additive` (contraposée du premier) |\n| Stabilité affine vNM | si $u$ représente $P$, toute $a\\cdot u+b$ ($a>0$) représente aussi $P$ | `Utility/Representation.lean:163` — `affine_rep_is_rep` |\n\nLe gain du livret de quatre tickets y est défini (`Coherence/DutchBook.lean:42`, `ieGain`) comme $s_A(\\mathbb{1}_A - q_A) + s_B(\\mathbb{1}_B - q_B) + s_{AB}(\\mathbb{1}_{A\\cap B} - q_{AB}) + s_{AU}(\\mathbb{1}_{A\\cup B} - q_{AU})$ — une mise $s$ **positive achète** le ticket (on paie $s\\cdot q$, on reçoit $s$ si l'événement se produit), une mise **négative le vend**. Le miroir Python ci-dessous reprend cette définition **mot pour mot**, en arithmétique exacte (`fractions.Fraction`) : ce que le lake prouve pour tout $\\Omega$ fini, le notebook le **mesure** sur une instance — certificat sur l'énoncé, mesure sur l'instance, la dette de dérivation reste explicite."
    ]
   },
   {
@@ -329,17 +321,7 @@
     "tags": []
    },
    "source": [
-    "### Lecture : le témoin disparaît — et ce que le balayage ne prouvé pas\n",
-    "\n",
-    "Le même livret qui rapportait $1/4$ partout rapporte maintenant **exactement $0$ dans chacun des quatre états** : l'écart de prix a disparu, et la position combinée — neutre dès l'instant zéro — ne devient rien à l'échéance non plus. La machine à gagner est démontée, jusqu'à la dernière pièce. Et le balayage de $390{,}625$ combinaisons de mises ($25^4$) n'en trouve **aucune** qui refasse un livre. Mais il faut dire précisément ce que ce balayage établit : *aucun livre à mises entières bornées*. La propriété générale — *aucun livre du tout* — n'est pas énumérable (les mises réelles sont infinies) ; elle est **démontrée** dans le lake (`DutchBook.lean:94`). C'est la frontière exacte du partage de travail :\n",
-    "\n",
-    "| | Générateur Python | Certificat Lean |\n",
-    "|---|---|---|\n",
-    "| Ce qu'il fournit | le livre concret, les montants, l'instance | l'impossibilité générale |\n",
-    "| Portée | une instance de prix | toute violation / toute cohérence |\n",
-    "| Statut | **mesure** | **preuve** |\n",
-    "\n",
-    "Confondre les deux colonnes serait exactement l'erreur que ce notebook documente par ailleurs (une carte employée sans justification)."
+    "### Lecture : le témoin disparaît — et ce que le balayage ne prouve pas\n\nLe même livret qui rapportait $1/4$ partout rapporte maintenant **exactement $0$ dans chacun des quatre états** : l'écart de prix a disparu, et la position combinée — neutre dès l'instant zéro — ne devient rien à l'échéance non plus. La machine à gagner est démontée, jusqu'à la dernière pièce. Et le balayage de $390{,}625$ combinaisons de mises ($25^4$) n'en trouve **aucune** qui refasse un livre. Mais il faut dire précisément ce que ce balayage établit : *aucun livre à mises entières bornées*. La propriété générale — *aucun livre du tout* — n'est pas énumérable (les mises réelles sont infinies) ; elle est **démontrée** dans le lake (`DutchBook.lean:94`). C'est la frontière exacte du partage de travail :\n\n| | Générateur Python | Certificat Lean |\n|---|---|---|\n| Ce qu'il fournit | le livre concret, les montants, l'instance | l'impossibilité générale |\n| Portée | une instance de prix | toute violation / toute cohérence |\n| Statut | **mesure** | **preuve** |\n\nConfondre les deux colonnes serait exactement l'erreur que ce notebook documente par ailleurs (une carte employée sans justification)."
    ]
   },
   {
@@ -356,11 +338,7 @@
     "tags": []
    },
    "source": [
-    "## vNM — l'affine est enfin légitime\n",
-    "\n",
-    "Passons du côté des préférences. Le théorème de représentation de von Neumann–Morgenstern relie un ordre sur les loteries à une utilité espérée ; le lemme `affine_rep_is_rep` (`Utility/Representation.lean:163`) en prouvé la partie cardinale : si $u$ représente $P$, alors $a \\cdot u + b$ ($a > 0$) représente **aussi** $P$ — car $E_p[a\\,u+b] = a\\,E_p[u] + b$, et une affine croissante préserve l'ordre.\n",
-    "\n",
-    "**Ce que le lemme légitime** : changer l'origine ($b$) et l'unité ($a$) d'une échelle d'utilité — température en Celsius ou Fahrenheit, utilité en points ou en dizaines. **Ce qu'il ne légitime pas** : toute autre forme. Le test suivant est une **discrimination expérimentale** : sur les 66 loteries simples d'un simplex à pas $1/10$ (toutes les $(p_1,p_2,p_3)$ entières sur dixièmes), on compare les ordres induits par $u$, par $v = 3u+2$ (affine), et par $w = u^2$ (non affine)."
+    "## vNM — l'affine est enfin légitime\n\nPassons du côté des préférences. Le théorème de représentation de von Neumann–Morgenstern relie un ordre sur les loteries à une utilité espérée ; le lemme `affine_rep_is_rep` (`Utility/Representation.lean:163`) en prouve la partie cardinale : si $u$ représente $P$, alors $a \\cdot u + b$ ($a > 0$) représente **aussi** $P$ — car $E_p[a\\,u+b] = a\\,E_p[u] + b$, et une affine croissante préserve l'ordre.\n\n**Ce que le lemme légitime** : changer l'origine ($b$) et l'unité ($a$) d'une échelle d'utilité — température en Celsius ou Fahrenheit, utilité en points ou en dizaines. **Ce qu'il ne légitime pas** : toute autre forme. Le test suivant est une **discrimination expérimentale** : sur les 66 loteries simples d'un simplex à pas $1/10$ (toutes les $(p_1,p_2,p_3)$ entières sur dixièmes), on compare les ordres induits par $u$, par $v = 3u+2$ (affine), et par $w = u^2$ (non affine)."
    ]
   },
   {
@@ -449,11 +427,7 @@
     "tags": []
    },
    "source": [
-    "### Lecture de l'invariance : zéro divergence — la carte affine est inoffensive\n",
-    "\n",
-    "Sur les $2\\,145$ paires de loteries, l'ordre induit par $u$ et celui induit par $v = 3u+2$ **coïncident exactement** : zéro divergence. C'est la mesure de l'invariance que `affine_rep_is_rep` prouvé en général — sur cette instance, elle est parfaite. Aucune décision, aucun classement, aucune préférence ne bouge quand on recarde l'échelle d'utilité par une affine positive : la carte $u \\mapsto 3u+2$ est **légitime**, et le lemme dit *pourquoi* — l'espérance se transforme en $E_p[3u+2] = 3E_p[u]+2$, et $x \\mapsto 3x+2$ est croissante sur $\\mathbb{R}$.\n",
-    "\n",
-    "Le carré, lui, diverge. Les deux cellules suivantes exhibent **les deux défauts** : une paire **indifférente** sous $u$ mais strictement ordonnée sous $w$ (le carré fabrique des préférences là où il n'y en avait pas), et une paire dont l'ordre **s'inverse** carrément."
+    "### Lecture de l'invariance : zéro divergence — la carte affine est inoffensive\n\nSur les $2\\,145$ paires de loteries, l'ordre induit par $u$ et celui induit par $v = 3u+2$ **coïncident exactement** : zéro divergence. C'est la mesure de l'invariance que `affine_rep_is_rep` prouve en général — sur cette instance, elle est parfaite. Aucune décision, aucun classement, aucune préférence ne bouge quand on recarde l'échelle d'utilité par une affine positive : la carte $u \\mapsto 3u+2$ est **légitime**, et le lemme dit *pourquoi* — l'espérance se transforme en $E_p[3u+2] = 3E_p[u]+2$, et $x \\mapsto 3x+2$ est croissante sur $\\mathbb{R}$.\n\nLe carré, lui, diverge. Les deux cellules suivantes exhibent **les deux défauts** : une paire **indifférente** sous $u$ mais strictement ordonnée sous $w$ (le carré fabrique des préférences là où il n'y en avait pas), et une paire dont l'ordre **s'inverse** carrément."
    ]
   },
   {