The planar trace atom traceZk (meromorphic-trace, cluster 2)

Unit: meromorphic-trace (docs/design/meromorphic-trace.md §2 D6, §4.4, §5 P4-P6). Purely planar (mathlib + MappingDegree.RootCounting + LocalMultiplicity.KthRoot + ResidueCalculus); no manifold content, independent of ToP1/OrderMultiplicity/ArgumentPrinciple.

• traceZk h k w := ∑ᶠ z ∈ {z | z ^ k = w}, h z — the trace of h over the (generically k-element) root set of z ↦ z ^ k at w. Junk traceZk h k 0 = h 0 (root set is {0}).
• Basic API: traceZk_eq_finset_sum (the master Finset conversion, any w), linearity (traceZk_add, guarded by k ≠ 0 — see the deviation note below, traceZk_const_mul, unconditional), traceZk_comp_pow.
• analyticAt_traceZk (P4): traceZk h k is analytic at any w₀ ≠ 0 at which all k-th roots of w₀ lie in h's domain of analyticity, via local root branches (AnalyticAt.exists_pow_eq) and a primitive k-th root of unity — no monodromy.
• meromorphicAt_traceZk (P5): traceZk h k is meromorphic at 0 when h is, via a growth bound on the root-sum and Riemann's removable singularity theorem — no convergent Laurent series needed for existence.
• traceZk_zpow: closed form for monomial traces, traceZk (·^e) k w = k * w^(e/k) if k ∣ e, 0 otherwise (w ≠ 0) — the geometric-sum collapse of k-th roots of unity, computed on the abstract root set (one root + a primitive root of unity), purely algebraically.
• laurentCoeffAt_traceZk (P6): the Laurent-coefficient formula laurentCoeffAt (traceZk h k) 0 m = k * laurentCoeffAt h 0 (k * m), tsum-free: exact finite Taylor remainder of the order presentation's unit factor (cutoff chosen so the remainder exponent is an exact multiple of k, making the remainder trace factor as w ^ s' * traceZk r k w with NO second growth bound), traceZk_zpow on the finitely many monomials, and residue-calculus's presentation-independent laurentCoeffAt characterization.

noncomputable def RS.MTrace.traceZk (h : ℂ → ℂ) (k : ℕ) (w : ℂ) : ℂ

The trace of h along z ↦ z ^ k at w: the sum of h over the (generically k-element) root set. Junk-free by convention: at w = 0 the root set is the singleton {0} (for k ≠ 0), giving h 0; at w with k = 0 the support is either empty or all of ℂ, and finsum junks to 0 in the latter case unless h itself has finite support there.

Equations

• RS.MTrace.traceZk h k w = ∑ᶠ (z : ℂ) (_ : z ∈ {z : ℂ | z ^ k = w}), h z

theorem RS.MTrace.traceZk_def (h : ℂ → ℂ) (k : ℕ) (w : ℂ) : traceZk h k w = ∑ᶠ (z : ℂ) (_ : z ∈ {z : ℂ | z ^ k = w}), h z

theorem RS.MTrace.traceZk_eq_finset_sum {k : ℕ} (h : ℂ → ℂ) (hk : k ≠ 0) (w : ℂ) : traceZk h k w = ∑ z ∈ ⋯.toFinset, h z

Master conversion to a Finset sum, valid for every w (the root set is always finite once k ≠ 0, regardless of w).

theorem RS.MTrace.traceZk_apply_of_ne_zero {h : ℂ → ℂ} {k : ℕ} {w : ℂ} (hk : k ≠ 0) (_hw : w ≠ 0) : traceZk h k w = ∑ z ∈ ⋯.toFinset, h z

theorem RS.MTrace.traceZk_zero_apply {h : ℂ → ℂ} {k : ℕ} (hk : k ≠ 0) : traceZk h k 0 = h 0

Honest but junk value at the branch point: traceZk h k 0 = h 0 (the root set of z ^ k = 0 is the singleton {0}). Never used to reason about MeromorphicAt/laurentCoeffAt/resAt at 0, all of which are 𝓝[≠]0-germ notions and hence blind to this junk (see the design's junk ledger, §6).

Linearity

theorem RS.MTrace.traceZk_add {h g : ℂ → ℂ} {k : ℕ} (hk : k ≠ 0) : traceZk (h + g) k = traceZk h k + traceZk g k

Additivity, guarded by k ≠ 0 (deviation from the design's unconditional statement: at k = 0, w = 1 the root set is all of ℂ, and additivity fails there whenever one summand has finite support on ℂ and the other does not — e.g. h₁ = Set.indicator {0} 1, h₂ = 1. With k ≠ 0 the root set is always finite, so this is not an issue.).

theorem RS.MTrace.traceZk_fun_add {h g : ℂ → ℂ} {k : ℕ} (hk : k ≠ 0) : traceZk (fun (z : ℂ) => h z + g z) k = fun (w : ℂ) => traceZk h k w + traceZk g k w

theorem RS.MTrace.traceZk_const_mul {h : ℂ → ℂ} (c : ℂ) (k : ℕ) : traceZk (fun (z : ℂ) => c * h z) k = fun (w : ℂ) => c * traceZk h k w

Unconditional in k (scalar multiplication by c does not change support-finiteness, so no k ≠ 0 guard is needed, unlike traceZk_add).

theorem RS.MTrace.traceZk_comp_pow {k : ℕ} (g : ℂ → ℂ) (hk : k ≠ 0) {w : ℂ} (hw : w ≠ 0) : traceZk (fun (z : ℂ) => g (z ^ k)) k w = ↑k * g w

Trace of a pullback (branch-point caveat: only away from 0, see the design's junk ledger, §6 — the identity is genuinely false at w = 0).

Analyticity away from the branch point (P4)

theorem RS.MTrace.analyticAt_traceZk {h : ℂ → ℂ} {k : ℕ} (hk : k ≠ 0) {ρ : ℝ} (hρ : 0 < ρ) (hh : AnalyticOnNhd ℂ h (Metric.ball 0 ρ \ {0})) {w₀ : ℂ} (hw₀ : w₀ ≠ 0) (hw₀ρ : ‖w₀‖ < ρ ^ k) : AnalyticAt ℂ (traceZk h k) w₀

traceZk h k is analytic at any w₀ ≠ 0 all of whose k-th roots lie in h's domain of analyticity ball 0 ρ \ {0}. Local branches (AnalyticAt.exists_pow_eq) witness analyticity; no monodromy — the branches are never assembled into a global formula across a branch cut.

Meromorphy at the branch point (P5)

theorem RS.MTrace.meromorphicAt_traceZk {h : ℂ → ℂ} {k : ℕ} (hh : MeromorphicAt h 0) (hk : k ≠ 0) : MeromorphicAt (traceZk h k) 0

traceZk h k is meromorphic at 0 whenever h is, via a norm/zpow growth bound on the root-sum and Riemann's removable-singularity theorem (Complex.differentiableOn_update_limUnder_of_bddAbove) — no monodromy, no convergent global Laurent series needed for existence.

The Laurent-coefficient formula (P6)

Route (tsum-free; a sharpening of the file's previously recorded candidate route (b)): expand the unit factor u of h's order presentation h =ᶠ[𝓝[≠]0] (·)^n₀ * u by the EXACT pointwise Taylor remainder u = P + (·)^M * r (RS.AnalyticAt.exists_taylor_remainder), choosing the cutoff M so that n₀ + M = k * s' is an exact multiple of k with s' > m. Then, summing over the root set of z ^ k = w (w ≠ 0):

• each monomial z ^ (n₀ + d) traces to the CLOSED FORM k · w ^ ((n₀+d)/k) if k ∣ n₀ + d and 0 otherwise (traceZk_zpow, the geometric-sum collapse — computed on the abstract root set via a single root and a primitive root of unity, no analytic branches);
• the remainder contributes z ^ (n₀+M) * r z = w ^ s' * r z EXACTLY (the whole point of the divisibility choice of M — z ^ (k s') = (z^k)^{s'} = w^{s'} per root), so the remainder term is w ^ s' * traceZk r k w with NO second growth bound needed; traceZk r k has an analytic repair at 0 (exists_analyticAt_traceZk, the bounded-case removable singularity), and s' > m makes it invisible to the m-th coefficient.

All coefficients are then read off by residue-calculus's presentation-independent characterization laurentCoeffAt_of_eventuallyEq and the built linearity/shift API.

theorem RS.MTrace.traceZk_zpow {k : ℕ} (hk : k ≠ 0) (e : ℤ) {w : ℂ} (hw : w ≠ 0) : traceZk (fun (z : ℂ) => z ^ e) k w = if ↑k ∣ e then ↑k * w ^ (e / ↑k) else 0

Closed form for the trace of a zpow monomial (w ≠ 0): the sum of z ^ e over the k roots of w collapses by the geometric sum of roots of unity to k * w ^ (e / k) when k ∣ e and to 0 otherwise. Purely algebraic — no branches, no analyticity.

theorem RS.MTrace.laurentCoeffAt_traceZk {h : ℂ → ℂ} {k : ℕ} (hh : MeromorphicAt h 0) (hk : k ≠ 0) (m : ℤ) : laurentCoeffAt (traceZk h k) 0 m = ↑k * laurentCoeffAt h 0 (↑k * m)

THE Laurent-coefficient formula for traceZk (P6): tracing along z ↦ z ^ k keeps exactly every k-th Laurent coefficient, scaled by k. See the section header for the proof route.

theorem RS.MTrace.resAt_traceZk {h : ℂ → ℂ} {k : ℕ} (hh : MeromorphicAt h 0) (hk : k ≠ 0) : resAt (traceZk h k) 0 = ↑k * laurentCoeffAt h 0 (-↑k)

Residue corollary of P6 (design §4.4): the residue of the trace is k times h's coefficient at index -k — NOT h's residue unless k = 1. (Miranda's residue identity Res(Tr(h·ω)) = ∑ Res(h·ω) needs the form's Jacobian factor to compensate this shift; that is form-trace-tower's job, confirming the scope split.)