GameTheory-3a — Chemins de swaps : à quelle distance sont deux jeux ?
Troisième temps de la géométrie ordinale des jeux 2×2. GameTheory-3 avait énuméré les 576 chambres strictes et leurs générateurs adjacents ; GameTheory-3b a montré que les jeux à égalités sont des murs entre chambres — des objets de codimension. Ce notebook répond à la question qui reste : à quelle distance de swap sont deux jeux, et par quels chemins les relie-t-on ?
Deux questions d’analyse d’algorithme s’y ajoutent, qui structurent tout le grain :
Le générateur propose — un parcours en largeur (BFS) explore l’espace niveau par niveau et produit un plus court chemin candidat.
Le certificat garantit — un module compagnon en Lean (game_theory_lean/Swaps/Basic.lean, écrit pour ce grain) certifie qu’un chemin proposé est bien formé et mène bien de l’arrivée au départ ; sur le cas témoin Dilemme → Chicken, il certifie aussi qu’aucun chemin plus court n’existe. Le générateur Python et le vérificateur Lean restent deux artefacts distincts,chacun à sa place.
Prérequis : GameTheory-3 (générateurs \(R_{12}/R_{23}/R_{34}/C_{12}/C_{23}/C_{34}\)), GameTheory-3b (codimension, murs, facettes), GameTheory-03h (deux espèces de flèches). Toutes les mesures de ce notebook sont calculées sur l’espace complet des 576 jeux stricts — le quotient par renommage des stratégies (144 classes) est une dette rapportée, jamais affirmée ici.
Plan
§1 La distance d’un jeu à l’autre — BFS depuis le Dilemme, tableau des distances aux archétypes, les trois cousins à distance 2.
§2 La distribution des distances — sphères emboîtées, symétrie parfaite, convolution des vecteurs de Mahler.
§3 Le théorème de décomposition — la distance d’un jeu à l’autre est la somme des longueurs de Coxeter des deux côtés ; vérification exhaustive sur les 331 776 paires.
§4 Multiplicités — combien de plus courts chemins relient deux jeux : de 2 (commutation) à 236 544 (l’anti-Dilemme).
§5 Générateur contre certificat — le miroir Python du vérificateur Lean, valide ≠ minimal, puis le module Swaps/Basic.lean lui-même, cité aux lignes mesurées.
§6 Exercices (3) — distance par sphères, diamètre depuis une autre source, certificat d’un chemin fourni.
from itertools import permutationsfrom collections import deque, Counter# Convention GameTheory-3 / GameTheory-21 : une table porte les rangs 1-4# des quatre cellules dans l'ordre (haut-gauche, haut-droit, bas-gauche,# bas-droit). Un jeu est le couple (table Ligne, table Colonne).PERMS =list(permutations((1, 2, 3, 4)))JEUX = [(r, c) for r in PERMS for c in PERMS] # 576 jeux strictsdef swap_adjacent(t, k):"""Générateur élémentaire : échange les cellules portant les rangs k et k+1. Vu des valeurs, c'est une relabellisation k <-> k+1 ; vu des cellules, c'est la traversée du mur où ces deux rangs coïncident (GT-3b, §3). """ pk, pk1 = t.index(k), t.index(k +1) l =list(t) l[pk], l[pk1] = l[pk1], l[pk]returntuple(l)def voisins(g):"""Les six voisins d'un jeu : trois générateurs par joueur.""" r, c = greturn ([(swap_adjacent(r, k), c) for k in (1, 2, 3)] + [(r, swap_adjacent(c, k)) for k in (1, 2, 3)])# Encodages ordinaux canoniques (identiques à GameTheory-3 et GT-21)CLASSIC = {"Dilemme": ((3, 1, 4, 2), (3, 4, 1, 2)),"Chicken": ((3, 2, 4, 1), (3, 4, 2, 1)),"Deadlock": ((2, 1, 4, 3), (2, 4, 1, 3)),"Chasse au cerf": ((4, 1, 3, 2), (4, 3, 1, 2)),"Harmonie": ((4, 3, 2, 1), (4, 2, 3, 1)),"Pennies": ((4, 1, 2, 3), (1, 4, 3, 2)),}def bfs(depart):"""Parcours en largeur : distances et parents depuis un jeu de départ.""" dist = {depart: 0} parent = {depart: None}file= deque([depart])whilefile: u =file.popleft()for v in voisins(u):if v notin dist: dist[v] = dist[u] +1 parent[v] = ufile.append(v)return dist, parentprint(f"Espace : {len(JEUX)} jeux stricts, {len(voisins(JEUX[0]))} générateurs par jeu")
Espace : 576 jeux stricts, 6 générateurs par jeu
1. La distance d’un jeu à l’autre
La distance de swap entre deux jeux est la longueur du plus court chemin de générateurs qui relie l’un à l’autre — le nombre minimal de murs traversés, au sens de GT-3b. C’est la distance de graphe sur les 576 sommets, et le parcours en largeur la mesure exactement : le BFS découvre les jeux par sphères croissantes, et la sphère où un jeu apparaît pour la première fois est sa distance au point de départ.
Lançons le BFS depuis le Dilemme du prisonnier — le jeu le plus commenté de la théorie — et demandons les distances aux cinq autres archétypes canoniques.
DIST_PD, PARENT_PD = bfs(CLASSIC["Dilemme"])print("jeux atteints depuis le Dilemme :", len(DIST_PD), "/ 576")print("excentricité du Dilemme :", max(DIST_PD.values()))print()print("Distances depuis le Dilemme :")for nom, g in CLASSIC.items():print(f" Dilemme -> {nom:16s} distance = {DIST_PD[g]}")
jeux atteints depuis le Dilemme : 576 / 576
excentricité du Dilemme : 12
Distances depuis le Dilemme :
Dilemme -> Dilemme distance = 0
Dilemme -> Chicken distance = 2
Dilemme -> Deadlock distance = 2
Dilemme -> Chasse au cerf distance = 2
Dilemme -> Harmonie distance = 6
Dilemme -> Pennies distance = 5
Interprétation : trois cousins à distance 2, un antagoniste à distance 12
Trois archétypes sont à distance 2 du Dilemme — Chicken, Deadlock et la chasse au cerf — et un seul est à distance 12 : son complément ordinal, le jeu où chaque rang \(r\) est remplacé par \(5 - r\) chez les deux joueurs (l’« anti-Dilemme », unique point de la sphère maximale). Entre les deux, Pennies à 5 et Harmonie à 6.
La distance 2 des trois cousins n’est pas un artefact d’encodage : chacun s’obtient du Dilemme en échangeant, chez chaque joueur, une paire différente de rangs adjacents :
Chicken : l’ordre des deux pires rangs (\(P \leftrightarrow S\)) — c’est tout ce qui sépare la coopération forcée du Dilemme de l’intimidation réciproque ;
Deadlock : l’ordre des rangs du milieu ;
la chasse au cerf : l’ordre des deux meilleurs rangs (\(T \leftrightarrow R\)) — le pari de confiance.
Reconstruisons ces chemins avec la table des parents du BFS.
def nommer_etape(g1, g2):"""Nom du générateur qui fait passer de g1 à son voisin g2.""" r1, c1 = g1 r2, c2 = g2for k in (1, 2, 3):if swap_adjacent(r1, k) == r2:returnf"R{k}{k +1}"if swap_adjacent(c1, k) == c2:returnf"C{k}{k +1}"raiseValueError("pas voisins")def reconstruire(arrivee, parent):"""Chemin du départ du BFS jusqu'à l'arrivée, en noms de générateurs.""" chemin = [] v = arriveewhile parent[v] isnotNone: chemin.append(nommer_etape(parent[v], v)) v = parent[v]returnlist(reversed(chemin))def complement(g):"""Le complément ordinal : chaque rang r devient 5 - r chez les deux joueurs."""return (tuple(5- v for v in g[0]), tuple(5- v for v in g[1]))for nom in ("Chicken", "Deadlock", "Chasse au cerf", "Pennies", "Harmonie"): chemin = reconstruire(CLASSIC[nom], PARENT_PD)print(f"Dilemme -> {nom:16s} (distance {DIST_PD[CLASSIC[nom]]:2d}) : "f"{' '.join(chemin)}")anti = complement(CLASSIC["Dilemme"])print(f"\nanti-Dilemme = {anti}")print(f"distance = {DIST_PD[anti]} ; jeux à cette distance :",sum(1for d in DIST_PD.values() if d ==12))
Le Dilemme habite un carrefour : ses trois cousins célèbres sont à deux pas, chacun dans une direction cardinale différente (bas, milieu, haut de l’échelle des rangs), et l’unique jeu le plus lointain — à 12 swaps — est son complément ordinal exact, celui où chaque cellule qui était un bon rang devient un mauvais. Dans ce jeu antagoniste, la situation du Dilemme est intégralement inversée : ce que la coopération produisait de mieux devient pire. La mesure dit autrement la même chose que GT-3b : traverser les 12 murs qui séparent un jeu de son complément, c’est renverser toute son échelle de valeurs — et aucun chemin ne peut être plus long, car changer les deux tables complètes exige au plus 6 swaps adjacents chacune (le retournement d’un ordre de 4 éléments).
Le point mérite d’être regardé de plus près : la structure de toutes ces distances est remarquablement régulière, et c’est l’objet de la section suivante.
2. La distribution des distances : des sphères emboîtées
Le BFS donne la distance de chaque jeu au Dilemme — autrement dit la cardinalité de chaque sphère \(S_d = \{G : d(\text{Dilemme}, G) = d\}\) pour \(d\) de 0 à 12. Si la géographie du Dilemme était quelconque, ces tailles n’auraient aucune raison d’être régulières. Mesurons.
distribution = Counter(DIST_PD.values())total =sum(distribution.values())print("d :", " ".join(f"{d:6d}"for d inrange(13)))print("N :", " ".join(f"{distribution[d]:6d}"for d inrange(13)))print("total :", total)print()for d inrange(13):print(f" d = {d:2d} | {'#'* (distribution[d] //2):48s}{distribution[d]:4d}")symetrie =all(distribution[d] == distribution[12- d] for d inrange(13))print("\nsymétrie d <-> 12 - d :", symetrie)print("maximum atteint en d = 6 :", distribution[6], "jeux")
d : 0 1 2 3 4 5 6 7 8 9 10 11 12
N : 1 6 19 42 71 96 106 96 71 42 19 6 1
total : 576
d = 0 | 1
d = 1 | ### 6
d = 2 | ######### 19
d = 3 | ##################### 42
d = 4 | ################################### 71
d = 5 | ################################################ 96
d = 6 | ##################################################### 106
d = 7 | ################################################ 96
d = 8 | ################################### 71
d = 9 | ##################### 42
d = 10 | ######### 19
d = 11 | ### 6
d = 12 | 1
symétrie d <-> 12 - d : True
maximum atteint en d = 6 : 106 jeux
Interprétation : une distribution symétrique et factorisée
La distribution est parfaitement symétrique autour de 6, en cloche, avec un unique jeu aux deux extrémités (\(d = 0\) le Dilemme lui-même, \(d = 12\) son complément) et un plateau de 106 jeux à distance 6. Cette régularité appelle une explication structurelle — et elle en a une, calculable de façon indépendante.
La distribution des longueurs de mots sur les 24 permutations d’un côté (la distribution des nombres d’inversions) est le vecteur de Mahler du permutoèdre : \(\{1, 3, 5, 6, 5, 3, 1\}\) pour \(S_4\). Si la distance d’un jeu à l’autre était la somme indépendante des distances de chaque côté — un théorème que la section 3 établira par énumération exhaustive — alors la distribution depuis n’importe quel jeu devrait être la convolution de ce vecteur avec lui-même. Vérifions la prédiction avant d’établir le théorème qui la justifie.
# Distribution des longueurs d'un côté : les nombres d'inversions sur S4.# La distance d'une permutation a l'identite (en swaps adjacents de valeurs)# est son nombre d'inversions -- la longueur de Coxeter.def inversions(t):returnsum(1for i inrange(4) for j inrange(i +1, 4) if t[i] > t[j])mahler_s4 = Counter(inversions(p) for p in PERMS)print("vecteur de Mahler de S4 :", [mahler_s4[k] for k inrange(7)],"(somme :", sum(mahler_s4.values()), "permutations )")# Convolution manuelle : u * vdef convol(u, v): w = [0] * (len(u) +len(v) -1)for i, a inenumerate(u):for j, b inenumerate(v): w[i + j] += a * breturn wpredite = convol([mahler_s4[k] for k inrange(7)], [mahler_s4[k] for k inrange(7)])mesuree = [distribution[d] for d inrange(13)]print("convolution (Mahler * Mahler) :", predite)print("distribution mesurée :", mesuree)print("coïncidence exacte :", list(predite) == mesuree)
La coïncidence exacte de la cellule précédente n’est pas un hasard : c’est la trace d’un théorème. Énonçons-le d’abord informellement.
Décomposition. La distance de swap entre deux jeux \(G = (r_G, c_G)\) et \(H = (r_H, c_H)\) est la somme des distances de chaque côté : \[d(G, H) = \ell(r_G, r_H) + \ell(c_G, c_H)\] où \(\ell(a, b)\) est la longueur de Coxeter de la relabellisation qui envoie \(a\) sur \(b\) : le nombre d’inversions de la permutation relative \(b \circ a^{-1}\), c’est-à-dire le nombre minimal de transpositions de valeurs adjacentes qui transforment \(a\) en \(b\).
L’intuition : les générateurs Ligne et Colonne sont indépendants — un chemin est un entrelacement d’un mot côté Ligne et d’un mot côté Colonne, et chaque côté se comporte comme le graphe de Cayley de \(S_4\) muni des trois transpositions adjacentes, dont la distance est exactement la longueur de Coxeter. Nous n’affirmerons pas cette preuve conceptuelle comme établie (elle est rapportée en dette) — mais nous pouvons faire mieux que la croire : vérifier l’énoncé sur chacune des 331 776 paires de jeux, en comparant le BFS (la mesure) à la formule (la prédiction), indépendamment l’une de l’autre.
def coxeter(a, b):"""Longueur de Coxeter de la relabellisation a -> b : nombre d'inversions de la permutation relative b . a^{-1}. """ pos = [0] *5# pos[v] = position de la valeur v dans afor i, v inenumerate(a): pos[v] = i pi = [b[pos[v]] for v in (1, 2, 3, 4)] # permutation relativereturnsum(1for i inrange(4) for j inrange(i +1, 4) if pi[i] > pi[j])# Exemples chiffrés, un par côté du chemin Dilemme -> Chicken :print("Ligne : (3,1,4,2) -> (3,2,4,1), coxeter =", coxeter((3, 1, 4, 2), (3, 2, 4, 1)))print("Colonne : (3,4,1,2) -> (3,4,2,1), coxeter =", coxeter((3, 4, 1, 2), (3, 4, 2, 1)))print("retournement (1,2,3,4) -> (4,3,2,1), coxeter =", coxeter((1, 2, 3, 4), (4, 3, 2, 1)))print("identite (1,2,3,4) -> (1,2,3,4), coxeter =", coxeter((1, 2, 3, 4), (1, 2, 3, 4)))
import time# Vérification exhaustive : pour chacune des 576 sources, un BFS complet# (la mesure), comparée a la formule de Coxeter (la prediction) sur les# 576 destinations. 576 x 576 = 331 776 paires.t0 = time.perf_counter()matrice = {}coherence =Truefor G in JEUX: dG, _ = bfs(G) matrice[G] = dGfor H in JEUX: formule = coxeter(G[0], H[0]) + coxeter(G[1], H[1])if dG[H] != formule: coherence =Falseprint("CONTRE-EXEMPLE :", G, H, dG[H], "!=", formule)breakifnot coherence:breakelapsed = time.perf_counter() - t0paires =sum(len(d) for d in matrice.values())print(f"paires vérifiées : {paires} / 331776 en {elapsed:.1f}s")print("décomposition d = coxeter(ligne) + coxeter(colonne) :", coherence)# Corollaires lus sur la matrice complète :excentricites = Counter(max(dG.values()) for dG in matrice.values())print("excentricités de tous les jeux :", dict(excentricites))spot = matrice[CLASSIC["Dilemme"]][CLASSIC["Chicken"]]print("spot-check matrice [Dilemme][Chicken] =", spot, "(BFS section 1 :", DIST_PD[CLASSIC["Chicken"]], ")")
paires vérifiées : 331776 / 331776 en 2.2s
décomposition d = coxeter(ligne) + coxeter(colonne) : True
excentricités de tous les jeux : {12: 576}
spot-check matrice [Dilemme][Chicken] = 2 (BFS section 1 : 2 )
Interprétation : le théorème établi par énumération
La décomposition vaut pour chacune des 331 776 paires. Comme le théorème de la condition de transformation dans GT-3h (vérifié sur les 3 456 paires jeu-générateur), l’énoncé est ici établi par énumération exhaustive : l’espace est fini, la vérification est complète, et le résultat se lit sur la sortie. La preuve conceptuelle — indépendance des deux côtés, graphe de Cayley de \(S_4\), produit cartésien — est rapportée en dette (§Sources) : nous n’en livrons pas la démonstration générale, seulement l’évidence exhaustive sur cet espace.
Trois corollaires immédiats, tous mesurés :
le diamètre vaut 12 = deux fois le maximum de la longueur de Coxeter d’un côté (6, le retournement) — cohérent avec la mesure GT-3b ;
chaque jeu a une excentricité de 12 : l’espace est parfaitement isotrope, aucun point n’est plus central qu’un autre ; le Dilemme n’occupe aucune position privilégiée — c’est une propriété de l’espace, pas du jeu ;
la distribution depuis n’importe quel jeu est la convolution des vecteurs de Mahler (cellule précédente) — ce qui explique la symétrie parfaite autour de 6.
Un point reste ouvert dans la géographie : si les distances sont simples, que dire du nombre de plus courts chemins ? C’est l’objet de la section 4.
4. Multiplicités : combien de plus courts chemins
La distance dit combien de pas ; elle ne dit pas par où. Deux jeux à même distance peuvent être reliés par un nombre très différent de chemins minimaux. Comptons-les en énumérant, pour une cible donnée, tous les chemins qui descendent strictement d’un niveau par étape (tout plus court chemin est une telle descente monotone).
def voisins_nommes(g):"""Les six voisins d'un jeu, avec le nom de leur générateur.""" r, c = g out = []for k in (1, 2, 3): out.append(((swap_adjacent(r, k), c), f"R{k}{k +1}")) out.append(((r, swap_adjacent(c, k)), f"C{k}{k +1}"))return outdef plus_courts_chemins(depart, arrivee):"""Enumere tous les plus courts chemins (descentes monotones de niveaux).""" d = bfs(depart)[0] n = d[arrivee] chemins = [(depart, [])]for _ inrange(n): chemins = [(v, p + [nom]) for g, p in cheminsfor v, nom in voisins_nommes(g) if d.get(v, 99) == d[g] +1]return [p for g, p in chemins if g == arrivee]from math import combfor nom in ("Chicken", "Deadlock", "Chasse au cerf", "Pennies", "Harmonie"): cs = plus_courts_chemins(CLASSIC["Dilemme"], CLASSIC[nom])print(f"Dilemme -> {nom:16s} distance {DIST_PD[CLASSIC[nom]]:2d} : "f"{len(cs):6d} plus courts chemins (ex : {' '.join(cs[0])})")anti = complement(CLASSIC["Dilemme"])n_anti =len(plus_courts_chemins(CLASSIC["Dilemme"], anti))# Interpretation structurelle du compte (mesuree independamment) :identite = ((1, 2, 3, 4), (1, 2, 3, 4))retourne_ligne = ((4, 3, 2, 1), (1, 2, 3, 4))mots_w0 =len(plus_courts_chemins(identite, retourne_ligne))print(f"\nDilemme -> anti-Dilemme : {n_anti} plus courts chemins")print("mots réduits du retournement, un côté :", mots_w0)print(f"entrelacements C(12,6) x 16 x 16 = {comb(12, 6)} x {mots_w0} x {mots_w0} =", comb(12, 6) * mots_w0 **2)
Dilemme -> Chicken distance 2 : 2 plus courts chemins (ex : R12 C12)
Dilemme -> Deadlock distance 2 : 2 plus courts chemins (ex : R23 C23)
Dilemme -> Chasse au cerf distance 2 : 2 plus courts chemins (ex : R34 C34)
Dilemme -> Pennies distance 5 : 20 plus courts chemins (ex : C12 C23 C12 R34 R23)
Dilemme -> Harmonie distance 6 : 80 plus courts chemins (ex : R12 C12 R34 R23 C34 C23)
Dilemme -> anti-Dilemme : 236544 plus courts chemins
mots réduits du retournement, un côté : 16
entrelacements C(12,6) x 16 x 16 = 924 x 16 x 16 = 236544
Interprétation : de la commutation à l’explosion combinatoire
Le spectre des multiplicités est vaste : exactement 2 chemins minimaux vers chacun des trois cousins (les deux étapes — une par côté — commutent, donc les deux ordres conviennent, et rien d’autre), 20 vers Pennies, 80 vers l’Harmonie, et 236 544 vers l’anti-Dilemme. Ce dernier compte se factorise exactement : \(\binom{12}{6} \times 16 \times 16\) — les 16 mots réduits du retournement d’un côté (mesurés par la même énumération, restreinte à un seul côté), au carré pour les deux côtés, entrelacés dans \(\binom{12}{6}\) ordres possibles. Le chemin minimal vers l’antagoniste absolu n’est donc pas une rareté : il est abondant, presque tout chemin glouton qui descend monotone y conduit.
La leçon structurelle : la distance (§3) est une fonction simple et additive, mais la géométrie fine des géodésiques porte l’information combinatoire — le nombre de mots réduits d’un élément de \(S_4\) est une donnée non triviale de la théorie des groupes de Coxeter, rapportée en dette comme le reste du vocabulaire. C’est précisément quand les objets deviennent abondants et faciles à générer que la question du certificat devient pressante : qui garantit qu’un chemin proposé est correct ? C’est la section suivante.
5. Générateur contre certificat
Récapitulons les deux rôles, qui resteront séparés jusqu’au bout :
le générateur (Python, ce notebook) explore : BFS, énumération des chemins, comptages. Il propose des chemins minimaux — mais un programme qui s’exécute n’est pas une preuve qu’il calcule ce qu’il prétend calculer ;
le certificat (Lean, game_theory_lean/Swaps/Basic.lean, écrit pour ce grain) garantit : qu’un chemin est bien formé (chaque étape est l’un des six générateurs — c’est structurel, le type des étapes ne contient rien d’autre), qu’il mène bien du départ à l’arrivée (évalué par le noyau Lean, rfl), et — sur le cas témoin — qu’aucun chemin plus court n’existe (énumération décidable).
Commençons par le miroir Python du vérificateur, pour voir ce qui se joue : un chemin valide (il arrive) n’est pas un chemin minimal (il arrive le plus vite possible).
def applique_etape(g, e):"""Miroir Python de appliqueEtape (Swaps/Basic.lean) : applique l'étape nommée e.""" r, c = g k =int(e[1])return (swap_adjacent(r, k), c) if e[0] =="R"else (r, swap_adjacent(c, k))def applique_chemin(g, chemin):"""Miroir Python de applique : application successive des étapes."""for e in chemin: g = applique_etape(g, e)return gdef chemin_valide(depart, arrivee, chemin):"""Certificat d'arrivée : le chemin mène bien de depart à arrivee. Ne dit RIEN de la minimalité."""return applique_chemin(depart, chemin) == arriveePD, CHICKEN = CLASSIC["Dilemme"], CLASSIC["Chicken"]c_minimal = ["R12", "C12"] # le chemin du BFS (section 1)c_detour = ["R12", "R23", "R23", "C12"] # un détour : R23 o R23 = identitéprint("chemin minimal ", c_minimal, ": valide =", chemin_valide(PD, CHICKEN, c_minimal))print("chemin détour ", c_detour, ": valide =", chemin_valide(PD, CHICKEN, c_detour))print()print("longueurs :", len(c_minimal), "vs", len(c_detour),"| distance BFS :", DIST_PD[CHICKEN])
Le certificat d’arrivée accepte les deux chemins — et il a raison : les deux mènent bien du Dilemme à Chicken (le détour insère un aller-retour \(R_{23} \circ R_{23}\), qui s’annule). Mais seul le premier est minimal : la longueur 4 du détour dépasse la distance 2. Un vérificateur d’arrivée est donc complet mais laxiste ; discriminer les chemins minimaux exige soit l’exploration exhaustive (ce que fait le BFS), soit une borne inférieure (ce que fait le module Lean sur le cas témoin : aucun chemin de longueur < 2 n’existe, par énumération décidable des cas).
C’est la division du travail que le grain installe : le générateur produit des candidats abondants (section 4 : des centaines de milliers vers l’anti-Dilemme), le certificat tranche — arrivée garantie toujours, minimalité garantie sur le témoin. Voyons le module Lean lui-même, cité aux lignes mesurées du fichier.
5-bis. Le module Swaps/Basic.lean, cité aux lignes mesurées
Le module compagnon vit dans game_theory_lean/Swaps/Basic.lean (même lake que les preuves Arrow et Shapley). Il est volontairement sans Mathlib : tout y est calcul fini décidable sur des listes littérales — les théorèmes se closent par rfl (évaluation par le noyau) ou decide (énumération décidable), sans tactique sophistiquée ni axiome. La cellule suivante lit le fichier depuis ce clone et imprime chaque définition et chaque théorème à sa ligne réelle — les citations du reste de la section s’appuient sur ces numéros, pas sur une mémoire.
from pathlib import Pathdef trouver_swaps_lean():"""Localise Swaps/Basic.lean depuis le répertoire courant ou ses parents (le notebook vit dans GameTheory/, le module dans game_theory_lean/)."""for base in [Path.cwd(), *Path.cwd().parents]:for rel in ("game_theory_lean/Swaps/Basic.lean","MyIA.AI.Notebooks/GameTheory/game_theory_lean/Swaps/Basic.lean"): cible = base / relif cible.exists():return ciblereturnNonechemin_module = trouver_swaps_lean()if chemin_module isNone:print("module Swaps/Basic.lean introuvable depuis ce répertoire —"" cloner le dépôt complet pour la lecture des citations")else: src = chemin_module.read_text(encoding="utf-8") lignes = src.splitlines()print(f"{chemin_module.name} : {len(lignes)} lignes")print()for i, l inenumerate(lignes, 1):if l.startswith(("def ", "theorem ", "inductive ", "structure ")):print(f" {i:4d}: {l.rstrip()[:100]}")print()print("occurrences de 'sorry' dans le module :", src.count("sorry"))
Basic.lean : 135 lignes
34: def Table : Type := List Nat
37: def Jeu : Type := Table × Table
46: def swapAdj (t : Table) (k : Nat) : Table :=
50: inductive Etape where
56: def Etape.k : Etape → Nat
62: def Etape.ligne : Etape → Bool
67: def appliqueEtape (g : Jeu) (e : Etape) : Jeu :=
71: def applique : Jeu → List Etape → Jeu
78: def dilemme : Jeu := (([3, 1, 4, 2] : Table), [3, 4, 1, 2])
81: def chicken : Jeu := (([3, 2, 4, 1] : Table), [3, 4, 2, 1])
84: def cerf : Jeu := (([4, 1, 3, 2] : Table), [4, 3, 1, 2])
89: def cheminDilemmeChicken : List Etape := [.R12, .C12]
95: theorem certificat_chemin : applique dilemme cheminDilemmeChicken = chicken := by rfl
101: theorem chemin_valide_non_minimal :
106: theorem aucun_chemin_court :
120: theorem distance_dilemme_chicken :
130: def cheminValide (depart arrivee : Jeu) (p : List Etape) : Prop :=
135: theorem certificat_cerf : cheminValide dilemme cerf [.R34, .C34] := by rfl
occurrences de 'sorry' dans le module : 0
Interprétation : ce que chaque théorème garantit
La lecture du module aligne les garanties, dans l’ordre où le notebook les a rencontrées :
certificat_chemin — applique dilemme cheminDilemmeChicken = chicken, clos par rfl : le chemin [R12, C12] proposé par le BFS mène bien du Dilemme à Chicken. C’est le certificat d’arrivée, garanti par évaluation du noyau Lean — pas par la ré-exécution d’un programme Python, mais par la réduction du terme lui-même.
chemin_valide_non_minimal — le détour [R12, R23, R23, C12] arrive aussi (la cellule miroir l’a mesuré côté Python) : le module Lean l’admet explicitement, pour montrer que le certificat d’arrivée n’exclut pas les détours.
aucun_chemin_court — aucun chemin de longueur 0 ou 1 ne relie le Dilemme à Chicken : longueur 0 rejetée par decide (les jeux diffèrent), longueur 1 par cases e <;> decide — les six générateurs sont énumérés un à un, chacun tranché par décision. C’est la borne inférieure.
distance_dilemme_chicken — la conjonction : un chemin de longueur 2 existe et aucun plus court n’existe. La distance vaut exactement 2 — énoncé complet, prouvé.
La minimalité générale (pour deux jeux quelconques) reste du côté du générateur : elle exige l’exploration. Le module Lean la certifie sur le témoin parce que l’espace des chemins de longueur < 2 est assez petit pour l’énumération décidable — c’est exactement la frontière où le certificat devient abordable, et le grain la marque explicitement plutôt que de la masquer. Le build du module (lake build Swaps) est sans dépendance Mathlib : il se compile en secondes, aucune preuve du lake n’est touchée.
6. Exercice 1 : distance par sphères, sans reconstruire tout le BFS
La fonction bfs de la section 1 calcule les distances vers tous les jeux. Pour une seule cible, c’est du gaspillage — et parfois impossible si l’espace était plus grand. Écrivez distance_par_spheres(depart, arrivee) qui n’explore que les sphères successives jusqu’à rencontrer l’arrivée : maintenez l’ensemble des jeux du niveau courant, engendez le niveau suivant par générateurs, arrêtez dès que l’arrivée apparaît, et renvoyez le niveau. La fonction doit renvoyer le même verdict que le BFS complet pour toute cible — testez-la au moins sur Chicken (distance 2) et sur l’anti-Dilemme (distance 12).
def distance_par_spheres(depart, arrivee):"""Distance de swap par exploration des sphères successives seulement. # Etape 1 : niveau courant = [depart], distance = 0 # Etape 2 : engendrer le niveau suivant par les six générateurs # Etape 3 : si l'arrivee y figure, renvoyer la distance ; sinon recommencer """# TODO etudiantreturnNone# a remplacerresultat_ex1 = distance_par_spheres(CLASSIC["Dilemme"], CLASSIC["Chicken"])# Indice : la reponse attendue est petite ; le chemin de cette longueur est# exhibe en section 1 et certifie par Swaps/Basic.lean (distance exacte 2).
6-bis. Exercice 2 : le diamètre depuis une autre source — le chiffre, pas l’impression
La section 3 a mesuré que tous les jeux ont une excentricité de 12. Vérifiez-le depuis une source différente du Dilemme : écrivez excentricite_depuis(source) (distance maximale de la source à tout autre jeu) et appliquez-la à Pennies. Puis identifiez combien de jeux sont à distance 12 de Pennies et lequel c’est — la réponse est un couple (chiffre, jeu), pas une impression.
def excentricite_depuis(source):"""Excentricité d'un jeu : sa distance maximale à tout autre jeu. # Etape 1 : BFS complet depuis source # Etape 2 : renvoyer le maximum des distances """# TODO etudiantreturnNone# a remplacerresultat_ex2 = excentricite_depuis(CLASSIC["Pennies"])# Indice : le theoreme de decomposition (section 3) predit la valeur sans# aucun calcul de BFS -- la formule de Coxeter suffit. Les deux doivent coïncider.
6-ter. Exercice 3 : le certificat d’un chemin fourni — valide, et minimal ?
On vous fournit un chemin du Dilemme à Chicken : ["R12", "R23", "R23", "C12"]. Écrivez certificat(depart, arrivee, chemin) qui renvoie un couple de booléens : (validité, minimalité).
la validité se certifie en appliquant le chemin (section 5, miroir Python) et en comparant l’arrivée — c’est ce que Swaps/Basic.lean garantit par rfl ;
la minimalité exige de comparer la longueur du chemin à la distance réelle — soit par re-BFS (exercice 1), soit par la formule de Coxeter (section 3).
Votre verdict sur le chemin fourni doit être (True, False) : il arrive, mais en 4 pas au lieu de 2. Puis produisez le certificat complet d’un chemin qui mérite les deux True.
chemin_fourni = ["R12", "R23", "R23", "C12"] # un detour, fournidef certificat(depart, arrivee, chemin):"""Verdict d'un chemin : couple (validite, minimalite). # Etape 1 : validite -- appliquer le chemin, comparer l'arrivee # Etape 2 : minimalite -- la longueur egale-t-elle la distance ? # Renvoyer (bool, bool) """# TODO etudiantreturnNone# a remplacerresultat_ex3 = certificat(CLASSIC["Dilemme"], CLASSIC["Chicken"], chemin_fourni)# Indice : attendu (True, False) pour le chemin fourni ; un chemin minimal# (section 1) merite (True, True).
7. Résumé
La distance de swap est mesurable exactement : BFS depuis n’importe quel jeu, sphères emboîtées. Depuis le Dilemme : Chicken, Deadlock et la chasse au cerf à distance 2 (chacun en échangeant une paire différente de rangs adjacents chez chaque joueur), Pennies à 5, Harmonie à 6, l’anti-Dilemme à 12.
Théorème de décomposition (établi par énumération exhaustive, 331 776 paires) : \(d(G, H) = \ell(r_G, r_H) + \ell(c_G, c_H)\), la somme des longueurs de Coxeter des permutations relatives. Corollaires mesurés : diamètre 12, excentricité 12 pour tous les jeux (isotropie parfaite), distribution depuis tout jeu = convolution des vecteurs de Mahler de \(S_4\).
Les multiplicités portent la combinatoire : de 2 chemins minimaux (commutation des deux côtés) vers chacun des trois cousins à 236 544 = \(\binom{12}{6} \times 16^2\) vers l’anti-Dilemme — les géodésiques abondent exactement là où la distance est maximale.
Générateur contre certificat : le BFS Python propose, le module Lean Swaps/Basic.lean garantit — arrivée par rfl, minimalité par énumération décidable sur le témoin Dilemme → Chicken (distance exactement 2). Le module est sans Mathlib et sans sorry ; la minimalité générale reste du côté du générateur, et la frontière est explicitée.
Position dans la série : après les chambres (GT-3) et les murs (GT-3b), les chemins — c’est la métrique de l’espace entier. Le maillon manquant (rapporté en dette) : le quotient par renommage et la structure \(S_4 \times S_4\) comme tore, dont notre espace complet est le dépliage.
Sources et dettes de dérivation
Mesuré dans ce notebook (chaque chiffre est l’output d’une cellule) : distances aux archétypes, distribution complète, vérification exhaustive de la décomposition (331 776 paires), excentricités, multiplicités des plus courts chemins, factorisation \(\binom{12}{6} \times 16^2\), miroir Python du vérificateur, citations de Swaps/Basic.lean aux lignes réelles.
Dettes rapportées, jamais affirmées (mêmes dettes que GT-3b, auxquelles s’ajoutent les nôtres) :
Le quotient 576 → 144 (classes de jeux à renommage des stratégies près) et la structure \(S_4 \times S_4\) comme tore — Robinson et Goforth rapportent cette lecture ; tout ce notebook travaille sur l’espace complet des 576 jeux et n’affirme rien du quotient.
La preuve conceptuelle de la décomposition (indépendance des côtés, graphe de Cayley, produit cartésien de graphes) — nous en livrons l’énumération exhaustive, pas la démonstration générale ; le vocabulaire Coxeter/Mahler est utilisé au strict minimum calculé.
Le tore à 37 trous et la topologie du quotient — hors scope, rapportée.
Les références arXiv (2309.15981, 2102.00053, 1704.02230) — identités vérifiées en première main (API arXiv, passe #11168 du 2026-08-31) : Tohmé & Viglizzo, A categorical representation of games · Czechowski & Piliouras, Poincaré-Bendixson Limit Sets in Multi-Agent Learning · Hedges, Coherence for lenses and open games ; la lecture intégrale des trois reste à faire.
La théorie des mots réduits (16 mots pour le retournement de \(S_4\)) — mesurée par énumération ; la théorie générale des groupes de Coxeter qui l’explique est rapportée.
Module compagnon : game_theory_lean/Swaps/Basic.lean (ce grain) — pur core Lean, sans Mathlib, sans sorry ; lake build Swaps sans dépendance.
Encodages : identiques à GameTheory-3 et GT-3h (tables de rangs 1-4, cellules dans l’ordre haut-gauche, haut-droit, bas-gauche, bas-droit).