A two-cell law (rule 15)

What we look at

In rule 15, each cell becomes the opposite of its left neighbour: black if the neighbour was white, white if it was black. Counting black cells does not work here. The conserved quantity is read on two neighbouring cells: the number of pairs of equal neighbours, two whites or two blacks side by side.

Reading the figure step by step

1. The ring has 20 cells. A mark sits on each pair of equal neighbours.
2. The number to the right of each row counts these pairs. It is 8 on every row.
3. Take two equal neighbours, at places i−1 and i. At the next step, cells i and i+1 become their opposites, so they are equal to each other.
4. Take two different neighbours: at the next step, the two cells one place further on are different too.
5. Every pair, equal or not, therefore reappears one cell to the right, with the same nature. The total cannot change.

The density

The law is a density of width 2. You read every window of two cells and give it a weight:

In Lean, this table is written tableFn 2 [1, 0, 0, 1].

The Lean statement

It is a library theorem, under its original name:

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)

The current is zero everywhere. In the Lean world’s offset reading, each window of two cells becomes a window of the same nature in the same place: nothing needs to cross a border. The kernel checks the equation on the 32 patterns of 5 cells.

What it proves

In rule 15, the number of pairs of equal neighbours is conserved, on rings of every size and for every configuration.

What it does not prove

• That this is rule 15’s only law: the library holds another one, of width 3.
• Anything outside this world.