Lean-16h : la tournée des motifs du Jeu de la Vie — compagnon formel natif de `Conway.Life.PatternTour`

Compagnon natif du module Conway/Life/PatternTour.lean du lake conway_lean : le module est importé et exécuté ici dans un kernel Lean 4 réel (lean4-wsl), et chaque théorème de la tournée est interrogé par #check, #eval ou #print axioms. Les sorties de ce notebook sont des sorties du compilateur Lean, pas de la prose à propos de Lean.

Ce module a une histoire : il a été conçu comme un chemin pédagogique (PR #9796 — « PatternTour pedagogical module ») qui relie quatre modules jusque-là indépendants (Oscillators, Spaceships, RLE, Computation) en un seul récit. Mais à sa livraison, aucun notebook ne le citait : la mesure de l’EPIC #11703 (visibilité des lakes) le comptait parmi les 16 modules noirs de conway_lean. Ce compagnon est la réponse — il existait un cours sans salle de classe.

Position dans la série 16. Lean-16d reconstruit le moteur du Jeu de la Vie à la main dans le notebook (la pédagogie de la construction) ; Lean-16b montre la simulation côté Python/Golly ; Lean-16e et Lean-16g visitent FRACTRAN et les canons. Ici, le geste est inverse : on monte dans le lake et on fait tourner la théorie telle qu’elle compile — la tournée des cinq régimes dynamiques du Jeu de la Vie, chaque étape à la fois regardée (#eval) et prouvée (theorem ... := by decide).

1. Le lake, le module, et les trois prédicats

conway_lean porte le cœur du Jeu de la Vie formalisé dans Conway/Life.lean : une Grid est la liste des cellules vivantes, step applique la règle B3/S23, evolve n itère, shift v translate. Sur ce moteur vivent trois prédicats de régime :

def isStillLife  (g : Grid)            : Bool := step g == g
def isOscillator (g : Grid) (n : Nat)  : Bool := evolve n g == g
def isSpaceship  (g : Grid) (n : Nat) (v : Int × Int) : Bool := -- evolve n g == shift v g

PatternTour importe ces définitions et ajoute le fil narratif : équilibre (still lifes) → cycle (oscillateurs) → translation (vaisseaux) → sérialisation (RLE) → accélération (Hashlife). La cellule suivante importe la session entière — toutes les importations de ce notebook viennent de là — et liste les huit théorèmes qui jalonnent la tournée.

-- Toutes les importations de la session (tete de session, pattern Lean-24) :
import Conway.Life
import Conway.Life.Oscillators
import Conway.Life.Spaceships
import Conway.Life.RLE
import Conway.Life.Computation
import Conway.Life.PatternTour

open Conway.Life
open Conway.Life.RLE

-- Les huit points d'ancrage de la tournee (tous dans Conway.Life.PatternTour) :
#check @loaf_is_still_life                  -- section 2  : equilibre
#check @tub_is_still_life                   -- section 2  : equilibre
#check @beacon_is_oscillator                -- section 3  : cycle
#check @pulsar_is_oscillator                -- section 3  : cycle (native_decide)
#check @glider_is_spaceship                 -- section 4  : translation
#check @lwss_is_spaceship                   -- section 4  : translation
#check @glider_two_periods_translation      -- section 4  : invariance d'echelle
#check @hashlife_fast_glider_translation_4  -- section 6  : acceleration

-- Toutes les importations de la session (tete de session, pattern Lean-24) :

import Conway.Life

import Conway.Life.Oscillators

import Conway.Life.Spaceships

import Conway.Life.RLE

import Conway.Life.Computation

import Conway.Life.PatternTour

open Conway.Life

open Conway.Life.RLE

-- Les huit points d'ancrage de la tournee (tous dans Conway.Life.PatternTour) :

#check @loaf_is_still_life                  -- section 2  : equilibre loaf_is_still_life : isStillLife loaf = true

#check @tub_is_still_life                   -- section 2  : equilibre tub_is_still_life : isStillLife tub = true

#check @beacon_is_oscillator                -- section 3  : cycle beacon_is_oscillator : isOscillator beacon 2 = true

#check @pulsar_is_oscillator                -- section 3  : cycle (native_decide) pulsar_is_oscillator : isOscillator pulsar 3 = true

#check @glider_is_spaceship                 -- section 4  : translation glider_is_spaceship : isSpaceship glider 4 (1, -1) = true

#check @lwss_is_spaceship                   -- section 4  : translation lwss_is_spaceship : isSpaceship lwss 4 (0, 2) = true

#check @glider_two_periods_translation      -- section 4  : invariance d'echelle glider_two_periods_translation : evolve 8 glider = shift (2, -2) glider

#check @hashlife_fast_glider_translation_4  -- section 6  : acceleration hashlife_fast_glider_translation_4 : evolveHashlifeFast 4 glider = shift (1, -1) glider

--% env 0

Raw input

{"cmd": "-- Toutes les importations de la session (tete de session, pattern Lean-24) :\nimport Conway.Life\nimport Conway.Life.Oscillators\nimport Conway.Life.Spaceships\nimport Conway.Life.RLE\nimport Conway.Life.Computation\nimport Conway.Life.PatternTour\n\nopen Conway.Life\nopen Conway.Life.RLE\n\n-- Les huit points d'ancrage de la tournee (tous dans Conway.Life.PatternTour) :\n#check @loaf_is_still_life                  -- section 2  : equilibre\n#check @tub_is_still_life                   -- section 2  : equilibre\n#check @beacon_is_oscillator                -- section 3  : cycle\n#check @pulsar_is_oscillator                -- section 3  : cycle (native_decide)\n#check @glider_is_spaceship                 -- section 4  : translation\n#check @lwss_is_spaceship                   -- section 4  : translation\n#check @glider_two_periods_translation      -- section 4  : invariance d'echelle\n#check @hashlife_fast_glider_translation_4  -- section 6  : acceleration"}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 13, "column": 0},
   "endPos": {"line": 13, "column": 6},
   "data": "loaf_is_still_life : isStillLife loaf = true"},
  {"severity": "info",
   "pos": {"line": 14, "column": 0},
   "endPos": {"line": 14, "column": 6},
   "data": "tub_is_still_life : isStillLife tub = true"},
  {"severity": "info",
   "pos": {"line": 15, "column": 0},
   "endPos": {"line": 15, "column": 6},
   "data": "beacon_is_oscillator : isOscillator beacon 2 = true"},
  {"severity": "info",
   "pos": {"line": 16, "column": 0},
   "endPos": {"line": 16, "column": 6},
   "data": "pulsar_is_oscillator : isOscillator pulsar 3 = true"},
  {"severity": "info",
   "pos": {"line": 17, "column": 0},
   "endPos": {"line": 17, "column": 6},
   "data": "glider_is_spaceship : isSpaceship glider 4 (1, -1) = true"},
  {"severity": "info",
   "pos": {"line": 18, "column": 0},
   "endPos": {"line": 18, "column": 6},
   "data": "lwss_is_spaceship : isSpaceship lwss 4 (0, 2) = true"},
  {"severity": "info",
   "pos": {"line": 19, "column": 0},
   "endPos": {"line": 19, "column": 6},
   "data":
   "glider_two_periods_translation : evolve 8 glider = shift (2, -2) glider"},
  {"severity": "info",
   "pos": {"line": 20, "column": 0},
   "endPos": {"line": 20, "column": 6},
   "data":
   "hashlife_fast_glider_translation_4 : evolveHashlifeFast 4 glider = shift (1, -1) glider"}],
 "env": 0}

Lecture. Huit théorèmes, cinq régimes. Notez les types : loaf_is_still_life : isStillLife loaf = true est une égalité de Bool — la preuve oblige Lean à réduire le calcul dans le noyau. C’est la signature de toute la tournée : chaque theorem est un calcul que le noyau refait lui-même, pas un argument que l’on raconte. Deux théorèmes échappent à la règle du « zéro axiome » (pulsar_is_oscillator bascule sur native_decide) — la section 3 montre pourquoi, et ce que cela coûte exactement.

2. Équilibre — les still lifes, regardés puis prouvés

Un still life n’est pas de l’inertie : chaque cellule vivante doit avoir exactement deux ou trois voisins, chaque cellule morte tout sauf trois, pour que rien ne bouge. Le loaf (pain, 7 cellules) et le tub (bac, 4 cellules) sont deux équilibres locaux de formes différentes. Le module pose le geste deux fois : le #eval regarde l’équilibre, le theorem le prouve.

-- On regarde : le calcul confirme la stabilite.
#eval isStillLife loaf        -- attendu : true
#eval step loaf == loaf       -- attendu : true (reduction explicite d'une etape)
#eval loaf                    -- la grille elle-meme : 7 cellules

-- On prouve : dans le noyau, sans axiome.
#print axioms loaf_is_still_life
#print axioms tub_is_still_life

-- On regarde : le calcul confirme la stabilite.

#eval isStillLife loaf        -- attendu : true true

#eval step loaf == loaf       -- attendu : true (reduction explicite d'une etape) true

#eval loaf                    -- la grille elle-meme : 7 cellules [(0, 1), (0, 2), (1, 0), (1, 3), (2, 1), (2, 3), (3, 2)]

-- On prouve : dans le noyau, sans axiome.

#print axioms loaf_is_still_life 'Conway.Life.loaf_is_still_life' does not depend on any axioms

#print axioms tub_is_still_life 'Conway.Life.tub_is_still_life' does not depend on any axioms

--% env 1

Raw input

{"cmd": "-- On regarde : le calcul confirme la stabilite.\n#eval isStillLife loaf        -- attendu : true\n#eval step loaf == loaf       -- attendu : true (reduction explicite d'une etape)\n#eval loaf                    -- la grille elle-meme : 7 cellules\n\n-- On prouve : dans le noyau, sans axiome.\n#print axioms loaf_is_still_life\n#print axioms tub_is_still_life", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 5},
   "data": "[(0, 1), (0, 2), (1, 0), (1, 3), (2, 1), (2, 3), (3, 2)]"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data": "'Conway.Life.loaf_is_still_life' does not depend on any axioms"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data": "'Conway.Life.tub_is_still_life' does not depend on any axioms"}],
 "env": 1}

Lecture du certificat. #print axioms répond 'loaf_is_still_life' does not depend on any axioms : la preuve est close, réduite jusqu’au fond par le noyau Lean — aucun sorry transitif, aucun native_decide, aucun Classical.choice. C’est le grade le plus élevé qu’une preuve calculatoire peut porter ici, et la tournée l’obtient sur loaf et tub. Le contraste arrive à la section suivante : le pulsar, trop gros pour ce grade exact, paiera d’un axiome.

3. Cycle — la bascule `decide` → `native_decide`

Un oscillateur de période n revient à lui-même après n étapes. Le beacon (phare, période 2) passe le noyau sans encombre. Le pulsar (48 cellules, période 3) dépasse la limite de récursion maxRecDepth du noyau : decide échoue, et le module bascule sur native_decide — qui compile le calcul au lieu de le réduire. Le coût est précis et mesurable : un axiome — ici pulsar_is_oscillator._native.native_decide.ax_1_1, l’auxiliaire que le compilateur génère pour ce native_decide précis (le rôle que les toolchains antérieurs confiaient au générique Lean.ofReduceBool) : « le compilateur et le noyau calculent la même chose ». C’est l’équivalent formel d’un #eval témoin : on croit le résultat, mais sur parole du compilateur.

-- Le beacon : le noyau y suffit.
#eval isOscillator beacon 2        -- attendu : true
#eval evolve 1 beacon == beacon    -- attendu : false (la demi-periode change la forme)

-- Le pulsar : le noyau ne suffit plus.
#eval isOscillator pulsar 3        -- attendu : true (par evaluation, pas par noyau)
#eval evolve 3 pulsar == pulsar    -- attendu : true (une periode complete)

-- Le certificat des deux preuves : le contraste est la lecon.
#print axioms beacon_is_oscillator
#print axioms pulsar_is_oscillator

-- Le beacon : le noyau y suffit.

#eval isOscillator beacon 2        -- attendu : true true

#eval evolve 1 beacon == beacon    -- attendu : false (la demi-periode change la forme) false

-- Le pulsar : le noyau ne suffit plus.

#eval isOscillator pulsar 3        -- attendu : true (par evaluation, pas par noyau) true

#eval evolve 3 pulsar == pulsar    -- attendu : true (une periode complete) true

-- Le certificat des deux preuves : le contraste est la lecon.

#print axioms beacon_is_oscillator 'Conway.Life.beacon_is_oscillator' does not depend on any axioms

#print axioms pulsar_is_oscillator 'Conway.Life.pulsar_is_oscillator' depends on axioms: [pulsar_is_oscillator._native.native_decide.ax_1_1]

--% env 2

Raw input

{"cmd": "-- Le beacon : le noyau y suffit.\n#eval isOscillator beacon 2        -- attendu : true\n#eval evolve 1 beacon == beacon    -- attendu : false (la demi-periode change la forme)\n\n-- Le pulsar : le noyau ne suffit plus.\n#eval isOscillator pulsar 3        -- attendu : true (par evaluation, pas par noyau)\n#eval evolve 3 pulsar == pulsar    -- attendu : true (une periode complete)\n\n-- Le certificat des deux preuves : le contraste est la lecon.\n#print axioms beacon_is_oscillator\n#print axioms pulsar_is_oscillator", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 5},
   "data": "false"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data": "'Conway.Life.beacon_is_oscillator' does not depend on any axioms"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 6},
   "data":
   "'Conway.Life.pulsar_is_oscillator' depends on axioms: [pulsar_is_oscillator._native.native_decide.ax_1_1]"}],
 "env": 2}

Lecture du contraste. beacon_is_oscillator : does not depend on any axioms. Une ligne plus bas, pulsar_is_oscillator : depends on axioms: [pulsar_is_oscillator._native.native_decide.ax_1_1] — l’auxiliaire nommé par théorème que la toolchain génère pour chaque native_decide (v4.32.1 à l’exécution de ces sorties ; le lake au HEAD pinne v4.33.0 depuis la migration #16341). La bascule decide → native_decide est exactement le diagnostic documenté dans le module (cycle c.736, decidable_instance_propagation.md) : sur les prédicats d’état du Jeu de la Vie, decide tient jusqu’à une profondeur de récursion modérée, puis cède. La tournée ne cache pas la bascule — elle la signale et en paie le prix au grand jour. C’est une leçon d’honnêteté formelle : un théorème par native_decide reste un théorème, mais son certificat porte la trace de ce qu’on a dû croire au noyau.

4. Translation — les vaisseaux et l’invariance d’échelle

Un vaisseau est un oscillateur dans le référentiel qui voyage avec lui : après n étapes, le motif réapparaît translaté de v. Le glider (5 cellules) est le plus petit vaisseau et le seul diagonal à c/4 — une cellule en diagonale toutes les 4 étapes. Le lwss (vaisseau léger) file à c/2, orthogonal. Le théorème d’invariance d’échelle (glider_two_periods_translation) ajoute la conclusion qui intéresse : le mouvement est linéaire — deux périodes = exactement le double du déplacement, le glider ne dérive pas.

-- Le glider : translation diagonale (1, -1) toutes les 4 etapes.
#eval isSpaceship glider 4 (1, -1)              -- attendu : true
#eval evolve 4 glider == shift (1, -1) glider   -- attendu : true (translation calculee)
#eval evolve 8 glider == shift (2, -2) glider   -- attendu : true (deux periodes -> double)

-- Le lwss : translation orthogonale (0, 2), vitesse c/2.
#eval isSpaceship lwss 4 (0, 2)                 -- attendu : true

-- Certificats : noyau pur sur les trois.
#print axioms glider_is_spaceship
#print axioms lwss_is_spaceship
#print axioms glider_two_periods_translation

-- Le glider : translation diagonale (1, -1) toutes les 4 etapes.

#eval isSpaceship glider 4 (1, -1)              -- attendu : true true

#eval evolve 4 glider == shift (1, -1) glider   -- attendu : true (translation calculee) true

#eval evolve 8 glider == shift (2, -2) glider   -- attendu : true (deux periodes -> double) true

-- Le lwss : translation orthogonale (0, 2), vitesse c/2.

#eval isSpaceship lwss 4 (0, 2)                 -- attendu : true true

-- Certificats : noyau pur sur les trois.

#print axioms glider_is_spaceship 'Conway.Life.glider_is_spaceship' does not depend on any axioms

#print axioms lwss_is_spaceship 'Conway.Life.lwss_is_spaceship' does not depend on any axioms

#print axioms glider_two_periods_translation 'Conway.Life.glider_two_periods_translation' does not depend on any axioms

--% env 3

Raw input

{"cmd": "-- Le glider : translation diagonale (1, -1) toutes les 4 etapes.\n#eval isSpaceship glider 4 (1, -1)              -- attendu : true\n#eval evolve 4 glider == shift (1, -1) glider   -- attendu : true (translation calculee)\n#eval evolve 8 glider == shift (2, -2) glider   -- attendu : true (deux periodes -> double)\n\n-- Le lwss : translation orthogonale (0, 2), vitesse c/2.\n#eval isSpaceship lwss 4 (0, 2)                 -- attendu : true\n\n-- Certificats : noyau pur sur les trois.\n#print axioms glider_is_spaceship\n#print axioms lwss_is_spaceship\n#print axioms glider_two_periods_translation", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data": "'Conway.Life.glider_is_spaceship' does not depend on any axioms"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 6},
   "data": "'Conway.Life.lwss_is_spaceship' does not depend on any axioms"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 6},
   "data":
   "'Conway.Life.glider_two_periods_translation' does not depend on any axioms"}],
 "env": 3}

Lecture. Trois #print axioms, trois does not depend on any axioms : même le théorème d’invariance d’échelle — qui compare evolve 8 glider (huit pas de simulation naïve) à shift (2, -2) glider (une translation formelle) — est réduit intégralement dans le noyau. La linéarité du mouvement du glider n’est pas observée sur un écran : elle est prouvée, et le certificat n’emprunte rien.

5. Sérialisation — le format RLE et l’opacité du parseur

Le format Run-Length Encoded est la lingua franca des motifs : une chaîne compacte (bo$2b3o!) encode une grille lisible par tous les simulateurs. Le lake définit chaque motif deux fois — une constante écrite à la main (glider : Grid) et la même grille parsée depuis sa chaîne (glider_parsed := parseRLE! glider_RLE) — et la tournée vérifie qu’elles coïncident. Le canon de Gosper (36 cellules, 1970), premier motif fini connu à croissance non bornée, n’existe dans le lake que sous forme RLE : gosper_gun := parseRLE! gosper_gun_RLE.

-- Le canon de Gosper, analyse depuis sa chaine RLE :
#eval gosper_gun.length                          -- attendu : 36
#eval (parseRLE gosper_gun_RLE).toOption.isSome  -- attendu : true (RLE bien forme)

-- Recoupements serialisation <-> constante manuelle :
#eval glider_parsed.length    -- attendu : 5 (meme cardinal que glider)
#eval lwss_parsed == lwss     -- attendu : true (coincidence exacte)

-- Le canon de Gosper, analyse depuis sa chaine RLE :

#eval gosper_gun.length                          -- attendu : 36 36

#eval (parseRLE gosper_gun_RLE).toOption.isSome  -- attendu : true (RLE bien forme) true

-- Recoupements serialisation <-> constante manuelle :

#eval glider_parsed.length    -- attendu : 5 (meme cardinal que glider) 5

#eval lwss_parsed == lwss     -- attendu : true (coincidence exacte) true

--% env 4

Raw input

{"cmd": "-- Le canon de Gosper, analyse depuis sa chaine RLE :\n#eval gosper_gun.length                          -- attendu : 36\n#eval (parseRLE gosper_gun_RLE).toOption.isSome  -- attendu : true (RLE bien forme)\n\n-- Recoupements serialisation <-> constante manuelle :\n#eval glider_parsed.length    -- attendu : 5 (meme cardinal que glider)\n#eval lwss_parsed == lwss     -- attendu : true (coincidence exacte)", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 5},
   "data": "36"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 5},
   "data": "5"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 5},
   "data": "true"}],
 "env": 4}

Lecture — pourquoi un #eval et pas un theorem ici. On pourrait vouloir énoncer theorem gosper_gun_has_36_cells : gosper_gun.length = 36 := by decide. Le module explique pourquoi il s’en abstient : gosper_gun est une def non-@[reducible] qui enveloppe le parseur, et le noyau ne déplie pas cette opacité lors de la synthèse de l’instance Decidable (cf. decidable_instance_propagation.md, cycle c.939). Le #eval, qui réduit par évaluation, est la preuve computationnelle honnête du compte de cellules — sans ajouter l’axiome Lean.ofReduceBool qu’exigerait native_decide. Devant un calcul que le noyau ne peut pas certifier proprement, la tournée choisit le témoin non-axiomatisé plutôt que le théorème axiomatisé : le degré de la preuve affiché correspond au degré réellement atteint.

6. Accélération — Hashlife contre la référence naïve, prouvés égaux

evolveHashlifeFast avance une grille de 2^k générations en une seule étape de l’algorithme récursif Hashlife, qui exploite la redondance du quadtree du plan. Pour les motifs périodiques, l’accélération est exponentielle : avancer de 2^k coûte essentiellement comme avancer de 2^(k-1). La correction de ce « chemin rapide » se prouve contre la référence naïve evolve — deux algorithmes aux complexités radicalement différentes, et l’égalité de leurs résultats dans le noyau, rendue possible par le fix ceilLog2 (#9536) qui a désopacisé la couche MacroCell pour le réducteur.

-- Hashlife vs reference : meme resultat sur le glider.
#eval evolveHashlifeFast 4 glider == evolve 4 glider    -- attendu : true
#eval evolveHashlifeFast 8 glider == evolve 8 glider    -- attendu : true

-- Le chemin rapide retrouve la translation prouvee en section 4 :
#eval evolveHashlifeFast 4 glider == shift (1, -1) glider  -- attendu : true
#eval evolveHashlifeFast 8 glider == shift (2, -2) glider  -- attendu : true

-- Certificat de la coincidence : noyau pur.
#print axioms hashlife_fast_glider_translation_4

-- Hashlife vs reference : meme resultat sur le glider.

#eval evolveHashlifeFast 4 glider == evolve 4 glider    -- attendu : true true

#eval evolveHashlifeFast 8 glider == evolve 8 glider    -- attendu : true true

-- Le chemin rapide retrouve la translation prouvee en section 4 :

#eval evolveHashlifeFast 4 glider == shift (1, -1) glider  -- attendu : true true

#eval evolveHashlifeFast 8 glider == shift (2, -2) glider  -- attendu : true true

-- Certificat de la coincidence : noyau pur.

#print axioms hashlife_fast_glider_translation_4 'Conway.Life.hashlife_fast_glider_translation_4' depends on axioms: [propext]

--% env 5

Raw input

{"cmd": "-- Hashlife vs reference : meme resultat sur le glider.\n#eval evolveHashlifeFast 4 glider == evolve 4 glider    -- attendu : true\n#eval evolveHashlifeFast 8 glider == evolve 8 glider    -- attendu : true\n\n-- Le chemin rapide retrouve la translation prouvee en section 4 :\n#eval evolveHashlifeFast 4 glider == shift (1, -1) glider  -- attendu : true\n#eval evolveHashlifeFast 8 glider == shift (2, -2) glider  -- attendu : true\n\n-- Certificat de la coincidence : noyau pur.\n#print axioms hashlife_fast_glider_translation_4", "env": 4}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "'Conway.Life.hashlife_fast_glider_translation_4' depends on axioms: [propext]"}],
 "env": 5}

Lecture. La boucle est bouclée : le shift (1, -1) prouvé pas à pas par la référence naïve en section 4 est retrouvé en une étape MacroCell par Hashlife, et l’égalité des deux chemins est réduite dans le noyau sans axiome. C’est le point d’aboutissement que le module annonce : la même évolution, calculée par deux algorithmes aux coûts opposés, prouvée égale. La tournée relie ainsi ses cinq régimes — l’accélération vient certifier la translation.

7. Exercices

Trois exercices, dans l’esprit de la tournée : utiliser le lake, construire soi-même, relier au théorème. Chaque cellule s’exécute telle quelle (sortie de stub) — à vous de remplacer le contenu par la vraie vérification.

Exercice 1 — Le bateau, encore à quai

Le lake définit boat (Oscillators.lean, 5 cellules) mais la tournée ne le prouve pas : seuls loaf et tub ont leur théorème. Complétez la vérification computationnelle — le #eval jumeau de ce que serait boat_is_still_life.

-- Exercice 1 : le bateau est-il un still life ?
-- TODO etudiant : remplacez le #eval place par la verification (attendu : true),
-- puis ajoutez le temoin de reduction explicite (une etape laisse la grille inchangee).
#eval 0 -- remplacez : isStillLife boat

-- Exercice 1 : le bateau est-il un still life ?

-- TODO etudiant : remplacez le #eval place par la verification (attendu : true),

-- puis ajoutez le temoin de reduction explicite (une etape laisse la grille inchangee).

#eval 0 -- remplacez : isStillLife boat 0

--% env 6

Raw input

{"cmd": "-- Exercice 1 : le bateau est-il un still life ?\n-- TODO etudiant : remplacez le #eval place par la verification (attendu : true),\n-- puis ajoutez le temoin de reduction explicite (une etape laisse la grille inchangee).\n#eval 0 -- remplacez : isStillLife boat", "env": 5}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 5},
   "data": "0"}],
 "env": 6}

Exercice 2 — Construire le blinker

Le blinker — trois cellules alignées, le plus petit oscillateur (période 2) — n’est pas défini dans le lake : construisez-le. Une Grid est une liste de paires d’entiers ; le glider du lake est écrit [(0, 0), (1, 0), (1, 2), (2, 0), (2, 1)] — suivez le même style. La définition incomplète ci-dessous s’exécute (le stub rend false) : c’est en complétant les trois cellules qu’elle doit rendre true.

-- Exercice 2 : definir le blinker (3 cellules alignees) et le verifier.
-- TODO etudiant : les 3 cellules du blinker (ligne verticale ou horizontale, au choix).
def blinker_ex : Grid := [(0, 0)]  -- incomplet : une seule cellule meurt

#eval isOscillator blinker_ex 2   -- attendu : false tant que la definition est incomplete

-- Exercice 2 : definir le blinker (3 cellules alignees) et le verifier.

-- TODO etudiant : les 3 cellules du blinker (ligne verticale ou horizontale, au choix).

def blinker_ex : Grid := [(0, 0)]  -- incomplet : une seule cellule meurt

#eval isOscillator blinker_ex 2   -- attendu : false tant que la definition est incomplete false

--% env 7

Raw input

{"cmd": "-- Exercice 2 : definir le blinker (3 cellules alignees) et le verifier.\n-- TODO etudiant : les 3 cellules du blinker (ligne verticale ou horizontale, au choix).\ndef blinker_ex : Grid := [(0, 0)]  -- incomplet : une seule cellule meurt\n\n#eval isOscillator blinker_ex 2   -- attendu : false tant que la definition est incomplete", "env": 6}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 5},
   "data": "false"}],
 "env": 7}

Exercice 3 — Trois périodes : prédire puis vérifier

Le théorème glider_two_periods_translation (section 4) dit : 8 étapes = 2 périodes = translation (2, -2). Le lake cache aussi Computation.glider_3periods : 12 étapes = 3 périodes = shift (3, -3) glider. Prédisez d’abord (sans exécuter) : si la linéarité prouvée tient, où sera le glider après trois périodes ? Puis vérifiez votre prédiction par le calcul.

-- Exercice 3 : la linearite du glider sur trois periodes.
-- TODO etudiant : ecrivez le #eval qui verifie evolve 12 glider == shift (3, -3) glider
-- (attendu : true). Indice : le squelette est en commentaire ci-dessous.
-- #eval evolve 12 glider == shift (3, -3) glider
#eval 1 + 1 -- remplacez par votre verification

-- Exercice 3 : la linearite du glider sur trois periodes.

-- TODO etudiant : ecrivez le #eval qui verifie evolve 12 glider == shift (3, -3) glider

-- (attendu : true). Indice : le squelette est en commentaire ci-dessous.

-- #eval evolve 12 glider == shift (3, -3) glider

#eval 1 + 1 -- remplacez par votre verification 2

--% env 8

Raw input

{"cmd": "-- Exercice 3 : la linearite du glider sur trois periodes.\n-- TODO etudiant : ecrivez le #eval qui verifie evolve 12 glider == shift (3, -3) glider\n-- (attendu : true). Indice : le squelette est en commentaire ci-dessous.\n-- #eval evolve 12 glider == shift (3, -3) glider\n#eval 1 + 1 -- remplacez par votre verification", "env": 7}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 5},
   "data": "2"}],
 "env": 8}

Conclusion — ce que la visibilité change

Du loaf immobile au canon de Gosper qui émet des vaisseaux, les cinq régimes du Jeu de la Vie sont ici à la fois regardés et prouvés — chaque theorem un point d’ancrage, chaque #eval un témoin vivant, chaque #print axioms un certificat au degré réel (noyau pur, ou axiome native_decide assumé et nommé). Le fil — équilibre, cycle, translation, sérialisation, accélération — relie des modules qui vivaient séparément : c’était la raison d’être de PatternTour, et ce notebook en est la salle de classe.

C’est aussi la réponse au constat de l’EPIC #11703 : un module pédagogique que personne ne lit n’existe pas. Après ce compagnon, PatternTour n’est plus un module noir — la mesure scan_lake_notebook_visibility.py le comptera parmi les modules cités. Pour prolonger : Lean-16b (la simulation côté Python et Golly), Lean-16e (FRACTRAN natif), Lean-16g (les canons à gliders) et le corpus Hashlife du lake (HashlifeCorrectness), dont les murs NE/SW attendent encore leur visiteur.

Retour au sommet

1. Le lake, le module, et les trois prédicats

2. Équilibre — les still lifes, regardés puis prouvés

3. Cycle — la bascule decide → native_decide

4. Translation — les vaisseaux et l’invariance d’échelle

5. Sérialisation — le format RLE et l’opacité du parseur

6. Accélération — Hashlife contre la référence naïve, prouvés égaux

7. Exercices

Exercice 1 — Le bateau, encore à quai

Exercice 2 — Construire le blinker

Exercice 3 — Trois périodes : prédire puis vérifier

Conclusion — ce que la visibilité change

3. Cycle — la bascule `decide` → `native_decide`