6.35. MappingDegree.LocalKFoldMultiplicity🔗

Jacobians.MappingDegree.LocalKFoldMultiplicity — source

KthRootSubstitution

Hypothesis bundle for the k-th root substitution.

For g : ℂ → ℂ analytic with g x₀ = w₀ and local order k at x₀, the analytic substitution v should satisfy, on a small closed disc of radius ρ:

• v is analytic on closedBall x₀ ρ,

• v x₀ = 0,

• deriv v x₀ ≠ 0,

• g z - w₀ = (v z) ^ k for every z ∈ closedBall x₀ ρ.

These four conditions are exactly the data needed to reduce the k-fold preimage-count theorem to ZZ74's k = 1 case applied to v.

For k = 1 the bundle is constructed unconditionally (kthRootSubstitution_of_localMultiplicityOne). For k ≥ 2 the construction requires an analytic k-th root branch of the unit factor u in the local form g - w₀ = (z - x₀)^k · u, which is the named-only gap analytic_kth_root_branch_exists_statement.

structure KthRootSubstitution (g : ℂ → ℂ) (x₀ w₀ : ℂ) (k : ℕ) : Prop where