The Jacobian-weighted planar trace atom (form-trace-tower, file 2/6)

Unit: form-trace-tower (docs/design/form-trace-tower.md §2 D3, §4.2, §5). RS.MTrace.traceZk (Jacobian/MeromorphicTrace/PlanarTrace.lean) is fully proved, zero sorries, including its Laurent-coefficient formula laurentCoeffAt_traceZk (P6 — CLOSED, see docs/build-log.md's [mtrace] entries) and its residue corollary resAt_traceZk. This file builds the "divide out the Jacobian factor" atom on top.

• traceZkForm h k w — divides the k · v^(k-1) Jacobian factor (that F^*(dz) = d(v^k) = k v^{k-1} dv produces in an adapted chart) back out of h's coefficient before applying traceZk. Junk-inherits traceZk's own convention at w = 0 (never used there).
• traceZkForm_hAdapted_eq_apply (the cancellation identity, task item 2's core step): applying traceZkForm to a coefficient that ALREADY carries the Jacobian factor recovers the bare traceZk of the un-weighted function, for every w ≠ 0 — this is why "the trace of the pair-form h·F^*dz" needs no new global object: its coefficient function IS RS.MTrace.trace. Deviation from the design: stated for w ≠ 0 (not as a full function equality) — the design's own proof sketch claims an unconditional (∀ w, no w ≠ 0 guard) function equality, but this is FALSE at w = 0 for k > 1 whenever g 0 ≠ 0 (the Jacobian factor k·v^{k-1} literally vanishes at v = 0 for k > 1, so dividing it back out at the branch point does not recover g 0) — a genuine gap in the design's claim, corrected here to the provable, and equally useful (all downstream uses are 𝓝[≠]0-germ notions), w ≠ 0 form.
• meromorphicAt_traceZkForm — existence of meromorphy, UNCONDITIONAL in k (needs only k ≠ 0), built only from RS.MTrace.meromorphicAt_traceZk (P5).
• laurentCoeffAt_traceZkForm / resAt_traceZkForm — the Laurent-coefficient / residue identities, now UNCONDITIONALLY PROVABLE (mtrace's P6 landed, see docs/build-log.md).

noncomputable def RS.FormTrace.traceZkForm (h : ℂ → ℂ) (k : ℕ) (w : ℂ) : ℂ

The Jacobian-weighted planar trace atom: divides the k·v^{k-1} Jacobian factor of F^*(dz) back out before applying RS.MTrace.traceZk.

Equations

• RS.FormTrace.traceZkForm h k w = RS.MTrace.traceZk (fun (v : ℂ) => h v * (↑k * v ^ (↑k - 1))⁻¹) k w

theorem RS.FormTrace.traceZkForm_def (h : ℂ → ℂ) (k : ℕ) (w : ℂ) : traceZkForm h k w = MTrace.traceZk (fun (v : ℂ) => h v * (↑k * v ^ (↑k - 1))⁻¹) k w

theorem RS.FormTrace.traceZkForm_hAdapted_eq_apply {g : ℂ → ℂ} {k : ℕ} (hk : k ≠ 0) {w : ℂ} (hw : w ≠ 0) : traceZkForm (fun (v : ℂ) => g v * ↑k * v ^ (↑k - 1)) k w = MTrace.traceZk g k w

The cancellation identity (task item 2's core step), w ≠ 0 form (see the module docstring for why the design's unconditional claim is false at w = 0).

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

Existence of meromorphy: builds ONLY on RS.MTrace.meromorphicAt_traceZk (P5, zero sorries) — NOT gated on P6.

theorem RS.FormTrace.laurentCoeffAt_traceZkForm {h : ℂ → ℂ} {k : ℕ} (hh : MeromorphicAt h 0) (hk : k ≠ 0) (j : ℤ) : laurentCoeffAt (traceZkForm h k) 0 j = laurentCoeffAt h 0 (↑k * j + (↑k - 1))

The Laurent-coefficient formula (design §4.2, ⚠ was gated on mtrace's P6 — now UNCONDITIONAL, P6 having landed with zero admitted goals).

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

Miranda Lemma 3.2, LOCAL case (single preimage): the residue is preserved EXACTLY (no factor of k — the Jacobian factor exactly cancels mtrace's k-multiplier at the residue index j = -1).