traceCoeff: the repaired planar trace coefficient (jacobian-functoriality §6, planar layer)

Unit: jacobian-functoriality. RS.FormTrace.traceZkForm h k (the Jacobian-weighted planar trace atom) has a removable singularity at the branch coordinate 0: its literal value there is junk (traceZk's w = 0 convention), and for k > 1 does not equal the limit from the punctured neighborhood — the precise defect that blocked the previous builder (see the root LEDGER). This file REPAIRS the value at 0 via mathlib's meromorphic normal form (toMeromorphicNFAt), and proves the repair is genuinely analytic across 0:

• RS.traceCoeff h k := toMeromorphicNFAt (traceZkForm h k) 0 — agrees with traceZkForm h k at every w ≠ 0 (traceCoeff_apply_of_ne_zero), analytic at 0 once h is (analyticAt_traceCoeff_zero), and analytic on the whole ball ball 0 (ρ ^ k) once h is analytic on ball 0 ρ (analyticOnNhd_traceCoeff — THE branch-point analyticity).
• Route for the 0-analyticity (design §6.3, route (a)): traceZkForm h k is meromorphic at 0 (meromorphicAt_traceZkForm), and its Laurent coefficients at negative indices all vanish by the already-proved shift formula laurentCoeffAt_traceZkForm plus analyticity of h — hence its meromorphic order is ≥ 0 (forall_neg_laurentCoeffAt_eq_zero_iff), hence the normal-form repair is analytic (MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt).
• traceZk_one/traceZkForm_one/traceCoeff_one — the k = 1 (unramified) trivializations.
• traceZkForm_fun_add/traceCoeff_fun_add, traceZkForm_const_mul/traceCoeff_const_mul — ℂ-linearity in h, including at the repaired point 0 (by uniqueness of limits).

k = 1 trivializations

theorem RS.MTrace.traceZk_one (h : ℂ → ℂ) (w : ℂ) : traceZk h 1 w = h w

theorem RS.FormTrace.traceZkForm_one (h : ℂ → ℂ) : traceZkForm h 1 = h

Linearity of traceZkForm in h (valid at every w, including 0)

theorem RS.FormTrace.traceZkForm_fun_add {h h' : ℂ → ℂ} {k : ℕ} (hk : k ≠ 0) : traceZkForm (fun (v : ℂ) => h v + h' v) k = fun (w : ℂ) => traceZkForm h k w + traceZkForm h' k w

theorem RS.FormTrace.traceZkForm_const_mul {h : ℂ → ℂ} (c : ℂ) (k : ℕ) : traceZkForm (fun (v : ℂ) => c * h v) k = fun (w : ℂ) => c * traceZkForm h k w

The repaired coefficient

noncomputable def RS.traceCoeff (h : ℂ → ℂ) (k : ℕ) : ℂ → ℂ

The repaired planar trace coefficient: traceZkForm h k with its removable singularity at the branch coordinate 0 repaired via mathlib's meromorphic normal form.

Equations

• RS.traceCoeff h k = toMeromorphicNFAt (RS.FormTrace.traceZkForm h k) 0

theorem RS.meromorphicAt_traceZkForm_of_analyticAt {h : ℂ → ℂ} {k : ℕ} (hh : AnalyticAt ℂ h 0) (hk : k ≠ 0) : MeromorphicAt (FormTrace.traceZkForm h k) 0

theorem RS.traceCoeff_apply_of_ne_zero {h : ℂ → ℂ} {k : ℕ} {w : ℂ} (hh : AnalyticAt ℂ h 0) (hk : k ≠ 0) (hw : w ≠ 0) : traceCoeff h k w = FormTrace.traceZkForm h k w

Off the branch coordinate, the repair is literal.

theorem RS.meromorphicOrderAt_traceZkForm_nonneg {h : ℂ → ℂ} {k : ℕ} (hh : AnalyticAt ℂ h 0) (hk : k ≠ 0) : 0 ≤ meromorphicOrderAt (FormTrace.traceZkForm h k) 0

traceZkForm h k has no negative Laurent coefficients at 0 when h is analytic there: its meromorphic order is nonnegative (design §6.3, the Laurent route).

theorem RS.analyticAt_traceCoeff_zero {h : ℂ → ℂ} {k : ℕ} (hh : AnalyticAt ℂ h 0) (hk : k ≠ 0) : AnalyticAt ℂ (traceCoeff h k) 0

The branch-point analyticity of the repaired coefficient (the previous builder's blocker, resolved): once h is analytic at 0, the repaired traceCoeff h k is honestly analytic at the branch coordinate 0.

theorem RS.analyticAt_traceZkForm_of_ne_zero {h : ℂ → ℂ} {k : ℕ} {w : ℂ} {ρ : ℝ} (hρ : 0 < ρ) (hk : k ≠ 0) (hh : AnalyticOnNhd ℂ h (Metric.ball 0 ρ)) (hw : w ≠ 0) (hwρ : ‖w‖ < ρ ^ k) : AnalyticAt ℂ (FormTrace.traceZkForm h k) w

Off-branch analyticity of the un-repaired traceZkForm (a re-packaging of RS.MTrace.analyticAt_traceZk with the Jacobian factor divided in).

theorem RS.analyticOnNhd_traceCoeff {h : ℂ → ℂ} {k : ℕ} {ρ : ℝ} (hρ : 0 < ρ) (hk : k ≠ 0) (hh : AnalyticOnNhd ℂ h (Metric.ball 0 ρ)) : AnalyticOnNhd ℂ (traceCoeff h k) (Metric.ball 0 (ρ ^ k))

The master repair lemma: if h is analytic on ball 0 ρ, the repaired trace coefficient traceCoeff h k is analytic on the whole ball ball 0 (ρ ^ k) — branch point included.

theorem RS.traceCoeff_one {h : ℂ → ℂ} (hh : AnalyticAt ℂ h 0) : traceCoeff h 1 = h

k = 1: the repair is literally h (no branching, nothing to repair).

Linearity of the repaired coefficient

theorem RS.traceCoeff_fun_add {h h' : ℂ → ℂ} {k : ℕ} (hk : k ≠ 0) (hh : AnalyticAt ℂ h 0) (hh' : AnalyticAt ℂ h' 0) : traceCoeff (fun (v : ℂ) => h v + h' v) k = fun (w : ℂ) => traceCoeff h k w + traceCoeff h' k w

theorem RS.traceCoeff_const_mul {h : ℂ → ℂ} {k : ℕ} (hk : k ≠ 0) (hh : AnalyticAt ℂ h 0) (c : ℂ) : traceCoeff (fun (v : ℂ) => c * h v) k = fun (w : ℂ) => c * traceCoeff h k w