Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -127,6 +127,14 @@
""
]
},
{
"cell_type": "markdown",
"id": "d2ccce31",
"metadata": {},
"source": [
"**Lecture de la sortie — la famille temoin et ses budgets.** Trois lignes suffisent a poser le decor : `BoundedAgent(COOPERATE_BOT, budget=0)`, `BoundedAgent(DEFECT_BOT, budget=0)`, `BoundedAgent(MIRROR, budget=1)`. Les deux bots vivent a budget nul — leur decision ne regarde ni l'historique ni l'adversaire, aucune memoire a payer. Le miroir seul porte `budget=1` : relire le dernier coup adverse coute exactement une unite, et c'est ce cout qui distinguera le miroir riche (b=1, il reflete) du miroir casse (b=0, l'exercice 1 y viendra) — la meme ligne de code, deux comportements selon un seul entier. Toute la question du notebook est deja la : que reste-t-il du jeu quand la lecture a un prix ?\n"
]
},
{
"cell_type": "markdown",
"id": "9747637e",
Expand Down Expand Up @@ -202,6 +210,14 @@
""
]
},
{
"cell_type": "markdown",
"id": "c53c2795",
"metadata": {},
"source": [
"**Lecture chiffree — les issues bornees, ligne par ligne.** La sortie egraine `outcome_bounded` sur chaque paire. Les lignes COOPERATE_BOT : `(cooperate, cooperate)` contre son semblable, `(cooperate, defect)` contre DEFECT_BOT — le coopereur ne s'adapte pas, il subit. Les lignes DEFECT_BOT font le symetrique : `(defect, cooperate)` puis `(defect, defect)`. La ligne qui instruit est la troisieme colonne : contre `MIRROR b=1`, COOPERATE_BOT obtient `('cooperate', 'cooperate')` — le miroir ouvre sur la cooperation, lit coop, et la boucle reste bloquee dessus ; DEFECT_BOT contre le miroir obtient la paire symetrique de defection : le miroir lit `defect` et le renvoie. Deux bots a budget nul ont des issues independantes du budget ; le miroir a b=1 est le seul dont l'issue depende de ce qu'il a pu lire — la famille temoin deliberate ce contraste.\n"
]
},
{
"cell_type": "markdown",
"id": "bbbfcf76",
Expand Down Expand Up @@ -261,6 +277,14 @@
""
]
},
{
"cell_type": "markdown",
"id": "8e515e4c",
"metadata": {},
"source": [
"**Lecture de la matrice — trois lignes, trois caracteres.** Le tableau croise condense la sortie precedente : ligne = agent, colonne = adversaire, format `action de l'agent / action de l'adversaire`. La ligne COOPERATE_BOT affiche trois `C/` : il coopere contre tous, sans exception ni memoire. La ligne DEFECT_BOT affiche trois `D/` : defection systématique, le complement exact. La ligne MIRROR recopie la colonne de son adversaire : `C/C` face au coopereur, `D/D` face au defecteur, `C/C` face a lui-meme — la matrice entiere de MIRROR se deduit de la premiere ligne des autres. Cette symetrie de copie est la signature visuelle du miroir : dans un tableau fini, il apparait comme la transposee du champ adverse.\n"
]
},
{
"cell_type": "markdown",
"id": "f6f4a732",
Expand Down Expand Up @@ -333,6 +357,14 @@
""
]
},
{
"cell_type": "markdown",
"id": "152d4bc3",
"metadata": {},
"source": [
"**Lecture chiffree — le rang de paiement encode l'ordre du dilemme.** La sortie applique le PD canonique `{'T': 5, 'R': 3, 'P': 1, 'S': 0}` aux quatre issues. Chaque ligne porte deux nombres : `('cooperate','cooperate') -> stage_payoff=3, payoffRank=3`, `('cooperate','defect') -> 0, 0`, `('defect','cooperate') -> 5, 5`, `('defect','defect') -> 1, 1`. Ici rang et gain coincident chiffre a chiffre parce que les quatre valeurs sont distinctes — le rang est l'ordre total T > R > P > S aplati sur des entiers. Le vocabulaire compte pour la suite : `payoffRank` servira d'echelle comparable entre familles de paiements differentes, la ou `stage_payoff` brut n'est portable d'un jeu a l'autre. Le certificat final du notebook (16 paires) portera precisement sur ce rang.\n"
]
},
{
"cell_type": "markdown",
"id": "71420efc",
Expand Down Expand Up @@ -431,6 +463,14 @@
""
]
},
{
"cell_type": "markdown",
"id": "b7c83ab8",
"metadata": {},
"source": [
"**Protocole de lecture — decoder une ligne de certificat.** Chaque ligne de sortie a suivre a la meme grammaire : un nom court (`mirror_mirror`), un verdict `Python=True`, une fleche `<-`, puis l'enonce Lean dont c'est la replique (`MutualCooperationBounded mirrorBot mirrorBot`). Trois choses a ne pas confondre : le verdict `True` dit que LE CALCUL Python rend vrai sur la famille temoin, pas que l'enonce general est demontre ; le nom court est une cle de lecture, pas l'enonce ; et la fleche pointe de la preuve calculee vers la cible formelle — le sens du rejeu. Les enonces quantifies (sur toute une famille d'adversaires) se lisent differemment des egalites simples : l'interpretation qui suit cette section detaille ce partage.\n"
]
},
{
"cell_type": "code",
"execution_count": 6,
Expand Down Expand Up @@ -477,6 +517,14 @@
""
]
},
{
"cell_type": "markdown",
"id": "9395a0fa",
"metadata": {},
"source": [
"**Lecture chiffree — les deux premieres egalites calculees.** `cooperate_cooperate Python=True <- MutualCooperationBounded cooperateBot cooperateBot` : les deux coopereurs bornes cooperent mutuellement — une egalite que la matrice de la section precedente montrait deja case par case (`C/ C` en haut a gauche), ici confrontee a l'enonce exact. `defect_defect Python=True <- outcomeBounded defectBotBounded defectBotBounded = (defect, defect)` : la paire de defecteurs se defie mutuellement, meme egalite sur l'autre coin diagonal. Les deux certificats bornent la matrice par ses deux extremites pures — cooperation universelle d'un cote, defection universelle de l'autre — avant que les suivants n'attaquent les cas ou la strategie depend de l'autre.\n"
]
},
{
"cell_type": "markdown",
"id": "6f8e1504",
Expand Down Expand Up @@ -536,6 +584,14 @@
""
]
},
{
"cell_type": "markdown",
"id": "2213d46f",
"metadata": {},
"source": [
"**Lecture chiffree — miroir, puis les deux inexploitabilites.** Trois lignes, trois natures. `mirror_mirror Python=True <- MutualCooperationBounded mirrorBot mirrorBot` : deux miroirs a budget positif cooperent entre eux — chacun lit la cooperation initiale et la renvoie indefiniment, le budget de 1 suffit a entretenir la boucle. `defectBotBounded_unexploitable Python=True <- UnexploitableInFamily defectBotBounded opponents` : le defecteur est inexploitable DANS la famille — personne ne tire mieux que T=5 contre lui, et c'est un enonce quantifie sur tous les adversaires, pas une egalite ponctuelle. `mirror_basicFamily_unexploitable Python=True <- unexploitableCheck mirrorBot basicFamily` : le miroir aussi, sur la meme famille temoin. Noter la difference d'echelle des trois preuves : la premiere se verifie sur une case, les deux autres exigent le balayage de la famille entiere.\n"
]
},
{
"cell_type": "markdown",
"id": "89de0ac6",
Expand Down Expand Up @@ -601,6 +657,14 @@
""
]
},
{
"cell_type": "markdown",
"id": "d1a17b8d",
"metadata": {},
"source": [
"**Lecture chiffree — la ligne la plus riche : les 16 paires.** Apres les certificats 6 et 7 (l'equilibre relatif de la defection mutuelle, en double ecriture proposition/organe), la sortie affiche `payoffRank_le_iff (16 paires) Python=True <- payoffRank_le_iff : rang fini iff ordre des paiements`. Le compte 16 est la vraie information : toutes les paires de paiements du PD canonique (issues et rangs croises) sont passees en revue, et pour chacune l'equivalence a ete evaluee — le rang et l'ordre s'accordent paire par paire, sans exception. La ligne finale `8/8 certificats conformes` solde le rejeu : chaque fait calculable du module a sa replique Python identique, le partage des roles reste ce que la section suivante en dit.\n"
]
},
{
"cell_type": "markdown",
"id": "57d0b6fb",
Expand Down Expand Up @@ -681,6 +745,14 @@
""
]
},
{
"cell_type": "markdown",
"id": "0e5b4e64",
"metadata": {},
"source": [
"**Lire la sortie d'un exercice non rempli.** « Exercice 1 a completer : verdicts_miroir_sans_budget() » — et l'indice pose la pente : « budget nul => act(MIRROR, _) renvoie toujours... ». Le contrat : construire `BoundedAgent(ProgramCode.MIRROR, 0)` (la ligne `mirror_broke` est deja la) et decider ce que devient le miroir quand il ne peut plus payer la lecture. La sortie attendue : une paire de verdicts vrais/faux sur ce miroir casse — la question de lecture etant de savoir si la cooperation mutuelle `mirror_mirror` survit au budget nul, ou si le miroir b=0 degénère en bot constant. L'indice s'arrete avant la reponse ; la definition de `act` en debut de notebook la contient deja.\n"
]
},
{
"cell_type": "markdown",
"id": "f0f7e44e",
Expand Down Expand Up @@ -747,6 +819,14 @@
""
]
},
{
"cell_type": "markdown",
"id": "10757275",
"metadata": {},
"source": [
"**Lire la sortie d'un exercice non rempli.** « Exercice 2 a completer : equilibres_famille_etendue() » avec l'indice : « contre un miroir a budget positif, que rapporte la deviation ? ». Le terrain : `basic_family_etendue` ajoute a la famille temoin des agents a budgets varies (le squelette est pose). Le contrat : enumerer les equilibres de la famille etendue — qui, contre qui, ne gagne rien a devier unilateralement. La lecture attendue opposera le defecteur (inexploitable, donc equilibre contre tous) au miroir riche (equilibre contre son semblable) ; la question de fond, annoncee par l'indice : la deviation contre le miroir rapporte P=1 la ou la cooperation rend R=3 — le miroir punit, donc l'equilibre depend du camp.\n"
]
},
{
"cell_type": "markdown",
"id": "9d2204ac",
Expand Down Expand Up @@ -808,6 +888,14 @@
""
]
},
{
"cell_type": "markdown",
"id": "31e528a6",
"metadata": {},
"source": [
"**Lire la sortie d'un exercice non rempli.** « Exercice 3 a completer : paiements_miroir() » avec l'indice le plus dense du lot : « inexploitable protege du pire (S=0), pas de l'optimum (T=5) ». Le contrat : calculer le paiement du miroir contre chaque membre de la famille et le retourner en dictionnaire. La lecture visera l'ecart entre inexploitabilite et optimalite : etre inexploitable garanti de ne jamais servir de proie (jamais S=0 encaisse), mais ne promet pas de battre le defecteur — contre DEFECT_BOT, le miroir engrange la suite D/D au rang P=1, loin du T=5 que le defecteur prend au coopereur. La sortie remplie quantifiera precisement cet ecart, colonne par colonne.\n"
]
},
{
"cell_type": "markdown",
"id": "873e7030",
Expand Down
Loading