Birkhoff-Kakutani theorem ($G\text{ metrizable}⟺G\text{ first countable}$)

A Hausdorff topological group admits a compatible left-invariant group metric exactly when it has a countable neighbourhood basis at the identity element. Choose symmetric neighbourhoods of the identity element $U_n$ with $U_{n+1}^3\subset U_n$ and trivial intersection. Assign a step in $U_n$ cost $2^{-n}$, and take the infimum of total costs of chains joining two points. The dyadic product estimate for group neighbourhoods makes this a genuine compatible metric. The Hausdorff assumption separates distinct points; without it the same construction can give only a pseudometric.

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\ge 1$, 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.