Dyadic product estimate for group neighbourhoods (source code)

= Dyadic product estimate for group neighbourhoods
{title2=$\sum_j2^{-n_j}\le2^{-n}\Longrightarrow\prod_jg_j\in U_{n-1}$}

Let $U_0=G$, and let the $U_n$ be decreasing symmetric sets containing the <identity element> with $U_n^3\subset U_{n-1}$. If $g_j\in U_{n_j}$ and their dyadic costs sum to at most $2^{-n}$ for $n\ge1$, split the ordered word at an edge crossing its half-cost point. The words on either side each have cost at most $2^{-n-1}$. Induction on word length puts both side words in $U_n$, while the middle edge also belongs to $U_n$. Their threefold product lies in $U_{n-1}$. This controls the short-chain collapse that would otherwise make a path-distance construction degenerate.