A verified
animation.

What the picture shows

A field of synthetic points in a few clusters. In each cluster, one central point links to every point within a fixed distance, and each point links to its two nearest neighbours in the cluster. Every point also links to its nearest point, and the clusters are joined by their closest pairs. Every two and a half seconds, a new origin starts in open space, while open space remains.

Each origin grows a tree. Its wave travels along the links at one speed, the same for every tree, and claims each free point it reaches through the link that brought it. Where two trees’ waves meet on a link, that meeting link is drawn darker and the trees join the network. A tree that grows 25 branches without meeting another stops, fades and frees its points for later origins. Lighter lines show where waves crossed other links.

Each visit shows one of 25 runs. A run completes in about a minute and ends as one network.

Enrichment analyses draw networks like this, each hub linked to its members, and single-cell analyses build neighbourhood graphs before clustering or embedding. Paths on such graphs underlie trajectory and pseudotime methods. A result that looks right can still be wrong: a time understated, a branch that does not match its link, a point held by two trees at once.

The specification

Origins in turn

Each origin is its tree’s first claim, at its start. Starts fall on the origin time slots, and each later origin starts later. Origins

Tight branches

Claims come in time order. Every claim other than an origin comes from an earlier claim of the same tree, its time is that claim’s time plus the link’s length, and its branch is drawn exactly to it. Tight

The budget

A tree whose wave never meets another grows at most 25 branches and stops exactly at the 25th. A tree that meets another never stops. Budget

One tree at a time

A point is claimed again only after the tree that held it has stopped, held and faded. Exclusive

Wave halves

Every drawn half follows a link from a claimed point, for no longer than the link and not after its tree stops. A branch half reaches its point as that point is claimed. Halves

Meetings

A meeting is two opposite halves from different trees that end together where the waves meet. No two meetings join the same two trees, and a tree’s meeting time is its earliest meeting. Meetings

Honest links

Link lengths are straight-line distances rounded to the nearest unit, and no link is listed twice. Links

What is proved

For any run that meets the specification, Lean proves that every claim’s time is its tree origin’s start plus the length of a walk from that origin along the tree’s drawn branches (reached). The proof is checked by Lean’s kernel and uses only its standard axioms, propositional extensionality and quotient soundness.

What is checked

Each published run is checked against the whole specification (runA_valid to runY_valid) and the theorem is instantiated for it. These instance checks run through Lean’s compiled evaluator, so they trust the Lean compiler as well as the kernel; the axioms report lists what each one adds.

A bridge script checks every drawn point and link half in the served page against the certified claims and halves: where each starts, how long it draws, where it ends and when it fades. It also checks that every point ends in a tree that met another. Each visit selects one of 25 runs, and the browser draws it on canvas.

The animation then holds its completed state. Pause and resume use the control below “Verified animation”.

Small runs that break the rules are rejected the same way: a branch shorter than its time, a tree over its budget, a point held by two trees, a half drawn past its link, a meeting in the wrong place and an origin off its slot (Examples.lean, kernel-checked).

What is not covered

The browser’s canvas drawing, playback timing and the generator’s randomness lie outside the proof. The generator chooses where each origin starts; the certificate checks what follows. The picture illustrates a method; it is not evidence about any dataset or pipeline.

The same discipline applies to real analysis networks. A specification can state what a result must satisfy, and a checker can refuse one that falls short.