Dwork's lemma: existence of prescribed ghost components

Let $R$ be a commutative ring, let $p$ be a natural number which is prime (as a Fact instance), and let $\sigma \colon R \to R$ be a ring homomorphism which lifts Frobenius in the sense that $\sigma(a) - a^{p}$ lies in the ideal generated by $p$ in $R$ for every $a \in R$. Let $n$ be a natural number and let $g \colon \mathbb{N} \to R$ be any sequence satisfying the congruences $g(k+1) - \sigma(g(k)) \in (p^{k+1})$ for every $k$ with $k + 1 < n$ (so only the finitely many congruences with indices below $n$ are required, and the values $g(k)$ for $k \ge n$ are unconstrained). Then there exists a Witt vector $x \in W(R)$ (the $p$-typical Witt vectors, WittVector p R) whose ghost components agree with $g$ below $n$: $\mathrm{ghostComponent}_k(x) = g(k)$ for all $k < n$, where $\mathrm{ghostComponent}_k(x) = \sum_{i=0}^{k} p^{i} x_i^{p^{k-i}}$. No hypothesis on $p$-torsion in $R$ is imposed; the assertion is existence only, at the finite level $n$.

This is the existence half of Dwork's lemma, characterising which sequences in $R$ arise as the ghost (Witt) components of a Witt vector over a ring carrying a Frobenius lift. It is used in the Čerednik–Drinfel'd part of the development, for instance in constructing Cartier-style digit expansions and in the analysis of formal $\mathcal{O}_D$-modules with prescribed Frobenius behaviour.