Solution (source code)

= Solution

Use the faithful logarithm realization from the root Solution: $\log:G\to A$ identifies $L_G$ with the <Lie algebra> $\log G$. For $x,y\in G$, the convergent exponential identity in $A$ gives
$$
\operatorname{BCH}(\log x,\log y)=\log(\exp(\log x)\exp(\log y))=\log(xy).
$$
Every <Lie polynomial> and its convergent sum are preserved by this realization of $L_G$. Therefore the BCH product on the underlying set of $L_G$ has exactly the same logarithm as the original product $xy$. Injectivity of the logarithm proves equality of the two products, with the same topology, identity and inverses:
$$
\boxed{(L_G,*)=G.}
$$
This proves the reverse direction of the <uniform pro-p group and powerful Lie lattice correspondence> directly; the forward identity alone would not imply it.