Integral lifting of the corrected cyclotomic logarithm (source code)

= Integral lifting of the corrected cyclotomic logarithm
{title2=$g'(0)=0\iff g=\frac1p\log(f^p/\phi(f))$}

Let $R=\mathbb Z_p[[T]]$, $p$ odd, and $\phi(T)=(1+T)^p-1$. An element $g\in R$ is the <Frobenius-corrected logarithm> of a <unit> $f$ with $f(0)\in1+p\mathbb Z_p$ if and only if $g'(0)=0$. Necessity follows by differentiating at zero, using $\phi'(0)=p$. For sufficiency put $H=\exp(pg)\in1+pR$ and solve $f^p=H\phi(f)$. Choose $f_0=\exp(pg_0/(p-1))$. The linear equation reduces to $H_1=0$, so $f_1$ is free. In degree $n\geq2$ the unknown $f_n$ has coefficient $p f_0^{p-1}(1-p^{n-1})$. The remaining terms are divisible by $p$ because reduction of any integral truncated $f$ satisfies $f^p\equiv\phi(f)\pmod p$. Division gives a unique integral $f_n$. Two lifts differ by $(1+T)^c$, $c\in\mathbb Z_p$, as follows from the logarithmic equation in the coordinate $z=\log(1+T)$. If also $Sg=0$, the <Coleman trace operator> gives $\log(Nf/f)=pSg=0$. As $Nf/f\in1+pR$, injectivity of the <p-adic logarithm> implies $Nf=f$.