01 / ConvergenceLean proof
One black cell.
Place one perturbation anywhere on the infinite grid. See how the proof covers every position and heading.
Try: choose a cell, then follow its proof branch.
A mathematical world in two colours
Follow the ant.
Explore the proof.
One simple rule creates a surprisingly rich geometry. Change a configuration, inspect a lifetime, or read a wake—and follow the argument behind what happens.
Six connected research stories. Exact dynamics. Proofs you can inspect.
The standard highway · period 104
01 / THE LABORATORIES
Choose a question.
Each laboratory begins with an experiment you control. Its proof steps explain how the observed mechanism extends to the complete input class covered by the theorem.
Showing all six laboratories.
02 / TimeExact clock
An ant on the clock.
A clock ticks on every update. Explore why a finite square cannot hold the ant forever.
Try: edit the square and inspect each clock increment.
03 / RigidityExact certificates
Read the wake.
Can a trail determine a highway? Turn a proposed wake into class counts, parity constraints, and a finite classification.
Try: move an odd class and see which condition changes.
04 / Local languageSharp witnesses
Ten turns tell a story.
Small windows constrain long futures. Inspect local violations and the balance between elapsed time and black mass.
Try: slide an interval onto the sharp equality witness.
05 / FeedbackComplete history
When memory returns.
Follow a black cell from its birth to its next read. See how finite memory predicts motion—and where the past returns.
Try: change memory length and inspect a remote lifetime.
06 / CompositionProtected interfaces
Build with highways.
Four black cells create a port. Compatible scattering rules join into finite routes while keeping their full history.
Try: compose two scattering rules and inspect their guard.
FOLLOW THE CONNECTIONS
What would you like to understand?
The same ant appears in every lab. Each proof asks a different question about its motion.
02 / FROM INTERACTION TO PROOF
Three ways to look closely.
Run the exact rule.
Replays turn, flip, and move on the complete finite field. Controls let you inspect a specific orbit, its true past, and the quantities that change.
Inspect a certificate.
Source-pinned data exposes finite witnesses, exact inequalities, and complete classifications. Each lab links to the code that regenerates its data.
Follow the general argument.
The proof steps explain coverage beyond any displayed example. The one-black theorem is Lean-checked; other results combine analytic arguments with the exact checks described in their papers.
Each theorem keeps its stated input class. Together these results illuminate the finite-support Highway Conjecture, which remains an open research question. Current drafts and published versions are identified in the publication portfolio.