Solution (source code)

= Solution

For a <pro-p group>, the <lower p-series> is the descending sequence of closed <characteristic subgroups>
$$
\boxed{P_1(G)=G,\qquad P_{i+1}(G)=\overline{P_i(G)^p[P_i(G),G]}.}
$$
The bar means <closure> of the <subgroup> generated by the displayed powers and <group commutators>. Throughout this question $p$ is odd. For a finitely generated <powerful pro-p group>, <group commutator> collection gives $P_i(G)=G^{p^{i-1}}$, each $P_i$ is powerful, and $\Phi(P_i)=P_{i+1}$. All these <subgroups> are open. A <uniform pro-p group> is such a <group> with all <subgroup> indices $[P_i:P_{i+1}]$ equal to $[G:P_2]$. We use the standard powerful-group torsion criterion: a finitely generated <powerful pro-p group> is uniform exactly when it is a <torsion-free group>. For a uniform <group> of generator number $d$, the indices are $p^d$, and $x\mapsto x^{p^a}$ is a <homeomorphism> from $G$ onto $G^{p^a}$.

We record explicitly the collection facts used for the operations below. With $U_b=G^{p^b}=P_{b+1}$, one has
$$
[U_a,U_b]\le U_{a+b+1},\qquad x\equiv y\pmod{U_b}\ \Longleftrightarrow\ x^{p^a}\equiv y^{p^a}\pmod{U_{a+b}}.
$$
The second statement is the power-congruence property: the $p$th-power map is an <isomorphism> on adjacent uniform layers, and collection gives $(yu)^p\equiv y^pu^p\pmod{U_{b+2}}$ for $u\in U_b$. Thus the first nonzero layer of a difference moves down exactly one step under a $p$th power. Iterating gives the asserted equivalence and also justifies taking roots of congruences. These facts follow from powerful-group <group commutator> collection, using divisibility by $p$ of $\binom p2$ and the successive-layer power isomorphisms; they are the uniform-group structure results being used here.

The <transported addition on a uniform pro-p group> is
$$
\boxed{x+_ny=(x^{p^n}y^{p^n})^{p^{-n}}\qquad(n\ge1).}
$$
The product is in $U_n$ and has a unique $p^n$th root in $G$. For the comparison at $n=1$ define $x+_0y=xy$. The numbered proofs below establish <associativity>, approximate <commutativity> and compatibility of these operations.

The intrinsic <Lie algebra of a uniform pro-p group> has underlying set $G$, zero equal to the <group> identity, additive inverse $x^{-1}$, and operations
$$
\boxed{x+_Ly=\lim_{n\to\infty}(x^{p^n}y^{p^n})^{p^{-n}},\qquad [x,y]_L=\lim_{n\to\infty}[x^{p^n},y^{p^n}]^{p^{-2n}},\qquad \lambda x=x^\lambda\ (\lambda\in\mathbb Z_p).}
$$
Here the <group commutator> is $[x,y]=x^{-1}y^{-1}xy$. For $\lambda\in\mathbb Z_p$, $x^\lambda$ is the limit of $x^{m_j}$ for integers $m_j\to\lambda$; the pro-$p$ <topology> makes it well defined. The addition sequence is <Cauchy> by the compatibility proved below. The <group commutator> estimate puts $[x^{p^n},y^{p^n}]$ in $U_{2n+1}$, so its displayed root exists and lies in $U_1$. Collection of <group commutators> shows that successive bracket approximants differ in layers tending to the identity, giving the other limit. The <group commutator> identities give additivity of the limiting bracket, and the <Hall-Witt identity> gives its <Jacobi identity>. Approximate <commutativity> makes limiting addition <commutative>. The resulting lattice $L_G$ is a <free module> over $\mathbb Z_p$ of rank $d(G)$, and $[L_G,L_G]\le pL_G$.

A <powerful Lie algebra over p-adic integers>, in the convention relevant here, is a <Lie algebra> $L$ whose underlying <module> is finite free over $\mathbb Z_p$ and whose bracket satisfies $[L,L]\le pL$. For $p=2$ the condition is instead $[L,L]\le4L$. For odd $p$, define multiplication on its underlying set by the convergent <Baker--Campbell--Hausdorff formula>
$$
x*y=\operatorname{BCH}(x,y)=x+y+\frac12[x,y]+\frac1{12}\bigl([x,[x,y]]+[y,[y,x]]\bigr)+\cdots.
$$
An iterated bracket of degree $m$ lies in $p^{m-1}L$. The BCH coefficient bound loses at most $\lfloor(m-1)/(p-1)\rfloor$ powers of $p$, so all higher-degree terms are integral, and their valuations tend to infinity. This explains both convergence and why multiplying a lattice with small bracket stays inside the lattice. Formal <associativity> of BCH passes to the convergent series, the identity is $0$, the inverse is $-x$, and every <group> power satisfies $x^{*m}=mx$. The quotients by $p^aL$ are <finite p-groups>. Hence the resulting <compact group> is a finitely generated <torsion-free group> and a <pro-p group>, and its <group commutator> lies in $pL$. Thus \b[$(L,*)$ is a <uniform pro-p group>], with $P_i(L,*)=p^{i-1}L$ and successive index $p^{\operatorname{rank}_{\mathbb Z_p}L}$.

The standard uniform-group/Lie-lattice correspondence identifies these constructions as mutually inverse: \b[$L_{(L,*)}\cong L$ and $(L_G,*)\cong G$]. To see why the <inverse limits> recover the lattice operations, the addition approximant for a BCH <group> is $p^{-n}\operatorname{BCH}(p^nx,p^ny)$: its linear term is $x+y$ and every higher term tends to zero. Similarly its <group commutator> approximant has limiting term $[x,y]$. In the other direction, a local <logarithm> in the complete normed <group algebra> identifies the intrinsic operations with algebra addition and <commutator> and identifies <group> multiplication with BCH; the uniform power maps extend the identification from a sufficiently small power <subgroup> to all of $G$. Continuous <group homomorphisms> respect powers, unique roots and limits, while <Lie algebra homomorphisms> respect every BCH term, so the equivalence also preserves morphisms.