MFormData.ord/resAt (D4), chart-invariance, and divisor (D6) — data layer

Unit: canonical-forms (docs/design/canonical-forms.md §2 D4–D6, §4.2). Everything here is stated for the RAW data carrier MFormData and descends to the quotient MForm in Quotient.lean (all reading maps are germ-at-the-chart-center facts, hence congruence-robust).

• MFormData.ord/MFormData.resAt (D4): read directly via the fixed chartAt, needing no invariance proof to be well-defined; MFormData.ord_eq_of_mem_source/MFormData.resAt_eq_of_mem_source supply the "read in any maximal-atlas chart" corollary (chart-invariance, via meromorphicOrderAt_comp_of_deriv_ne_zero/RS.resAt_comp_mul_deriv).
• MFormData.eventually_ord_eq_top/MFormData.eventually_ord_eq_zero: local propagation of the order, the chart-crossing analogues of eventually_ordAtX_eq_top/eventually_ordAtX_eq_zero (Jacobian/Meromorphic/Predicates.lean), via compat.
• MFormData.divisor/MFormData.degree (D6): local finiteness is connectedness-free, mirroring MeroGermOn.divisorOn's proof exactly.

noncomputable def RS.MFormData.ord {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) (x : X) : WithTop ℤ

D4: the order of θ at x, read via the (fixed) preferred chart at x.

Equations

• θ.ord x = meromorphicOrderAt (θ.coeffAt x) (↑(chartAt ℂ x) x)

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

D4: the residue of θ at x, read via the (fixed) preferred chart at x.

Equations

• θ.resAt x = RS.resAt (θ.coeffAt x) (↑(chartAt ℂ x) x)

theorem RS.MFormData.meromorphicAt_coeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) (x : X) : MeromorphicAt (θ.coeffAt x) (↑(chartAt ℂ x) x)

theorem RS.MFormData.ord_eq_top_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {θ : MFormData X} {x : X} : θ.ord x = ⊤ ↔ θ.coeffAt x =ᶠ[nhdsWithin (↑(chartAt ℂ x) x) {↑(chartAt ℂ x) x}ᶜ] 0

A one-line corollary of meromorphicOrderAt_eq_top_iff (the MFormData-level analogue of ordAtX_eq_top_iff).

theorem RS.MFormData.ord_eq_of_mem_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {θ : MFormData X} {x : X} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hx : x ∈ e.source) : θ.ord x = meromorphicOrderAt (fun (z : ℂ) => deriv (↑(chartAt ℂ x) ∘ ↑e.symm) z * θ.coeffAt x (↑(chartAt ℂ x) (↑e.symm z))) (↑e x)

Convenience (chart-invariance of ord, via meromorphicOrderAt_comp_of_deriv_ne_zero): the order of θ at x may be computed reading θ.coeffAt x through ANY maximal-atlas chart e valid at x, not just chartAt ℂ x. Not DAG-required by any current consumer, offered as a documented, non-blocking convenience (§4.2).

theorem RS.MFormData.resAt_eq_of_mem_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {θ : MFormData X} {x : X} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hx : x ∈ e.source) : θ.resAt x = RS.resAt (fun (z : ℂ) => deriv (↑(chartAt ℂ x) ∘ ↑e.symm) z * θ.coeffAt x (↑(chartAt ℂ x) (↑e.symm z))) (↑e x)

Convenience (chart-invariance of resAt, via RS.resAt_comp_mul_deriv): the residue of θ at x may be computed reading θ.coeffAt x through ANY maximal-atlas chart e valid at x.

theorem RS.MFormData.coeffAt_eventuallyEq_of_mem_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) {x y : X} (hy : y ∈ (chartAt ℂ x).source) : θ.coeffAt y =ᶠ[nhds (↑(chartAt ℂ y) y)] fun (z : ℂ) => deriv (↑(chartAt ℂ x) ∘ ↑(chartAt ℂ y).symm) z * θ.coeffAt x (↑(chartAt ℂ x) (↑(chartAt ℂ y).symm z))

Auxiliary cross-point transport: θ.coeffAt y, on a whole neighborhood of its own chart center, is given by the compat formula against θ.coeffAt x for any x with y ∈ (chartAt ℂ x).source. The engine behind eventually_ord_eq_top/eventually_ord_eq_zero.

theorem RS.MFormData.ord_eq_meromorphicOrderAt_of_mem_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) {x p : X} (hp : p ∈ (chartAt ℂ x).source) : θ.ord p = meromorphicOrderAt (θ.coeffAt x) (↑(chartAt ℂ x) p)

Cross-point order reading: the order of θ at any point p of the chart source at x is the planar order of the single coefficient function θ.coeffAt x at the chart image chartAt ℂ x p — no transition factor survives (its order is 0). This is the bridge that lets OmegaSpace-membership (a pointwise ord condition at every chart CENTER) control the coefficient at every TARGET point (D12's repair construction, LinearSystems.lean).

theorem RS.MFormData.eventually_ord_eq_top {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] {θ : MFormData X} {x : X} (h : θ.ord x = ⊤) : ∀ᶠ (y : X) in nhds x, θ.ord y = ⊤

MFormData.ord propagates to ⊤ on a whole neighborhood, once it is ⊤ at the center (mirrors eventually_ordAtX_eq_top, Predicates.lean:231).

theorem RS.MFormData.eventually_ord_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {θ : MFormData X} {x : X} (h : θ.ord x ≠ ⊤) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, θ.ord y = 0

MFormData.ord is eventually 0 away from a point where it is finite (mirrors eventually_ordAtX_eq_zero, Predicates.lean:314). Feeds the local finiteness of divisor.

noncomputable def RS.MFormData.divisor {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] (θ : MFormData X) : Divisor X

D6: the divisor of θ (local finiteness, connectedness-free — mirrors MeroGermOn.divisorOn exactly, Divisor.lean:134).

Equations

• θ.divisor = { toFun := fun (x : X) => (θ.ord x).untop₀, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }

@[simp]

theorem RS.MFormData.divisor_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] (θ : MFormData X) (x : X) : θ.divisor x = (θ.ord x).untop₀

noncomputable def RS.MFormData.degree {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [T2Space X] [CompactSpace X] (θ : MFormData X) : ℤ

D6: the degree of θ's divisor.

Equations

• θ.degree = Function.locallyFinsuppWithin.degree θ.divisor

@[simp]

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