Une loi sur deux cases (règle 15)

Ce qu’on regarde

Dans la règle 15, chaque case devient le contraire de sa voisine de gauche : noire si la voisine était blanche, blanche si elle était noire. Compter les cases noires ne marche pas ici. La quantité conservée se lit sur deux cases voisines : le nombre de paires de voisines égales, deux blanches ou deux noires côte à côte.

Lire la figure pas à pas

1. L’anneau a 20 cases. Un repère marque chaque paire de voisines égales.
2. Le nombre à droite de chaque ligne compte ces paires. Il vaut 8 à chaque ligne.
3. Prenez deux voisines égales, aux places i−1 et i. Au pas suivant, les cases i et i+1 deviennent leurs contraires, donc elles sont égales entre elles.
4. Prenez deux voisines différentes : au pas suivant, les deux cases d’après sont différentes elles aussi.
5. Chaque paire, égale ou non, se retrouve donc une case plus à droite, avec la même nature. Le total ne peut pas changer.

La densité

La loi est une densité de largeur 2. On lit chaque fenêtre de deux cases et on lui donne un poids :

En Lean, cette table s’écrit tableFn 2 [1, 0, 0, 1].

L’énoncé Lean

C’est un théorème de la bibliothèque, sous son nom d’origine :

theorem eca_15_b00006 :
    Conserved (eca 15) (tableFn 2 [1, 0, 0, 1]) 2 :=
  conserved_of_fluxCheck _ _
    (tableFn 2 [0, 0, 0, 0, 0, 0, 0, 0,
                0, 0, 0, 0, 0, 0, 0, 0]) 2
    (by decide +kernel)

Le courant est nul partout. Dans la lecture décalée du monde Lean, chaque fenêtre de deux cases devient exactement une fenêtre de même nature à la même place : rien n’a besoin de traverser une frontière. Le noyau vérifie l’équation sur les 32 motifs de 5 cases.

Ce que cela démontre

Dans la règle 15, le nombre de paires de voisines égales est conservé, sur des anneaux de toutes les tailles et pour toutes les configurations.

Ce que cela ne démontre pas

• Que cette loi soit la seule de la règle 15 : la bibliothèque en contient une autre, de largeur 3.
• Quoi que ce soit hors de ce monde.