Claims and certificates

A claim

A conservation claim says: “this quantity never changes”. The quantity is a density. You read each cell, or each window of a few cells, give it a weight, and add up over the whole ring. For traffic, a cell weighs 1 if it holds a car and 0 otherwise, and the total is the number of cars.

The difficulty: “never changes” must hold for rings of 3 cells, of 1,000 cells, of every size. You cannot simulate them all.

The idea of the certificate

Think of rooms connected by doors. If the number of people in each room changes only because people walk through doors, then the total number of people does not change: everyone who leaves one room enters the next. On a ring there is no edge through which anyone could leave.

The certificate says exactly this for a density. It gives a current, a number on each border between two cells, such that the change in every cell equals what comes in minus what goes out.

In the figure, a car that moves forward crosses a border. The cell it leaves loses 1, the cell it enters gains 1, and the current counts 1 on that border. Every change is explained by what crosses the borders, so the total stays the same.

Why a finite check is enough

The equation “change in the cell = what comes in − what goes out” depends only on a few neighbouring cells. For traffic, it is enough to look at patterns of 4 cells, which makes 16 patterns. The Lean kernel checks every one of them.

Then a theorem proved once and for all goes from local to global. It is called conserved_of_fluxCheck and says: if the density and the current satisfy the equation on every local pattern, then the total of the density is conserved on rings of every size, for every configuration. The proof adds up the equations of all the cells: around the ring the currents cancel in pairs.

What it looks like

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)

• Conserved (eca 184) (tableFn 2 [0, 1]) 1: in rule 184, the width-1 density that is 0 for an empty cell and 1 for a car is conserved.
• tableFn 2 [1, 1, 1, 1, 1, 1, 0, 0]: the current, one value for each of the 8 patterns of 3 cells.
• by decide +kernel: the kernel checks the equation on every pattern.

The Lean world reads the rule with a one-cell offset (see World), so its current table does not match the arrows in the figure word for word. It plays the same role. A current is only defined up to a constant: adding the same value everywhere changes no difference. The engine may therefore print another table that is just as valid.