One-dimensionality over ℳ(X) (D8) and the canonical divisor K (D10)

Unit: canonical-forms (docs/design/canonical-forms.md §2 D8/D10, proof plan §5 P5).

• MForm.smul_eq_zero_iff/MForm.smul_left_injective: ℳ(X)-scaling by a nonzero form is injective (the D5 dichotomy + the ord_smul_mero dictionary).
• D8 MForm.exists_unique_smul_of_ne_zero: MForm X is one-dimensional over ℳ X — every meromorphic 1-form is a unique ℳ(X)-multiple of any fixed nonzero reference θ₀. The ratio is built chart-locally (q x := θ.coeffAt x / θ₀.coeffAt x, transitions cancel — "the ratio of two 1-forms is a function") and glued by MeroGermOn.exists_glue; on the QUOTIENT the class equation needs only 𝓝[≠]-agreement at each center, where θ₀'s coefficient is eventually nonzero (D5), so no removable-singularity repair is needed at the zeros of θ₀.
• D10 canonicalDivisorOf θ₀ := θ₀.divisor ("a" canonical divisor, seeded by an explicit nonzero reference — no silent choice), MForm.divisor_smul_mero (divisors add under the ℳ(X)-action), and canonicalDivisorOf_linearEquiv (any two canonical divisors differ by a principal divisor — Forster 16.7-style well-definedness up to linear equivalence).

D10 lives here rather than in the design's Existence.lean slot because Existence.lean (D9) remains gated on Jacobian/Finiteness/Chi.lean (not on disk); canonicalDivisorOf has no finiteness dependence.

Hypothesis note: D8 needs only [T1Space X] [ConnectedSpace X] (the design listed an extra [T2Space X], which is not required — the dichotomy and Mero.ord_ne_top are T1-level).

theorem RS.MForm.smul_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [ConnectedSpace X] {h : Mero X} {Θ : MForm X} : h • Θ = 0 ↔ h = 0 ∨ Θ = 0

ℳ(X)-scaling detects zero (the uniqueness engine for D8): h • Θ = 0 iff one factor is.

theorem RS.MForm.smul_left_injective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [ConnectedSpace X] {Θ₀ : MForm X} (h₀ : Θ₀ ≠ 0) : Function.Injective fun (h : Mero X) => h • Θ₀

Scaling a fixed nonzero reference is injective (D8 uniqueness half).

theorem RS.MForm.exists_smul_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [ConnectedSpace X] {Θ₀ : MForm X} (h₀ : Θ₀ ≠ 0) (Θ : MForm X) : ∃ (h : Mero X), Θ = h • Θ₀

D8, existence half: every meromorphic 1-form is an ℳ(X)-multiple of any fixed nonzero reference (chart-local ratio + MeroGermOn.exists_glue).

theorem RS.MForm.exists_unique_smul_of_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [ConnectedSpace X] {Θ₀ : MForm X} (h₀ : Θ₀ ≠ 0) (Θ : MForm X) : ∃! h : Mero X, Θ = h • Θ₀

D8, one-dimensionality: every meromorphic 1-form is a UNIQUE ℳ(X)-multiple of any fixed nonzero reference θ₀ — MForm X is a one-dimensional ℳ(X)-vector space.

D10: the canonical divisor K

@[reducible, inline]

noncomputable abbrev RS.canonicalDivisorOf {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] (Θ₀ : MForm X) : Divisor X

D10: "a" canonical divisor, seeded by an explicit nonzero reference (no silent Classical.choice-baked default; downstream fixes one when a definite K is needed).

Equations

• RS.canonicalDivisorOf Θ₀ = Θ₀.divisor

theorem RS.MForm.divisor_smul_mero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [T2Space X] [ConnectedSpace X] {h : Mero X} {Θ : MForm X} (hh : h ≠ 0) (hΘ : Θ ≠ 0) : (h • Θ).divisor = RS.divisor h + Θ.divisor

Divisors add under the ℳ(X)-action (pointwise from ord_smul_mero; both orders are finite by the D5 dichotomy and Mero.ord_ne_top).

theorem RS.canonicalDivisorOf_linearEquiv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [T2Space X] [ConnectedSpace X] {Θ₀ Θ₀' : MForm X} (h₀ : Θ₀ ≠ 0) (h₀' : Θ₀' ≠ 0) : ∃ (f : Mero X), f ≠ 0 ∧ canonicalDivisorOf Θ₀' = canonicalDivisorOf Θ₀ + divisor f

D10 (Forster 16.7): the canonical divisor is well defined up to linear equivalence — any two nonzero references have divisors differing by a principal divisor.