Every One-Black-Cell Langton Ant Reaches the Period-104 Highway: A Lean-Checked Proof

Langton's ant is a deterministic walk on the square lattice whose blank-plane orbit eventually exhibits a diagonal period-104 highway, but the corresponding finite-support Highway Conjecture remains open. We prove a complete unbounded subfamily: from every initial state having exactly one black cell, with no restriction on that cell's position or on the ant's pose, the classical two-colour ant eventually reaches permanent period-104 behaviour. The proof normalizes the pose, couples the perturbed orbit to the first 9,977 steps of the blank orbit, and reduces every untouched defect to one of 22 affine frontier channels. Twenty-one channels admit an ordinary scattering induction after a channel-specific finite cutoff. The remaining channel first creates a reverse period-104 highway; in the physical historical state it returns to a fixed old cell, with collision time increasing by 208 steps per unit depth, and then enters the forward highway after a checked finite transient. The infinite reductions, geometric separation arguments, recurrence relations, and certificate-soundness theorems are formalized in Lean 4. Three closed finite reports---the blank highway, 1,376 prefix contacts, and the shared scattering certificate---are evaluated with \texttt{native\_decide}. We state this trust boundary explicitly: native evaluation adds Lean's compiler, runtime, and code-generation path to the trusted base. The checked sources, witness tables, and reproduction command are available in the public \href{https://github.com/kehao95/langtons-ant-core}{source-code and Lean-proof repository}.