Hg toolkit hyperbolic group and stable length

For completeness, the realization is geodesic as asserted in the definition. For two interior-edge points, any finite edge route either stays on their common edge, when there is one, or first reaches one of the at most two endpoints of the first edge and finally leaves one of the endpoints of the last edge. Between those vertices its length is at least their word distance. Conversely each of these at most four endpoint routes is attained by a shortest word, with the specified initial and final partial edges. Include the direct same-edge interval as another candidate. The minimum of this finite list is attained and positive for distinct points; it defines the path metric. Concatenation gives the triangle inequality. A minimizing route, parametrized by length, is isometric, since a shorter route between two of its points would shorten it. At vertices the same argument gives exactly word distance. Loops are covered by the two ends of their interval before identification; coincident endpoints cause no problem.

Put $a_n=\mathrm{\mid }{g}^n\mathrm{\mid }$ and $a_0=0$. Then $0\le a_{n+m}\le a_n+a_m$, so the nonempty set $\{a_k\mathrm{/}k:k\ge 1\}$ is bounded below by zero. Its infimum $t$ exists and satisfies $0\le t\le a_1$.

Fix $\eta >0$. By the defining property of the infimum there is a positive integer $k$ such that $a_k\mathrm{/}k<t+\eta \mathrm{/}2$. For each $n\ge 1$ write $n=qk+r$, $0\le r<k$. Repeated subadditivity gives $a_n\le q{a}_k+a_r$. With $C={\max }_{0\le r<k}{a}_r$, it follows that $t\le a_n\mathrm{/}n\le a_k\mathrm{/}k+C\mathrm{/}n$. Here $q\mathrm{/}n\le 1\mathrm{/}k$ and $a_k\ge 0$ justify the last inequality.

For all sufficiently large $n$, $C\mathrm{/}n<\eta \mathrm{/}2$, giving $t\le a_n\mathrm{/}n<t+\eta$. The requisite large integers exist in a real complete ordered field: if the natural numbers had a finite supremum $u$, some natural $m>u-1$ would give $m+1>u$, a contradiction. Thus $a_n\mathrm{/}n\to t$. This also treats $C=0$ and $k=1$ directly. If $g=e$, every $a_n$ and $t$ is zero; if $g$ has finite order $m$, $a_m=0$ gives $t=0$. Only one witness $k$ for a given tolerance and finitely many endpoint routes were used, so no AC is needed.