GameTheory-6b — Jeux répétés en Lean : le lake game_theory_lean dévoilé
Compagnon formel de GameTheory-06c-RepeatedGames-FolkTheorem-Python. Le 6c dérive à la main, en Python, l’effondrement par induction arrière, la condition de crédibilité du grim trigger \(\delta \geq (T-R)/(T-P)\) et le Folk Theorem. Ce notebook 6b montre les briques formelles disponibles dans le lake game_theory_lean : jeu de stage, flux actualisés, transition grim irréversible et condition d’incitation en une déviation. Le lake ne formalise pas encore une sémantique complète des historiques et profils de stratégies/SPNE.
Pourquoi ce compagnon existe : la mesure de visibilité de l’EPIC #11703 (scripts/lean/scan_lake_notebook_visibility.py) montrait 7 modules noirs sur 19 dans game_theory_lean — sept fichiers Lean dont aucune déclaration n’était citée par quelque notebook du dépôt que ce soit : Stage, Discounting, GrimTrigger, Folk, ConeKernel, SortedListCounting, _SmokeTest. Un travail formel invisible est un travail formel que le lecteur ne rencontre jamais : ce notebook les rend visibles, par extraction directe depuis les fichiers du lake.
Module
Rôle
RepeatedGames/Stage.lean
Le jeu de stage : le Dilemme du Prisonnier paramétré T, R, P, S
Méthode (pattern des compagnons Lean-15c / Lean-17c) : chaque section extrait les déclarations du fichier réel (parsing léger du source), affiche la première ligne de docstring — le texte que le lecteur verrait en ouvrant le fichier — et croise avec la théorie du 6c. Aucune cellule ne « recopie » une preuve : le fichier Lean est la source formelle ; ici on apprend où elle vit et ce qu’elle dit exactement.
Repère d’orientation : si vous explorez le disque, le répertoire repeated_games_lean/ du dossier GameTheory a été retiré du disque (coquille archive, #4362) — depuis la PR #6146 (EPIC #4365 Phase-4), les quatre modules sources (Stage, Discounting, GrimTrigger, Folk) sont absorbés byte-identique dans game_theory_lean/RepeatedGames/, home canonique (@[default_target] du lakefile de game_theory_lean). C’est ce home canonique que ce notebook lit.
import refrom pathlib import PathLAKE = Path("MyIA.AI.Notebooks/GameTheory/game_theory_lean")# Les 7 modules noirs mesures par scan_lake_notebook_visibility.py (EPIC #11703)DARK_MODULES = [ LAKE /"RepeatedGames/Stage.lean", LAKE /"RepeatedGames/Discounting.lean", LAKE /"RepeatedGames/GrimTrigger.lean", LAKE /"RepeatedGames/Folk.lean", LAKE /"CooperativeGames/ConeKernel.lean", LAKE /"SocialChoice/SortedListCounting.lean", LAKE /"SocialChoice/_SmokeTest.lean",]DECL_RE = re.compile(r"^(theorem|lemma|def|noncomputable def|structure|inductive|instance)\s+([A-Za-z_][A-Za-z0-9_']*)")def strip_lean_noise(text: str) ->str:"""Retire docstrings /- -/ et commentaires -- pour ne garder que le code.""" text = re.sub(r"/-.*?-/", " ", text, flags=re.S) # docstrings (non imbriquees) text = re.sub(r"--[^\n]*", " ", text) # commentaires de lignereturn textdef decls_of(path: Path):"""Extrait (kind, name, premiere ligne de docstring) d'un fichier Lean reel.""" lines = path.read_text(encoding="utf-8").splitlines() out, in_doc, doc_buf = [], False, []for i, ln inenumerate(lines): s = ln.strip()if s.startswith("/-") andnot s.startswith("/-!"): in_doc, doc_buf =True, []if s.endswith("-/") andlen(s) >2: in_doc =Falsecontinueif in_doc:if s.endswith("-/"): in_doc =Falseelif s andnot s.startswith("#") andnot s.startswith("="): doc_buf.append(s)continue m = DECL_RE.match(s)if m: out.append((m.group(1), m.group(2), doc_buf[0] if doc_buf else"")) doc_buf = []return outdef code_sorry_count(path: Path) ->int:"""Compte les occurrences de `sorry` sur lignes de CODE (prose retiree)."""returnlen(re.findall(r"\bsorry\b", strip_lean_noise(path.read_text(encoding="utf-8"))))print("Lake:", LAKE)for p in DARK_MODULES: n =len(decls_of(p))print(f" {p.relative_to(LAKE)}: {n} declarations, {code_sorry_count(p)} sorry (code)")
Les fichiers existent, et le compte de sorry sur lignes de code (prose retirée) donne déjà le paysage : Folk.lean fait exception — le sorry STRETCH du lake jeux répétés, assumé par l’issue #4880 (« le 0-sorry n’est exigé que sur le théorème-phare »). C’est le même instrument que count_code_sorry.py au principe près : ici, par fichier, pour la lecture pédagogique.
1. Stage.lean — le jeu de stage : un Dilemme du Prisonnier forcé par le type
Le fichier définit PDAction (coopérer / dévier) et la structure PrisonersDilemma. Le geste fort : les quatre inégalités canoniques de Gibbons (1992) — T > R > P > S et 2R > T + S — sont des champs de preuve de la structure. Aucun lemme en aval n’a besoin d’hypothèse implicite : le PD « bien formé » est un type, pas une convention. Le 6c posait la matrice en dur ; ici la matrice stagePayoff est une fonction totale sur PDAction x PDAction, et defect_strictly_dominatesprouve que dévier domine strictement — c’est précisément ce qui rend la coopération irrationnelle en one-shot, et donc non triviale à soutenir dans le jeu répété.
p = LAKE /"RepeatedGames/Stage.lean"print(f"--- {p.relative_to(LAKE)} ({len(p.read_text(encoding='utf-8').splitlines())} lignes) ---")for kind, name, doc in decls_of(p):print(f" {kind:12s}{name:38s}{doc[:72]}")print("sorry (code):", code_sorry_count(p))
--- RepeatedGames\Stage.lean (75 lignes) ---
inductive PDAction
structure PrisonersDilemma contraintes `T > R > P > S` et `2 * R > T + S` comme champs de preuve,
def stagePayoff de l'adversaire. Matrice de paiement standard :
lemma defect_strictly_dominates adverse : `T > R` (adversaire coopère) et `P > S` (adversaire dévie).
lemma mutual_coop_better_than_mutual_defect
lemma temptation_gt_reward
lemma punishment_gt_sucker
sorry (code): 0
Lecture du résultat : des briques sans dette
stagePayoff (la matrice), PrisonersDilemma (le PD contraint), puis les lemmes qui déplient les champs : defect_strictly_dominates (la dominance stricte, le fait fondateur du one-shot), mutual_coop_better_than_mutual_defect (R > P), et les inégalités restantes en lecture directe. Tout est prouvé — la domination stricte n’est pas une intuition, c’est un cases b plus les deux champs hTR / hPS.
2. Discounting.lean — sommes géométriques et seuil critique
La brique analytique : geom_sum (Mathlib tsum_geometric_of_lt_one) donne \(\sum_{n} \delta^n = (1-\delta)^{-1}\), d’où les formes closes coopValue\(= R/(1-\delta)\) et deviateValue\(= T + \delta P/(1-\delta)\). Le lemme clé coop_ge_deviate_iff établit l’équivalence si et seulement si avec le seuil \(\delta \geq (T-R)/(T-P)\) — exactement le \(\delta^* = 0.5\) du 6c pour \(T=3, R=2, P=1, S=0\). La preuve est de l’algèbre réelle pure : le_div_iff₀, field_simp, linarith — sans aucun calcul numérique cité.
p = LAKE /"RepeatedGames/Discounting.lean"print(f"--- {p.relative_to(LAKE)} ---")for kind, name, doc in decls_of(p):print(f" {kind:12s}{name:38s}{doc[:72]}")print("sorry (code):", code_sorry_count(p))# Pont numerique avec le 6c : le seuil sur le PD canonique T=3, R=2, P=1, S=0T, R, P, S =3.0, 2.0, 1.0, 0.0delta_star = (T - R) / (T - P)print(f"\nSeuil theorique delta* = (T-R)/(T-P) = {delta_star}")for d in (0.4, delta_star, 0.6): coop, dev = R / (1- d), T + d * P / (1- d) regime ="cooperation soutenable"if coop >= dev else"deviation profitable"print(f" delta={d:.2f}: V_C={coop:6.2f} V_D={dev:6.2f} -> {regime}")
Lecture du résultat : le théorème vit déjà dans les nombres du 6c
Sous le seuil (\(\delta = 0.4\)), dévier rapporte plus ; au seuil exactement, égalité ; au-dessus (\(\delta = 0.6\)), la coopération perpétuelle domine. C’est la vérification numérique du pont ICT-13 (#4879) : le seuil dérivé à la main dans le 6c et le lemme coop_ge_deviate_iff du lake racontent le même phénomène — l’un en flottants, l’autre en iff prouvé sur les réels de Mathlib.
Exercice 1 — tracer la frontière du seuil
Le lemme coop_ge_deviate_iff dit que la frontière est exactement la droite \(\delta^* = (T-R)/(T-P)\). Complétez frontiere pour qu’elle retourne, pour chaque \(\delta\) d’une grille, l’écart \(V_C - V_D\) — puis vérifiez numériquement que le changement de signe arrive bien à \(\delta^*\) pour plusieurs PD valides (par exemple \((T,R,P,S) = (3,2,1,0)\), \((5,3,2,1)\), \((4,3,1,0)\) — vérifiez au passage que chacun satisfait \(T > R > P > S\) et \(2R > T+S\)).
Indice : l’écart \(V_C - V_D\) est monotone croissant en \(\delta\) dès que \(T > P\) ; une recherche par dichotomie sur la grille suffit à localiser le zéro à \(10^{-6}\) près.
def frontiere(T, R, P, delta):"""Ecart V_C - V_D pour un PD (T, R, P, S) et un facteur d'escompte delta. Etape 1 : former V_C = R / (1 - delta) et V_D = T + delta * P / (1 - delta). Etape 2 : retourner V_C - V_D. """# TODO etudiantreturnNone# TODO etudiant# TODO etudiant : pour chaque PD de la liste, localiser par dichotomie le zero de# `frontiere` et verifier qu'il coïncide avec (T - R) / (T - P) a 1e-6 pres.print("Exercice a completer : frontiere + dichotomie sur 3 PD canoniques")
Exercice a completer : frontiere + dichotomie sur 3 PD canoniques
3. GrimTrigger.lean — transition grim et condition d’incitation
La transition grimNext encode désormais explicitement les deux états du grim trigger : coopération tant qu’aucune défection n’a été observée, puis punition irréversible. Les lemmes de transition vérifient notamment que defect est un état absorbant.
grim_trigger_sustains_iff établit ensuite la condition d’incitation en une déviation : le flux coopératif domine une déviation suivie de la punition si et seulement si\(\delta \geq (T-R)/(T-P)\). La preuve Lean, sans sorry, réduit cette comparaison au seuil de Discounting (exact coop_ge_deviate_iff g h0 h1).
Cette équivalence est une brique de la preuve classique par déviation en un coup, pas encore une formalisation complète d’un SPNE : le module ne définit ni historiques ni profils de stratégies.
p = LAKE /"RepeatedGames/GrimTrigger.lean"print(f"--- {p.relative_to(LAKE)} ---")for kind, name, doc in decls_of(p):print(f" {kind:12s}{name:38s}{doc[:72]}")print("sorry (code):", code_sorry_count(p))
--- RepeatedGames\GrimTrigger.lean ---
def grimNext `defect` signifie que la phase de punition a déjà commencé. Cet état est
theorem grimNext_cooperate_cooperate
theorem grimNext_cooperate_defect
theorem grimNext_defect_cooperate
theorem grimNext_defect_defect
theorem grimPunishment_absorbing
theorem grim_trigger_sustains_iff `δ ≥ (T − R) / (T − P)`.**
sorry (code): 0
Lecture du résultat : la frontière formelle est maintenant explicite
Le module expose la transition grim, ses lemmes de cas et l’état de punition absorbant, puis une équivalence iff exacte pour la condition d’incitation. Le compte sorry (code) certifie ces briques. Il ne certifie pas une sémantique complète d’équilibre : cette extension demanderait de formaliser les historiques, les profils de stratégies et les déviations admissibles.
4. Folk.lean — le Folk Theorem, un STRETCH honnête
Ici le lake assume sa frontière. IndividuallyRational et Feasible sont forcés par le type (leçon Lidman L39, PR #4899) : les définitions sont des contraintes structurelles sur les projections de PrisonersDilemma, aucune donnée numérique citée. discountedPayoff généralise coopValue/deviateValue à une trajectoire arbitraire. Puis folk_theorem_discounted : tout paiement faisable strictement individuellement rationnel est réalisable pour \(\delta\) assez proche de 1 — Fudenberg-Maskin 1986. Son sorry est la direction difficile authentique (topologie du polytope des paiements faisables), explicitement STRETCH : la conclusion est une équation réelle, pas un True masqué. Et le cas frontière folk_theorem_boundary (\(\delta = 0\) : le jeu répété collapse au one-shot) est prouvé.
Le détail qui mérite d’être raconté : le bord de l’énoncé a été réparé le 2026-08-15 — l’ancien « \(\forall d \geq \delta^*\) » sans borne \(d < 1\) rendait le théorème faux (à \(d \geq 1\) les séries \(\sum' d^n\) divergent et tsum vaut 0, valeur indésirable : aucun \(u \neq 0\) n’est réalisable). La borne \(d < 1\) répare sans renforcer. Une leçon d’énoncé : un quantificateur omis peut transformer un théorème vrai en théorème faux sans que la preuve change d’apparence.
p = LAKE /"RepeatedGames/Folk.lean"print(f"--- {p.relative_to(LAKE)} ---")for kind, name, doc in decls_of(p):print(f" {kind:12s}{name:38s}{doc[:72]}")print("sorry (code):", code_sorry_count(p))
--- RepeatedGames\Folk.lean ---
def IndividuallyRational individuellement rationnel si chaque coordonnée excède le paiement de
def Feasible espéré d'une certaine distribution sur les actions jointes. Dans une DP
noncomputable def discountedPayoff d'actions conjointes `a` et facteur d'escompte `δ`. Généralise
theorem folk_theorem_discounted Pour tout paiement faisable strictement individuellement rationnel
theorem folk_theorem_boundary réduisent aux paiements de stage — le jeu répété collapse au jeu one-sho
sorry (code): 1
Lecture du résultat : un sorry qui dit la vérité
folk_theorem_discounted porte le sorry STRETCH du versant jeux répétés — compté, documenté, priorité BG faible (#4880). Tout le reste (définitions forcées par le type, cas frontière \(\delta = 0\)) est prouvé. C’est ce qu’un STRETCH honnête looks like : la dette est dans l’énoncé difficile, pas cachée dans un True.
Exercice 2 — exhiber des poids faisables
Feasible g u_row u_col demande quatre poids \(p_{CC}, p_{CD}, p_{DC}, p_{DD} \geq 0\) sommant à 1 qui réalisent \((u_{row}, u_{col})\) comme paiement espéré. Complétez poids_faisables pour qu’elle retourne les poids (tuple de 4 flottants) réalisant un cible donnée quand elle est faisable, et None sinon. Testez sur \((R, R) = (2, 2)\) (faisable : \(p_{CC} = 1\)), sur l’alternance \((2.5, 1.5)\) (faisable : \(p_{CD} = p_{DC} = 0.5\)), et sur \((3, 3)\) (hors enveloppe : le max de \(u_{row} + u_{col}\) est \(2R = 4\)).
Indice : les quatre sommets de l’enveloppe sont \((R,R), (S,T), (T,S), (P,P)\) ; un point est faisable ssi il est dans leur enveloppe convexe. Pour les trois cas demandés, les poids se posent à la main — pas besoin de solveur.
def poids_faisables(T, R, P, S, u_row, u_col):"""Poids (pCC, pCD, pDC, pDD) realisant (u_row, u_col), ou None si non faisable. Etape 1 : poser le systeme 2x4 (u_row et u_col comme combinaisons des sommets). Etape 2 : verifier somme = 1 et poids >= 0 ; sinon retourner None. """# TODO etudiantreturnNone# TODO etudiant# TODO etudiant : les trois cas (2,2), (2.5,1.5), (3,3) sur T=3, R=2, P=1, S=0.print("Exercice a completer : poids_faisables sur 3 cibles")
Exercice a completer : poids_faisables sur 3 cibles
5. ConeKernel.lean — le noyau Bondareva-Farkas
Changement de versant : ce module est la machinerie autonome de la preuve arrière de Bondareva-Shapley par la route Farkas / séparation par hyperplan (épopée #2959, croisée avec le compagnon GameTheory-15b pour le versant coopératif). Le geste architectural : il est indépendant de TUGame — la machinerie du cône augmenté est paramétrée par une fonction caractéristique nue v : Finset N → ℝ, ce qui rompt le cycle d’imports qui confinait la preuve à un brouillon. On y trouve phiAugLinear (l’application d’incidence augmentée), augCone_mem_iff (l’appartenance au cône comme témoin w ≥ 0), augCone_dual_iff (dualité sur les générateurs), separatingFunctional_none_neg (la condition de signe du décodage) — et le résultat structural : l’enveloppe conique d’un ensemble fini de vecteurs linéairement indépendants est fermée.
p = LAKE /"CooperativeGames/ConeKernel.lean"decls = decls_of(p)print(f"--- {p.relative_to(LAKE)} ({len(p.read_text(encoding='utf-8').splitlines())} lignes) ---")print(f"{len(decls)} declarations ; affichage des 14 premieres :")for kind, name, doc in decls[:14]:print(f" {kind:12s}{name:38s}{doc[:72]}")print("sorry (code):", code_sorry_count(p))
--- CooperativeGames\ConeKernel.lean (753 lignes) ---
16 declarations ; affichage des 14 premieres :
noncomputable def phiAugLinear `some i` porte les sommes d'incidence de coalition `∑_{S ∋ i} w S` ;
noncomputable def phiAugCont
noncomputable def augCone
theorem conicHull_linearIndependent_isClosed directement à `augCone v`. Étant donné un point hors de `augCone v`, on
theorem mem_cone_iff_exists_li_subset Tout point d'un cône engendré par un ensemble fini appartient au cône
theorem finGenCone_isClosed
theorem augCone_mem_iff
def balancedUnit
lemma augCone_dual_iff `f` est non-négative sur `augCone v` ssi elle est non-négative sur chacu
lemma gen_apply_some `i ∈ S`, sinon `0`. Généralise le cas particulier de la grande coalition
lemma gen_apply_none
lemma gen_decomp vaut la combinaison d'incidence sur `S` (un vecteur de base `some i` par
lemma gen_apply_linear linéaire `f`, `f (générateur S) = ∑ i ∈ S, f (base-some i) + v S * f (ba
lemma separatingFunctional_none_neg vérifie `f (Pi.single none 1) < 0`. Preuve : `0 ≤ f` sur le générateur
sorry (code): 0
Lecture du résultat : la plus grosse pièce noire du lake, sans dette
Toute la machinerie cône-fermé de Bondareva-Farkas est prouvée. C’était le module invisible le plus lourd du lake — un travail de fond (#2959) qu’aucun notebook ne montrait.
6. SortedListCounting.lean et _SmokeTest.lean — l’infrastructure SocialChoice
Des fichiers utilitaires, noirs eux aussi. SortedListCounting factorise l’argument structurel de comptage requis par Voting.lean median_voter_theorem_strict : décomposer une liste triée en take k ++ drop k autour du pivot médian, majorer countP (· < l[k]) par k, minorer countP (l[k] ≤ ·) — le pont qui réduit les anciens sorries L355/L385 du median voter. _SmokeTest est le scaffold de smoke test du lake : un lemme trivial (zero_add_smoke), dont le rôle est de vérifier que le pipeline compile, pas de porter de la théorie.
for rel in ("SocialChoice/SortedListCounting.lean", "SocialChoice/_SmokeTest.lean"): p = LAKE / rel decls = decls_of(p)print(f"--- {rel} ({len(p.read_text(encoding='utf-8').splitlines())} lignes, {len(decls)} decls) ---")for kind, name, doc in decls[:6]:print(f" {kind:12s}{name:38s}{doc[:72]}")print("sorry (code):", code_sorry_count(p))
--- SocialChoice/SortedListCounting.lean (185 lignes, 5 decls) ---
theorem countP_lt_kth_le_half strictement inférieurs à `l[k]` est au plus `k`.
theorem countP_ge_kth_ge_half_succ `≥ l[k]` est au moins `l.length - k`.
theorem countP_le_kth_ge_half_succ et un pivot `l[k]`, le nombre d'éléments `≤ l[k]` est au moins `k + 1`.
theorem finset_filter_card_eq_toList_countP
theorem finset_filter_lt_card_eq_toList_map_countP `A.card = (univ.toList.map f).countP p` (sans passer par le filtre).
sorry (code): 0
--- SocialChoice/_SmokeTest.lean (8 lignes, 1 decls) ---
theorem zero_add_smoke
sorry (code): 0
Lecture du résultat : l’infra a sa place dans la carte
SortedListCounting porte des preuves complètes (les sorries initiaux ont été comblés — cycle 25, ai-01 backup po-2026 track 2), et _SmokeTest son lemme trivial, prouvé. L’un réduit la dette du median voter, l’autre garde le pipeline vivant : invisible ne veut pas dire inutile.
Exercice 3 — le pont vers median_voter_theorem_strict
L’en-tête de SortedListCounting.lean décrit la chaîne de réduction : A.card = (univ.toList.filter ...).length = ... = sortedPeaksList.countP (· < median) puis ≤ k par le lemme de comptage. Complétez plan_pont pour retourner, sous forme d’une liste de chaînes, les quatre étapes de cette chaîne appliquées au lemme countP_lt_kth_le_half — c’est-à-dire : pourquoi prouver les helpers de comptage suffit à décharger les sorries L355/L385 de Voting.lean.
Indice : chaque étape est une réécriture (Finset.card → length du filter, Perm.countP_eq pour passer de univ.toList.map peaks à la liste triée, puis le majorant k = length / 2). Étape 1 : la définition de A. Étape 2 : le passage card → length. Étape 3 : la permutation. Étape 4 : le majorant.
def plan_pont():"""Les 4 etapes de la reduction des sorries L355/L385 de Voting.lean. Etape 1 : definir A (le Finset filtre des pics sous la mediane). Etape 2 : reecrire A.card comme length d'un filter sur toList. Etape 3 : passer a la liste triee via Perm.countP_eq. Etape 4 : majorer par k via le lemme de comptage sur listes triees. """# TODO etudiantreturnNone# TODO etudiantprint("Exercice a completer : plan_pont (4 etapes)")
Exercice a completer : plan_pont (4 etapes)
7. Re-mesure : le lake n’a plus de module noir
La boucle est bouclée : on relance l’instrument de l’EPIC #11703 sur l’arbre courant. Avant ce compagnon, game_theory_lean comptait 7 modules noirs sur 19. Chaque section ci-dessus cite les déclarations des sept fichiers (l’extraction les affiche), donc le scanner doit maintenant les voir tous.
1135 notebooks lus, 21 lakes, 3003 declarations
lake decl large strict noirs compagnon principal
game_theory_lean 499 181 116 0/20 GameTheory/GameTheory-06b-Lean-RepeatedGames.ipynb
TOTAL 930/3027 (borne haute) 683/3027 (borne basse) modules invisibles: 34/197
Lecture du résultat : 7 modules noirs → 0
La ligne game_theory_lean du scanner confirme : plus aucun module noir. Les déclarations du lake restent loin d’être toutes citées (la visibilité large n’est pas l’objectif — l’EPIC vise l’absence de modules totalement invisibles), mais chaque fichier a maintenant sa vitrine : le stage game et sa dominance stricte, la transition grim absorbante et sa condition d’incitation 0-sorry, le Folk STRETCH au bord réparé, le noyau Bondareva-Farkas, et l’infra SocialChoice.
Ce que ce notebook ajoute au dépôt : le chemin du lecteur entre la théorie dérivée à la main (6c) et les briques réellement formalisées dans le lake — là où il n’existait rien. See #11703.