Planar root counting (mapping-degree, planar layer)

Everything about the roots of z ^ k = w in ℂ that the surface-level fiber count needs:

• RS.exists_pow_eq — k-th roots exist (via exp/log, avoiding the FTA import);
• RS.setOf_pow_eq_finite, RS.ncard_setOf_pow_eq — the root set is finite, of cardinality k when w ≠ 0;
• RS.norm_lt_of_pow_eq — roots are trapped in the ball whose k-th power ball contains w;
• RS.analyticOrderAt_pow_zero, RS.analyticOrderAt_pow_sub_pow — vanishing orders of z ↦ z ^ k (order k at 0) and z ↦ z ^ k - ζ ^ k (order 1 at ζ ≠ 0);
• RS.sum_toNat_analyticOrderAt_pow_sub — THE planar counting identity: the total multiplicity of z ↦ z ^ k over any w : ℂ is k, uniformly in w (no branched/unbranched case split for consumers).

This file has zero project imports; LocalConstancy.lean bridges analyticOrderAt to RS.multiplicity via local-multiplicity's chart invariance.

theorem RS.exists_pow_eq {k : ℕ} (hk : k ≠ 0) {w : ℂ} (hw : w ≠ 0) : ∃ (α : ℂ), α ^ k = w

k-th roots exist in ℂ (via exp/log; deliberately avoids IsAlgClosed.exists_pow_nat_eq, whose instance would drag in the FTA import).

theorem RS.setOf_pow_eq_zero {k : ℕ} (hk : k ≠ 0) : {z : ℂ | z ^ k = 0} = {0}

theorem RS.setOf_pow_eq_coe_toFinset {k : ℕ} (hk : k ≠ 0) (w : ℂ) : {z : ℂ | z ^ k = w} = ↑(Polynomial.nthRoots k w).toFinset

The root set of z ^ k = w, as the coercion of the nthRoots finset.

theorem RS.setOf_pow_eq_finite {k : ℕ} (hk : k ≠ 0) (w : ℂ) : {z : ℂ | z ^ k = w}.Finite

theorem RS.card_nthRoots_toFinset {k : ℕ} (hk : k ≠ 0) {w : ℂ} (hw : w ≠ 0) : (Polynomial.nthRoots k w).toFinset.card = k

theorem RS.ncard_setOf_pow_eq {k : ℕ} (hk : k ≠ 0) {w : ℂ} (hw : w ≠ 0) : {z : ℂ | z ^ k = w}.ncard = k

theorem RS.norm_lt_of_pow_eq {k : ℕ} (hk : k ≠ 0) {z w : ℂ} {ρ : ℝ} (hρ : 0 ≤ ρ) (h : z ^ k = w) (hw : ‖w‖ < ρ ^ k) : ‖z‖ < ρ

Roots are trapped in the ball whose k-th power ball contains w.

theorem RS.analyticOrderAt_pow_zero (k : ℕ) : analyticOrderAt (fun (z : ℂ) => z ^ k) 0 = ↑k

theorem RS.analyticOrderAt_pow_sub_pow {k : ℕ} (hk : k ≠ 0) {ζ : ℂ} (hζ : ζ ≠ 0) : analyticOrderAt (fun (z : ℂ) => z ^ k - ζ ^ k) ζ = 1

theorem RS.sum_toNat_analyticOrderAt_pow_sub {k : ℕ} (hk : k ≠ 0) (w : ℂ) : ∑ᶠ (ζ : ℂ) (_ : ζ ∈ {z : ℂ | z ^ k = w}), (analyticOrderAt (fun (z : ℂ) => z ^ k - w) ζ).toNat = k

THE planar counting identity: the total multiplicity of z ↦ z ^ k over any w is k (one root of order k when w = 0; k simple roots otherwise). Uniform in w, so surface consumers need no branched/unbranched case split.