02 / Clock and escape
A clock that always advances.
The ant can turn back, revisit cells and erase its own trail. A quantity attached to the complete state still increases at every update. Inside a finite box, that clock has only a finite range.
Build a finite square
Before running, click a cell to flip its colour. Choose “Place ant” to move the starting point. Coordinates and the whole finite black field are retained.
Keyboard coordinate editing
Ready.
The proof in three moves
From one update to inevitable escape
1. Keep a parity invariant.
Let \(\chi(x,y)=(-1)^{x+y}\). The sign \(\sigma=\chi(p)\) for a vertical heading and \(-\chi(p)\) for a horizontal heading stays fixed: every update changes both position parity and heading axis.
2. Balance the field against the heading.
Only the current cell changes colour. Its field contribution and the new heading correction combine to give an integer gain of at least one. Choose \(c=n-1\) for the square \(\{0,\ldots,n-1\}^2\).
3. Spend a finite clock range.
Restrict the sum to the square. Until the first exit, outside cells stay fixed and the same increment identity applies. The range is at most \(R_n=E(n)-1\). If the first exit is at update \(T\), the first \(T-1\) updates stay inside, so
Long, thin rectangles behave differently
For fixed height \(H\), a separate rational clock gives a polynomial escape bound in the long side \(N\), of degree \(\lfloor H/2\rfloor+1\). The square clock above is useful for its exact universal increment; the rectangle proof chooses different weights.
Degree 2 in N.
What is established here?
The square and rectangle bounds are analytic theorems with exact algebraic checks. The repository also contains Lean proofs for the earlier supercritical local identities; the improved integer-clock square bound has its own analytic proof and exact checks.
Integer clock source · Exhaustive small-square checks
python3 clock_escape/reproduce.py --integer-only