ofForm1, the ℳ(X)-module structure, d, dlog (D7), data + quotient layers

Unit: canonical-forms (docs/design/canonical-forms.md §2 D7, §4.3, proof plan §5 P1).

Data layer (MFormData, raw):

• MFormData.ofForm1/Form1.toMFormData: the holomorphic special case, using η's own analytic chart coefficients (Form1.analyticOnNhd_coeffIn) and the SAME transition rule coeffIn_trans already proves — no new computation.
• MFormData.smul: the ℳ(X)-action, via the canonical, choice-free MeroGermOn.holoRepr.
• MFormData.d: the differential of a meromorphic function; the compat-at-poles case split is isolated as the reusable deriv_comp_chart_congr (no hypothesis on the transported function — poles are handled by the junk-collapse argument in BOTH directions).

Quotient layer (MForm, the honest 1-form type):

• MForm.ofForm1/Form1.toMForm : Form1 X →ₗ[ℂ] MForm X (the design's frozen bridge name).
• SMul (ℳ X) (MForm X), the full Module (ℳ X) (MForm X) instance, plus IsScalarTower ℂ (ℳ X) (MForm X)/SMulCommClass ℂ (ℳ X) (MForm X). The module laws that FAIL for raw families (add_smul/mul_smul/one_smul need holoRepr-of-a-sum identities that break at poles) hold on the quotient: holoRepr of f + g/f * g/c • f agrees with the pointwise combination on 𝓝[≠] x for EVERY x (holoRepr_eventuallyEq_nhdsNE against the combined representative), which is exactly the quotient's equality granularity.
• MForm.d with MForm.d_add (same mechanism: (f+g).holoRepr agrees with f.holoRepr + g.holoRepr near every center, and deriv respects punctured-neighborhood agreement, Filter.EventuallyEq.nhdsNE_deriv) and MForm.d_const.
• MForm.dlog f := f⁻¹ • MForm.d f, with the argument-principle atom MForm.resAt_dlog (junk-robust, no f ≠ 0 hypothesis — via MeromorphicAt.resAt_deriv_div).
• MForm.ord_smul_mero : (h • Θ).ord x = h.ord x + Θ.ord x (the D10/D11 divisor dictionary's pointwise engine).

theorem RS.differentiableAt_comp_chart_of_mem_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {g : X → ℂ} {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {p : X} (hp : p ∈ e.source) (hp' : p ∈ e'.source) (hd : DifferentiableAt ℂ (g ∘ ↑e.symm) (↑e p)) : DifferentiableAt ℂ (g ∘ ↑e'.symm) (↑e' p)

Chart-invariance of DifferentiableAt, both directions (spike-verified, scratch_canon.lean item 4): if g ∘ e.symm is differentiable at e p, so is g ∘ e'.symm at e' p, for any two maximal-atlas charts both containing p. No hypothesis on g.

theorem RS.deriv_comp_chart_congr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {g : X → ℂ} {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {z : ℂ} (hz : z ∈ ↑e' '' (e.source ∩ e'.source)) : deriv (g ∘ ↑e'.symm) z = deriv (↑e ∘ ↑e'.symm) z * deriv (g ∘ ↑e.symm) (↑e (↑e'.symm z))

The unit's central new lemma (P1, scratch_canon.lean item 4, generalized to a full by_cases on differentiability): for ANY g : X → ℂ (no hypothesis at all — poles handled by the junk-collapse of both sides to 0), the derivative-through-charts transition rule.

MFormData.ofForm1: the holomorphic special case (D7)

noncomputable def RS.MFormData.ofForm1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) : MFormData X

The holomorphic special case: a Form1 gives an MFormData with the same chart coefficients (no poles). compat is exactly coeffIn_trans — no new work.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.MFormData.ofForm1_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η η' : Form1 X) : ofForm1 (η + η') = ofForm1 η + ofForm1 η'

theorem RS.MFormData.ofForm1_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) (η : Form1 X) : ofForm1 (c • η) = c • ofForm1 η

theorem RS.MFormData.ofForm1_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : ofForm1 0 = 0

noncomputable def RS.Form1.toMFormData {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Form1 X →ₗ[ℂ] MFormData X

The holomorphic-to-meromorphic bridge as a ℂ-linear map (item 3(d) of the task brief).

Equations

• RS.Form1.toMFormData = { toFun := RS.MFormData.ofForm1, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.MFormData.ofForm1_ord_nonneg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) (x : X) : 0 ≤ (ofForm1 η).ord x

Holomorphic 1-forms give MFormDatas with nonnegative order everywhere (they land in OmegaSpace 0, D12/§6).

MFormData.smul: the ℳ(X)-module action (D7)

noncomputable def RS.MFormData.smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (h : Mero X) (θ : MFormData X) : MFormData X

Multiplication of a meromorphic 1-form by a meromorphic function, via the canonical, choice-free representative MeroGermOn.holoRepr.

Equations

• RS.MFormData.smul h θ = { coeffAt := fun (x : X) (z : ℂ) => RS.MeroGermOn.holoRepr h (↑(chartAt ℂ x).symm z) * θ.coeffAt x z, coeffAt_zero_off := ⋯, meromorphicOn_coeffAt := ⋯, compat := ⋯ }

@[instance_reducible]

noncomputable instance RS.MFormData.instSMulMero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : SMul (Mero X) (MFormData X)

Equations

• RS.MFormData.instSMulMero = { smul := RS.MFormData.smul }

@[simp]

theorem RS.MFormData.coeffAt_smul_mero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (h : Mero X) (θ : MFormData X) (x : X) (z : ℂ) : (h • θ).coeffAt x z = MeroGermOn.holoRepr h (↑(chartAt ℂ x).symm z) * θ.coeffAt x z

MFormData.d: the differential of a meromorphic function (D7, P1)

noncomputable def RS.MFormData.d {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) : MFormData X

The differential of a meromorphic function f, via f.holoRepr — a genuine, Classical.choice-free function ℳ X → MFormData X. compat (the pole case-split) is deriv_comp_chart_congr instantiated at g := f.holoRepr.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.MFormData.coeffAt_d {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) (x : X) {z : ℂ} (hz : z ∈ (chartAt ℂ x).target) : (d f).coeffAt x z = deriv (MeroGermOn.holoRepr f ∘ ↑(chartAt ℂ x).symm) z

theorem RS.MFormData.d_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) : d ((algebraMap ℂ (Mero X)) c) = 0

d of a constant is 0 (no poles at all, hence no junk subtlety).

MFormData.dlog

noncomputable def RS.MFormData.dlog {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) : MFormData X

The logarithmic differential dlog f := f⁻¹ • df.

Equations

• RS.MFormData.dlog f = RS.MFormData.smul f⁻¹ (RS.MFormData.d f)

holoRepr germ identities for the quotient module laws

holoRepr of a sum/product/scalar is NOT the pointwise combination (junk at poles), but it AGREES with it on 𝓝[≠] x for every x (holoRepr_eventuallyEq_nhdsNE read against the combined representative) — exactly the granularity of MFormData.Eqv, which is why the Module (ℳ X) (MForm X) laws hold on the quotient.

theorem RS.Mero.holoRepr_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f g : Mero X) (x : X) : MeroGermOn.holoRepr (f + g) =ᶠ[nhdsWithin x {x}ᶜ] MeroGermOn.holoRepr f + MeroGermOn.holoRepr g

theorem RS.Mero.holoRepr_mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f g : Mero X) (x : X) : MeroGermOn.holoRepr (f * g) =ᶠ[nhdsWithin x {x}ᶜ] MeroGermOn.holoRepr f * MeroGermOn.holoRepr g

theorem RS.Mero.holoRepr_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) (f : Mero X) (x : X) : MeroGermOn.holoRepr (c • f) =ᶠ[nhdsWithin x {x}ᶜ] c • MeroGermOn.holoRepr f

theorem RS.Mero.holoRepr_inv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) (x : X) : MeroGermOn.holoRepr f⁻¹ =ᶠ[nhdsWithin x {x}ᶜ] (MeroGermOn.holoRepr f)⁻¹

theorem RS.Mero.holoRepr_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) : MeroGermOn.holoRepr 0 =ᶠ[nhdsWithin x {x}ᶜ] fun (x : X) => 0

theorem RS.Mero.holoRepr_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) : MeroGermOn.holoRepr 1 =ᶠ[nhdsWithin x {x}ᶜ] fun (x : X) => 1

theorem RS.Mero.ord_eq_meromorphicOrderAt_holoRepr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) (x : X) : MeroGermOn.ord f x = meromorphicOrderAt (MeroGermOn.holoRepr f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)

The order of a meromorphic-function class, read through holoRepr in the preferred chart (the form the ord_smul_mero dictionary consumes).

Quotient layer: MForm.ofForm1, the Module (ℳ X) structure, MForm.d, MForm.dlog

noncomputable def RS.MForm.ofForm1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) : MForm X

D7: the holomorphic embedding, on classes.

Equations

• RS.MForm.ofForm1 η = RS.MForm.mk (RS.MFormData.ofForm1 η)

theorem RS.MForm.ofForm1_ord_nonneg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) (x : X) : 0 ≤ (ofForm1 η).ord x

noncomputable def RS.Form1.toMForm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Form1 X →ₗ[ℂ] MForm X

The holomorphic-to-meromorphic bridge as a ℂ-linear map (the design's frozen name, targeting the QUOTIENT; the raw version is Form1.toMFormData).

Equations

• RS.Form1.toMForm = { toFun := RS.MForm.ofForm1, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.MForm.ofForm1_injective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Function.Injective ofForm1

ofForm1 is injective into classes: punctured-neighborhood agreement of the ANALYTIC coefficients at each center forces value agreement at the center by continuity (D12's injectivity half).

The ℳ(X)-module structure

@[instance_reducible]

noncomputable instance RS.MForm.instSMulMero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : SMul (Mero X) (MForm X)

Equations

• RS.MForm.instSMulMero = { smul := fun (h : RS.Mero X) => Quotient.map (fun (θ : RS.MFormData X) => RS.MFormData.smul h θ) ⋯ }

@[simp]

theorem RS.MForm.mero_smul_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (h : Mero X) (θ : MFormData X) : h • mk θ = mk (MFormData.smul h θ)

@[instance_reducible]

noncomputable instance RS.MForm.instModuleMero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Module (Mero X) (MForm X)

Equations

• RS.MForm.instModuleMero = Module.ofMinimalAxioms ⋯ ⋯ ⋯ ⋯

instance RS.MForm.instIsScalarTowerComplexMero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : IsScalarTower ℂ (Mero X) (MForm X)

theorem RS.MForm.ord_smul_mero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (h : Mero X) (Θ : MForm X) (x : X) : (h • Θ).ord x = MeroGermOn.ord h x + Θ.ord x

The order dictionary for the ℳ(X)-action: orders add (the D10/D11 engine). Junk-robust — no nonvanishing hypotheses (⊤-arithmetic absorbs the degenerate cases).

MForm.d and MForm.dlog

noncomputable def RS.MForm.d {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) : MForm X

D7: the differential of a meromorphic function, on classes (a genuine, Classical.choice-free function ℳ X → MForm X via holoRepr).

Equations

• RS.MForm.d f = RS.MForm.mk (RS.MFormData.d f)

theorem RS.MForm.d_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) : d ((algebraMap ℂ (Mero X)) c) = 0

theorem RS.MForm.d_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f g : Mero X) : d (f + g) = d f + d g

Additivity of the differential — FALSE at the raw-family level (junk of holoRepr at the poles of the summands), true on the quotient: (f+g).holoRepr agrees with f.holoRepr + g.holoRepr near every center, and deriv respects punctured agreement.

noncomputable def RS.MForm.dlog {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) : MForm X

D7: the logarithmic differential, on classes.

Equations

• RS.MForm.dlog f = f⁻¹ • RS.MForm.d f

theorem RS.MForm.resAt_dlog {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) (x : X) : (dlog f).resAt x = ↑(MeroGermOn.ord f x).untop₀

The argument-principle atom (design §4.3 item 4): the residue of dlog f at x is the order of f at x. Junk-robust: no f ≠ 0 hypothesis (for f = 0 both sides are 0).