An Ant on the Clock: Exponential Escape Bounds for Langton's Ant

For the classical white-right/black-left Langton ant, an explicit rational clock increases by at least 2/5 per update. A finite-square range estimate proves first exit from an n by n square within 8 n 3^n + 1 updates, uniformly over all internal colourings and poses. This gives an exponential upper bound in the side length, improving the asymptotic order of the factorial square bound. The same clock yields decidable complete-state reachability, orbit equivalence, and a computable orbit normal form. The analytic proofs are accompanied by Lean 4.30.0 proofs of the local algebra and telescoping lemmas, exact rational checks, and exhaustive verification of all 4,213,000 colour/pose states for squares of sides one through four. The supplementary artifact supplies the manuscript, proof sources, verification logs, reproduction commands and SHA256 manifests.