D9: existence of a nonconstant meromorphic function and a nonzero meromorphic 1-form

Unit: canonical-forms (docs/design/canonical-forms.md §2 D9, §4.4, proof plan §5 P-exist). This is the unit's raison d'être: finiteness-and-chi's χ ledger, gated on cech's Skyscraper fragment, has now LANDED (Jacobian/Finiteness/Chi.lean), so the file the design's own file plan flagged as "the ONLY file gated on finiteness-and-chi" can finally be written.

What this file delivers

• Function.locallyFinsuppWithin.degree_single — closes the §1.6 gap note honestly: no separate Divisor.single constructor was ever needed. Mathlib's own Function.locallyFinsuppWithin.single already lands in locallyFinsuppWithin (Set.univ) Y (see its statement in Mathlib/Topology/LocallyFinsupp.lean:153), which is RS.Divisor X (the abbrev unfolds), so Function.locallyFinsuppWithin.single P n is directly usable as a point-divisor of any integer value n at P. Finiteness/Chi.lean's own degree_single already exploits exactly this (at the fixed value n = 1); this generalizes it to arbitrary n, needed to build divisors of prescribed degree in the existence argument below.
• MForm.d_ne_zero (moved, not duplicated): residue-theorem's Reduction.lean had already proved "the differential of a nonconstant meromorphic function is nonzero" — but purely as an internal step of its own theorem, using only canonical-forms/meromorphic-and-divisors machinery (no residue-theorem-specific content: no ℙ¹, no trace, no calibration). Since residue-theorem is DOWNSTREAM of canonical-forms (its root docstring calls exists_nonconstant_mero "canonical-forms D9's exact export shape"), importing it back from here would be a cycle. This is exactly the D9 existence-chain's own nonzero-ness step (§2 D9: "exists_ne_zero_mform is then ⟨MForm.d f, ...⟩"), so canonical-forms is its clean home; the proof is transplanted verbatim (renaming the bound meromorphic function φ ↦ f to match MForm.d's own parameter name), and residue-theorem's Reduction.lean now imports it from here instead (see that file's updated note).
• exists_nonconstant_mero/exists_ne_zero_mform (D9 itself, Forster 16.11 pattern): pick any point P; choose a divisor D := single P n of large enough degree that chi 0 + D.degree ≥ 2 (always possible, n is free); chi_zero_add_degree_le_l gives l D ≥ 2; since l 0 = 1 (Liouville, linSys_zero_eq_span_one) and LinSys 0 ≤ LinSys D (linSys_mono, 0 ≤ D), the finite-dimensional inclusion LinSys 0 ≤ LinSys D is proper (unequal finrank), so some f ∈ LinSys D lies outside LinSys 0 = span{1} — i.e. f is not any constant. exists_ne_zero_mform is the one-liner ⟨MForm.d f, MForm.d_ne_zero hf⟩.
• exists_canonicalDivisor: the D10 existence corollary — a canonical divisor concretely exists (D10's canonicalDivisorOf/canonicalDivisorOf_linearEquiv, already proved in OneDimensional.lean since they have no finiteness dependence, need a witness θ₀ ≠ 0 to be instantiated at all; D9 supplies it).

Compat: Function.locallyFinsuppWithin.degree_single at an arbitrary value

theorem Function.locallyFinsuppWithin.degree_single {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [DecidableEq X] (P : X) (n : ℤ) : degree (single P n) = n

Compat (upstream candidate; generalizes RS.Finiteness.degree_single's fixed value 1 to an arbitrary n): the degree of the point-divisor single P n is n.

MForm.d_ne_zero: moved here from residue-theorem/Reduction.lean (clean home, see the

module docstring above for why the import direction forced the move).

theorem RS.MForm.d_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [ConnectedSpace X] {f : Mero X} (hf : ∀ (c : ℂ), f ≠ (algebraMap ℂ (Mero X)) c) : d f ≠ 0

The differential of a nonconstant meromorphic function is a nonzero meromorphic 1-form (identity-theorem dichotomy: were d f = 0, the chart derivative would vanish near some nonnegative-order point, forcing f.holoRepr to be locally — hence codiscretely — constant).

D9: the existence chain

theorem RS.exists_nonconstant_mero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] : ∃ (f : Mero X), ∀ (c : ℂ), f ≠ (algebraMap ℂ (Mero X)) c

D9 (Forster 16.11 pattern): a compact connected Riemann surface admits a nonconstant meromorphic function. Proved from finiteness-and-chi's χ-ledger: at a divisor D := single P n of large enough degree, χ(0) + deg D ≤ l(D) forces l(D) ≥ 2 > 1 = l(0), so L(0) = span{1} is a PROPER subspace of L(D) — any witness outside it is not a constant.

theorem RS.exists_ne_zero_mform {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] : ∃ (θ : MForm X), θ ≠ 0

D9: a compact connected Riemann surface admits a nonzero meromorphic 1-form — the differential of the nonconstant function exists_nonconstant_mero supplies.

D10 corollary: a canonical divisor concretely exists

theorem RS.exists_canonicalDivisor {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] : ∃ (K : Divisor X) (θ₀ : MForm X), θ₀ ≠ 0 ∧ K = canonicalDivisorOf θ₀

A canonical divisor exists (D10's canonicalDivisorOf/canonicalDivisorOf_linearEquiv, already proved finiteness-free in OneDimensional.lean, need a witness θ₀ ≠ 0 to be instantiated at all — D9 supplies it).