Asymptotic gromov sequences form an equivalence relation

A Gromov sequence $x$ satisfies $x\sim x$ by exactly the joint divergence in F1. Symmetry follows from $(x_n\mathrm{\mid }{y}_m{)}_o=(y_m\mathrm{\mid }{x}_n{)}_o$, interchanging the two quantified indices. These assertions are also valid when no Gromov sequences exist, since they quantify over that set.

Suppose $x\sim y$ and $y\sim z$, and fix a real threshold $R$. There is a common integer $N$ such that $(x_n\mathrm{\mid }{y}_k{)}_o>R+\kappa$ and $(y_k\mathrm{\mid }{z}_m{)}_o>R+\kappa$ for all $n,k,m\ge N$, by taking the larger of the two divergence cutoffs. Fix the single index $k=N$. The product inequality gives $(x_n\mathrm{\mid }{z}_m{)}_o>R$ for every $n,m\ge N$, proving transitivity with joint quantifiers.

Put $D=d(o,o^{\mathrm{\prime }})$. The reverse triangle inequality gives $\mathrm{\mid }d(o,x)-d(o^{\mathrm{\prime }},x)\mathrm{\mid }\le D$ for every $x$. Expanding the two products therefore gives $\mathrm{\mid }(x\mathrm{\mid }y{)}_o-(x\mathrm{\mid }y{)}_{o^{\mathrm{\prime }}}\mathrm{\mid }\le D$. A joint-divergence cutoff at threshold $R+D$ for one basepoint is a cutoff at $R$ for the other. Apply this first to a sequence paired with itself, then to two sequences. Interchanging $o,o^{\mathrm{\prime }}$ proves both directions of basepoint independence.

Steps 1.1–1.2 prove equivalence and therefore justify the quotient specified in F1; step 1.3 identifies the same classes at every basepoint. F2 supplies the stated geodesic specialization. There is no selection of a family of representatives and no AC. All arguments include $\kappa =0$ and $D=0$.