GameTheory-21 — Loi II, seconde jambe : synthétiser un translateur Life
GameTheory-20-Chemin-Minimal-Robinson-Goforth-Python.ipynb a livré la première jambe de la Loi II : un constructeur produit un chemin dans un graphe de swaps 2x2, un vérificateur séparé re-dérive indépendamment sa validité et sa minimalité, avec trois verdicts distincts. Une loi attestée sur un substrat reste une observation sur ce substrat. Ce notebook porte la même loi sur un substrat génuinement différent — le Jeu de la Vie de Conway — pour les trois axes où elle peut casser autrement :
l’espace de recherche n’est pas fini-énumérable à la main (aucun graphe pré-construit) ;
le témoin est un objet (une configuration de cellules), pas un chemin ;
la vérification est une simulation, pas une re-dérivation combinatoire.
et, quand il n’y a pas de témoin, un certificat d’impossibilité — jamais un silence. Un générateur qui ne rend rien est indiscernable d’un générateur débranché.
Rappel de la Loi II : une claim sur un système combinatoire ne vaut que si elle s’accompagne d’un téoin — un objet fini que quiconque peut inspecter — et d’un vérificateur indépendant capable de dire non. GT-20 l’avait instanciée avec trois verdicts (VALIDE + MINIMAL / VALIDE mais NON MINIMAL / INVALIDE) : le vérificateur y re-dérivait la minimalité par un BFS exhaustif sur le graphe entier. Ici le vérificateur ne re-dérive rien de combinatoire : il re-joue la physique. C’est un test beaucoup plus faible à construire — et pourtant il suffit à attester, parce que la définition d’un translateur est un énoncé de simulation. Le choix du substrat fait qu’ici, la vérification la plus simple possible est aussi la bonne.
import numpy as npfrom itertools import combinationsfrom time import timedef step(grid):"""Une génération du Jeu de la Vie (B3/S23) sur grille bornée, bord mort.""" r, c = grid.shape g = np.pad(grid, 1, mode="constant") n = np.zeros((r, c), dtype=int)for dr in (-1, 0, 1):for dc in (-1, 0, 1):if dr or dc: n += g[1+dr:1+dr+r, 1+dc:1+dc+c] vivante = grid.astype(bool)return ((n ==3) | (vivante & (n ==2))).astype(np.int8)# Contrôle sanitaire du moteur : le bloc 2x2 est un still life.bloc = np.array([[1, 1], [1, 1]], dtype=np.int8)print("bloc après 1 génération ->", step(bloc).tolist(), "(inchangé : still life)")
bloc après 1 génération -> [[1, 1], [1, 1]] (inchangé : still life)
1. Le vérificateur indépendant
Définition. Un translateur de vitesse \((dx, dy)\) et de période \(p\) est un motif fini qui, après \(p\) générations de simulation, réapparaît identique à lui-même, translaté d’exactement \((dx, dy)\) — et qui ne laisse rien derrière lui : toute la matière doit se déplacer, aucun débris.
Les cas dégénérés existent et le vocabulaire les distingue : \((0,0)\) à toute période pour un still life, période \(p\) sans déplacement pour un oscillateur. Le vérificateur ci-dessous n’exige que la définition littérale — un still life passe donc comme translateur de vitesse nulle, et nous garderons ce fait visible.
L’organe.verifier_translateur ne connaît que la simulation : il reçoit un motif et une claim\((dx, dy, p)\), simule, compare la boîte englobante finale au motif initial translaté. Il ne reprend aucun code du générateur — c’est la condition de séparation des deux organes qui donne à son verdict une valeur d’attestation.
def verifier_translateur(P, dx, dy, p, marge=12):"""Organe VÉRIFICATEUR : simule p générations et compare. Ignore la recherche.""" P = np.asarray(P, dtype=np.int8) h, w = P.shape H, W = h +abs(dx) +2* marge, w +abs(dy) +2* marge g = np.zeros((H, W), dtype=np.int8) oy, ox = marge, marge g[oy:oy+h, ox:ox+w] = Pfor _ inrange(p): g = step(g) ys, xs = np.where(g >0)iflen(ys) ==0:returnFalse, "INVALIDE : motif éteint après la période" y0, y1, x0, x1 = ys.min(), ys.max(), xs.min(), xs.max() S = g[y0:y1+1, x0:x1+1] deplace = (int(y0 - oy), int(x0 - ox))if S.shape != P.shape:returnFalse, f"INVALIDE : boîte englobante modifiée {S.shape} != {P.shape}"ifnot np.array_equal(S, P):returnFalse, "INVALIDE : le motif a muté (débris ou changement de forme)"if deplace != (dx, dy):returnFalse, f"INVALIDE : déplacement observé {deplace}, demandé {(dx, dy)}"returnTrue, f"VALIDE : translateur (dx,dy)=({dx},{dy}), période {p}, {int(P.sum())} cellules"GLIDER = np.array([[0, 1, 0], [0, 0, 1], [1, 1, 1]], dtype=np.int8)print(verifier_translateur(GLIDER, 1, 1, 4)) # la claim exacte du gliderprint(verifier_translateur(GLIDER, 1, 1, 5)) # mauvaise période -> rejetprint(verifier_translateur(bloc, 0, 0, 1)) # vitesse nulle : still life
(True, 'VALIDE : translateur (dx,dy)=(1,1), période 4, 5 cellules')
(False, 'INVALIDE : le motif a muté (débris ou changement de forme)')
(True, 'VALIDE : translateur (dx,dy)=(0,0), période 1, 4 cellules')
2. Le générateur : énumération exhaustive bornée
Le générateur reçoit la demande (v, bornes) — une vitesse \((dx, dy)\), une période \(p\), et des bornes : une boîte \(b \times b\) et une population maximale \(k\). Sa famille est finie : tous les motifs d’au plus \(k\) cellules vivantes dans la boîte \(b \times b\), au plus \(\sum_{i \le k} \binom{b^2}{i}\) objets. Il les énumère tous, consulte le vérificateur pour chacun, et rend un certificat : ce qui a été énuméré, combien de témoins trouvés. Son seul métier est d’épuiser la famille — il ne décide rien lui-même, le verdict appartient toujours au vérificateur.
C’est la borne qui rend l’épuisement possible : « exhaustif » signifie ici exhaustif dans la famille, et la section 4 montrera pourquoi cette nuance porte tout le poids épistémologique du grain.
def synthetiseur(b, k, dx, dy, p):"""Organe GÉNÉRATEUR : épuise la famille (<= k cellules dans b x b, période p). Rend toujours un certificat — jamais un silence.""" cellules = [(r, c) for r inrange(b) for c inrange(b)] enumeration, temoins =0, []for taille inrange(1, k +1):for comb in combinations(cellules, taille): enumeration +=1 P = np.zeros((b, b), dtype=np.int8)for (r, c) in comb: P[r, c] =1 verdict, _ = verifier_translateur(P, dx, dy, p)if verdict: temoins.append(P)return {"famille": f"motifs d'au plus {k} cellules dans une boîte {b}x{b}","demande": f"(dx,dy)=({dx},{dy}), période {p}","enumeres": enumeration,"temoins": temoins, }t0 = time()cert_glider = synthetiseur(b=3, k=5, dx=1, dy=1, p=4)print("famille :", cert_glider["famille"])print("demande :", cert_glider["demande"])print("motifs énumérés :", cert_glider["enumeres"], f"en {time()-t0:.1f} s")print("témoins trouvés :", len(cert_glider["temoins"]))for T in cert_glider["temoins"]:print(T.tolist())
famille : motifs d'au plus 5 cellules dans une boîte 3x3
demande : (dx,dy)=(1,1), période 4
motifs énumérés : 381 en 0.1 s
témoins trouvés : 4
[[1, 0, 1], [0, 1, 1], [0, 1, 0]]
[[1, 0, 0], [0, 1, 1], [1, 1, 0]]
[[0, 1, 0], [0, 0, 1], [1, 1, 1]]
[[0, 0, 1], [1, 0, 1], [0, 1, 1]]
Lecture du résultat
381 motifs énumérés, 4 témoins — et les quatre sont les rotations du même objet : le glider de Conway, 5 cellules, le plus petit translateur de Life. L’énumération l’a retrouvé sans aucune connaissance préalable : la famille contenait le glider, l’épuisement l’a fait sortir. C’est la première preuve de la chaîne : le générateur produit le témoin, il ne l’invente pas.
Le certificat rendu est un objet positif et vérifiable : n’importe qui peut recompter les 381 motifs, rejouer l’épuisement, constater que la famille est fermée. La preuve n’est pas un argument, c’est un fait énumératif.
D’où vient le nombre 381 ? La boîte 3x3 a 9 cellules ; les motifs d’au plus 5 cellules vivantes sont \(\sum_{i=1}^{5} \binom{9}{i} = 9 + 36 + 84 + 126 + 126 = 381\). Le compte est fermé, fini, recomptable — c’est ce qui distingue un épuisement attesté d’une recherche abandonnée. Et noter l’économie du geste : nous n’avons codé aucune connaissance du glider ; la seule chose sujette à caution était le choix des bornes, et c’est précisément ce que la section 4 transformera en leçon centrale.
# Chaque témoin rendu par le générateur REPASSE par le vérificateur indépendant.# Le générateur a trouvé ; c'est le vérificateur qui atteste.print("Re-vérification indépendante des", len(cert_glider["temoins"]), "témoins :")for i, T inenumerate(cert_glider["temoins"], 1): verdict, raison = verifier_translateur(T, 1, 1, 4)print(f" témoin {i} : {raison}")
Re-vérification indépendante des 4 témoins :
témoin 1 : VALIDE : translateur (dx,dy)=(1,1), période 4, 5 cellules
témoin 2 : VALIDE : translateur (dx,dy)=(1,1), période 4, 5 cellules
témoin 3 : VALIDE : translateur (dx,dy)=(1,1), période 4, 5 cellules
témoin 4 : VALIDE : translateur (dx,dy)=(1,1), période 4, 5 cellules
3. Le cas sans témoin : impossibilité physique
Demandons maintenant l’impossible : un translateur de vitesse \((2, 0)\) à la période 3 — soit \(2/3\) de cellule par génération en orthogonal. Life a une limite de vitesse, le \(c/2\) orthogonal (une cellule toutes les deux générations) : aucun motif fini ne peut se translater plus vite. Notre demande est supra-luminale.
Le point du grain n’est pas que la recherche échoue — c’est ce qu’elle rend quand elle échoue. Un générateur débranché rend un silence. Le nôtre rend un certificat d’impossibilité : l’épuisement attesté de la famille, la cause citée, la portée écrite. L’exigence vient du corps de l’issue #12387 : le cas sans solution doit produire quelque chose de POSITIF — jamais un silence.
t0 = time()cert_lumiere = synthetiseur(b=5, k=5, dx=2, dy=0, p=3)print("="*64)print("CERTIFICAT D'IMPOSSIBILITÉ (portée : la famille énumérée)")print("="*64)print("demande : translateur (dx,dy)=(2,0), période 3 -> vitesse 2/3 c")print("famille :", cert_lumiere["famille"])print("épuisement :", cert_lumiere["enumeres"], "motifs énumérés, "f"{len(cert_lumiere['temoins'])} témoin(s), en {time()-t0:.1f} s")print("verdict : AUCUN translateur de vitesse (2,0,3) dans la famille.")print("portée : cohérent avec la limite c/2 de Life — borne physique citée,")print(" non dérivée ici. Au-delà de la famille, l'impossibilité")print(" repose sur cette borne, pas sur l'énumération.")
================================================================
CERTIFICAT D'IMPOSSIBILITÉ (portée : la famille énumérée)
================================================================
demande : translateur (dx,dy)=(2,0), période 3 -> vitesse 2/3 c
famille : motifs d'au plus 5 cellules dans une boîte 5x5
épuisement : 68405 motifs énumérés, 0 témoin(s), en 12.9 s
verdict : AUCUN translateur de vitesse (2,0,3) dans la famille.
portée : cohérent avec la limite c/2 de Life — borne physique citée,
non dérivée ici. Au-delà de la famille, l'impossibilité
repose sur cette borne, pas sur l'énumération.
Lecture du certificat
Deux choses sont prouvées, et elles n’ont pas le même statut. Prouvé par épuisement : aucun motif d’au plus 5 cellules dans une boîte 5x5 ne translate à \((2,0,3)\) — un fait fini, recomptable. Cité, non prouvé : la raison profonde pour laquelle aucune taille n’y arriverait — la limite \(c/2\). Le certificat honore cette frontière en l’écrivant : c’est la différence entre attester et déclarer.
Notez le choix délibéré de la boîte : 5x5 est assez grande pour contenir la boîte englobante des vaisseaux orthogonaux connus — le vide constaté n’est donc pas un artefact de boîte trop petite. C’est la vitesse demandée qui est hors d’atteinte.
Un mot sur la forme du certificat : il énumère ce qui a été couvert (la famille), ce qui a été demandé (la vitesse), et ce qui a été trouvé (rien) — puis sépare explicitement le fait énumératif de la borne physique citée. Cette structure est réutilisable telle quelle pour n’importe quel autre substrat : c’est le gabarit minimal d’un rendu positif sur échec.
4. La leçon de scope : le piège du certificat
Reculons d’un cran sur la même famille : demandons \((2, 0)\) à la période 4 — soit exactement \(c/2\), la limite physique elle-même. Cette vitesse est réalisable : le LWSS (lightweight spaceship) l’atteint. Mais il a 9 cellules — hors de notre famille \(\le 5\).
La recherche sur la même famille rend donc vide aussi — et voilà le piège : un certificat d’épuisement ne prouve jamais l’impossibilité globale. Il prouve l’absence dans la famille. \((2,0,3)\) est vide pour une raison physique ; \((2,0,4)\) est vide pour une raison de famille — et les deux vidanges se ressemblent exactement dans les logs. Ce qui les distingue n’est pas la sortie du programme, c’est la connaissance externe du substrat. C’est LA leçon que ce substrat apporte et que le graphe 2x2 de GT-20 ne pouvait pas montrer aussi nettement.
t0 = time()cert_c2 = synthetiseur(b=5, k=5, dx=2, dy=0, p=4) # exactement c/2print("(2,0,4) sur la même famille :", cert_c2["enumeres"], "motifs énumérés,",f"{len(cert_c2['temoins'])} témoin, en {time()-t0:.1f} s")print()# Mais le témoin existe -- hors de la famille : le LWSS, 9 cellules.LWSS = np.array([[0, 1, 0, 0, 1], [1, 0, 0, 0, 0], [1, 0, 0, 0, 1], [1, 1, 1, 1, 0]], dtype=np.int8)for nom, W_ in [("LWSS", LWSS), ("LWSS miroir", np.fliplr(LWSS))]:for (dx, dy) in [(2, 0), (-2, 0), (0, 2), (0, -2)]: verdict, raison = verifier_translateur(W_, dx, dy, 4)if verdict:print(f"{nom} ({W_.sum()} cellules) : {raison}")print()print("Contrast : (2,0,3) vide par PHYSIQUE ; (2,0,4) vide par FAMILLE (LWSS existe à 9 cellules).")
(2,0,4) sur la même famille : 68405 motifs énumérés, 0 témoin, en 15.6 s
LWSS (9 cellules) : VALIDE : translateur (dx,dy)=(0,-2), période 4, 9 cellules
LWSS miroir (9 cellules) : VALIDE : translateur (dx,dy)=(0,2), période 4, 9 cellules
Contrast : (2,0,3) vide par PHYSIQUE ; (2,0,4) vide par FAMILLE (LWSS existe à 9 cellules).
Lecture du contraste
Les deux épuisements (68 405 motifs chacun) sont indiscernables dans leurs logs : mêmes bornes, même famille, zéro témoin. Tout ce qui les sépare est la connaissance externe du substrat — la limite \(c/2\) d’un côté, l’existence du LWSS de l’autre. La leçon opérationnelle pour quiconque lit un certificat d’épuisement : la sortie du programme ne dit jamais laquelle des deux vidanges on a devant soi. C’est au rédacteur du certificat d’écrire la portée, et au lecteur de la demander.
C’est aussi ce qui rend le témoin LWSS précieux ici : il joue le rôle de contre-preuve vivante contre la sur-interprétation du certificat \((2,0,4)\). Sans lui, rien dans le notebook ne distinguerait « impossible dans la famille » de « impossible » — et c’est exactement la classe d’erreur qu’un certificat mal scopé fabrique en silence.
5. Contrôle positif : le témoin faux injecté
Un lot tout-vert est indiscernable d’un vérificateur débranché. Pour prouver que le vérificateur peut dire non, on lui injecte des claims fausses sur des motifs vrais : le glider annoncé à une vitesse qu’il n’a pas, à une période qu’il n’a pas, dans une direction qu’il ne prend pas. Chacune doit être rejetée, avec la raison du rejet.
Ce contrôle est l’analogue exact du détour construit exprès dans GT-20 : là, le vérificateur devait attraper un chemin volontairement non minimal ; ici, il doit attraper une claim volontairement fausse sur un objet réel. Dans les deux cas, le test du négatif est ce qui distingue un vérificateur qui atteste d’un vérificateur qui acquiesce. Notez que chaque rejet vient avec sa raison (déplacement observé, mutation, boîte modifiée) — un verdict non motivé serait aussi peu auditable qu’un silence.
controles = [ (GLIDER, 2, 2, 4, "claim trop rapide : glider annoncé à (2,2,4) = c/2 diagonal"), (GLIDER, 1, 1, 5, "claim de période : glider annoncé à la période 5"), (GLIDER, 1, 0, 4, "claim de direction : glider annoncé orthogonal (1,0,4)"),]for (P, dx, dy, p, etiquette) in controles: verdict, raison = verifier_translateur(P, dx, dy, p)print(f"[{etiquette}]")print(f" -> {'REJETÉ'ifnot verdict else'ACCEPTÉ (défaut !)'} : {raison}")
[claim trop rapide : glider annoncé à (2,2,4) = c/2 diagonal]
-> REJETÉ : INVALIDE : déplacement observé (1, 1), demandé (2, 2)
[claim de période : glider annoncé à la période 5]
-> REJETÉ : INVALIDE : le motif a muté (débris ou changement de forme)
[claim de direction : glider annoncé orthogonal (1,0,4)]
-> REJETÉ : INVALIDE : déplacement observé (1, 1), demandé (1, 0)
6. Frontières écrites
Ce que « exhaustif » couvre exactement ici :
motifs d’au plus \(k\) cellules vivantes dans une boîte \(b \times b\) ;
période exactement\(p\) (un translateur de période 4 n’est pas trouvé pour une demande de période 8 — la définition exige l’identité à la génération \(p\)) ;
déplacement exactement\((dx, dy)\) sur cette période ;
grille de simulation bornée avec marge morte — valide pour les tailles manipulées ici.
Ce qui reste conjectural :
tout ce qui dépasse la famille — l’épuisement ne dit rien des motifs de plus de \(k\) cellules (le couple \((2,0,3)\)-physique vs \((2,0,4)\)-famille en est la démonstration) ;
la limite \(c/2\) est citée, pas dérivée — le certificat la prend comme borne externe ;
les vitesses diagonales maximales (\(c/4\) pour le glider) suivent la même logique mais ne sont pas démontrées ici.
C’est la frontière honnête du grain : constructeur → témoin → vérificateur indépendant, certificat scopé. La certification formelle (jambe Lean) est explicitement hors scope — si elle vient, ce sera un variant -b. Le cran visé ici est exactement celui de l’acceptance : deux organes séparés, un cas avec témoin, un cas sans témoin à rendu positif, un témoin faux rejeté, des frontières écrites.
7. Exercices
Trois exercices, dans l’esprit du grain : produire un certificat, durcir le vérificateur, sonder une frontière.
Exercice 1 — Certificat sur une autre vitesse supra-luminale
Choisir une vitesse impossible au-dessus de la limite (ex. (3,0,4), (0,3,4), ou le diagonal (2,2,4)) et faire rendre au générateur son certificat d’épuisement. Écrire la portée exacte du certificat rendu.
Indice : synthetiseur(b, k, dx, dy, p) rend toujours la structure du certificat.
# Exercice 1 -- Certificat sur une autre vitesse supra-luminale# Choisir une vitesse impossible au-dessus de la limite (ex. (3,0,4), (0,3,4),# ou le diagonal (2,2,4)) et faire rendre au générateur son certificat# d'épuisement. Écrire la portée exacte du certificat rendu.# Indice : synthetiseur(b, k, dx, dy, p) rend toujours la structure du certificat.# TODO étudiant : lancer la recherche et commenter le verdict.print("Exercice à compléter")
Exercice à compléter
Exercice 2 — Un verdict à quatre valeurs
Le vérificateur actuel accepte un still life comme translateur de vitesse nulle. Le durcir en quatre verdicts : TRANSLATEUR (déplacement non nul), STILL LIFE ((0,0) à toute période), OSCILLATEUR (période p, déplacement nul), INVALIDE. Le tester sur le glider, le bloc et un blinker.
Indice : un blinker est [[1,1,1]] — il oscille de période 2.
# Exercice 2 -- Un verdict à quatre valeurs# Le vérificateur actuel accepte un still life comme translateur de vitesse# nulle. Le durcir en QUATRE verdicts : TRANSLATEUR (déplacement non nul),# STILL LIFE (0,0 à toute période), OSCILLATEUR (période p, déplacement nul),# INVALIDE. Le tester sur le glider, le bloc et un blinker.# Indice : un blinker est [[1,1,1]] -- il oscille de période 2.# TODO étudiant : implémenter puis tester.print("Exercice à compléter")
Exercice à compléter
Exercice 3 — La boîte compte les translations séparément
Relancer la recherche du glider (1,1,4) dans une boîte 4x4 (même k=5) et comparer le nombre de témoins au résultat 3x3. Expliquer la différence : combien de positions distinctes un même glider 3x3 occupe-t-il dans 4x4 ?
Indice : C(16,<=5) = 6884 motifs — quelques secondes d’énumération.
# Exercice 3 -- La boîte compte les translations séparément# Relancer la recherche du glider (1,1,4) dans une boîte 4x4 (même k=5) et# comparer le nombre de témoins au résultat 3x3. Expliquer la différence :# combien de positions distinctes un même glider 3x3 occupe-t-il dans 4x4 ?# Indice : C(16,<=5) = 6884 motifs -- quelques secondes d'énumération.# TODO étudiant : lancer, compter, expliquer.print("Exercice à compléter")
Exercice à compléter
Conclusion
La Loi II tient sur ce second substrat, et elle y prend un sens neuf. Ce qui a tenu : la chaîne générateur → témoin → vérificateur indépendant, les contrôles positifs (le témoin faux rejeté), l’exigence d’un rendu positif sur le cas sans solution. Ce qui a changé de visage :
le témoin est un objet — une configuration de cellules — que l’épuisement fait sortir d’une famille finie, quand GT-20 extrayait un chemin d’un graphe déjà construit ;
la vérification est une simulation : le vérificateur re-joue la physique, il ne re-dérive pas une structure combinatoire ;
l’impossibilité est un certificat scopé dont la portée doit être écrite — et le couple \((2,0,3)/(2,0,4)\) montre que deux vidanges de famille identiques en apparence ont deux raisons radicalement différentes, physique pour l’une, artefact de famille pour l’autre.
Une loi attestée sur deux substrats genuinement différents commence à être une loi. La jambe Lean, si elle vient, sera un variant -b. En attendant, le lecteur retiendra le geste complet : une demande, deux organes, trois issues — témoin trouvé et attesté ; échec rendu comme certificat scopé ; claim fausse rejetée avec sa raison. Tout le reste — la boîte, la population, la période — n’est que le réglage fin de la famille dans laquelle on accepte de chercher.
Voir #12387 (grain) et #12205 (Chantier 2 — génération de témoins). Série : GT-20 GameTheory-20-Chemin-Minimal-Robinson-Goforth-Python.ipynb.
Suivant : GameTheory-20e – Perplexite structurelle Hashlife – la perception structurelle Hashlife (instrument K_trajectory entropie LZ + verdict CONJECTURE-NON-VERIFIEE-AVEC-CORPUS-COURANT, cf. issue #18446) prolonge la Loi II sur le meme substrat Conway mais transpose le verify-once en measure-once. (la perception structurelle Hashlife, transpose du probleme verify-once, introduit une discusion entropie + LZ + banc Turing-complet pour la mesure de confirmation – cf. issue #18446).