**Single-level interpolation** (RJW TeX 2538–2547, T904b): every norm-one
`u ∈ 𝒪_n` is the value `f(π_n)` of a unit power series `f ∈ ℤ_p⟦T⟧^×`.

Proof (the source's greedy `π_n`-adic digits): define the remainder/digit recursion
`r_0 = u`, `a_k = ` the `ℤ_p`-residue of `r_k` (`exists_residue_pi`), `r_{k+1} =
(r_k − a_k)/π_n ∈ 𝒪_n` (`quot_mem_O`); set `f = Σ_k a_k T^k`. The telescoping identity
`u − Σ_{j<m} a_j π_n^j = π_n^m · r_m` with `‖r_m‖ ≤ 1` gives `‖u − S_m‖ ≤ ‖π_n‖^m → 0`,
so the partial sums `S_m` converge to `u`; they also converge to `f(π_n) = evalPi f n`
(partial sums of the defining `tsum`), so `evalPi f n = u` by uniqueness of limits. As
`‖u‖ = 1 > ‖π_n‖ ≥ ‖u − a_0‖`, the ultrametric isoceles step gives `‖a_0‖ = ‖u‖ = 1`,
so `a_0 = constantCoeff f` is a `ℤ_p`-unit and `f ∈ ℤ_p⟦T⟧^×`. 

**Coleman's theorem** (RJW `thm:coleman power series`, TeX 2553–2560; `thm:coleman map 2`,
TeX 2796–2807): for every norm-compatible system of units `u = (u_n)_n ∈ 𝒰_∞`, there is a
*unique* unit power series `f ∈ ℤ_p⟦T⟧^×` that is `𝒩`-invariant (`𝒩 f = f`) and interpolates
`u` (`f(π_n) = u_n` for all `n ≥ 1`).

**Uniqueness** is the Weierstrass `evalPi_injective` (T905, RJW lem:unique-coleman): two such
`f, g` agree at every `π_n`, `n ≥ 1`, hence are equal (the `IsUnit`/`𝒩`-invariance clauses are
not needed for uniqueness).

**Existence** is the diagonal/compactness argument (TeX 2763–2791):
* (a) per-level interpolants `F_m` (`exists_evalPi_eq`, `‖u_m‖ = 1` from `norm_elems_eq_one`);
* (b) the norm-iterate evaluation `𝒩^{[k]} F_{n+k}(π_n) = u_n` (induction on `k`, via
  `evalPi_normOp` (T907) and `u.compat`);
* (c) the diagonal `g_m := 𝒩^{[m]} F_{2m}` and a coefficientwise-convergent subsequence
  `g_{φ j} → f_u` (`exists_subseq_tendsto`, T909/compactness);
* (d) `f_u(π_n) = u_n`: the value `g_{φ j}(π_n)` tends to `f_u(π_n)`
  (`tendsto_evalPi_of_tendsto`) *and* to `u_n` (the congruence `u_n ≡ g_m(π_n) mod p^{m+1}`
  from `normOp_iterate_modEq` (T908 iv) + `norm_evalPi_sub_le_of_modEqPow`, squeezed as
  `φ j → ∞`), so the two limits agree;
* (e) `IsUnit f_u`: each `g_m` is a unit (`normOp_iterate_isUnit`) and the units are closed
  (`isClosed_isUnit`, `IsClosed.mem_of_tendsto`);
* (f) `𝒩 f_u = f_u`: `𝒩 f_u` also interpolates `u` (`evalPi_normOp` + `u.compat`), so
  `evalPi_injective` forces `𝒩 f_u = f_u`. 

**Multiplicativity of the Coleman map** (RJW `thm:coleman map 2`, TeX 2796–2807): the map
`u ↦ colemanSeries u` is a homomorphism, `colemanSeries (u·v) = colemanSeries u · colemanSeries v`.
The product `colemanSeries u · colemanSeries v` satisfies all three defining clauses of
`coleman_existsUnique (u·v)` (`IsUnit.mul`, `normOp_mul`, `evalPi_mul` against
`(u·v).elems n = u_n·v_n`), so it equals `colemanSeries (u·v)` by uniqueness. 

**Injectivity of the Coleman map** (RJW `thm:coleman map 2`, TeX 2796–2807, the "injective
homomorphism" claim), in the honest form pinned to the `n ≥ 1` interpolation data:
`colemanSeries u = colemanSeries v ↔ ∀ n ≥ 1, u_n = v_n`.

Forward: equal series have equal values `u_n = colemanSeries(·)(π_n) = v_n` for `n ≥ 1`
(`evalPi_colemanSeries`), and `Units.ext`. Backward: if `u_n = v_n` for all `n ≥ 1`, then
`colemanSeries v` interpolates `u` as well, so `coleman_existsUnique u`'s uniqueness gives
`colemanSeries u = colemanSeries v`.

Note (T910): the `n ≥ 1` restriction is *forced*, not a weakening — the level-0 unit `elems 0`
is unconstrained by the tower (`compat` starts at `n = 1`, the `K_0 = ℚ_p` design of T903), so
`colemanSeries` cannot see it; full `elems`-injectivity would be false. The source's
`𝒰_∞ = lim_{n≥1}` has no level-0 component, matching this iff.