Lean 16g — Canons : le barreau 2 de l’échelle des témoins Life

Le dépôt sait vérifier une structure du Jeu de la Vie : le lake conway_lean prouve evolve 8 glider = shift (2, -2) glider par decide (conway_lean/Conway/Life/Computation.lean:176). Il ne sait pas encore construire : étant donné une propriété, produire une configuration qui la satisfait.

Ce notebook franchit un barreau de cette échelle — le barreau 2, et lui seul :

Barreau	Demande	État
1	une quasi-particule — configuration à translation périodique (le planeur)	vérifié côté lake
2	une source périodique — configuration bornée émettant périodiquement un vaisseau	ce notebook
3	une configuration réalisant le graphe d’un automate fini	hors d’atteinte, nommé tel quel
4	une configuration émulant une machine de Turing	hors d’atteinte, nommé tel quel

Vocabulaire. Le planeur est une quasi-particule : une excitation localisée qui se propage. Un flux de planeurs est un faisceau de quasi-particicles. Le canon de Gosper est une source périodique : un noyau borné qui, chaque période, détache une quasi-particule du même type. Ce vocabulaire décrit ce que l’objet est ; il remplace toute notation grecque par principe (le grep du dépôt ne trouve d’ailleurs nulle notation alpha/gamma en vigueur sur les objets Life — seuls un paramètre matplotlib et l’univers de types α de Lean portent ces lettres : la nomenclature ci-dessus s’applique d’emblée).

Sous-série Conway : 16a (l’homme et l’œuvre), 16b (Life en Lean), 16c (Golly), 16d (native), 16e (FRACTRAN), 16f (théorème du libre arbitre). Ici : 16b pose le substrat Grid/evolve que nous citons ; le README de la série situe l’ensemble.

import sys
from pathlib import Path

sys.path.insert(0, str(Path.cwd()))
from lean_notebook_utils import (
    find_lean_project, get_lean_project_path, run_lake, run_lean_snippet,
)
import random
from collections import Counter

# --- Moteur Life Python (stdlib pur, deterministe) ---
def step(cells):
    s = set(cells)
    cnt = Counter()
    for (x, y) in s:
        for dx in (-1, 0, 1):
            for dy in (-1, 0, 1):
                if dx or dy:
                    cnt[(x + dx, y + dy)] += 1
    return sorted((x, y) for (x, y), n in cnt.items()
                  if n == 3 or (n == 2 and (x, y) in s))

def islands(cells):
    s = set(cells); seen = set(); out = []
    for c in s:
        if c in seen: continue
        comp, stack = [], [c]; seen.add(c)
        while stack:
            (x, y) = stack.pop(); comp.append((x, y))
            for dx in (-1, 0, 1):
                for dy in (-1, 0, 1):
                    n = (x + dx, y + dy)
                    if n in s and n not in seen:
                        seen.add(n); stack.append(n)
        out.append(sorted(comp))
    return out

def norm(isl):
    mx = min(a for a, b in isl); my = min(b for a, b in isl)
    return sorted((a - mx, b - my) for a, b in isl)

# Le planeur canonique du lake (Conway.Life.glider) et ses 3 phases suivantes,
# puis les miroirs : 4 directions x 4 phases = 16 formes normalisees.
g0 = [(0, 0), (1, 0), (1, 2), (2, 0), (2, 1)]
def flipx(isl): return sorted((-a, b) for a, b in isl)
def flipy(isl): return sorted((a, -b) for a, b in isl)
GLIDER_FORMS = set()
for start in (g0, flipx(g0), flipy(g0), flipx(flipy(g0))):
    g = start
    for _ in range(4):
        GLIDER_FORMS.add(tuple(norm(g))); g = step(g)
print("formes de quasi-particule reconnues (4 directions x 4 phases) :", len(GLIDER_FORMS))

formes de quasi-particule reconnues (4 directions x 4 phases) : 16

Le substrat : ce qui est déjà vérifié, et où est le trou

La cellule suivante importe le motif du canon depuis le lake lui-même — le RLE du canon de Gosper est encodé dans conway_lean/Conway/Life/RLE.lean:268 avec sa grille analysée gosper_gun : Grid (36 cellules vivantes). Nous recopions le corps RLE et le décodons côté Python avec le même algorithme run-length que parseRLE : les deux définitions du dépôt et du notebook parlent du même objet — à une convention près, pédagogiquement utile : le lake encodie une cellule comme un couple (ligne, colonne) (RLE.lean inverse le corps run-length « pour retrouver l’ordre d’insertion row-major »), tandis que notre décodeur Python produit (colonne, ligne). Même motif, miroir de coordonnées — un mini-exercice de recoordonnancement avant le gros.

Ce que le lake prouve déjà (côté vérificateur) : - evolve 8 glider = shift (2, -2) glider, par decide — la quasi-particule se déplace d’une cellule en diagonale toutes les 4 générations (Computation.lean:176) ; - gosper_gun_parse_ok et gosper_gun_cell_count : gosper_gun.length = 36 (RLE.lean:332-343).

Ce que personne n’a encore : une définition vérifiable de « source périodique », mesurée sur le vrai canon, puis un certificat évaluable. C’est le barreau 2.

# Corps RLE du canon (identique a RLE.lean:268, sans l'en-tete de commentaires)
GUN_RLE_BODY = ("24bo11b$22bobo11b$12b2o6b2o12b2o$11bo3bo4b2o12b2o"
                "$2o8bo5bo3b2o14b$2o8bo3bob2o4bobo11b$10bo5bo7bo11b"
                "$11bo3bo20b$12b2o!")

def parse_rle_body(body):
    cells, x, y, num = [], 0, 0, ""
    for ch in body:
        if ch.isdigit(): num += ch
        elif ch == "b": x += int(num or 1); num = ""
        elif ch == "o":
            for i in range(int(num or 1)): cells.append((x + i, y))
            x += int(num or 1); num = ""
        elif ch == "$": y += int(num or 1); x = 0; num = ""
        elif ch == "!": break
    return sorted(set(cells))

GUN = parse_rle_body(GUN_RLE_BODY)
X0, X1 = min(a for a, b in GUN), max(a for a, b in GUN)
Y0, Y1 = min(b for a, b in GUN), max(b for a, b in GUN)
print("cellules du canon :", len(GUN), "(RLE.lean:343 attend 36)")
print("boite englobante : x", X0, "..", X1, ", y", Y0, "..", Y1)
print()
grid = {c: "O" for c in GUN}
for y in range(Y0, Y1 + 1):
    print("".join(grid.get((x, y), ".") for x in range(X0, X1 + 1)))

cellules du canon : 36 (RLE.lean:343 attend 36)
boite englobante : x 0 .. 35 , y 0 .. 8

........................O...........
......................O.O...........
............OO......OO............OO
...........O...O....OO............OO
OO........O.....O...OO..............
OO........O...O.OO....O.O...........
..........O.....O.......O...........
...........O...O....................
............OO......................

Exemple guidé 1 — Reconnaître : période, transitoire, classe émise

Une source périodique de période \(p\) est la conjonction de deux faits mesurables :

le noyau est périodique : la partie de la configuration qui intersecte la boîte du motif initial revient identique à elle-même toutes les \(p\) générations (sans translation — le noyau ne dérive pas) ;
l’émission est synchrone avec la période : à chaque fenêtre de \(p\) générations, une nouvelle quasi-particule s’est détachée du noyau et s’éloigne.

Historique : Bill Gosper (MIT, novembre 1970) répond au défi de Conway — 50 USD pour un motif fini à croissance non bornée. Le canon est le premier objet de ce type jamais trouvé ; il a déclenché la recherche de constructions auto-réplicants qui culmine avec Gemini (Wade, 2010). Voir RLE.lean:213-219 pour la même histoire contée par le lake.

def core(cells):
    """Noyau = iles qui INTERSECTENT la boite du canon a t=0.
    Les quasi-particules emises sont des iles disjointes, hors boite."""
    parts = [isl for isl in islands(cells)
             if any(X0 <= a <= X1 and Y0 <= b <= Y1 for (a, b) in isl)]
    return sorted(c for isl in parts for c in isl)

def gliders_out(cells):
    out = [(a, b) for (a, b) in cells if not (X0 <= a <= X1 and Y0 <= b <= Y1)]
    return [isl for isl in islands(out) if tuple(norm(isl)) in GLIDER_FORMS]

hist = [GUN]
for t in range(1, 121):
    hist.append(step(hist[-1]))

c0 = core(hist[0])
periode = next(p for p in range(1, 61) if core(hist[p]) == c0)
print("periode du noyau :", periode)
print("noyau cyclique des t=0 :", core(hist[30]) == c0 and core(hist[60]) == c0 and core(hist[90]) == c0)
print("taille du noyau (t=0, 30, 60, 90) :", [len(core(hist[t])) for t in (0, 30, 60, 90)])

premiers = {}
for t in range(1, 121):
    for k in range(1, len(gliders_out(hist[t])) + 1):
        premiers.setdefault(k, t)
print("premiere apparition de chaque quasi-particule :", dict(sorted(premiers.items())))
cadences = [premiers[k + 1] - premiers[k] for k in range(1, 4)]
print("cadences entre emissions :", cadences)

pos = {}
for t in range(34, 47):
    gls = gliders_out(hist[t])
    if gls:
        cx = sum(a for a, b in gls[0]) / len(gls[0])
        cy = sum(b for a, b in gls[0]) / len(gls[0])
        pos[t] = (round(cx, 1), round(cy, 1))
print("centre de masse de la 1re quasi-particule, t=34..39 :", {t: pos[t] for t in sorted(pos)[:6]})
print("population totale (t=0,30,60,90,120) :", [len(hist[t]) for t in (0, 30, 60, 90, 120)])

periode du noyau : 30
noyau cyclique des t=0 : True
taille du noyau (t=0, 30, 60, 90) : [36, 36, 36, 36]
premiere apparition de chaque quasi-particule : {1: 28, 2: 58, 3: 88, 4: 118}
cadences entre emissions : [30, 30, 30]
centre de masse de la 1re quasi-particule, t=34..39 : {34: (24.8, 11.2), 35: (25.2, 11.4), 36: (25.2, 11.8), 37: (25.4, 12.2), 38: (25.8, 12.2), 39: (26.2, 12.4)}
population totale (t=0,30,60,90,120) : [36, 41, 46, 51, 56]

Lecture du résultat : une horloge à quasi-particules

Période 30, transitoire 0 : la phase encodée par le RLE est déjà sur le cycle — le noyau de 36 cellules revient à lui-même exactement toutes les 30 générations, sans jamais dériver.
Cadence d’émission exactement 30 : les détachements surviennent à \(t = 28, 58, 88, 118\) (la première quasi-particule met 28 générations à devenir une île disjointe ; ensuite, chaque période en détache une nouvelle). Émission et période du noyau sont une seule horloge.
Classe émise : planeur diagonal c/4 — le centre de masse avance de \((+1{,}4, +1{,}2)\) en 5 générations, soit environ une case diagonale toutes les 4 générations, la vitesse du planeur prouvée par le lake (Computation.lean:176 : 8 générations → translation \((2,-2)\)).
Croissance non bornée depuis un objet fini : la population passe de 36 à \(36 + 5\lfloor t/30 \rfloor\) — chaque période ajoute 5 cellules qui ne reviendront jamais.

Reconnaître a coûté \(p \times H\) pas de simulation (ici \(30 \times 120\)) : c’est un budget, pas un mystère.

Exemple guidé 2 — Générer : une recherche bornée, et son résultat honnête

Le geste inverse — produire une source périodique au lieu de la constater — est d’une autre nature. Reconnaître est décidable en \(O(pH)\) une fois le candidat donné ; construire exige de chercher dans \(2^{k^2}\) boîtes de \(k \times k\). C’est exactement l’écart vérificateur → constructeur (la Loi II du chantier #12205).

Protocole, énoncé avant le tirage :

Budget : 3 000 soupes aléatoires déterministes (graines 0..2999), boîte \(12 \times 12\), densité 0,35, horizon 240 générations — soit au plus 720 000 pas de simulation (maj oration ; la détection de cycle anticipe l’arrêt).
Détection en deux phases : (1) le noyau (cellules dans la boîte + marge 2, normalisées par translation) entre-t-il dans un cycle de période \(p\) ? (2) après l’entrée en cycle, une nouvelle quasi-particule apparaît-elle dans chacune des 3 fenêtres suivantes de durée \(p\) ? Une explosion transitoire qui jette des planeurs puis se stabilise n’est pas une source : ses émissions précèdent le cycle.
Résultat attendu : inconnu. Le résultat honnête peut être « aucune dans ce budget » — et ce sera une mesure.

def classify_soup(seed, box=12, density=0.35, horizon=240):
    rng = random.Random(seed)
    cells = [(x, y) for x in range(box) for y in range(box) if rng.random() < density]
    seen, emitted, m = {}, 0, 2
    cur = sorted(cells)
    def count_qp(state):
        out = [(a, b) for (a, b) in state
               if not (-m <= a < box + m and -m <= b < box + m)]
        return len([isl for isl in islands(out) if tuple(norm(isl)) in GLIDER_FORMS])
    for t in range(1, horizon + 1):
        cur = step(cur)
        emitted = max(emitted, count_qp(cur))
        inside = sorted((a, b) for (a, b) in cur
                        if -m <= a < box + m and -m <= b < box + m)
        if not inside:
            return ("eteint", 0, emitted, False)
        key = tuple(norm(inside))
        if key in seen:
            p = t - seen[key]
            kind = "stable" if p == 1 else "oscillateur"
            counts = [count_qp(cur)]
            st = cur
            for _ in range(p): st = step(st)
            for _ in range(3):
                counts.append(count_qp(st))
                for _ in range(p): st = step(st)
            periodique = all(counts[i + 1] > counts[i] for i in range(3))
            return (kind, p, emitted, periodique)
        seen[key] = t
    return ("indecis", None, emitted, False)

stats, osc_ps, emit_any, sources = Counter(), Counter(), 0, 0
N = 3000
for seed in range(N):
    kind, p, emitted, periodique = classify_soup(seed)
    stats[kind] += 1
    if kind == "oscillateur": osc_ps[p] += 1
    if emitted >= 1: emit_any += 1
    if periodique: sources += 1

print("budget :", N, "soupes, boite 12x12, densite 0.35, horizon 240")
print("classification :", dict(stats))
print("periodes des oscillateurs :", dict(sorted(osc_ps.items())))
print("soupes ayant emis >= 1 quasi-particule (transitoire compris) :", emit_any, "/", N)
print("SOURCES periodiques trouvees :", sources)

budget : 3000 soupes, boite 12x12, densite 0.35, horizon 240
classification : {'eteint': 197, 'stable': 1387, 'oscillateur': 1155, 'indecis': 261}
periodes des oscillateurs : {2: 1048, 3: 28, 4: 51, 5: 5, 6: 5, 7: 1, 8: 3, 9: 1, 10: 3, 13: 1, 14: 1, 15: 1, 16: 2, 18: 1, 20: 1, 21: 1, 32: 1, 131: 1}
soupes ayant emis >= 1 quasi-particule (transitoire compris) : 1220 / 3000
SOURCES periodiques trouvees : 0

Lecture du résultat : un zéro calibré

0 source périodique en 3 000 soupes. Et ce zéro est calibré : le même détecteur, sur le même budget, trouve 1 155 oscillateurs (dont 1 048 clignotants de période 2), 1 387 formes stables, et 1 220 soupes qui ont réellement émis au moins une quasi-particule — mais par explosion transitoire, suivie d’une stabilisation. Le détecteur voit abondamment tout ce qui est presque une source ; il ne voit aucune source. Le zéro mesure le budget, pas un aveuglement de l’instrument.
La rareté a une cause structurelle : une source exige que l’émission coïncide avec la période du noyau — deux conditions conjointes, chacune rare, et leur conjonction l’est quadratiquement. Le canon de Gosper (36 cellules choisies parmi \(2^{36 \cdot 9}\)) n’a pas été tiré au hasard : l’équipe du MIT l’a construit par recherche dirigée, en assemblant des composants connus. Construire n’est pas échantillonner — c’est le geste que le barreau 2 isole.

# CONTROLE POSITIF : le detecteur, applique au canon lui-meme, doit dire SOURCE.
def gun_control():
    m = 2
    def inside_of(state):
        return sorted((a, b) for (a, b) in state
                      if X0 - m <= a <= X1 + m and Y0 - m <= b <= Y1 + m)
    def count_qp(state):
        out = [(a, b) for (a, b) in state if not (X0 <= a <= X1 and Y0 <= b <= Y1)]
        return len([isl for isl in islands(out) if tuple(norm(isl)) in GLIDER_FORMS])
    seen, cur = {}, GUN
    for t in range(1, 241):
        cur = step(cur)
        key = tuple(norm(inside_of(cur)))
        if key in seen:
            p = t - seen[key]
            counts = [count_qp(cur)]
            st = cur
            for _ in range(p): st = step(st)
            for _ in range(3):
                counts.append(count_qp(st))
                for _ in range(p): st = step(st)
            return p, all(counts[i + 1] > counts[i] for i in range(3)), counts
        seen[key] = t
    return None, False, []

p_ctrl, est_source, fenetres = gun_control()
print("controle positif — periode :", p_ctrl, "| source detectee :", est_source)
print("comptages par fenetre (doivent croitre strictement) :", fenetres)

controle positif — periode : 30 | source detectee : True
comptages par fenetre (doivent croitre strictement) : [1, 2, 3, 4]

Pourquoi le contrôle positif n’est pas un luxe

Un zéro de détecteur et un zéro de corpus sont indiscernables sans témoin positif : si le détecteur était cassé (formes de planeur incomplètes, marge mal calibrée), il rendrait le même « 0 sources » que la vérité. La cellule précédente applique l’instrument, sans aucune modification, au seul objet du dépôt dont on sait (quand même — par la mesure de l’exemple guidé 1) qu’il est une source : il répond periode 30, source detectee True, fenetres [1, 2, 3, 4]. L’instrument est sain ; le zéro de la recherche est un fait du monde.

Notez aussi pourquoi les 1 220 émetteurs transitoires ne comptent pas : leurs quasi-particules partent pendant l’explosion initiale, avant que le noyau n’entre dans son cycle. Une source exige l’émission pendant le régime périodique — l’horloge, pas le bang.

Exemple guidé 3 — Le certificat : énoncer la propriété de façon vérifiable

Reconnaître (exemple guidé 1) mesurait en Python. Un certificat doit être énoncé dans le langage du dépôt — un prédicat Bool sur Grid — et évalué par le moteur de Lean, sur un horizon fini explicite. Le lake fournit les briques : Grid = List (Int × Int) (Life.lean:66), evolve : Nat → Grid → Grid (Life.lean:155), gosper_gun : Grid (RLE.lean:277) — toutes sous le namespace Conway.Life / Conway.Life.RLE, avec la convention (ligne, colonne) pour les cellules.

Le prédicat du barreau 2, restreint à un horizon fini \(H\) :

core (evolve p g) = core g pour chaque multiple de \(p\) jusqu’à \(H\), où core restreint une grille à la boîte du motif initial.

Deux précisions d’honnêteté : - le filtre core doit exister dans le certificat — sans lui l’égalité est fausse, puisque le canon croît (les quasi-particules s’accumulent hors boîte) ; - #eval évalue (interpréteur Lean) ; ce n’est pas une preuve au sens du noyau. Le passage de #eval à decide — ce que Computation.lean:176 a fait pour le planeur (barreau 1) — est un travail lake-side, nommé ici comme tel.

LEAN_PROJECT = get_lean_project_path('conway_lean')  # forme /mnt/c/... pour run_lean_snippet
snippet = '''
import Conway.Life
import Conway.Life.RLE
open Conway.Life
open Conway.Life.RLE

/-- Boite stricte du canon a t=0, en convention (ligne, colonne) du lake :
    lignes 0..8, colonnes 0..35 (RLE.lean annonce x=36, y=9). -/
def inBox (c : Int × Int) : Bool := 0 ≤ c.1 ∧ c.1 < 9 ∧ 0 ≤ c.2 ∧ c.2 < 36

/-- Noyau = cellules dans la boite stricte. -/
def core (g : Grid) : Grid := g.filter inBox

-- Certificat horizon fini : le noyau revient a lui-meme a chaque periode
#eval core (evolve 30 gosper_gun) == core gosper_gun
#eval core (evolve 60 gosper_gun) == core gosper_gun
#eval core (evolve 90 gosper_gun) == core gosper_gun

-- Le noyau est exactement le canon : 36 cellules, rien de moins
#eval (core gosper_gun).length
#eval core gosper_gun == gosper_gun

-- Le complementaire apres une periode : la quasi-particule emise (5 cellules)
#eval ((evolve 30 gosper_gun).filter (fun c => !inBox c)).length
'''
out = run_lean_snippet(LEAN_PROJECT, snippet, timeout=120, snippet_id="canon_certificat")
print(out)

true
true
true
36
true
5

Lecture du certificat

Six réponses attendues : true, true, true, 36, true, 5.

les trois true disent : à chaque multiple de 30 générations (horizon 30, 60, 90), le noyau est exactement le canon initial — la partie bornée du système est une horloge, vérifiée par le moteur de Lean sur un horizon fini et explicite ;
36 et true : le noyau n’est ni tronqué ni étendu — le filtre inBox ne cache rien ;
5 : après une période, le complémentaire hors boîte compte 5 cellules — une quasi-particule complète, cohérente avec la mesure Python de l’exemple guidé 1 (une émission par période).

Ce que le certificat ne prétend pas : - il ne dit rien des instants entre les multiples de 30 (le noyau excursione hors boîte pendant le cycle — mesuré : y jusqu’à 11 pendant t = 0..29) ; - il ne prouve pas la périodicité pour tout \(t\) : cela exigerait une induction sur les horizons et l’argument que la quasi-particule émise ne réinteragit jamais avec le noyau — un théorème lake-side, pas une évaluation ; - #eval reste une évaluation. La version decide (preuve noyau) du barreau 1 existe pour le planeur (Computation.lean:176) ; son analogue au canon est le prochain geste du lake.

Ce qui reste hors d’atteinte — nommé, pas maquillé

Barreau	Ce qu’il faudrait	Pourquoi ce n’est pas « une perspective »
3 — automate fini	une configuration dont le faisceau de quasi-particules réalise le graphe de transitions d’un automate donné	les canons connus n’émettent pas l’information ; il faut des collisionneurs, des réflecteurs, une synthèse dirigée de composants — pas un tirage de soupes
4 — machine de Turing	l’encodage explicite d’une machine et sa construction	c’est le programme Gemini (Wade, 2010) : des années-homme de design dirigé

La leçon des deux exemples guidés est la même des deux côtés de l’échelle : l’écart entre vérifier et construire n’est pas un manque d’ingéniosité, il est structurel. Le vérificateur est un algorithme polynomial en l’horizon ; le constructeur navigue un espace exponentiel dont la structure n’est connue que par fragments (gliders, canons, collisionneurs). C’est précisément pourquoi le chantier #12205 parle de témoin : le canon de Gosper est le témoin que « croissance non bornée depuis un objet fini » est réalisable — et le barreau 2 s’arrête là où sa réalisation vérifiée s’arrête.

Exercices

Exercice 1 — Reconnaître un autre objet : le pulsar

Le lake encode aussi le pulsar (pulsar_RLE, RLE.lean:247) : oscillateur de période 3, 48 cellules, le grand oscillateur le plus courant dans les soupes (votre recherche en a d’ailleurs trouvé, période 3 : 28 instances). Appliquez le protocole de l’exemple guidé 1 : mesurez sa période, puis montrez qu’il échoue au critère 2 — aucune émission. Un oscillateur n’est pas une source : il n’y a d’horloge que pour lui-même.

# TODO etudiant
# 1. Parser le RLE du pulsar (corps ci-dessous, meme decodeur que c04)
PULSAR_RLE_BODY = ("2b3o3b3o2b$13b$o4bobo4bo$o4bobo4bo$o4bobo4bo$2b3o3b3o2b"
                   "$13b$2b3o3b3o2b$o4bobo4bo$o4bobo4bo$o4bobo4bo$13b$2b3o3b3o2b!")
# 2. Mesurer la periode du noyau (methode c06)
# 3. Compter les quasi-particules emises sur 90 generations (methode gliders_out)
# 4. Conclure : periode = ?, emissions = 0, donc oscillateur / non source
resultat_ex1 = None  # TODO etudiant

Exercice 2 — Étendre le budget : le zéro résiste-t-il ?

Le résultat « 0 sources en 3 000 soupes » est une mesure à budget donné. Étendez : boîte \(16 \times 16\), densité 0,35, 30 000 soupes (dix fois le budget). Deux issues honnêtes : le zéro tient (renforcez la borne), ou une source apparaît — alors mesurez sa période, son transitoire, sa classe émise, et passez-la au contrôle de la cellule c11. Attention au coût : 30 000 soupes × horizon 240 ≈ quelques minutes ; mesurez et affichez votre budget réel.

# TODO etudiant
# 1. Reexecuter classify_soup avec box=16 et le triple horizon si besoin
# 2. Boucle sur 30000 graines (mesurez le temps reel et affichez-le)
# 3. Rapporter : classification, periodes, sources (0 attendu ? a mesurer)
resultat_ex2 = None  # TODO etudiant

Exercice 3 — Le certificat pour le pulsar, côté Lean

Reprenez le snippet de c14 : remplacez gosper_gun par une définition du pulsar (décodez le RLE en Grid — ou encodez les 48 cellules à la main), et évaluez core (evolve 3 pulsar) == core pulsar sur les horizons 3, 6, 9. La périodicité du noyau doit se vérifier ; le complémentaire hors boîte doit rester vide — c’est la signature Lean d’un oscillateur : périodicité sans émission.

# TODO etudiant
# Ecrire le snippet Lean (methode c14) : inBoxPulsar, corePulsar, #eval sur horizons 3/6/9
# puis run_lean_snippet(LEAN_PROJECT, snippet, timeout=280, snippet_id="pulsar_certificat")
resultat_ex3 = None  # TODO etudiant

Conclusion — où en est l’échelle

Barreau	Vérifié ?	Construit ?	Témoignage
1 — quasi-particule	oui, par le lake (`decide`, `Computation.lean:176`)	le planeur est une donnée, pas une construction	la translation périodique existe
2 — source périodique	oui, ici : période 30 + cadence 30 mesurées, certificat `#eval` sur horizon 90	non, et mesuré : 0/3 000 soupes, zéro calibré par contrôle positif	le canon de Gosper : croissance non bornée depuis 36 cellules
3 — automate fini	non	non	nécessite une synthèse dirigée — hors d’atteinte, dit comme tel
4 — machine de Turing	non	non	programme Gemini : des années de design

Le barreau 2 referme un cycle complet : reconnaître (mesures), générer (le zéro honnête, qui est une information positive sur la rareté), certifier (prédicat vérifiable, évalué sur horizon fini). Le barreau suivant ne se franchira pas en échantillonnant plus fort — le protocole de l’exercice 2 le dira à quiconque essaie — mais en assemblant des composants : c’est un changement de nature, pas de budget.

Lean-16g — Canons, barreau 2 de l’échelle des témoins (issue #12223, chantier #12205). Substrat et citations : lake conway_lean (Life.lean, RLE.lean, Computation.lean), consommé en lecture — aucun .lean modifié. Vocabulaire : quasi-particule, faisceau, source périodique.

Retour au sommet