Mutome (external site)
Menu

Traffic (rule 184)

Step by step: why the number of cars never changes in rule 184, and exactly what the Lean theorem proves.

What we look at

A circular road of 28 cells. A black cell is a car, a white cell is free. At each step every car moves at once, following one rule: move one cell to the right if the cell in front is free, otherwise wait.

Rule 184: traffic

View

Step 16: 14 cars

stepcars0141142143144145146147148149141014111412141314141415141614

carfree cellconserved count

Simulated in your browser, centred convention. The number of cars, on the right, does not change. The proof covers every ring.

Reading the figure step by step

  1. The first row is the road at the start, with 14 cars.
  2. Each following row is the road one step later. Time runs downwards.
  3. Follow a lone car: it moves one cell per row, diagonally to the right.
  4. Follow a jam: only the front car can move, the others wait. The jam dissolves from the front.
  5. The number to the right of each row counts the cars. It is 14 on every row.

Why the number does not change

A car never disappears: it either stays put or moves into the next cell. And two cars never arrive in the same cell, since a car only moves when the cell ahead is free. Every change in a cell is therefore explained by a car crossing a border.

What leaves one cell enters the next

View

Step 0: 4 cars cross a border

Step 0Step 1+10−1+1−1+1000−1+1−1change of each cell = what comes in − what goes out77

cara car crosses a borderconserved count

Each arrow is a car crossing a border. A cell loses what goes out and gains what comes in; around the ring, losses and gains cancel.

That is exactly what the certificate says: the change in every cell equals what comes in minus what goes out. Around the ring, what leaves one cell enters the next. See Claims and certificates.

The Lean statement

Lean 4
theorem traffic :
    Conserved (eca 184) (tableFn 2 [0, 1]) 1 :=
  conserved_of_fluxCheck _ _
    (tableFn 2 [1, 1, 1, 1, 1, 1, 0, 0]) 1
    (by decide +kernel)

The library holds the same law in another form: it counts free cells, with the density tableFn 2 [1, 0]. On a ring of fixed size, counting free cells and counting cars amount to the same thing.

What it proves

In rule 184 as defined in Lean, the number of cars never changes, on rings of every size and from every starting configuration. The kernel checked the certificate on the 16 patterns of 4 cells, and the theorem conserved_of_fluxCheck does the rest.

What it does not prove

  • Anything about real road traffic. Rule 184 is a model, and this is a proof in a world.
  • Anything about speed or jams: only the conservation of the number of cars is proved.
  • The figure is not the proof. It shows 16 steps from one configuration; the proof covers them all.