**RJW thm:log der (TeX 3280–3285) — the Coleman–Coates–Wiles short exact sequence.**
Surjectivity half: every `ψ`-fixed series is the logarithmic derivative of a `𝒩`-fixed
unit. (The kernel half is `rem:ker Δ`: `μ_{p−1}`.)

Proof (T1203c, CLOSED via the `ξ`-free route). RJW reduce surjectivity (`lem:log der red
mod p`, TeX 3315–3332) to the mod-`p` identity `A = B` (`A = Δ(𝒲) mod p`, `B = (ψ=id) mod p`):
* `A ⊆ B` mod `p` is `dlog_mem_psiIdSeries` reduced mod `p` (used inside the step lemma).
* `B ⊆ A` mod `p` (`lem:B mod p`) is `exists_normOp_dlog_modEq`: `lem:B mod p 2`
  (`fp_series_eq_dlog_add_frobC`) writes `f̄ = Δā + b̄`; lift `ā` to `g ∈ 𝒲` (`lem:A mod p`);
  the residual `(T+1)/T·C`-part `b̄` is killed by `psiId_one_add_X_div_X_phi_eq_zero`. The
  `ψ`-fixedness of `(T+1)/T` (RJW's `Eqphipsi`-based `LemmaPsiInvariant`, TeX 1521) is
  replaced by the **`ξ`-free series projection formula** `ψ(φd·F) = d·ψF`
  (`psiSeries_phiSeries_mul_zmod`) together with honest `ψ` over `𝔽_p⟦T⟧`
  (`existsUnique_digits_zmod`, via the `θ = (1+T)∂` eigenvalue argument) and `ψ(T^{p−1}) = 1`.
* The reduction (here) iterates the step (`exists_approx_seq`) to `g_i ∈ 𝒲`, `f_i ∈ (ψ=id)`
  with `Δ(g_i) − f_{i−1} = p f_i`, forms `h_n = ∏_{k=1}^n g_k^{(−1)^{k−1} p^{k−1}}`
  (`approxProd`), so `Δ h_n = f_0 − (−p)^n f_n` (`dlog_approxProd`), and takes a convergent
  subsequence in the compact `ℤ_p⟦T⟧^×` (`exists_subseq_tendsto`) with limit `h ∈ 𝒲`. The
  `Δ`-limit is passed through the **cleared** form `(1+T)·∂h = f_0·h` (avoiding
  inverse-continuity): `(1+T)·∂(h_{φj})` converges both to `(1+T)·∂h` (continuity of `∂`)
  and to `f_0·h` (the `(−p)^{φj}f_{φj}` term `→ 0`), so by limit uniqueness they agree. 

**RJW lem:log der 1 (TeX 3292–3306)**: `Δ(𝒲) ⊆ ℤ_p⟦T⟧^{ψ=id}`, where
`𝒲 = (ℤ_p⟦T⟧^×)^{𝒩=id}`.

RJW's proof differentiates the `μ_p`-product `φ(f) = ∏_η f((1+T)η−1)` (replan R10.4: *not*
a formal power-series identity) and deduces `ψ(Δf) = Δf` by `φ`-injectivity. We give the
formal substitute via the **determinant/Jacobi route**. Write `M = digitMatrix f`,
`N = digitMatrix(f⁻¹) = M⁻¹`; the hypothesis `𝒩f = f` reads `f = det M`. Then
`digitMatrix(dlog f) = digitMatrix(Δf)·N`, and by identity K (`digitMatrix_del`),
`digitMatrix(Δf) = D + p·ΔM` with `D_{ij} = (i−j)•M_{ij}` and `ΔM` the entrywise `Δ`. Hence
`trace(digitMatrix(dlog f)) = trace(D·N) + p·trace(ΔM·N)`. The first trace vanishes
(`trace_D_N_zero`, from `MN = NM = 1`), and `Δf = f·trace(ΔM·N)` (Jacobi, `del_det_eq_smul_trace`
with `adjugate M = f•N`) gives `trace(ΔM·N) = f⁻¹·Δf = dlog f`. So
`p·ψ(dlog f) = trace(digitMatrix(dlog f)) = p·dlog f` (`trace_digitMatrix`), and cancelling `p`
(`mul_p_cancel`) yields `ψ(dlog f) = dlog f`. The diagonal `(digitMatrix(Δf))_{ii} = p·Δ(M_{ii})`
of identity K is exactly the formal shadow of RJW's chain-rule step
`Δ(f((1+T)η−1)) = (Δf)((1+T)η−1)`. 

The kernel of `Δ = ∂log` on `𝒩`-fixed units is `μ_{p−1}` (RJW rem:ker Δ, TeX
3176–3178): a constant `𝒩`-fixed unit `f` satisfies `f^p = f`. Stated as: `dlog g = 0`
and `𝒩 g = g` ⟹ `g` is a `(p−1)`-th root of unity (constant). 

**RJW lem:log der 1 (TeX 3292–3306)**: `Δ(𝒲) ⊆ ℤ_p⟦T⟧^{ψ=id}`, where
`𝒲 = (ℤ_p⟦T⟧^×)^{𝒩=id}`.

RJW's proof differentiates the `μ_p`-product `φ(f) = ∏_η f((1+T)η−1)` (replan R10.4: *not*
a formal power-series identity) and deduces `ψ(Δf) = Δf` by `φ`-injectivity. We give the
formal substitute via the **determinant/Jacobi route**. Write `M = digitMatrix f`,
`N = digitMatrix(f⁻¹) = M⁻¹`; the hypothesis `𝒩f = f` reads `f = det M`. Then
`digitMatrix(dlog f) = digitMatrix(Δf)·N`, and by identity K (`digitMatrix_del`),
`digitMatrix(Δf) = D + p·ΔM` with `D_{ij} = (i−j)•M_{ij}` and `ΔM` the entrywise `Δ`. Hence
`trace(digitMatrix(dlog f)) = trace(D·N) + p·trace(ΔM·N)`. The first trace vanishes
(`trace_D_N_zero`, from `MN = NM = 1`), and `Δf = f·trace(ΔM·N)` (Jacobi, `del_det_eq_smul_trace`
with `adjugate M = f•N`) gives `trace(ΔM·N) = f⁻¹·Δf = dlog f`. So
`p·ψ(dlog f) = trace(digitMatrix(dlog f)) = p·dlog f` (`trace_digitMatrix`), and cancelling `p`
(`mul_p_cancel`) yields `ψ(dlog f) = dlog f`. The diagonal `(digitMatrix(Δf))_{ii} = p·Δ(M_{ii})`
of identity K is exactly the formal shadow of RJW's chain-rule step
`Δ(f((1+T)η−1)) = (Δf)((1+T)η−1)`. 

**RJW lem:A mod p (TeX 3337–3343)**: `𝒲 mod p = 𝔽_p⟦T⟧^×` — every unit power
series over `𝔽_p` lifts to a `𝒩`-fixed unit (via `𝒩^k`-convergence, the mod-`p^k`
continuity of `normOp`). Stated as the lift existence. 

**RJW lem:B mod p 2 (TeX 3359–3373) — "the most delicate and technical part"**: the
`𝔽_p⟦T⟧` decomposition `𝔽_p⟦T⟧ = Δ(𝔽_p⟦T⟧^×) + (T+1)/T·C` with
`C = {∑_{n≥1} a_n T^{pn}}`.

Statement note (T1203b, faithful form — statement-fix authorised). The skeleton's
existential was a placeholder (`∃ a c, IsUnit a ∧ c ∈ range φ`, vacuously true). The
faithful claim, with `Δ a = (1+T)·a′·a⁻¹` the `𝔽_p` log-derivative and the `(T+1)/T·c`
factor cleared of its `1/T` pole (`T·b = (T+1)·c`, i.e. `X·b = (1+X)·c`), is: every
`g : 𝔽_p⟦T⟧` is `Δ a + b` for a unit `a` and a `b` with `X·b = (1+X)·c`, `c ∈ φ(𝔽_p⟦T⟧)`
(so `c = ∑ a_n T^{pn} ∈ C`, using `φ(T^m) = T^{pm}` over `𝔽_p`, `phiSeries_eq_pow_zmod`).
This is the precise form `lem:B mod p` consumes: it kills the `b`-part using `ψ b = b`.

Proof note (T1203b, CLOSED). RJW's route (TeX 3366–3373) builds `α_i` so that the unit
`a = ∏(1−α_n T^n)` (a T-adic infinite product, needing `multipliable` + `Δ`-continuity)
has `Δ a = (T+1)/T·h`. We take a topology-free coefficient recursion (the same pattern as
`solCoeff`), building `a` and `w := T·a′·a⁻¹` *directly* by their coefficients rather than
as a product. Write `u = 1+T` (a unit over `𝔽_p`), `H := T·g·u⁻¹`. The map `a ↦ T·a′·a⁻¹`
sends a unit `a` with `a(0)=1` to a series `w` with `w(0)=0` whose `n`-th coefficient
satisfies `n·a_n = w_n + ∑_{j=1}^{n−1} a_{n−j}·w_j` (clear `T·a′ = a·w`). For `(n,p)=1`
the leading `n·a_n` is invertible so `a_n` is determined by a chosen `w_n`; for `p∣n` the
LHS vanishes (`n=0` in `𝔽_p`), forcing `w_n` and freeing `a_n`. So we jointly recurse
(`AWfp`): set `w_n := H_n`, `a_n := n⁻¹(H_n + S_n)` when `(n,p)=1`; `a_n := 0`,
`w_n := −S_n` when `p∣n` (`S_n` the partial sum). Then `T·a′ = a·w` (`X_deriv_eq_aw`),
`a` is a unit (`a(0)=1`), `w = T·a′·a⁻¹`, and `w` agrees with `H` off multiples of `p`, so
`c := H − w` is supported on `pℕ`, hence a `p`-th power `= φ(d)` (over `𝔽_p`,
`range φ = {p-th powers}`; `mem_range_phiSeries_of_dvd`). Finally `b := g − Δa` gives
`X·b = u·c` by `X·Δa = u·w` and `u·H = T·g`, and `g = Δa + b` trivially. No infinite
product, no `Δ`-continuity. 

**RJW thm:fund exact seq (TeX 3411–3418), left-exactness**: the kernel of `Col` on
`𝒰_{∞,1}` is `ℤ_p(1)`.

The composite `Col = (x⁻¹·) ∘ Res_{ℤ_p^×} ∘ 𝒜⁻¹ ∘ ∂log ∘ colemanSeries` is pulled back:
`Col_eq_zero_iff` reduces `Col u = 0` to `(1−φ)(∂log f_u) = 0` (through `unitsCmul invCM` and
`ι` injective, `mahlerTransform_psi`); `phiHom_fixed_eq_C` then gives `∂log f_u = C c`; the
`∂log = C c` ODE (`eq_C_mul_binomialSeries_of_dlog_eq_C`) writes `f_u = C(g₀)·binomialSeries
c`; `𝒩`-fixedness (`normOp_binomialSeries`, `normOp_mul`, `normOp_C`) forces `g₀^p = g₀`, and
`g₀` is a principal unit (the interpolation `f_u(π_n) = u_n ∈ 𝒰_{∞,1}` against
`binomialSeries c(π_n) = ξ_n^c`), so `g₀ = 1` (`oneUnit_pow_p_sub_one_eq_one`); hence
`f_u = binomialSeries c` and `u_n = ξ_n^c`. Conversely `u ∈ ZpOne` gives
`f_u = binomialSeries a` (`colemanSeries_eq_binomialSeries_of_mem_ZpOne`), `∂log = C a`,
`(1−φ)(C a) = 0`.

Carries `hp2 : p ≠ 2` (errata #14): the forward direction uses `normOp_binomialSeries`, hence
the cyclotomic norm `levelNorm_zpPow_zetaSys`, which is false at `p = 2`. RJW §12 fixes `p`
odd throughout (TeX 2470); the §12.5 milestone `iwasawa_theorem` already carries `hp2`. 

**RJW thm:fund exact seq, right-exactness / cokernel**: the image of `Col` on
`𝒰_{∞,1}` is the kernel of the `χ`-moment `μ ↦ ∫_𝒢 χ·μ = μ(x)` (cokernel `ℤ_p(1)`).

The forward inclusion `image(Col) ⊆ ker(χ-moment)` is `Col_apply_unitsPowCM_one_eq_zero`:
`Col u (unitsPowCM 1) = constantCoeff((1−φψ)(∂log f_u)) = 0`, since `φ` and `ψ` both fix the
constant coefficient (`∂log f_u ∈ ψ=id`).

The converse `ker ⊆ image` is assembled from three pieces. (1) The **inverse Coleman map**
`invColeman` (above) realises any `𝒩`-fixed unit `g` as `colemanSeries (invColeman g)`
(`colemanSeries_invColeman`), with `compat` from `evalPi_normOp`. (2) `exists_invColeman_Col_eq`
solves `Col (invColeman g) = μ` for such a `g` by inverting the measure transport off the
diagram `ℤ_p⟦T⟧^{ψ=id} →[1−φ] ℤ_p⟦T⟧^{ψ=0} → ℤ_p` (`exists_one_sub_phi_eq` +
`dlog_surjective_onto_psiId`, `mahlerTransform_psi`/`_res_units`, `iota_comp_extendByZero`),
the `μ(unitsPowCM 1)=0` condition feeding the `F(0)=0` hypothesis. (3) The resulting
`u₀ = invColeman g` need not be *principal*; instead of the deferred `𝒪_n`-residue split, we
divide off the **constant `ℤ_[p]`-Teichmüller system** `v = teichNCU a` for `a = constantCoeff
g` (a unit since `g` is): `Col v = 0` (`Col_eq_zero_of_torsion` + `teichNCU_torsion`), so by
`Col_add` `Col (u₀·v⁻¹) = Col u₀ = μ`, and `w := u₀·v⁻¹` is principal because
`g(π_n) ≡ a mod 𝔭_n` (`norm_evalPi_sub_constantCoeff_lt_one`) and `a·ω(a)⁻¹ ≡ 1 mod p`
(`teichmullerFun_sub_self_mem`), so `w.elems n ≡ 1 mod 𝔭_n`.

This `←` direction is now genuinely sorry-free: it no longer uses the deferred
`normCompat_eq_teichmuller_mul_principal` (only the already-formalised `ℤ_[p]` Teichmüller of
`Interpolation/Branches.lean`). No `p`-odd hypothesis enters the converse.