[proofplan]
We construct the Witt expansion $a = \sum_{n=0}^\infty [a_n] p^n$ by a successive-approximation procedure: at each stage, we subtract the Teichmüller lift of the residue class, divide by $p$, and repeat. The $p$-torsion-freeness of $A$ ensures that the division by $p$ is well-defined. The $p$-adic completeness ensures convergence. Uniqueness follows from injectivity of the reduction map and the structure of the Teichmüller lift.
[/proofplan]
[step:Construct the coefficients $a_n$ by successive approximation]
Let $a \in A$. We construct a sequence $(a_n)_{n \geq 0}$ in $A/pA$ and a sequence $(r_n)_{n \geq 0}$ in $A$ such that
\begin{align*}
a = \sum_{k=0}^{n} [a_k] p^k + p^{n+1} r_n \quad \text{for all } n \geq 0.
\end{align*}
**Base case ($n = 0$).** Let $a_0 \in A/pA$ be the image of $a$ under the reduction map $A \to A/pA$. Then $[a_0] \equiv a \pmod{p}$ (by the lifting property of the [Teichmüller Map](/theorems/???)), so $a - [a_0] \in pA$. Since $A$ is $p$-torsion free, the element $r_0 := p^{-1}(a - [a_0])$ is the unique element of $A$ with $p \cdot r_0 = a - [a_0]$. Thus $a = [a_0] + p r_0$.
**Inductive step.** Given $r_n \in A$, define $a_{n+1} \in A/pA$ as the reduction of $r_n$ modulo $p$, and set $r_{n+1} = p^{-1}(r_n - [a_{n+1}])$. Then $r_n = [a_{n+1}] + p r_{n+1}$, so
\begin{align*}
a = \sum_{k=0}^{n} [a_k] p^k + p^{n+1} r_n = \sum_{k=0}^{n} [a_k] p^k + p^{n+1}([a_{n+1}] + p r_{n+1}) = \sum_{k=0}^{n+1} [a_k] p^k + p^{n+2} r_{n+1}.
\end{align*}
[guided]
The construction is analogous to reading off the digits of a $p$-adic number. We repeatedly:
1. Read off the leading coefficient: reduce $r_n$ modulo $p$ to get $a_{n+1} \in A/pA$.
2. Subtract and divide: form $r_{n+1} = (r_n - [a_{n+1}])/p$.
The division by $p$ is well-defined because $r_n - [a_{n+1}] \in pA$ (since both $r_n$ and $[a_{n+1}]$ reduce to $a_{n+1}$ modulo $p$), and $A$ is $p$-torsion free (so $p \cdot x = p \cdot y$ implies $x = y$, making $p^{-1}$ well-defined on $pA$).
The $p$-torsion-freeness hypothesis is essential here. Without it, $pA$ might have a nontrivial kernel and division by $p$ would be ambiguous.
[/guided]
[/step]
[step:Verify convergence of the series $\sum_{n=0}^\infty [a_n] p^n$ to $a$]
From the construction, $a - \sum_{k=0}^{n} [a_k] p^k = p^{n+1} r_n$ for all $n \geq 0$. Since $r_n \in A$ and the $p$-adic absolute value of $p^{n+1} r_n$ satisfies $|p^{n+1} r_n| \leq |p|^{n+1} \to 0$ (as $|p| < 1$ in any strict $p$-ring), the partial sums converge $p$-adically to $a$. By $p$-adic completeness of $A$, the series $\sum_{n=0}^\infty [a_n] p^n$ converges and its sum equals $a$.
[/step]
[step:Prove uniqueness of the representation]
Suppose $a = \sum_{n=0}^\infty [a_n] p^n = \sum_{n=0}^\infty [b_n] p^n$ with $a_n, b_n \in A/pA$. Reducing modulo $p$: $[a_0] \equiv a \equiv [b_0] \pmod{p}$. By the lifting property, $[a_0] \equiv a_0 \pmod{p}$ and $[b_0] \equiv b_0 \pmod{p}$, so $a_0 = b_0$ in $A/pA$.
Subtracting $[a_0] = [b_0]$ from both sides gives $\sum_{n=1}^\infty [a_n] p^n = \sum_{n=1}^\infty [b_n] p^n$, i.e., $p \sum_{n=0}^\infty [a_{n+1}] p^n = p \sum_{n=0}^\infty [b_{n+1}] p^n$. Since $A$ is $p$-torsion free, we may cancel $p$ to get $\sum_{n=0}^\infty [a_{n+1}] p^n = \sum_{n=0}^\infty [b_{n+1}] p^n$. By induction on the leading coefficient, $a_{n+1} = b_{n+1}$ for all $n \geq 0$, giving $a_n = b_n$ for all $n$.
[guided]
The uniqueness argument works by "reading off" coefficients one at a time, starting from the constant term. The logic is:
1. Reduce both expansions modulo $p$. The Teichmüller lifting property gives $[a_0] \equiv a_0 \pmod{p}$, and similarly for $[b_0]$. So $a_0 = b_0$ in $A/pA$.
2. Cancel the leading term and divide by $p$. This is valid because $A$ is $p$-torsion free: if $p \cdot x = p \cdot y$ then $x = y$.
3. Repeat by induction. Each step peels off one coefficient and confirms it is uniquely determined.
This is exactly the same logic by which the digits of a $p$-adic integer are unique: the $n$-th digit is determined by reducing the $n$-th remainder modulo $p$.
[/guided]
[/step]