`c_n(a)` has norm `1` (RJW TeX 2573): numerator and denominator are conjugate
uniformisers of equal norm (`norm_zetaSys_pow_sub_one_eq`). 

**Norm compatibility of the cyclotomic units** (RJW TeX 2581–2585):
`N_{n+1,n}(c_{n+1}(a)) = c_n(a)` for `n ≥ 1`. Apply the norm collapse
`levelNorm_zetaSys_pow_sub_one` to the numerator (`b = a`) and to the denominator
(`b = 1`, i.e. `levelNorm_pi`), then take the quotient. 

**RJW prop:coleman zetap (TeX 2595–2608)**, cleared form: the logarithmic
derivative of `f_{c(a)} = geomSum a` is `(a−1) − F_a`, i.e.
`(1+T)·(geomSum a)′ = ((a−1) − F_a)·geomSum a`.

Proof (the §8 T704 template): differentiate `geomSum a · T = (1+T)^a − 1` to get
`(geomSum a)′·T + geomSum a = ∂((1+T)^a)`; multiply by `(1+T)` and use
`(1+T)·∂((1+T)^a) = a·(1+T)^a`; the target multiplied by `T` reduces, via
`((1+T)^a−1)·F_a = geomSum a − a` and `geomSum a · T = (1+T)^a − 1`, to the same
expression. Cancel the regular element `T`. 

**RJW prop:coleman zetap (TeX 2589–2592)**: the Coleman power series of the
cyclotomic-unit tower `c(a)` is `f_{c(a)} = geomSum a = ((1+T)^a − 1)/T`. (The source
notes it "is even a polynomial".)

Proof via the uniqueness of the Coleman series (`coleman_existsUnique`): `geomSum a`
satisfies all three defining clauses of `colemanSeries (cyclo a)`:
* `IsUnit (geomSum a)` (`isUnit_geomSum`, `a` coprime to `p`);
* `𝒩`-invariance `normOp (geomSum a) = geomSum a`: both sides interpolate the
  norm-compatible tower `c(a)` (`evalPi_normOp` rewrites `(𝒩 geomSum)(π_n)` as
  `N_{n+1,n}(geomSum(π_{n+1})) = N_{n+1,n}(c_{n+1}(a)) = c_n(a) = geomSum(π_n)` via
  `evalPi_geomSum` + `levelNorm_cycloUnit`), so `evalPi_injective` gives equality;
* interpolation `(geomSum a)(π_n) = c_n(a) = (cyclo a).elems n` for `n ≥ 1`
  (`evalPi_geomSum`; `(cyclo a).elems n = cycloUnit p a n` at `n ≥ 1`). 

`∂log (geomSum a) = (a−1) − F_a` (RJW prop:coleman zetap, TeX 2595–2608): the
cleared identity `(1+T)·(geomSum a)′ = ((a−1)−F_a)·geomSum a`
(`one_add_mul_derivative_log_geomSum`) becomes, on multiplying by `geomSum a⁻¹`
(`Ring.mul_inverse_cancel`, `geomSum a` a unit), `∂log (geomSum a) = (a−1) − F_a`. 

**RJW lem:relate cyclo to mua (TeX 2611–2624)**, series/measure-level form:
`Res_{ℤ_p^×}(μ_{(a−1)−F_a}) = −Res_{ℤ_p^×}(μ_a)`, where `μ_{(a−1)−F_a}` is the
measure with Mahler transform `(a−1) − F_a`. Linearity of `𝓐⁻¹` and of `Res`
splits off the constant part `a−1`, whose residue vanishes (`res_units_symm_C`);
the remaining `−𝓐⁻¹(F_a) = −μ_a`.