Une loi réfutée (règle 30)

Ce qu’on regarde

La règle 30 est un automate élémentaire célèbre pour son comportement d’apparence aléatoire. Quelqu’un affirme : « dans la règle 30, le nombre de cases noires ne change jamais ». On cherche le plus petit anneau, d’au moins 3 cases, où ce nombre change en un pas.

Lire la figure pas à pas

1. L’anneau a 3 cases : blanche, blanche, noire. Une case noire.
2. Chaque case lit son voisinage, en se souvenant que l’anneau se referme : la première case a pour voisine de gauche la dernière.
3. La règle 30 donne une case noire pour les voisinages 100, 011, 010 et 001, et une case blanche pour les autres.
4. Les trois cases voient 100, 001 et 010. Elles deviennent toutes noires.
5. Le nombre de cases noires passe de 1 à 3. L’affirmation est fausse.

La figure fait ce calcul dans votre navigateur : elle essaie les anneaux de 3 cases dans l’ordre et garde le premier où le total change.

L’énoncé Lean

theorem rule30_refuted :
    ¬ Conserved (eca 30) (tableFn 2 [0, 1]) 1 :=
  not_conserved_of_witness _ _ 1 [0, 0, 1]
    (by decide) (by decide +kernel) (by decide +kernel)

Le monde Lean lit la règle avec un décalage d’une case, mais sur cet anneau le résultat est le même : trois cases noires après un pas. Le moteur, lui, peut proposer un témoin encore plus petit, un anneau d’une seule case ; les deux sont valables.

Ce que cela démontre

Le nombre de cases noires n’est pas conservé par la règle 30. Un seul contre-exemple suffit, et le noyau l’a vérifié.

Ce que cela ne démontre pas

• Que la règle 30 n’a aucune loi de conservation. Ce théorème ne réfute qu’une seule affirmation. Le fait que la bibliothèque ne contienne aucune loi de largeur au plus 3 pour la règle 30 est un autre résultat, issu de la recherche exhaustive qui a construit la bibliothèque.
• Quoi que ce soit sur des densités plus larges.