GameTheory 20 : Le chemin minimal, témoin construit et vérifié indépendamment — de Robinson-Goforth au vérificateur séparé
Grain B2 de l’EPIC #12205 (Chantier 2 — Génération de témoins et synthèse certifiée : franchir la Loi II).
La loi que ce notebook met à l’épreuve — Loi II du deuxième voyage de digestion ICT :
recoordonner + passer du vérificateur au constructeur : le précédent important n’est pas seulement le changement de coordonnées ; c’est changement de coordonnées plus passage du vérificateur au constructeur.
Elle est franchie une fois sur le substrat Life (Lean-16b : la machine redécouvre le glider au lieu de le recopier, #12286). Le grain B2 demande la même loi sur un substrat totalement différent : l’univers fini des jeux 2×2 ordinaux de Robinson-Goforth. Si la loi ne tient que sur Life, ce n’est pas une loi.
Ici, le vérificateur c’est le solveur qui reconnaît qu’un chemin d’échanges élémentaires relie deux jeux. Le constructeur, c’est la machine qui produit ce chemin — puis un vérificateur séparé qui vérifie, indépendamment, que le chemin est valide et minimal. Le chemin produit est un témoin construit et vérifié indépendamment, pas un certificat au sens formel : dans un univers fini et énumérable, la minimalité se prouve par recherche exhaustive — c’est cette énumération, refaite de zéro, qui fait foi.
Dette de vérification soldée au passage : les chiffres structurels de l’espace de Robinson-Goforth (75 ordres faibles, 5625 jeux à rangs, 576 chambres) étaient au statut RAPPORTÉ depuis la digestion. Chaque section ci-dessous les re-dérive depuis zéro, pur stdlib — rien n’est recopié de GT-3b.
0. Configuration
Représentation héritée de GT-3b / GT-21 : un jeu ordinal 2×2 = une paire de tables de rangs (ligne, colonne), chacune un 4-uplet de rangs {1..4} lu en ligne-major — t[0] et t[1] sont la première ligne, t[2] et t[3] la seconde. Le rang 4 est le meilleur payoff. Tout est pur stdlib : l’univers tient en mémoire, aucune dépendance n’est nécessaire pour énumérer un espace fini.
# === Configuration : GameTheory 20, chemin minimal - temoin construit et verifie independamment ===from itertools import productfrom collections import Counter, dequeprint("GameTheory 20 : chemin minimal (temoin construit et verifie independamment)")print("Representation : jeu = (table_ligne, table_colonne), rangs {1..4}, 4 = meilleur")print("Loi II : le constructeur PRODUIT le chemin, le verificateur separé le VERIFIE independamment")
GameTheory 20 : chemin minimal (temoin construit et verifie independamment)
Representation : jeu = (table_ligne, table_colonne), rangs {1..4}, 4 = meilleur
Loi II : le constructeur PRODUIT le chemin, le verificateur separé le VERIFIE independamment
1. L’univers fini, re-dérivé depuis zéro
Un ordre faible sur 4 cases = un classement avec ex æquo possibles. La clé canonique relabelle les valeurs distinctes par ordre de première apparition : deux 4-uplets décrivant le même classement partagent la même clé. Le nombre d’ordres faibles sur 4 éléments est le nombre de Fubini F₄ ; le notebook le mesure au lieu de le réciter.
# === Section 1.1 : enumeration des ordres faibles sur 4 cases ===def canonique(t):"""Cle canonique d'un 4-uplet : relabelage croissant des valeurs distinctes.""" vals =sorted(set(t))returntuple(vals.index(v) +1for v in t)ordres_faibles =sorted({canonique(t) for t in product(range(1, 5), repeat=4)})stricts = [t for t in ordres_faibles iflen(set(t)) ==4]avec_ex_aequo = [t for t in ordres_faibles iflen(set(t)) <4]print("Ordres faibles sur 4 cases :", len(ordres_faibles), "(nombre de Fubini F4)")print(" stricts (futurs chambers) :", len(stricts))print(" avec ex aequo (futurs murs) :", len(avec_ex_aequo))print("Univers des jeux a rangs : ", len(ordres_faibles), "x", len(ordres_faibles), "=",len(ordres_faibles) **2)print("Univers des chambres strictes :", len(stricts) **2)
Ordres faibles sur 4 cases : 75 (nombre de Fubini F4)
stricts (futurs chambers) : 24
avec ex aequo (futurs murs) : 51
Univers des jeux a rangs : 75 x 75 = 5625
Univers des chambres strictes : 576
Lecture de la sortie committée : 75 ordres faibles — c’est bien le nombre de Fubini F₄, re-dérivé et non récité. Ils se partitionnent en 24 stricts et 51 avec ex æquo, d’où : 5625 jeux à rangs (l’univers complet, murs compris) et 576 chambres strictes (l’univers de Robinson-Goforth classique). Ces trois chiffres étaient RAPPORTÉS depuis la digestion ; ils sont désormais VÉRIFIÉS par ce notebook, indépendamment de GT-3b.
1.2 Les jeux canoniques, encodés
Trois jeux classiques servent de bornes concrètes au constructeur. Encodage standard : pour un jeu symétrique de dilemme 2×2 avec payoffs ordinaux T > R > P > S (défection tentante, punition mutuelle), la table ligne lit (R, S, T, P) et la table colonne (R, T, S, P) — la transposition reflète le fait que chaque joueur lit la même grille de son propre côté. Le Dilemme du Prisonnier suit T > R > P > S, la Poule (Chicken) T > R > S > P, la Chasse au Cerf R > T > P > S.
Dilemme du Prisonnier
Ligne | 3 1 | Colonne | 3 4 |
| 4 2 | | 1 2 |
strict (chambre) : True
Poule (Chicken)
Ligne | 3 2 | Colonne | 3 4 |
| 4 1 | | 2 1 |
strict (chambre) : True
Chasse au Cerf
Ligne | 4 1 | Colonne | 4 3 |
| 3 2 | | 1 2 |
strict (chambre) : True
Identite
Ligne | 1 2 | Colonne | 1 2 |
| 3 4 | | 3 4 |
strict (chambre) : True
Renversement
Ligne | 4 3 | Colonne | 4 3 |
| 2 1 | | 2 1 |
strict (chambre) : True
Les cinq bornes canoniques sont des chambres strictes, toutes dans les 576.
2. Les six swaps générateurs : le permutaèdre des chambres
Sur les chambres, la transformation élémentaire de Robinson-Goforth est l’échange des valeurs adjacentes k et k+1 dans une table : on permute les cases portant ces deux rangs. Trois échanges sont possibles par table (k = 1, 2, 3), donc six par jeu — ce sont les « six swaps générateurs » de la digestion. Le graphe obtenu sur les 24 ordres d’un côté est le permutaèdre S₄ ; sur les 576 chambres, son carré.
# === Section 2.1 : generateur de swap et adjacences des chambres ===def swap_valeurs_adjacentes(t, k):"""Echange les cases portant les valeurs k et k+1 (traversee de la facette k<->k+1).""" pk, pk1 = t.index(k), t.index(k +1) l =list(t) l[pk], l[pk1] = l[pk1], l[pk]returntuple(l)def swap_jeu(jeu, cote, k): row, col = jeuif cote =="ligne":return (swap_valeurs_adjacentes(row, k), col)return (row, swap_valeurs_adjacentes(col, k))# Adjacences sur les 576 chambres : 6 voisins par jeuchambres = [(r, c) for r in stricts for c in stricts]adj_chambres = {g: [swap_jeu(g, cote, k) for cote in ("ligne", "colonne") for k in (1, 2, 3)]for g in chambres}print("Chambres :", len(chambres), "| degre de chaque sommet :", len(adj_chambres[chambres[0]]))# BFS exhaustif depuis l'identite : connexite, diametre, distribution des distancesdef bfs_complet(depart, voisins): dist = {depart: 0} q = deque([depart])while q: u = q.popleft()for v in voisins(u):if v notin dist: dist[v] = dist[u] +1 q.append(v)return distdist_identite = bfs_complet(IDENTITE, lambda g: adj_chambres[g])print("Graphe des chambres : connexe =", len(dist_identite) ==576,"| diametre =", max(dist_identite.values()))print(" repartition des distances :", dict(sorted(Counter(dist_identite.values()).items())))
Lecture de la sortie committée : le graphe des 576 chambres est connexe, de diamètre 12 — six par côté, la distance d’un jeu étant la somme des distances de ses deux tables. La distribution est symétrique (même effectif à d et 12−d) : l’involution qui renverse tous les rangs des deux tables est une isométrie du permutaèdre. Le diamètre par table seule est 6, atteint par le renversement (1,2,3,4) → (4,3,2,1) : chacune des six paires de positions doit être corrigée exactement une fois.
3. Le constructeur
C’est le geste que le vérificateur ne sait pas faire : étant donnés deux jeux G et H, produire une suite d’échanges élémentaires qui mène de l’un à l’autre. Le constructeur parcourt le permutaèdre en largeur depuis G, mémorise pour chaque sommet visité le move qui y a mené, puis remonter la chaîne des parents depuis H exhume le chemin. Il ne connaît ni les jeux classiques, ni les noms — il ne connaît que le graphe.
# === Section 3.1 : construire_chemin -- le constructeur temoin ===def construire_chemin(depart, arrivee, voisins):"""Produit une suite (jeu, move) de depart a arrivee par BFS + remontee des parents.""" parent = {depart: None} q = deque([depart])while q: u = q.popleft()if u == arrivee:breakfor v in voisins(u):if v notin parent: parent[v] = u q.append(v)if arrivee notin parent:returnNone chaine = [] cur = arriveewhile parent[cur] isnotNone: pred = parent[cur] chaine.append((pred, cur)) cur = pred chaine.reverse()return chainedef nommer_pas(pred, cur):"""Nomme le move elementaire entre deux jeux consecutifs (cote, valeurs echangees)."""for cote, table in (("ligne", 0), ("colonne", 1)):if pred[table] != cur[table]:for k in (1, 2, 3):if swap_jeu(pred, cote, k) == cur:returnf"swap {cote} ({k} <-> {k +1})"return"?"chemin_pd_poule = construire_chemin(PD, POULE, lambda g: adj_chambres[g])print("Chemin minimal construit : Dilemme du Prisonnier -> Poule")print(f" {PD[0]} | {PD[1]} (depart)")for pred, cur in chemin_pd_poule:print(f" -- {nommer_pas(pred, cur)} --> {cur[0]} | {cur[1]}")print(f"Longueur du chemin produit : {len(chemin_pd_poule)} pas")
Chemin minimal construit : Dilemme du Prisonnier -> Poule
(3, 1, 4, 2) | (3, 4, 1, 2) (depart)
-- swap ligne (1 <-> 2) --> (3, 2, 4, 1) | (3, 4, 1, 2)
-- swap colonne (1 <-> 2) --> (3, 2, 4, 1) | (3, 4, 2, 1)
Longueur du chemin produit : 2 pas
Lecture de la sortie committée : le constructeur produit le chemin — deux pas exactement : un échange (1 ↔︎ 2) côté ligne (la punition mutuelle P et la soumission S échangent leurs rangs) et un échange (1 ↔︎ 2) côté colonne. Géométriquement, PD et Poule sont deux chambres voisines-à-deux- pas dans le permutaèdre : ils ne diffèrent que par l’ordre des deux mauvais payoffs, le meilleur (T) et le moyen (R) étant aux mêmes positions. Le dilemme et le jeu du poule : deux mondes séparés par la seule question « quelle misère préférer ». La machine ne le savait pas — elle l’a construit.
# === Section 3.2 : le constructeur sur l'antipode ===chemin_renverse = construire_chemin(IDENTITE, RENVERSE, lambda g: adj_chambres[g])print("Chemin minimal construit : Identite -> Renversement (les deux antipodes du permutaedre)")for i, (pred, cur) inenumerate(chemin_renverse):print(f" pas {i +1:>2} : {nommer_pas(pred, cur)}")print(f"Longueur : {len(chemin_renverse)} pas (le diametre exact du permutaedre S4 x S4)")chemin_pd_cerf = construire_chemin(PD, CERF, lambda g: adj_chambres[g])print()print("Dilemme -> Chasse au Cerf :", len(chemin_pd_cerf), "pas :", [nommer_pas(p, c) for p, c in chemin_pd_cerf])
Chemin minimal construit : Identite -> Renversement (les deux antipodes du permutaedre)
pas 1 : swap ligne (1 <-> 2)
pas 2 : swap ligne (2 <-> 3)
pas 3 : swap ligne (1 <-> 2)
pas 4 : swap ligne (3 <-> 4)
pas 5 : swap ligne (2 <-> 3)
pas 6 : swap ligne (1 <-> 2)
pas 7 : swap colonne (1 <-> 2)
pas 8 : swap colonne (2 <-> 3)
pas 9 : swap colonne (1 <-> 2)
pas 10 : swap colonne (3 <-> 4)
pas 11 : swap colonne (2 <-> 3)
pas 12 : swap colonne (1 <-> 2)
Longueur : 12 pas (le diametre exact du permutaedre S4 x S4)
Dilemme -> Chasse au Cerf : 2 pas : ['swap ligne (3 <-> 4)', 'swap colonne (3 <-> 4)']
Lecture de la sortie committée : l’antipode exige les 12 pas du diamètre — chaque paire de positions des deux tables doit être corrigée exactement une fois, et le constructeur les exhume toutes. Ces douze pas se répartissent en deux blocs de six — swaps ligne aux pas 1 à 6, puis swaps colonne aux pas 7 à 12 : chaque table est renversée indépendamment, image directe de la structure produit S₄ × S₄. PD → Cerf est plus proche qu’il n’y paraît : deux pas, les échanges (3 ↔︎ 4) de chaque côté — seul l’ordre du meilleur payoff (coopération mutuelle R contre défection tentante T) change. La paire dilemme/cerf, structuralement opposée en théorie des jeux (dilemme social contre jeu de coordination), est géométriquement contiguë : c’est la lecture de Robinson-Goforth, reconstruite par la machine.
4. Le vérificateur séparé — le témoin
Produire un chemin ne suffit pas : encore faut-il le vérifier indépendamment — validité et minimalité. Le témoin honnête exige un vérificateur qui ne réutilise aucun état du constructeur : il re-dérive tout. Trois verdicts doivent être distingués — sinon le vérificateur n’est qu’un tampon :
VALIDE + MINIMAL : chaque pas est un swap élémentaire, les extrémités sont exactes, et la longueur égale la distance exhaustive d(G, H) ;
VALIDE + NON MINIMAL : le chemin marche mais un détour existe ;
INVALIDE : au moins un pas n’est pas un move élémentaire (ou les extrémités mentent).
La minimalité se prouve par recherche exhaustive : BFS complet depuis G — l’univers est fini, 5625 ou 576 sommets, l’énumération totale EST la preuve qu’aucun raccourci n’existe.
# === Section 4.1 : verifier_chemin -- le verificateur independant ===def pas_elementaire_valide(pred, cur):"""True ssi cur s'obtient de pred par exactement un swap elementaire."""return cur in adj_chambres.get(pred, [])def verifier_chemin(depart, arrivee, chaine, voisins):"""Verdict independant : re-derive TOUT, ne reutilise rien du constructeur."""if chaine isNoneorlen(chaine) ==0:return"INVALIDE : chemin vide"if chaine[0][0] != depart or chaine[-1][1] != arrivee:return"INVALIDE : les extremites ne sont pas celles annoncees"for pred, cur in chaine:ifnot pas_elementaire_valide(pred, cur):returnf"INVALIDE : pas non elementaire vers {cur}" dist = bfs_complet(depart, voisins) # recherche exhaustive : la preuve de minimalite d_reel = dist[arrivee]iflen(chaine) != d_reel:returnf"VALIDE mais NON MINIMAL : {len(chaine)} pas, distance reelle {d_reel}"returnf"VALIDE + MINIMAL : {len(chaine)} pas = distance exhaustive d(G,H)"# Les trois verdicts, demontres sur des cas construits pour euxprint("1. Le chemin du constructeur (PD -> Poule) :")print(" ", verifier_chemin(PD, POULE, chemin_pd_poule, lambda g: adj_chambres[g]))voisin_poule = swap_jeu(POULE, "ligne", 1) # un voisin quelconque de l'arriveechemin_detour = chemin_pd_poule + [ # aller-retour artificiel : revient bien a POULE (POULE, voisin_poule), (voisin_poule, POULE)]print("2. Le meme chemin rallonge d'un aller-retour :")print(" ", verifier_chemin(PD, POULE, chemin_detour, lambda g: adj_chambres[g]))faux_pas = [(PD, CERF)] # un seul saut PD -> Cerf : les jeux ne sont PAS adjacentsprint("3. Un 'chemin' en un pas vers un jeu non adjacent :")print(" ", verifier_chemin(PD, CERF, faux_pas, lambda g: adj_chambres[g]))
1. Le chemin du constructeur (PD -> Poule) :
VALIDE + MINIMAL : 2 pas = distance exhaustive d(G,H)
2. Le meme chemin rallonge d'un aller-retour :
VALIDE mais NON MINIMAL : 4 pas, distance reelle 2
3. Un 'chemin' en un pas vers un jeu non adjacent :
INVALIDE : pas non elementaire vers ((4, 1, 3, 2), (4, 3, 1, 2))
Lecture de la sortie committée : les trois verdicts tombent, distincts. Le chemin du constructeur est VALIDE + MINIMAL (2 pas = distance exhaustive). Le même chemin avec un aller-retour greffé est VALIDE mais NON MINIMAL — le vérificateur voit le détour. Et le saut direct PD → Cerf est INVALIDE : un pas non élémentaire, parce que les deux chambres ne sont pas adjacentes. Le vérificateur n’est pas un tampon : il rend trois réponses différentes sur trois défauts différents. C’est la séparation constructeur/vérificateur de la Loi II — le même geste que la preuve by decide du translateur de Life, ici sur le substrat fini des jeux.
4.2 La non-unicité : compter les géodésiques
Un chemin minimal n’est jamais seul. Les géodésiques entre deux jeux forment les « mondes minimaux » — autant de façons distinctes de transformer l’un en l’autre sans un pas de trop. Le comptage se fait par le DAG des couches BFS : un sommet de couche d reçoit ses chemins de ses prédécesseurs de couche d−1. Pour le renversement d’une table (l’antipode du permutaèdre S₄), la combinatoire des groupes de Coxeter prédit que le nombre de mots réduits de l’élément le plus long w₀ de S₄ vaut 16 — une prédiction externe que la mesure peut contredire.
# === Section 4.2 : comptage des geodesiques par le DAG des couches ===def compter_geodesiques(depart, arrivee, voisins):"""Nombre de chemins minimaux : produits des chemins entrants, couche par couche.""" dist = bfs_complet(depart, voisins) d = dist[arrivee] nb = {depart: 1}for couche inrange(1, d +1):for u, du in dist.items():if du == couche: nb[u] =sum(nb[v] for v in voisins(u) if dist.get(v) == couche -1)return nb[arrivee]# Cote seul : 24 ordres, antipode (1,2,3,4) -> (4,3,2,1)adj_table = {t: [swap_valeurs_adjacentes(t, k) for k in (1, 2, 3)] for t in stricts}geos_table = compter_geodesiques((1, 2, 3, 4), (4, 3, 2, 1), lambda t: adj_table[t])print("Geodesiques (1,2,3,4) -> (4,3,2,1) sur une table :", geos_table,"(mots reduits de w0 dans S4 : 16 attendus)")# Jeu complet : PD -> Poulegeos_pd_poule = compter_geodesiques(PD, POULE, lambda g: adj_chambres[g])print("Geodesiques PD -> Poule sur les 576 chambres :", geos_pd_poule)geos_renverse = compter_geodesiques(IDENTITE, RENVERSE, lambda g: adj_chambres[g])print("Geodesiques Identite -> Renversement (diametre 12) :", geos_renverse)
Geodesiques (1,2,3,4) -> (4,3,2,1) sur une table : 16 (mots reduits de w0 dans S4 : 16 attendus)
Geodesiques PD -> Poule sur les 576 chambres : 2
Geodesiques Identite -> Renversement (diametre 12) : 236544
Lecture de la sortie committée : la mesure donne 16 géodésiques pour le renversement d’une table — exactement le nombre de mots réduits de w₀ dans S₄ que prédit la théorie des groupes de Coxeter. La mesure rejoint la combinatoire connue : le DAG des couches ne calcule rien d’autre que les expressions réduites du plus long élément. Pour le jeu complet, la composition n’est pas un simple produit : les pas des deux côtés s’entrelacent. PD → Poule (un pas par table) offre 2 géodésiques — l’ordre des deux pas ; l’antipode complet en offre 236 544 = 16 × 16 × 924, les mots réduits par côté multipliés par les C(12,6) = 924 entrelacements des deux séquences de six pas. Le chemin produit au §3 n’était qu’un tirage parmi cette flore.
5. L’univers à rangs complet : traverser les murs
Le permutaèdre ne couvre que les chambres. L’univers à rangs complet (5625) inclut les murs — les jeux à égalités, strates de codimension ≥ 1 de GT-3b. Deux moves élémentaires s’ajoutent aux swaps : make_tie (coalescence des valeurs k et k+1 : la chambre descend sur un mur) et son inverse break_tie (résoudre l’ex æquo dans un sens ou l’autre : traverser). En graphe non orienté, les deux directions d’un même edge suffisent : coalescer depuis chacune des chambres adjacentes énumère toutes les résolutions du mur.
La question que seul l’univers complet peut trancher : les murs sont-ils des raccourcis ? Un chemin qui passe par un mur peut-il être plus court que la géodésique des chambres ? L’intuition suggère que oui — un swap dans un mur déplace un bloc fusionné d’un seul coup. La mesure va décider, et elle ne suit pas l’intuition.
# === Section 5.1 : l'univers complet, swaps + make_tie, et son diametre ===def faire_le_tie(t, k):"""Coalescence des valeurs k et k+1 -> forme canonique du mur."""return canonique(tuple(k if v == k +1else v for v in t))def voisins_complets(jeu):"""Swaps (toujours valides dans une table a rangs) + make_tie (descente sur un mur). Break_tie = le meme edge pris dans l'autre sens.""" row, col = jeu res = []for cote, t in (("ligne", row), ("colonne", col)): valeurs =set(t)for k in (1, 2, 3):if k in valeurs and k +1in valeurs: res.append(swap_jeu(jeu, cote, k)) t2 = faire_le_tie(t, k)if t2 != t: res.append((t2, col) if cote =="ligne"else (row, t2))return resunivers = [(r, c) for r in ordres_faibles for c in ordres_faibles]dist_univers = bfs_complet(IDENTITE, voisins_complets)print("Univers complet :", len(univers), "sommets, atteints :", len(dist_univers),"(connexe :", len(dist_univers) ==len(univers), ")")print("Diametre de l'univers complet :", max(dist_univers.values()))print(" (a comparer au diametre 12 du seul permutaedre des chambres)")print(" repartition :", dict(sorted(Counter(dist_univers.values()).items())))
Univers complet : 5625 sommets, atteints : 5625 (connexe : True )
Diametre de l'univers complet : 12
(a comparer au diametre 12 du seul permutaedre des chambres)
repartition : {0: 1, 1: 12, 2: 68, 3: 240, 4: 578, 5: 990, 6: 1232, 7: 1128, 8: 785, 9: 402, 10: 149, 11: 36, 12: 4}
Lecture de la sortie committée : l’univers complet est connexe — coalescences et traversées relient les 5625 — mais son diamètre reste 12, identique au permutaèdre des chambres, avec les mêmes 4 antipodes. La répartition culmine à 1232 sommets à la distance 6 — le milieu exact de l’intervalle [0, 12] — la distribution garde sa masse maximale en couche 6 et retombe exactement sur les mêmes extrêmes. L’intuition « les murs raccourcissent » vient de se heurter à un premier fait : au niveau du diamètre, rien ne bouge. Reste à savoir si les murs raccourcissent certaines distances locales — c’est l’objet du §5.2, qui le décide par énumération exhaustive.
# === Section 5.2 : les murs raccourcissent-ils ? decision par enumeration exhaustive ===# Les generateurs ne touchent qu'un cote a la fois : les deux graphes sont des produits.# Donc d_jeu(G, H) = d_cote(row_G, row_H) + d_cote(col_G, col_H) dans CHAQUE univers.# Il suffit donc de comparer, cote par cote, les distances des 24 x 24 paires d'ordres stricts# dans le permutaedre (24 noeuds) et dans l'espace a rangs complet (75 noeuds).def voisins_cote_perm(t):return [swap_valeurs_adjacentes(t, k) for k in (1, 2, 3) if k in t and k +1in t]def voisins_cote_full(t): res = []for k in (1, 2, 3):if k in t and k +1in t: res.append(swap_valeurs_adjacentes(t, k)) t2 = faire_le_tie(t, k)if t2 != t: res.append(t2)return resecarts =0for a in stricts: d_perm = bfs_complet(a, voisins_cote_perm) d_full = bfs_complet(a, voisins_cote_full)for b in stricts:if d_perm[b] != d_full[b]: ecarts +=1print("Paires d'ordres stricts comparees (24 x 24) : 576")print("Paires ou l'espace complet (murs autorises) est PLUS COURT que le permutaedre :", ecarts)print()print("Par structure produit, le verdict couvre les 576 x 576 = 330 776 paires de chambres :")print(" les murs ne raccourcissent AUCUNE distance inter-chambres.")# Le constructeur, confirme sur un cas : il ignore les murs de lui-memechemin_full = construire_chemin(PD, RENVERSE, voisins_complets)murs_traverses =sum(1for _, cur in chemin_fulliflen(set(cur[0])) <4orlen(set(cur[1])) <4)chemin_pur = construire_chemin(PD, RENVERSE, lambda g: adj_chambres[g])print()print(f"PD -> Renversement : univers complet {len(chemin_full)} pas dont {murs_traverses} sur un mur ;",f"chambres seules {len(chemin_pur)} pas")print("Verificateur (univers complet) :", verifier_chemin(PD, RENVERSE, chemin_full, voisins_complets))
Paires d'ordres stricts comparees (24 x 24) : 576
Paires ou l'espace complet (murs autorises) est PLUS COURT que le permutaedre : 0
Par structure produit, le verdict couvre les 576 x 576 = 330 776 paires de chambres :
les murs ne raccourcissent AUCUNE distance inter-chambres.
PD -> Renversement : univers complet 5 pas dont 0 sur un mur ; chambres seules 5 pas
Verificateur (univers complet) : VALIDE + MINIMAL : 5 pas = distance exhaustive d(G,H)
Lecture de la sortie committée : la décision est nulle et exhaustive — sur les 576 paires d’ordres stricts comparées côté par côté, aucune n’est plus courte par les murs ; et parce que les générateurs ne touchent qu’un côté à la fois (structure produit), ce verdict par côté couvre les 330 776 paires de chambres sans exception. Le mécanisme se voit sur le cas concret : le constructeur lâché dans l’univers complet produit un chemin qui ne pose jamais le pied sur un mur — la même longueur, 5 pas, que dans les chambres seules, et le vérificateur séparé l’atteste minimal dans l’univers élargi. Descendre sur un mur coûte un pas, en sortir en coûte un autre, et le swap qui déplace le bloc fusionné ne récupère jamais plus que ces deux pas investis. Les murs de GT-3b ne sont donc pas des tunnels : ce sont des strates que la géométrie des chambres regarde traverser sans jamais y gagner un pas. Un résultat négatif — mais prouvé par énumération complète, et c’est lui qui donne sa valeur au témoin : la minimalité ne dit pas seulement « pas de détour », elle dit « pas de détour, même par les murs ».
6. L’epaisseur des murs — les chambres en forme extensive
Les cinq sections precedentes repondent a une question de classement : quelle chambre contient cette matrice, et quel est le chemin minimal d’une chambre a l’autre. En forme normale, le mur entre deux chambres est une frontiere de nomenclature : on le franchit en changeant de matrice, pas en jouant. La question extensive deplace le sujet : quel chemin causal et informationnel rend une issue atteignable a matrice fixee ? Le mur cesse d’etre une etiquette pour devenir un objet traversable-sous-conditions — ce qui le franchit est une promesse ou une menace croyable, et la croyabilite est exactement ce que l’arbre sait calculer (sous-jeux, induction a rebours), comme GT-22 traite le mur w = l comme separateur de codimension 1 plutot que comme un nom.
Le dispositif. Avant le jeu de base, le joueur Ligne choisit un engagement observable : se taire, promettre (se lier a Cooperer — la force acquise en se privant d’une option, Schelling), ou menacer (programmer une punition si Colonne defectionne). Chaque variante devient un arbre explicite : noeuds de decision, ensembles d’information (singletons ici, l’engagement etant observe — la partition est imprimee avec l’arbre), feuilles valorisees. La croyabilite n’est jamais assertee : elle se decide par induction a rebours au sous-jeu de punition.
Unites. Les issues du jeu de base gardent les rangs {1..4} de la chambre ; l’issue de punition porte des utilites cardinales (0,0), sous le plancher ordinal des rangs — n’importe quelle utilite coherente avec l’ordre de la chambre donne le meme verdict (robustesse ordinale).
# === Section 6.1 : moteur de forme extensive — arbre, ensembles d'information, induction a rebours ===def feuille(u1, u2, nom):return {"type": "feuille", "u": (u1, u2), "nom": nom}def decision(joueur, enfants, info):# info : etiquette de l'ensemble d'information (singleton = information parfaite)return {"type": "decision", "joueur": joueur, "enfants": enfants, "info": info}def valeur_spe(noeud):"""Valeur d'equilibre parfait en sous-jeux par induction a rebours."""if noeud["type"] =="feuille":return noeud["u"] joueur = noeud["joueur"] meilleures, best = [], Nonefor action, enfant in noeud["enfants"].items(): v = valeur_spe(enfant)if best isNoneor v[joueur] > best[joueur]: best, meilleures = v, [action]elif v[joueur] == best[joueur]: meilleures.append(action)return bestdef chemin_spe(noeud, trace=None):"""Decompte du chemin d'equilibre (actions choisies a chaque noeud).""" trace = [] if trace isNoneelse traceif noeud["type"] =="feuille":return [(list(trace), noeud["nom"], noeud["u"])] joueur = noeud["joueur"] best_u = valeur_spe(noeud) sorties = []for action, enfant in noeud["enfants"].items(): v = valeur_spe(enfant)if v[joueur] == best_u[joueur]: sorties.extend(chemin_spe(enfant, trace + [f"J{joueur+1}:{action}"]))return sortiesdef partition_information(noeud, acc=None):"""Recense les ensembles d'information explicites de l'arbre.""" acc = [] if acc isNoneelse accif noeud["type"] =="decision": acc.append(noeud["info"])for enfant in noeud["enfants"].values(): partition_information(enfant, acc)return accprint("Moteur : induction a rebours sur arbre fini, ensembles d'information explicites.")print("Test de coherence sur un mini-arbre a menace choisie :")# mini-arbre de controle : J1 punit ou laisse apres une defection observeetest = decision(0, {"laisser": feuille(1, 4, "laisser (S,T)"),"punir": feuille(0, 0, "punir (0,0)"),}, "test:punition")u = valeur_spe(test)choix = chemin_spe(test)[0][0][-1]print(f" sous-jeu de punition : valeur SPE = {u}, action retenue = {choix}")print(f" -> punir rapporte 0 < laisser 1 au punisseur : la menace CHOISIE est INCROYABLE")print(" (le verdict vient de l'induction, pas d'une assertion).")
Moteur : induction a rebours sur arbre fini, ensembles d'information explicites.
Test de coherence sur un mini-arbre a menace choisie :
sous-jeu de punition : valeur SPE = (1, 4), action retenue = J1:laisser
-> punir rapporte 0 < laisser 1 au punisseur : la menace CHOISIE est INCROYABLE
(le verdict vient de l'induction, pas d'une assertion).
Lecture de la sortie commitee : sur le sous-jeu de punition seul, l’induction retient laisser (1 > 0 pour le punisseur) — une menace laissee au choix de son auteur ne survit pas a l’induction a rebours. C’est le critere operational de la section : la meme menace, programmee (branche retiree de l’arbre), devient croyable par construction. Reste a mesurer ce que chaque forme d’engagement fait au jeu de base, chambre par chambre.
# === Section 6.2 : le Dilemme en forme extensive — trois engagements, trois arbres ===def extraire_cellule(jeu, i, j):# (table_ligne, table_colonne) -> utilites cardinales (u1, u2) de la case (i,j) tl, tc = jeureturn (tl[2* i + j], tc[2* i + j])PD_CELLULES = {(i, j): extraire_cellule(PD, i, j) for i in (0, 1) for j in (0, 1)}CERF_CELLULES = {(i, j): extraire_cellule(CERF, i, j) for i in (0, 1) for j in (0, 1)}P = PD_CELLULES # alias compact pour le Dilemmedef arbre_dilemme(mode):"""Arbre extensif du Dilemme selon l'engagement de Ligne (J0). mode = 'silence' : jeu de base simultane approxime par la forme normale (aucune influence) mode = 'promesse' : J1 se lie a C (branche D retiree), engagement OBSERVABLE mode = 'menace_choisie' : apres (C,D), J1 choisit encore punir/laisser mode = 'menace_programmee' : apres (C,D), la punition est automatique (branche retiree) """if mode =="silence":# forme strategique du Dilemme : enumeration des reponses, meilleure pour J2def suite_silence(j2):# J1 joue sa meilleure reponse a j2 dans la matrice du Dilemme u_cd, u_dd = P[(1, j2)], None meilleure_j1 =0if P[(0, j2)][0] > P[(1, j2)][0] else1return P[(meilleure_j1, j2)]return decision(1, {"C": feuille(*suite_silence(0), "(BR,C)"),"D": feuille(*suite_silence(1), "(BR,D)"), }, "silence:J2-jeu-de-base")if mode =="promesse":return decision(1, {"C": feuille(*P[(0, 0)], "(C,C)"),"D": feuille(*P[(0, 1)], "(C,D)"), }, "promesse:J2-observe-C-force")if mode =="menace_choisie": punition = decision(0, {"laisser": feuille(*P[(0, 1)], "(C,D)-laissee"),"punir": feuille(0, 0, "(C,D)-punie"), }, "menace:J1-choisit")return decision(1, {"C": feuille(*P[(0, 0)], "(C,C)"),"D": punition, }, "menace-choisie:J2-observe")if mode =="menace_programmee":return decision(1, {"C": feuille(*P[(0, 0)], "(C,C)"),"D": feuille(0, 0, "(C,D)-punie-automatiquement"), }, "menace-programmee:J2-observe")VERDICTS = {}for mode in ("silence", "promesse", "menace_choisie", "menace_programmee"): arbre = arbre_dilemme(mode) u = valeur_spe(arbre) chemins = chemin_spe(arbre) infos = partition_information(arbre) VERDICTS[mode] = uprint(f"--- Dilemme / engagement = {mode}")print(f" ensembles d'information : {infos}")for trace, nom, uu in chemins:print(f" chemin SPE {' -> '.join(trace):38s} issue {nom:32s} utilites {uu}")print(f" valeur SPE : {u}")print()cooperative = P[(0, 0)]print(f"Play cooperatif (C,C) = {cooperative} (utilites du Dilemme)")for mode, u in VERDICTS.items(): atteint ="ATTEINTE "if u == cooperative else"inatteignable"print(f" {mode:18s} -> {u} : transition vers le play cooperatif : {atteint}")
Lecture de la sortie commitee : a matrice fixee dans la chambre Dilemme, la transition vers le play cooperatif (3,3) est inatteignable au silence (l’equilibre de meilleure reponse reste la defection mutuelle), inatteignable par la promesse seule (Colonne exploite la main liee : (1,4)), inatteignable par la menace choisie (l’induction du sous-jeu de punition la retourne : laisser domine punir, et Colonne anticipe) — et atteinte par la menace programmee observable (3,3), la punition ne s’executant jamais : c’est une dissuasion. Le mur n’a pas ete franchi dans l’atlas des 576 chambres — la matrice n’a pas bouge d’un rang — mais le play a traverse ce que la forme normale tenait pour une frontiere. C’est l’epaisseur du mur : non pas une distance dans le permutaedre, mais un ensemble d’arbres d’engagement capables ou non de conduire a l’issue.
# === Section 6.3 : la Chasse au Cerf — la meme promesse, une autre epaisseur ===CC = CERF_CELLULESdef arbre_cerf_promesse():# Ligne se lie a traquer le cerf (C), engagement observable ; Colonne repondreturn decision(1, {"C": feuille(*CC[(0, 0)], "(C,C)"),"D": feuille(*CC[(0, 1)], "(C,D)"), }, "cerf:J2-observe-C-force")def arbre_cerf_silence():def suite_silence(j2): meilleure_j1 =0if CC[(0, j2)][0] > CC[(1, j2)][0] else1return CC[(meilleure_j1, j2)]return decision(1, {"C": feuille(*suite_silence(0), "(BR,C)"),"D": feuille(*suite_silence(1), "(BR,D)"), }, "cerf-silence:J2-jeu-de-base")for mode, arbre in [("silence", arbre_cerf_silence()), ("promesse observable", arbre_cerf_promesse())]: u = valeur_spe(arbre)print(f"--- Cerf / engagement = {mode}")print(f" ensembles d'information : {partition_information(arbre)}")for trace, nom, uu in chemin_spe(arbre):print(f" chemin SPE {' -> '.join(trace):38s} issue {nom:10s} utilites {uu}")print(f" valeur SPE : {u}")print()print(f"Play cooperatif (C,C) du Cerf = {CC[(0, 0)]}")print("Au silence, le Cerf coordonne aussi sur (C,C) par meilleures reponses croisees :")print("la promesse y est AUTO-EXECUTOIRE (C est deja meilleure reponse a C), le mur du Cerf")print("etait poreux ; celle du Dilemme exigeait l'automatisation de la punition.")print("Memoriser : la MEME promesse, deux chambres, deux epaisseurs de mur.")
--- Cerf / engagement = silence
ensembles d'information : ['cerf-silence:J2-jeu-de-base']
chemin SPE J2:C issue (BR,C) utilites (4, 4)
valeur SPE : (4, 4)
--- Cerf / engagement = promesse observable
ensembles d'information : ['cerf:J2-observe-C-force']
chemin SPE J2:C issue (C,C) utilites (4, 4)
valeur SPE : (4, 4)
Play cooperatif (C,C) du Cerf = (4, 4)
Au silence, le Cerf coordonne aussi sur (C,C) par meilleures reponses croisees :
la promesse y est AUTO-EXECUTOIRE (C est deja meilleure reponse a C), le mur du Cerf
etait poreux ; celle du Dilemme exigeait l'automatisation de la punition.
Memoriser : la MEME promesse, deux chambres, deux epaisseurs de mur.
Lecture de la sortie commitee : la promesse liee-au-cerf est auto-executoire — dans la chambre Cerf, cooperer est deja la meilleure reponse a cooperer, l’engagement ne retire qu’un risk de coordination, le play cooperatif etait atteignable sans lui. Dans la chambre Dilemme, la meme promesse livree a Colonne ne vaut que le rang du dindon de la farce (1,4). La forme extensive ne deplace pas la chambre ; elle mesure la resistance du mur a chaque engin de traversree — et cette resistance est une propriete ordinale de la chambre (T>R>P>S vs R>T>P>S), donc un invariant de l’atlas Robinson-Goforth lui-meme : deux chambres adjacentes peuvent porter des epaisseurs tres differentes pour le meme engagement.
7. Ce que la loi autorise à dire — et ce qu’elle n’autorise pas
Ce qui est acquis : le passage du vérificateur au constructeur est fait sur un second substrat. Étant donnés deux jeux, la machine produit la suite d’opérations élémentaires qui transforme l’un en l’autre, et un vérificateur séparé vérifie indépendamment validité et minimalité par énumération exhaustive de l’univers. Les trois verdicts du vérificateur sont distincts et opposables ; le comptage des géodésiques rejoint la combinatoire de Coxeter (16 mots réduits de w₀ par table, composés en 236 544 par entrelacement) ; et le théorème négatif du §5 est prouvé par énumération complète : les murs ne raccourcissent aucune distance inter-chambres — le diamètre reste 12. La loi n’était pas une spécificité de Life, et le substrat des jeux a livré une géométrie que le seul permutaèdre ne montrait pas.
Ce qui n’est PAS acquis — les frontières honnêtes :
Ordinal 2×2 uniquement. L’espace des jeux à payoffs cardinaux, ou même 3×3 ordinaux, n’est ni énuméré ni borné ici ; la vérification par exhaustivité meurt avec la finitude.
Le chemin est une géométrie, pas une dynamique. Rien ne dit qu’un processus d’adaptation suiverait une géodésique ; les swaps ne sont pas des coups que des joueurs jouent.
La minimalité est relative au jeu de moves. Avec swaps seuls, ou swaps + murs, les distances diffèrent (12 contre 6) : le verdict énonce « minimal pour CES générateurs », jamais « le plus court possible dans l’absolu ».
Pas de jambe Lean dans ce grain. La vérification est l’énumération exhaustive Python ; la formalisation by decide de la validité d’un pas est la variante naturelle suivante — c’est exactement la forme d’itération (-b, -c) que l’EPIC #12205 prescrit.
Sources — Robinson & Goforth (1978), The Topology of the 2×2 Games (cité, RAPPORTÉ) ; Bruns-Kimmich via GT-3b (#12213, VÉRIFIÉ sur ce substrat) ; chambres/murs/make_tie : GT-3b livré (#12253) ; le précédent constructeur : Lean-16b translateur Life (#12286). Chiffres structurels re-dérivés ici : 75, 576, 5625, diamètre 12 dans les deux univers, théorème du non-raccourci, géodésiques 16 / 2 / 236 544 (VÉRIFIÉS par ce notebook).
Exercices
Les trois exercices utilisent le constructeur, le vérificateur et le compteur de géodésiques définis plus haut. Le notebook s’exécute de bout en bout même sans les compléter.
Exercice 1 — Le chemin retour
Construire le chemin Poule → Dilemme et le soumettre au vérificateur séparé. Vérifier que le constructeur produit bien le même nombre de pas qu’à l’aller — et expliquer pourquoi la distance est symétrique.
# Exercice 1 : chemin retour Poule -> Dilemme, construit puis verifie independamment.# Etape 1 : chemin_retour = construire_chemin(POULE, PD, lambda g: adj_chambres[g])# Etape 2 : verdict = verifier_chemin(POULE, PD, chemin_retour, lambda g: adj_chambres[g])# Indice : la symetrie vient de ce que chaque swap est sa propre reciproque.chemin_retour =None# TODO etudiantprint("Exercice 1 : a completer (chemin retour Poule -> Dilemme)")
Exercice 1 : a completer (chemin retour Poule -> Dilemme)
Exercice 2 — Les géodésiques d’une autre paire
Compter les géodésiques Dilemme → Chasse au Cerf dans l’univers complet (murs autorisés), et comparer au compte dans les chambres seules. Le mur crée-t-il de nouveaux mondes minimaux ?
# Exercice 2 : geodesiques PD -> Cerf, univers complet vs chambres.# Etape 1 : compter_geodesiques(PD, CERF, voisins_complets)# Etape 2 : comparer a compter_geodesiques(PD, CERF, lambda g: adj_chambres[g])# Indice : si la distance change entre les deux univers, le compte change aussi.nb_geodesiques_complet =None# TODO etudiantnb_geodesiques_chambres =None# TODO etudiantprint("Exercice 2 : a completer (geodesiques PD -> Cerf, deux univers)")
Exercice 2 : a completer (geodesiques PD -> Cerf, deux univers)
Exercice 3 — Un couple antipodal de l’univers complet
Trouver un jeu H à distance maximale du Dilemme dans l’univers complet (5625), construire le chemin, et le soumettre au vérificateur séparé. Indice : la distribution des distances du §5.1 dit quelle couche chercher.
# Exercice 3 : antipode du Dilemme dans l'univers complet (5625).# Etape 1 : recalculer bfs_complet(PD, voisins_complets), chercher les sommets de distance max.# Etape 2 : construire_chemin + verifier_chemin vers l'un d'eux.# Indice : l'antipode n'est pas unique -- la couche maximale compte plusieurs sommets.antipode_pd =None# TODO etudiant : le jeu (row, col) a distance maximale de PDprint("Exercice 3 : a completer (antipode du Dilemme dans l'univers complet)")
Exercice 3 : a completer (antipode du Dilemme dans l'univers complet)
Exercice 4 — La Poule en forme extensive
La chambre Poule (T>R>S>P) a deux equilibres purs en strategies : (C,D) et (D,C). Un eleve de Robinson-Goforth propose : « Ligne s’engage OBSERVABLEMENT a faire le mort (se lier a D) ; Colonne, voyant la roue abandonnee, fait pareil par prudence… non, s’ecarte ! »
Construisez l’arbre arbre_poule_engagement_D (Ligne liee a D, observable, Colonne repond), executeriez l’induction, et comparez a (C,C). Le mur de la Poule est-il poreux a cet engin-là ? Quel engagement rendrait (C,C) atteignable — et pourquoi la reponse est-elle plus difficile que pour le Cerf ?
# Exercice 4 : Poule en forme extensive — Ligne liee a D, observable.# Indice : reutilisez extraire_cellule(POULE, i, j), decision(), valeur_spe(), chemin_spe().# Etape 1 : construire POULE_CELLULES.# Etape 2 : construire l'arbre (branche D de Ligne retiree, Colonne observe).# Etape 3 : verdict — valeur SPE vs (C,C), chemin d'equilibre.POULE_CELLULES =None# TODO etudiantarbre_poule_engagement_D =None# TODO etudiantprint("Exercice a completer : verdict de l'engagement D observable sur la Poule.")
Exercice a completer : verdict de l'engagement D observable sur la Poule.