monodromy: continuation of log f along pole/zero-avoiding paths

Unit: monodromy (docs/design/monodromy.md §4.2). The DAG-critical deliverable: a continuous branch of log f (equivalently, a primitive of dlog f = df/f) along any path avoiding the zeros/poles of a meromorphic function f : ℳ X, with the defining exponential compatibility exp (F t) = f.holoRepr (γ.extend t).

dlogForm is built by reusing Jacobian/Forms/MDifferential.lean's RS.mdifferential (the differential of a holomorphic function) and RS.Form1.smulFun (multiplication of a form by a holomorphic function) — both already proved generically over any X satisfying the standing surface hypotheses — instantiated with X := poleZeroLocus f (the open locus, Jacobian/Monodromy /OpenLocus.lean). This sidesteps entirely the chart-transition/subtypeRestr bookkeeping a from-scratch Form1CoeffData construction would need: f.holoRepr restricted to the locus is ContMDiff (mathlib's contMDiffAt_subtype_iff — smoothness of an open-submanifold restriction is exactly a per-point statement), nonvanishing there (order 0 at every point of the locus, by construction), hence its logarithmic derivative (f.holoRepr)⁻¹ • d(f.holoRepr) assembles as a genuine Form1 (poleZeroLocus f) via the two already-built combinators, no new coefficient-data proof needed.

The exponential-compatibility theorem (exp_eq_holoRepr_of_isPrimitiveAlong) shows any primitive of dlogForm normalized at the starting value is an honest branch of log f, by exhibiting H t := f.holoRepr (γ.extend t) * exp (-(F t)) as locally constant (zero-derivative argument, via RS.eventuallyEq_of_hasDerivAt_eq) and hence globally constant (ℝ preconnected) — no branch-cut case analysis on Complex.log/Complex.arg anywhere.

Main declarations:

• RS.Monodromy.poleZeroLocus, RS.Monodromy.dlogForm — the pole/zero-free locus and the logarithmic-derivative 1-form on it.
• RS.Monodromy.exp_eq_holoRepr_of_isPrimitiveAlong — the exponential-compatibility theorem.
• RS.Monodromy.exists_logBranchAlong, RS.Monodromy.logBranchAlong_unique — existence with a prescribed initial branch value, and uniqueness (both bookkeeping over Path's already-built existence/uniqueness API).

The pole/zero-free locus

noncomputable def RS.Monodromy.poleZeroLocus {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) : TopologicalSpace.Opens X

The zero/pole locus of f as an open pole-free locus ((divisor f).support is finite by compactness, hence closed by T2Space).

Equations

• RS.Monodromy.poleZeroLocus f = RS.Monodromy.openLocusOfFinite ⋯

theorem RS.Monodromy.mem_poleZeroLocus_iff {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : Mero X} (hf : f ≠ 0) {x : X} : x ∈ poleZeroLocus f ↔ MeroGermOn.ord f x = 0

def RS.Monodromy.Path.liftPoleZeroLocus {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : Mero X} {x y : X} (γ : Path x y) (hγ : ∀ (t : ↑unitInterval), γ t ∉ Function.locallyFinsuppWithin.support (divisor f)) : Path ⟨x, ⋯⟩ ⟨y, ⋯⟩

Lift a path avoiding f's zeros/poles into poleZeroLocus f.

NB: this is a thin specialization of Path.liftOpenLocus (OpenLocus.lean) landing directly in poleZeroLocus f rather than in the definitionally-equal-but-syntactically-different openLocusOfFinite (finite_support_divisor f). This is not cosmetic: with the general Path.liftOpenLocus (finite_support_divisor f).isClosed γ hγ spelling, X's ChartedSpace/ IsManifold instance search for RS.IsPrimitiveAlong/RS.Form1 gets confused whenever both that term's type and a separately-mentioned poleZeroLocus f (from dlogForm f hf) occur in the same elaboration problem — Lean's instance cache keys on the syntactic form, and the two (defeq) forms of the locus type produce inconsistent cached instance terms, a synthInstance failure with no direct paper-mathematics content (confirmed by direct trace inspection: Opens.instChartedSpace resolves correctly for either form in isolation, but not when both appear together). Landing liftPoleZeroLocus's output type in poleZeroLocus f syntactically, once and for all, sidesteps the issue for every downstream use.

Equations

• RS.Monodromy.Path.liftPoleZeroLocus γ hγ = { toFun := fun (t : ↑unitInterval) => ⟨γ t, ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

theorem RS.Monodromy.Path.liftPoleZeroLocus_extend {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : Mero X} {x y : X} (γ : Path x y) (hγ : ∀ (t : ↑unitInterval), γ t ∉ Function.locallyFinsuppWithin.support (divisor f)) (t : ℝ) : ↑((liftPoleZeroLocus γ hγ).extend t) = γ.extend t

The lift's extend recovers γ.extend pointwise.

f.holoRepr restricted to the locus is a nonvanishing holomorphic function

theorem RS.Monodromy.contMDiff_holoRepr_poleZeroLocus {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) (hf : f ≠ 0) : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ fun (p : ↥(poleZeroLocus f)) => MeroGermOn.holoRepr f ↑p

theorem RS.Monodromy.holoRepr_ne_zero_of_ord_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : Mero X} {x : X} (h0 : MeroGermOn.ord f x = 0) : MeroGermOn.holoRepr f x ≠ 0

f.holoRepr does not vanish anywhere on the order-zero locus (a helper for the general "order exactly zero ⇒ the canonical representative is nonzero there" fact, R2 in the design).

theorem RS.Monodromy.holoRepr_poleZeroLocus_ne_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) (hf : f ≠ 0) (p : ↥(poleZeroLocus f)) : MeroGermOn.holoRepr f ↑p ≠ 0

dlogForm: the logarithmic-derivative 1-form on the locus

noncomputable def RS.Monodromy.dlogForm {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) (hf : f ≠ 0) : Form1 ↥(poleZeroLocus f)

The logarithmic-derivative 1-form df/f of f, a genuine holomorphic 1-form on the pole/zero-free open locus poleZeroLocus f — assembled from RS.mdifferential/RS.Form1.smulFun (both already built, generically over any surface satisfying the standing hypotheses), instantiated with X := poleZeroLocus f.

Equations

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

theorem RS.Monodromy.coeffIn_dlogForm {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) (hf : f ≠ 0) {e : OpenPartialHomeomorph ↥(poleZeroLocus f) ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ ↥(poleZeroLocus f)) {z : ℂ} (hz : z ∈ e.target) : coeffIn e (dlogForm f hf) z = (MeroGermOn.holoRepr f ↑(↑e.symm z))⁻¹ * deriv ((fun (p : ↥(poleZeroLocus f)) => MeroGermOn.holoRepr f ↑p) ∘ ↑e.symm) z

dlogForm's coefficient in any maximal-atlas chart of the locus, on the chart target: the familiar (f'/f)-shape logarithmic derivative, read through the chart.

The exponential-compatibility theorem

theorem RS.Monodromy.exp_eq_holoRepr_of_isPrimitiveAlong {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : Mero X} (hf : f ≠ 0) {x y : X} {γ : Path x y} (hγ : ∀ (t : ↑unitInterval), γ t ∉ Function.locallyFinsuppWithin.support (divisor f)) {F : ℝ → ℂ} (hF : IsPrimitiveAlong (Path.liftPoleZeroLocus γ hγ) (dlogForm f hf) F) (hc₀ : Complex.exp (F 0) = MeroGermOn.holoRepr f x) (t : ℝ) : Complex.exp (F t) = MeroGermOn.holoRepr f (γ.extend t)

The exponential-compatibility theorem. Any primitive of dlogForm f hf along a pole/zero-avoiding path is an honest continuous branch of log f along the path, PROVIDED it is normalized so that exp (F 0) = f.holoRepr x: exp (F t) = f.holoRepr (γ.extend t) for every t. Proved by exhibiting H t := f.holoRepr (γ.extend t) * exp (-(F t)) as locally constant (zero-derivative argument on each chart) and hence globally constant (ℝ preconnected) — no branch-cut case analysis on Complex.log/Complex.arg anywhere.

Existence and uniqueness of a log branch with a prescribed initial value

theorem RS.Monodromy.exists_logBranchAlong {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : Mero X} (hf : f ≠ 0) {x y : X} (γ : Path x y) (hγ : ∀ (t : ↑unitInterval), γ t ∉ Function.locallyFinsuppWithin.support (divisor f)) {c₀ : ℂ} (hc₀ : Complex.exp c₀ = MeroGermOn.holoRepr f x) : ∃ (F : ℝ → ℂ), IsPrimitiveAlong (Path.liftPoleZeroLocus γ hγ) (dlogForm f hf) F ∧ F 0 = c₀ ∧ ∀ (t : ℝ), Complex.exp (F t) = MeroGermOn.holoRepr f (γ.extend t)

Existence, with a prescribed initial branch value: a continuous branch of log f along any path avoiding the zeros/poles of f, starting at a chosen c₀ with exp c₀ = f.holoRepr x.

theorem RS.Monodromy.logBranchAlong_unique {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : Mero X} (hf : f ≠ 0) {x y : X} {γ : Path x y} {hγ : ∀ (t : ↑unitInterval), γ t ∉ Function.locallyFinsuppWithin.support (divisor f)} {F F' : ℝ → ℂ} (hF : IsPrimitiveAlong (Path.liftPoleZeroLocus γ hγ) (dlogForm f hf) F) (hF' : IsPrimitiveAlong (Path.liftPoleZeroLocus γ hγ) (dlogForm f hf) F') (h0 : F 0 = F' 0) : F = F'

Uniqueness (free, from Path's own sub_eq_sub): two branches agreeing at t = 0 agree everywhere — no new proof, a direct instantiation over the open locus.