toP1: the f-to-ℙ¹ bridge (meromorphic-trace, cluster 1)

Unit: meromorphic-trace (docs/design/meromorphic-trace.md §2 D2/D3, §4.1, §5 P1). Standing surface hypotheses throughout (CONVENTIONS.md).

• toP1 f x : OnePoint ℂ — ∞ at poles, the limiting value along the punctured neighborhood elsewhere (D2). Total; junk elsewhere for non-meromorphic f.
• toP1_contMDiff (P1): for f meromorphic everywhere, toP1 f : X → ℙ¹ is holomorphic. Deviation from the design's proof plan: meromorphic-and-divisors's MeroGermOn/OrderEval layer (ℳ X, evalAt, holoRepr, holoRepr_contMDiffAt) — which the design doc explicitly recorded as "not yet built" at design time — is now built; we route through it (toP1 f agrees everywhere with toP1 (mk f hf).holoRepr, since both ordAtX and limUnder are 𝓝[≠]x-germ notions and holoRepr matches any representative 𝓝[≠]x-eventually at every x), which handles the "poles/zeros are isolated" bookkeeping the design's hand-written plan struggled with, and lets us cite MeroGermOn.holoRepr_contMDiffAt/ContMDiffAt.onePointCoe (ProjectiveLine.Holomorphy, also since-landed) directly instead of re-deriving the chart-local analytic-repair argument from scratch. This is a strictly shorter, more robust proof of the same theorem; the exported statement is unchanged.
• toP1_not_const (D3): an everywhere-meromorphic, not-codiscretely-constant f induces a nonconstant toP1 f.

noncomputable def RS.MTrace.toP1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : X → ℂ) (x : X) : OnePoint ℂ

The canonical ℙ¹-valued lift of a raw meromorphic function: ∞ at poles, the limiting value along the punctured neighborhood elsewhere. Total (junk elsewhere for non-meromorphic f); the honest content is toP1_contMDiff.

Equations

• RS.MTrace.toP1 f x = if 0 ≤ RS.ordAtX f x then ↑((nhdsWithin x {x}ᶜ).limUnder f) else OnePoint.infty

theorem RS.MTrace.toP1_eq_infty_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} : toP1 f x = OnePoint.infty ↔ ordAtX f x < 0

theorem RS.MTrace.toP1_eq_coe_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} {c : ℂ} : toP1 f x = ↑c ↔ 0 ≤ ordAtX f x ∧ (nhdsWithin x {x}ᶜ).limUnder f = c

toP1_contMDiff (P1)

theorem RS.MTrace.toP1_contMDiff {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} (hf : MeromorphicOnX f Set.univ) : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (toP1 f)

Reusable holoRepr facts (for OrderMultiplicity/ArgumentPrinciple)

theorem RS.MTrace.toP1_eq_toP1_holoRepr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} (hf : MeromorphicOnX f Set.univ) : toP1 f = toP1 (MeroGermOn.mk f hf).holoRepr

f agrees with its holoRepr in toP1, everywhere (both ordAtX and limUnder are 𝓝[≠]x-germ notions, and holoRepr matches any representative there, at every x).

theorem RS.MTrace.ordAtX_holoRepr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} (hf : MeromorphicOnX f Set.univ) (y : X) : ordAtX (MeroGermOn.mk f hf).holoRepr y = ordAtX f y

theorem RS.MTrace.meromorphicOnX_holoRepr' {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} (hf : MeromorphicOnX f Set.univ) : MeromorphicOnX (MeroGermOn.mk f hf).holoRepr Set.univ

theorem RS.MTrace.holoRepr_contMDiffAt_of_nonneg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} (hf : MeromorphicOnX f Set.univ) {y : X} (hy : 0 ≤ ordAtX (MeroGermOn.mk f hf).holoRepr y) : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (MeroGermOn.mk f hf).holoRepr y

theorem RS.MTrace.toP1_holoRepr_eq_coe_of_nonneg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} (hf : MeromorphicOnX f Set.univ) {y : X} (hy : 0 ≤ ordAtX (MeroGermOn.mk f hf).holoRepr y) : toP1 (MeroGermOn.mk f hf).holoRepr y = ↑((MeroGermOn.mk f hf).holoRepr y)

Wherever f's holoRepr has nonnegative order, toP1 of it is the literal coercion — a pointwise fact (no "isolated zeros" propagation needed: holoRepr_contMDiffAt gives continuity of the holoRepr AT that point directly).

theorem RS.MTrace.toP1_holoRepr_eventuallyEq_coe_of_nonneg {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} (hf : MeromorphicOnX f Set.univ) {y : X} (hy : 0 ≤ ordAtX (MeroGermOn.mk f hf).holoRepr y) : toP1 (MeroGermOn.mk f hf).holoRepr =ᶠ[nhds y] fun (z : X) => ↑((MeroGermOn.mk f hf).holoRepr z)

Full-neighborhood upgrade of toP1_holoRepr_eq_coe_of_nonneg: at a regular point (finite or ⊤ order), toP1 (holoRepr) agrees with the coercion on a full neighborhood (isolated zeros/poles).

theorem RS.MTrace.invChart_toP1_holoRepr_eventuallyEq_of_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} (hf : MeromorphicOnX f Set.univ) {y : X} (hy : ordAtX (MeroGermOn.mk f hf).holoRepr y < 0) : ↑P1.invChart ∘ toP1 (MeroGermOn.mk f hf).holoRepr ∘ ↑(chartAt ℂ y).symm =ᶠ[nhdsWithin (↑(chartAt ℂ y) y) {↑(chartAt ℂ y) y}ᶜ] ((MeroGermOn.mk f hf).holoRepr ∘ ↑(chartAt ℂ y).symm)⁻¹

The invChart chart-composite of toP1 (holoRepr) at a pole matches the (inverted) chart composite of holoRepr itself, off the pole.

Nonconstancy (D3)

def RS.MTrace.NotEventuallyConstX {X : Type u_1} [TopologicalSpace X] (f : X → ℂ) : Prop

The natural raw-function nonconstancy hypothesis: f is not codiscretely equal to any single constant. (What callers holding ℳ X nonzero-ness will have once that field is in hand; stated here germ-level so we do not need it.)

Equations

• RS.MTrace.NotEventuallyConstX f = ∀ (c : ℂ), ¬(fun (x : X) => f x - c) =ᶠ[Filter.codiscrete X] 0

theorem RS.MTrace.toP1_not_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : X → ℂ} (hf : MeromorphicOnX f Set.univ) (hnc : NotEventuallyConstX f) : ¬∃ (c : OnePoint ℂ), ∀ (x : X), toP1 f x = c

The translation: an everywhere-meromorphic f on connected X that is not codiscretely a constant induces a nonconstant toP1 f. Both degenerate cases (toP1 f ≡ ↑c and toP1 f ≡ ∞) are ruled out by the SAME eventuallyEq_zero_codiscrete_of_forall_ordAtX_pos engine, applied to f - c (finite case) resp. f⁻¹ (the ∞ case, via ordAtX_inv unconditional).