Order↔multiplicity bridges (meromorphic-trace, cluster 1)

Unit: meromorphic-trace (docs/design/meromorphic-trace.md §2 D4, §4.2, §5 P2). Standing surface hypotheses throughout.

• multiplicity_toP1_of_ordAtX_pos: at a zero of f, CC4's multiplicity of toP1 f (read in coeChart, the chart at ↑0) IS the vanishing order.
• multiplicity_toP1_of_ordAtX_neg: at a pole of f, CC4's multiplicity of toP1 f (read in invChart, the chart at ∞) IS the order of the pole (made positive).

Route: both hard cases reduce to CC3's ordAtX_of_contMDiffAt_eq_zero (already built, local-multiplicity/meromorphic-and-divisors) applied to f' := holoRepr (resp. f'⁻¹ for the pole case), plus ONE shared CC4-level inChartAt-germ comparison (multiplicityENat_toP1_eq_of_eventuallyEq) identifying multiplicityENat (toP1 f') x with the multiplicityENat of the appropriate ℂ-valued companion, using the reusable holoRepr/toP1 facts exported by ToP1.lean.

Deviation: the design's third export, multiplicity_toP1_of_ordAtX_eq_zero (ordAtX f x = 0 → multiplicity (toP1 f) x = 1), is mathematically false as stated and is NOT proved here. Counterexample: f (z) = 1 + z ^ 2 near z = 0 has ordAtX f 0 = 0 (f 0 = 1 ≠ 0, a "regular value" in the vanishing-order sense) but toP1 f has multiplicity 2 at 0 as a map (f y - f 0 = y ^ 2, a genuine ramification point — ordAtX f x = 0 says nothing about deriv f x, only that f does not vanish/pole at x). The design itself flags this lemma as a non-essential "cheap corollary... even though we do not need it ourselves" for form-trace-tower's glue; nothing in this unit's own proof obligations needs it, so it is simply dropped rather than patched into a different (correct) statement under the same name.

theorem RS.MTrace.multiplicity_toP1_of_ordAtX_pos {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} {x : X} (hf : MeromorphicOnX f Set.univ) (hx : 0 < ordAtX f x) : ↑(multiplicity (toP1 f) x) = (ordAtX f x).untop₀

Zero case (P2): at a zero of f, CC4's multiplicity of toP1 f IS the vanishing order.

theorem RS.MTrace.multiplicity_toP1_of_ordAtX_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} {x : X} (hf : MeromorphicOnX f Set.univ) (hx : ordAtX f x < 0) : ↑(multiplicity (toP1 f) x) = -(ordAtX f x).untop₀

Pole case (P2): at a pole of f, CC4's multiplicity of toP1 f IS the order of the pole (made positive).