06 / Ports and scattering
Build a highway. Bend it. Bring it back.
Four cells can keep an ant inside a half-plane forever. Protected collisions can be joined into finite trains. A longer packet sends the ant away and brings it back to read its own old wake.
Choose a proof witness
Loading exact construction data…
Loading…
Every update flips its actual cell. Highlighted points show the original obstacle locations; after a read they may be white. Whole-field view retains all debris; long trails are drawn as a sampled trace. Follow view changes only the camera.
The proof architecture
Why these finite witnesses extend to infinite time
1. First, a sharp entrance.
Starting at \((0,0)\), facing east, the seed \(\{(0,-1),(1,1),(1,3),(2,2)\}\) stays in \(x\ge0\) and reaches a permanent P104 tail after 182 updates. Every initial black set of at most three cells inside that half-plane exits by update 918. The three-cell witness attains 918 exactly.
2. Seal the interface.
A collision certificate specifies the complete field in a protected half-plane, the recovery path, and an all-future standard tail. Thirty rules cover NE and SE incoming highways. Their 448 compatible adjacent pairs satisfy strict separation inequalities at every gap of at least 100 whole periods.
3. Compose without deleting history.
All obstacles are placed in the initial field. At each collision, a forward-moving boundary separates old debris from the next recovery. The inequalities and exact interface equality close an induction over any finite compatible rule sequence.
4. Allow a controlled return.
A three-marker packet makes a northwest excursion, reverses, reads an old black cell, then restores an outgoing NE interface. For every integer \(n\ge100\), the old cell’s lifetime is exactly \(208n+53684\). The browser offers three finite witnesses; the affine inequalities in the proof cover every admissible \(n\).
Test the boundary, not a guess
A second rule is compatible precisely when its incoming orientation matches the first rule’s outgoing orientation. Try a different rule or a shorter gap: the builder identifies the missing certificate condition. A rejected construction makes no claim about its eventual dynamics.
The sharp three-cell witness and the four-cell port share the same initial pose. Their difference is visible in the laboratory; the universal three-cell bound is established by the complete first-visit branching proof.
Exact data, explicit proof ownership
The port theorem combines analytic reductions and exact computational certificates. The exporter imports the publication-owned checkers, verifies each kernel’s all-future tail, and records source hashes. The browser runs the literal finite dynamics and compares the resulting endpoint.
Guarded scattering checker · Return checker · Exported witnesses
python3 four_cell_port/reproduce.py