Abstract
<title>Abstract</title> <p> We study the classical two-colour Langton's ant on Z² from a finite-support colouring, assuming its turn trace is eventually periodic with nonzero drift. We give a decidable necessary-and-sufficient criterion for a finite word to admit such a realisation, with an explicit seed. Every resulting highway has strictly positive net black growth divisible by four, and a signed mod-four residue identity for the growing wake yields the bound <italic>g</italic> ≥ 2 max(| <italic>a</italic> |, | <italic>b</italic> |) for drift ( <italic>a</italic> , <italic>b</italic> ). We also give an exact medial (Tait)-graph formulation and a collision-chain parity identity. For diagonal drift we prove a transverse rigidity theorem: the two extremal level lines are horizontal, carry only R, and each of their cells reached by the periodic tail is entered once, so the highway runs between guard rails of permanent wake and has even transverse width. Width two is therefore impossible. A computer-assisted argument excludes width four at every period: crossing sequences at untouched five-cell columns form a twelve-edge directed graph on which an explicit rank strictly decreases; two independent enumerators reproduce the edge table and Lean checks the rank consequence. Hence every diagonal periodic highway has width at least six, and a residue-theorem-free audited enumeration excludes all periods at most 48. Selected finite algebraic kernels are checked in Lean 4, though their extraction from an ant trace is not formalised end to end. These results constrain periodic highways but prove neither that every finite-support orbit becomes periodic nor that the standard period-104 highway is unique. </p>