diff --git a/MyIA.AI.Notebooks/GameTheory/GameTheory-06g-Bounded-Agents-Lean.ipynb b/MyIA.AI.Notebooks/GameTheory/GameTheory-06g-Bounded-Agents-Lean.ipynb index 72ceef4a03..6d702f74e2 100644 --- a/MyIA.AI.Notebooks/GameTheory/GameTheory-06g-Bounded-Agents-Lean.ipynb +++ b/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", diff --git a/MyIA.AI.Notebooks/GameTheory/GameTheory-08d-Lean-CGT-Native.ipynb b/MyIA.AI.Notebooks/GameTheory/GameTheory-08d-Lean-CGT-Native.ipynb index 3ca732d96b..ead495f4dd 100644 --- a/MyIA.AI.Notebooks/GameTheory/GameTheory-08d-Lean-CGT-Native.ipynb +++ b/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." ] } ], diff --git a/MyIA.AI.Notebooks/GameTheory/GameTheory-17c-Lean-Lemons-Certificat.ipynb b/MyIA.AI.Notebooks/GameTheory/GameTheory-17c-Lean-Lemons-Certificat.ipynb index ae13e54b57..500f62e274 100644 --- a/MyIA.AI.Notebooks/GameTheory/GameTheory-17c-Lean-Lemons-Certificat.ipynb +++ b/MyIA.AI.Notebooks/GameTheory/GameTheory-17c-Lean-Lemons-Certificat.ipynb @@ -609,6 +609,19 @@ "example : ¬ poolingTenable marche prior50 := by decide" ] }, + { + "cell_type": "markdown", + "id": "8790cb6a", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture — trois prédicats d'une même signature\n", + "\n", + "La sortie aligne les trois régimes du marché comme trois prédicats de **même signature** : `poolingTenable`, `lemonsOnlyPossible`, `noTrade` prennent tous un marché et un prior et rendent une `Prop`. Le lexique est complet dès le départ : les trois états que la suite distinguera (pooling tenable, marché réduit aux lemons, interdiction d'échanger) sont des **propositions**, pas des valeurs — c'est le notebook qui prouvera chaque instance. Les deux `example` qui suivent montrent le registre « preuve » sur le marché canonique : l'exemple (a) du module est re-prouvé **en direct** (témoin `P = 0`, `S(0) = [low]`, `E = 0`) et l'exemple (d) — pooling mort à `pi = 50` — est clos par `decide`. Les cellules suivantes citeront encore (e), (f), (g) : le notebook re-prouve les exemples du module un par un au lieu de les admettre." + ] + }, { "cell_type": "markdown", "id": "febdc602", @@ -840,6 +853,19 @@ "example : poolingTenable marcheSeuil ⟨75, by decide⟩ := by decide" ] }, + { + "cell_type": "markdown", + "id": "fb98f728", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Ce que la sortie ne dit pas : la preuve par le silence\n", + "\n", + "Dans la sortie de la cellule, le contraste est instructif : le `#eval poolingThresholdNum marcheSeuil` imprime `─────▶ 3000`, et les deux `example` qui suivent — `¬ poolingTenable ... ⟨74⟩` puis `poolingTenable ... ⟨75⟩` — n'impriment **rien du tout**. Ce silence est le succès : en Lean, une preuve publiée ne produit aucun message ; seul son échec afficherait une erreur. Le fichier brut de la sortie le confirme — un seul message `data: \"3000\"`, aucun pour les deux exemples. La falaise que le balayage mesurera (74 casse, 75 tient) est ici **décidée** par le kernel à chaque exécution : contrairement à une table pré-calculée, les deux lignes ne peuvent pas vieillir séparément." + ] + }, { "cell_type": "markdown", "id": "b6caf6a4", @@ -1275,6 +1301,19 @@ "#eval demoSpiral marcheMort prior50 (demoPrixInitial marcheMort 50)" ] }, + { + "cell_type": "markdown", + "id": "8bcfc94c", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Anatomie de la spirale : trois mécanismes, zéro surprise\n", + "\n", + "`demoSpiral` montre mieux que sa table ce que le certificat délimite. Trois détails de la cellule sont à lire. **(1) Le point fixe est un test d'égalité** — `if e = P` arrête la boucle quand le prix n'évolue plus : la spirale n'a pas besoin de savoir *pourquoi* elle s'arrête, seule la coïncidence des deux nombres l'intéresse. **(2) Le carburant** — `fuel` plafonne à 8 étapes : la simulation est bornée, le théorème ne l'est pas, et c'est le partage de travail honnête annoncé par la section précédente. **(3) La reconstruction** — `acc.reverse` remet la liste dans l'ordre chronologique après accumulation à l'envers. Sur les trois marchés, le prix **initial** est le même — `P₀ = 2`, l'anticipation où l'acheteur paie comme si les deux types restaient — et les spirales divergent ensuite : `[(2, 2)]` pour le marché tenable, `[(2, 0), (0, 0)]` pour les deux autres. La même donnée de départ, trois destins : c'est la copie visible de ce que `poolingTenable_iff_cross` prévoyait à l'avance." + ] + }, { "cell_type": "markdown", "id": "b096f462", @@ -1678,6 +1717,19 @@ "#check poolingTenable_mono\n" ] }, + { + "cell_type": "markdown", + "id": "7aa45e57", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Les trois exercices : une échelle, trois gestes\n", + "\n", + "Les trois stubs forment une progression. **Exercice 1** — marché `(1, 12, 2, 10)` : le coût de la haute qualité (12) excède sa valeur (10) ; aucun prior ne peut sauver le pooling, et la question finale du commentaire demande exactement cette lecture `c_H > v_H`. **Exercice 2** — marché `(3, 5, 1, 4)` : le coût de la basse qualité (3) excède sa valeur (1) — `v_L < c_L` — le marché construit est **no-trade** ; la dernière question demande d'y répondre *en utilisant l'exercice 1* : `c_H = 5 > v_H = 4`, le marché n'est tenable à aucun prior. L'échelle est explicite : l'exercice 2 se résout par l'insight de l'exercice 1. **Exercice 3** — bascule de registre : on ne construit plus rien, on **réutilise** — l'exemple (f) (pooling à 75) est monté à 90 par `poolingTenable_mono` ; la preuve du seuil n'est pas refaite, elle est importée. Définir, inférer, réutiliser : les trois gestes du certificat." + ] + }, { "cell_type": "markdown", "id": "cfd3ec06",