Hg toolkit gromov sequences and boundary product

Fix a nonempty metric space $(X,d)$, a basepoint $o\in X$, and a product constant $\kappa \ge 0$ as in Hg toolkit slim triangles products and four point constants. Indices below are positive integers. A sequence $x=(x_n)$ is Gromov if for every real $R$ there is $N$ such that $(x_n\mathrm{\mid }{x}_m{)}_o>R$ whenever $n,m\ge N$. Write $x\sim y$ when for every $R$ some $N$ satisfies $(x_n\mathrm{\mid }{y}_m{)}_o>R$ for all $n,m\ge N$. This is joint divergence, not merely diagonal divergence.

For a nonnegative double sequence set ${\mathrm{lim\hspace{0.17em}inf}}_{n,m\to \mathrm{\infty }}{a}_{nm}={\sup }_{N\ge 1}\inf \{a_{nm}:n,m\ge N\}\in [0,+\mathrm{\infty }]\mathrm{.}$ Each inner set is nonempty and bounded below. Its infimum exists by the real completeness convention; the increasing family of infima has its supremum if bounded, and otherwise we assign $+\mathrm{\infty }$. No subtraction of infinite values is intended.

Once the equivalence relation has been proved, the Gromov-sequence boundary $\mathrm{\partial }X$ is the set of equivalence classes of Gromov sequences. Until then all expressions are indexed by sequences themselves. For classes $\xi ,\eta$ define the extended boundary product by $(\xi \mathrm{\mid }\eta {)}_o=\sup \{{\mathrm{lim\hspace{0.17em}inf}}_{n,m\to \mathrm{\infty }}(x_n\mathrm{\mid }{y}_m{)}_o:x\in \xi ,y\in \eta \}\in [0,+\mathrm{\infty }]\mathrm{.}$ For any fixed pair of classes the set in braces is nonempty, since each class contains a representing sequence, and its nonnegative supremum is interpreted as above. The quotient is a set, being a subset of the power set of $X^{\mathbb{N}}$; defining it does not select representatives for a family of classes. The boundary can be empty, for instance for a bounded space: products are bounded by distances from $o$, so no Gromov sequence exists. No properness, geodesicity or AC is assumed here.