enrich(gametheory,#13410): densite Lean natif 17c/06g/08d — lectures de sorties (tranche markdown)

MyIA.AI.Notebooks/GameTheory/GameTheory-06g-Bounded-Agents-Lean.ipynb

@@ -147,6 +147,19 @@
    ],
    "outputs": []
   },
+  {
+   "cell_type": "markdown",
+   "id": "aad86956",
+   "metadata": {
+    "papermill": {},
+    "tags": []
+   },
+   "source": [
+    "### Ce que la cellule vérifie : la paire, le profil, le témoin négatif\n",
+    "\n",
+    "La cellule mobilise trois niveaux. Les deux `#check` nomment les **preuves universelles** — `cooperate_cooperate`, `mirror_mirror` : des théorèmes sur toute paire d'arguments, pas sur un cas particulier. Les `#reduce` du milieu restreignent à des **entrées concrètes** : `mutualCooperationCheck cooperateBot cooperateBot` réduit à la forme normale — le profil joué par la paire — et la ligne miroir fait de même. Le dernier `#reduce` installe un **témoin négatif** : la référence commentée exige que `defect_defect` retourne `(defect, defect)`, pas `(cooperate, cooperate)` — un diagnostic visible si le module confondait les profils. Le couple preuve-universelle / organe booléen posé par l'en-tête est à l'œuvre dès la première famille."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "g06g-md",
@@ -190,6 +203,19 @@
    ],
    "outputs": []
   },
+  {
+   "cell_type": "markdown",
+   "id": "79bcb52e",
+   "metadata": {
+    "papermill": {},
+    "tags": []
+   },
+   "source": [
+    "### L'inexploitation en deux registres, sur la famille témoin\n",
+    "\n",
+    "Même structure que la famille 1 : deux théorèmes (`defectBotBounded_unexploitable`, `mirror_basicFamily_unexploitable`) et deux réductions sur des entrées concrètes. L'entrée typique de l'organe est un **couple (adversaire, famille)** : `unexploitableCheck defectBotBounded basicFamily` demande s'il existe, dans la famille donnée, un programme qui exploite le bot testé — le `Bool` rend la réponse computationnelle. La cohérence entre l'organe et la propriété universelle n'est pas une affaire de foi : la conclusion du notebook la rappelle famille par famille, et l'exercice 3 testera la fragilité du couple quand la famille s'étend."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "g06g-md",
@@ -237,6 +263,19 @@
    ],
    "outputs": []
   },
+  {
+   "cell_type": "markdown",
+   "id": "8ccc816f",
+   "metadata": {
+    "papermill": {},
+    "tags": []
+   },
+   "source": [
+    "### Nash borné : un profil candidat, un organe, une équivalence prouvée\n",
+    "\n",
+    "La famille 3 pose la question de l'équilibre dans le cadre borné. Les `#check` nomment la propriété universelle (`defect_profile_programNash`) et l'équivalence qui la relie à l'organe décidable (`programNashCheck_eq_true`) ; le `#reduce` du milieu teste le **profil candidat** — `(defectBotBounded, defectBotBounded)` — sur la famille témoin via `programNashCheck basicFamily`. Le point conceptuel est préparé par la famille suivante : le classement `payoffRank` des paiements canoniques est ce qui rend une déviation profitable *détectable* — sans ordre fini sur les gains, pas de Nash décidable à budget borné."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "g06g-md",
@@ -283,6 +322,19 @@
    ],
    "outputs": []
   },
+  {
+   "cell_type": "markdown",
+   "id": "6e3071f2",
+   "metadata": {
+    "papermill": {},
+    "tags": []
+   },
+   "source": [
+    "### L'ordre fini des gains : la graduation qui rend le Nash décidable\n",
+    "\n",
+    "`payoffRank_le_iff` formalise le classement des issues du dilemme ; les `#reduce` de la cellule visent le **paramétrage canonique** posé par l'en-tête (`canonicalPD`, valeurs T, R, P, S — 5, 3, 1, 0). L'intérêt du rang est d'être un ordre **total fini** : chaque sortie de partie a une position, deux gains quelconques sont comparables, et la comparaison se réduit algorithmiquement — c'est la graduation qui rend le Nash décidable sur les entrées bornées du module, là où une quantification sur des paiements non ordonnés resterait hors d'atteinte du `reduce`."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "g06g-md",
@@ -371,6 +423,19 @@
    ],
    "outputs": []
   },
+  {
+   "cell_type": "markdown",
+   "id": "b739c427",
+   "metadata": {
+    "papermill": {},
+    "tags": []
+   },
+   "source": [
+    "### L'exercice 2 : le miroir à budget nul, bascule en défection\n",
+    "\n",
+    "Le constructeur est le point d'attention : `⟨.mirror, 0⟩` assemble un programme — le miroir qui répond à la dernière action adverse — avec un budget **nul**. La consigne de la section attend la vérification que ce bot se comporte comme `defectBotBounded` : sans budget, le miroir ne peut refléter la moindre action, et son jeu coïncide avec la défection systématique. La cellule dispose du bon instrument — `#reduce outcomeBounded mirrorBudget0 cooperateBot` et ses deux variantes contre `defectBotBounded` puis `mirrorBot` : l'issue de chaque paire est un terme qui se réduit, la comparaison des trois profils départage la lecture. La conclusion B du notebook annonce la bascule ; l'exercice la fait constater à l'exécution."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "g06g-md",
@@ -414,6 +479,19 @@
    ],
    "outputs": []
   },
+  {
+   "cell_type": "markdown",
+   "id": "db179310",
+   "metadata": {
+    "papermill": {},
+    "tags": []
+   },
+   "source": [
+    "### L'exercice 3 : étendre la famille, re-scanner l'inexploitabilité\n",
+    "\n",
+    "Le geste est minimal : `basicFamily ++ [cooperateBudget, mirrorBudget0]` — une liste, deux ajouts — et toute la question se repose. Les trois `#reduce` relancent `unexploitableCheck` sur la famille étendue contre les trois bots témoins. La conclusion C du notebook annonce la leçon : l'inexploitabilité est **fragile** à l'ajout d'un bot miroir à budget nul — un théorème universel (le miroir n'exploite personne dans `basicFamily`) et un fait booléen peuvent diverger dès qu'une entrée nouvelle entre dans le domaine. C'est le sens du couple preuve/organe : l'organe ne s'étend pas automatiquement, il se **re-réduit**."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "g06g-md",

MyIA.AI.Notebooks/GameTheory/GameTheory-08d-Lean-CGT-Native.ipynb

@@ -227,6 +227,19 @@
     "#check IGame.Impartial.grundy   -- la valeur de Grundy d'un jeu impartial"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "79451af0",
+   "metadata": {
+    "papermill": {},
+    "tags": []
+   },
+   "source": [
+    "### Lecture de l'import : le périmètre du lake en seize lignes\n",
+    "\n",
+    "La cellule d'import est une cartographie : **seize** `import` énumèrent le périmètre exact de la visite. Les trois couches de la section 2 y sont déjà — `Game.Basic` (les pré-jeux), `Game.Order` et `Game.Canonical` (l'ordre de Conway et les formes normales), `Game.Player` ; les surréels avec leur arithmétique complète (`Surreal.Basic`, `Multiplication`, `Division`, `Dyadic`, `Ordinal`) ; les nimbers (`Nimber.Basic`, `Nimber.Field`) ; le théorème de Sprague-Grundy (`Game.Impartial.Grundy`) ; deux jeux concrets pour les exercices (`Specific.Nim`, `Specific.Domineering`) — et `CGTTour`, le module de visite du lake. Les trois `#check` alignent les repères : `IGame` (concret), `Game` (quotient), `grundy` (valeur) — le plan du notebook tient dans ces trois signatures."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "ccb43730",
@@ -519,7 +532,14 @@
     "Les surreals portent les operations completes d'un corps (multiplication dans\n",
     "`Surreal.Multiplication`, division dans `Surreal.Division`), et deux familles\n",
     "concretes s'y plongent : les rationnels dyadiques (exactement les surreals\n",
-    "d'anniversaire fini) et les ordinaux."
+    "d'anniversaire fini) et les ordinaux.\n",
+    "La signature exacte de `equiv_of_forall_not_fits` mérite une lecture ligne à ligne :\n",
+    "\n",
+    "```\n",
+    "∀ {x y : IGame} [x.Numeric], x.Fits y → (∀ (p : Player), ∀ z ∈ IGame.moves p x, ¬z.Fits y) → x ≈ y\n",
+    "```\n",
+    "\n",
+    "Deux détails font le théorème. La quantification `∀ (p : Player)` porte sur les **deux** joueurs : la simplicité exige que la borne tienne pour les options de Gauche *et* de Droite — rien d'étonnant pour des jeux partizans, tout se joue dans l'absence d'option qui « tient » d'un côté ou de l'autre. Et la conclusion est une équivalence de jeux `x ≈ y`, pas une égalité point par point : la simplicité identifie les **valeurs**, quitte à ce que les arbres diffèrent."
    ]
   },
   {
@@ -646,7 +666,8 @@
     "\n",
     "Les nimbers sont des ordinaux munis de l'arithmetique de nim : `∗o` designe\n",
     "`Nimber.of o`. L'addition de nim est le **mex** (minimum exclus) des sommes des\n",
-    "options — pour deux tas de Nim, c'est le XOR familier de la strategie de 8b."
+    "options — pour deux tas de Nim, c'est le XOR familier de la strategie de 8b.\n",
+    "La cellule affiche trois plongements, et chacun a son type précis. `inferInstance : CommRing Surreal` — pas une déclaration, une **résolution** : le solver de classes trouve l'anneau commutatif sans que l'appel n'en dise plus ; c'est le prix d'entrée de l'usage « corps » de la section 4. `Dyadic.toIGame : Dyadic → IGame` — le rationnel dyadique entre d'abord comme **jeu** (production d'options) ; il ne devient « nombre » qu'à travers le quotient de la section 3. `NatOrdinal.toSurreal : NatOrdinal ↪o Surreal` — le symbole `↪o` désigne un plongement d'**ordre préservant** : l'ordre ordinal (omega plus grand que tous les finis) survit au transfert, alors qu'une simple fonction aurait pu l'aplatir. La hiérarchie est visible dans les types — Dyadic vers *IGame*, NatOrdinal vers *Surreal* : les dyadiques sont des jeux d'abord, les ordinaux des surréels d'emblée."
    ]
   },
   {
@@ -777,7 +798,14 @@
     "Le notebook 8b esquisait la strategie gagnante du Nim multi-tas par le XOR des\n",
     "tailles. La forme generale — **tout jeu impartial est equivalent au nim de sa\n",
     "valeur de Grundy** — est ici un theoreme ferme de la dependance\n",
-    "(`CombinatorialGames.Game.Impartial.Grundy`) :"
+    "(`CombinatorialGames.Game.Impartial.Grundy`) :\n",
+    "La définition de l'addition de nim est visible dans la première signature :\n",
+    "\n",
+    "```\n",
+    "a + b = sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ\n",
+    "```\n",
+    "\n",
+    "C'est le **mex** écrit en logique : l'ensemble entre accolades énumère les valeurs atteignables en déplaçant un tas (côté `a` ou côté `b`), le complémentaire `ᶜ` retire ces valeurs, et `sInf` prend le plus petit élément du reste — le minimum exclu. La seconde signature est la réciproque indispensable : `exists_of_lt_add` garantit que **toute** valeur strictement inférieure à `a + b` est atteinte d'un côté ou de l'autre — aucune lacune entre les valeurs exclues, ce qui distingue précisément le mex d'un simple « plus petit qui tombe ». Sans elle, deux sommes différentes pourraient partager leur borne ; avec elle, l'addition est une fonction bien définie, et `Field Nimber` (caractéristique 2 : chaque élément est son propre opposé) a un sens algébrique plein."
    ]
   },
   {
@@ -938,7 +966,8 @@
     "## 6. Exercices\n",
     "\n",
     "Les trois exercices suivent la convention du depot : le notebook s'execute de\n",
-    "bout en bout meme non complete (C.1). Decommentez la commande, executez, lisez.\n"
+    "bout en bout meme non complete (C.1). Decommentez la commande, executez, lisez.\n",
+    "Complétons la lecture : la sortie de la cellule aligne **cinq** signatures, et les deux premières font la chaîne. `IGame.nim : Nimber → IGame` — chaque nimber fournit le jeu « un tas de cette taille » : le point d'entrée matériel de la théorie. `IGame.Impartial.grundy : (x : IGame) → [x.Impartial] → Nimber` — la valeur de Grundy est une fonction **totale** sur les jeux impartiaux, la classe implicite `[x.Impartial]` en conditionnant la définition. Les trois signatures suivantes montent la chaîne : construire le tas équivalent (`nim_grundy_equiv`), composer les tas (`nim_add_equiv` — le XOR de la stratégie de 8b comme *équivalence de jeux*), tester les P-positions (`grundy_eq_zero_iff`). Le bundle vaut par son ordre : chaque théorème suppose le précédent, et la cellule les vérifie tous d'une traite."
    ]
   },
   {
@@ -1211,6 +1240,19 @@
     "example : True := trivial    -- cellule neutre tant que la solution est commentee"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "432d01cb",
+   "metadata": {
+    "papermill": {},
+    "tags": []
+   },
+   "source": [
+    "### Exercices : trois questions, trois lectures\n",
+    "\n",
+    "Les trois cellules d'exercice committent la **cellule neutre** — `example : True := trivial` reste la seule ligne active tant que la solution est commentée (règle C.1 du dépôt) : le notebook s'exécute de bout en bout même incomplet. L'exercice 1 interroge la **base d'axiomes** de Sprague-Grundy — la consigne annonce le triplet standard `[propext, Classical.choice, Quot.sound]` et l'absence de `sorryAx`, la section 7 le confirmera en affichant exactement ce triplet. L'exercice 2 joue sur l'asymétrie : `IGame.Domineering.left` contre `right` — les dominos verticaux ou horizontaux — et l'indice souligne que, contrairement au Nim, Domineering est **partizan** : c'est exactement pour cela que la forme normale de Conway tient deux ensembles d'options. L'exercice 3 relie l'**anniversaire** à la profondeur de l'arbre : le nim à un tas a exactement l'anniversaire de sa taille, le jeu le plus simple de cet anniversaire."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "cgt-tour-intro",
@@ -1356,7 +1398,8 @@
     "chaîne de preuve traverse CombinatorialGames sans `sorryAx` ni\n",
     "`native_decide`. La promesse de la section 1 est maintenant littéralement\n",
     "tenue : ce notebook importe et exécute le module de visite depuis les\n",
-    "oleans du lake."
+    "oleans du lake.\n",
+    "Le croisement avec le notebook 17c (le marché des lemons) fait ressortir ce que l'empreinte ne dit pas d'elle-même. Là-bas, `#print axioms poolingTenable_iff_cross` répond `[propext, Quot.sound]` — **deux** axiomes, sans `Classical.choice` : le marché à deux qualités est fini, tout y est décidable, aucun choix n'est nécessaire. Ici, les deux certificats de la cellule rendent le **triplet** complet, `Classical.choice` en plus. La lecture : la théorie combinatoire des jeux quotiente des objets dont les options sont des ensembles (potentiellement infinis) et raisonne sur des `sInf` — le choix garantit que ces bornes existent. L'empreinte axiomatique est un instrument de diagnostic : elle ne mesure pas la difficulté d'une preuve, elle dit exactement quels principes elle mobilise."
    ]
   },
   {
@@ -1392,7 +1435,8 @@
     "(lecture guidee en .lean), le depot upstream\n",
     "[vihdzp/combinatorial-games](https://github.com/vihdzp/combinatorial-games),\n",
     "et Conway, *On Numbers and Games* (2001), chapitres 7-8 pour la theorie de\n",
-    "Grundy.\n"
+    "Grundy.\n",
+    "La visite comptée : **dix** cellules de code exécutées (`execution_count` de 1 à 10), un import de **seize** modules puis `CGTTour`, **cinq** signatures Sprague-Grundy dans une seule sortie, **deux** certificats d'axiomes, **trois** exercices en cellule neutre, deux familles de plongements (dyadiques, ordinaux). Le compagnon a fait exactement ce que `CGTTour` promettait : importer la théorie, la faire tourner sur les exemples, laisser le compilateur certifier la base axiomatique."
    ]
   }
  ],