Power congruences in a uniform pro-p group (source code)

= Power congruences in a uniform pro-p group
{title2=$x^{p^a}\equiv y^{p^a}\pmod{G^{p^{a+b}}}$}

For a <uniform pro-p group> with $U_i=G^{p^i}$, the map $x\mapsto x^{p^a}$ transports congruences by
$$
x\equiv y\pmod{U_b}\quad\Longleftrightarrow\quad x^{p^a}\equiv y^{p^a}\pmod{U_{a+b}}.
$$
<Commutator> collection gives $(yu)^p\equiv y^pu^p\pmod{U_{b+2}}$ for $u\in U_b$, and the power map is an <isomorphism> $U_b/U_{b+1}\to U_{b+1}/U_{b+2}$. Thus a nontrivial first difference moves down exactly one layer when taking a $p$th power. Iterating gives the equivalence; completeness supplies unique roots when the congruence is read in reverse.