Compat: small MForm helpers needed by residue-theorem (candidates for canonical-forms)

Unit: residue-theorem (docs/design/residue-theorem.md). Per CONVENTIONS.md's Compat rule and the task brief's file discipline, these three one-step corollaries of canonical-forms' frozen quotient API live in a clearly-marked NEW file rather than editing Jacobian/CanonicalForms/:

• RS.MForm.resAt_eq_zero_of_ord_nonneg — residues vanish where the order is nonnegative (the §1.2 gap flagged in the residue-theorem design; RS.resAt_of_order_nonneg composed with the definition of MForm.resAt).
• RS.MForm.finite_setOf_ord_neg — the pole set of a meromorphic 1-form on a compact surface is finite (via the divisor's finite support; no connectedness needed).
• RS.MForm.finite_support_resAt — hence resAt has finite support.

Request filed in docs/requests/canonical-forms.md-spirit: these belong upstream eventually.

theorem RS.MForm.resAt_eq_zero_of_ord_nonneg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Θ : MForm X} {x : X} (h : 0 ≤ Θ.ord x) : Θ.resAt x = 0

The residue of a meromorphic 1-form vanishes at any point of nonnegative order.

theorem RS.MForm.finite_setOf_ord_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [T2Space X] [CompactSpace X] (Θ : MForm X) : {x : X | Θ.ord x < 0}.Finite

The pole set of a meromorphic 1-form on a compact surface is finite (via the divisor's finite support; connectedness-free).

theorem RS.MForm.finite_support_resAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [T2Space X] [CompactSpace X] (Θ : MForm X) : (Function.support fun (x : X) => Θ.resAt x).Finite

MForm.resAt has finite support on a compact surface.