A refuted law (rule 30)

What we look at

Rule 30 is an elementary automaton famous for its random-looking behaviour. Someone claims: “in rule 30, the number of black cells never changes”. We look for the smallest ring, of at least 3 cells, on which that number changes in one step.

Reading the figure step by step

1. The ring has 3 cells: white, white, black. One black cell.
2. Each cell reads its neighbourhood, remembering that the ring closes: the first cell’s left neighbour is the last cell.
3. Rule 30 gives a black cell for the neighbourhoods 100, 011, 010 and 001, and a white cell for the others.
4. The three cells see 100, 001 and 010. They all turn black.
5. The number of black cells goes from 1 to 3. The claim is false.

The figure does this computation in your browser: it tries rings of 3 cells in order and keeps the first one on which the total changes.

The Lean statement

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)

The Lean world reads the rule with a one-cell offset, but on this ring the result is the same: three black cells after one step. The engine itself may offer an even smaller witness, a ring of a single cell; both are valid.

What it proves

The number of black cells is not conserved by rule 30. One counterexample is enough, and the kernel checked it.

What it does not prove

• That rule 30 has no conservation law at all. This theorem refutes a single claim. The fact that the library holds no law of width at most 3 for rule 30 is a different result, coming from the exhaustive search that built the library.
• Anything about wider densities.