Tr_F h: the surface-level fibre trace (meromorphic-trace, cluster 2)

Unit: meromorphic-trace (docs/design/meromorphic-trace.md §2 D7, §4.5, §5 P7). Standing surface hypotheses on X; Y a second Riemann surface ([T2Space Y], no compactness/connectedness needed on Y itself).

• trace F h y₀ — the fibre trace of h along F, evaluated via an arbitrary FiberStack chosen (per point) by Classical.choice; total via an if-dispatch on Nonempty (FiberStack F y₀) so the definition carries no ContMDiff/nonconstancy hypothesis (design §5.7's "Design correction", needed because exists_fiberStack itself needs hne).
• trace_of_forall_eq — junk guard: trace vanishes identically for constant F (R2 resolved honestly below: Nonempty (FiberStack F y₀) is shown FALSE outright at y₀ = c too, via a short cardinality argument, not left open as the design worried it might have to be).
• Well-definedness, resolved (design risk R1): trace_eq_finsum — at ANY point where a FiberStack exists at all, trace F h y₀ = ∑ᶠ x ∈ F⁻¹{y₀}, h x, the naive fibre sum, independent of the stack Classical.choice picked (no holomorphy/nonconstancy hypotheses). Engine: sum_traceZk_stack, the planar-to-fibre reindexing of the stack formula along the adapted-chart bijection (the h-weighted analogue of mapping-degree's sum_multiplicity_inter_source, via the same BijOn), valid over ALL of S.V, not just at y₀. This bypasses R1's "compare two stacks" problem exactly as this file's earlier scope note predicted. trace_eq_finsum' is the every-point version (via exists_fiberStack); trace_eq_stack_sum re-expresses trace through an ARBITRARY stack on its whole neighborhood S.V — the consumption shape form-trace-tower's resAtP1_trace_eq_sum needs.
• meromorphicAtX_trace (P7, the file's centerpiece): Tr_F h is MeromorphicAtX at every point of Y, by reading trace through one fixed stack (trace_eq_stack_sum), so that in the target charts it is a finite sum of planar traceZks (each MeromorphicAt 0 by P5) composed with the maximal-atlas charts (S.A i).e'; CC3 chart invariance (meromorphicAtX_iff_of_mem_source) transports each summand.
• trace_of_regular — the design's sanity anchor: at a regular value the trace is the naive sum over the sheets. (Stated with the design's IsRegularValue hypothesis for interface stability, though trace_eq_finsum' proves the identity at every point.)

noncomputable def RS.MTrace.trace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (h : X → ℂ) (y₀ : Y) : ℂ

The fibre trace of h along F, evaluated via an arbitrary chosen FiberStack at y₀. Total: 0 if no stack can be witnessed at y₀ (the only case this can happen for holomorphic F is at the single value of a constant map, trace_of_forall_eq).

Equations

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

theorem RS.MTrace.trace_def {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (h : X → ℂ) (y₀ : Y) (hS : Nonempty (FiberStack F y₀)) : trace F h y₀ = ∑ i : Fin hS.some.n, traceZk (h ∘ ↑(hS.some.A i).e.symm) (multiplicity F (hS.some.pt i)) (↑(hS.some.A i).e' y₀)

theorem RS.MTrace.trace_of_not_nonempty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {h : X → ℂ} {y₀ : Y} (hns : ¬Nonempty (FiberStack F y₀)) : trace F h y₀ = 0

theorem RS.MTrace.trace_of_forall_eq {X : Type u_1} [TopologicalSpace X] [T2Space X] [ConnectedSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {h : X → ℂ} (c : Y) : trace (fun (x : X) => c) h = fun (x : Y) => 0

Junk convention (R2, resolved): trace vanishes identically for constant F. Away from the constant value, the fibre is empty, giving a genuine (degenerate, n = 0) FiberStack directly; AT the constant value, X being infinite (infinite_of_chartedSpace_complex) makes Nonempty (FiberStack F y₀) outright impossible (a FiberStack's pt : Fin n → X would have to enumerate all of X bijectively onto its range, impossible for infinite X, finite n).

Well-definedness: trace IS the naive fibre sum (design risk R1, resolved)

The engine is the adapted-chart bijection between the part of the fibre inside the i-th chart source and the planar root set {ζ | ζ ^ k = e' y} — the same BijOn as mapping-degree's (private) FiberStack.bijOn_e (LocalConstancy.lean), reproved here verbatim since it is not exported there, then used to reindex h-weighted sums instead of multiplicity counts.

theorem RS.MTrace.sum_traceZk_stack {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {h : X → ℂ} {y₀ : Y} (S : FiberStack F y₀) {y : Y} (hy : y ∈ S.V) : ∑ i : Fin S.n, traceZk (h ∘ ↑(S.A i).e.symm) (multiplicity F (S.pt i)) (↑(S.A i).e' y) = ∑ᶠ (x : X) (_ : x ∈ F ⁻¹' {y}), h x

The stack formula computes the naive fibre sum — over ALL of S.V, not just at y₀ (the h-weighted analogue of mapping-degree's FiberStack.fiberMultSum_eq_sum). No holomorphy or nonconstancy hypotheses: the identity is forced by the stack structure alone.

theorem RS.MTrace.trace_eq_finsum {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {h : X → ℂ} {y₀ : Y} (hS : Nonempty (FiberStack F y₀)) : trace F h y₀ = ∑ᶠ (x : X) (_ : x ∈ F ⁻¹' {y₀}), h x

Well-definedness of trace (design risk R1, resolved): at any point where a FiberStack exists at all, trace equals the naive fibre sum ∑ᶠ x ∈ F⁻¹{y₀}, h x — in particular the stack picked by Classical.choice in trace's definition is immaterial.

theorem RS.MTrace.trace_eq_finsum' {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {h : X → ℂ} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (y : Y) : trace F h y = ∑ᶠ (x : X) (_ : x ∈ F ⁻¹' {y}), h x

Every-point version of trace_eq_finsum for holomorphic nonconstant F (stacks exist everywhere, exists_fiberStack).

theorem RS.MTrace.trace_eq_stack_sum {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {h : X → ℂ} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) {y₀ : Y} (S : FiberStack F y₀) {y : Y} (hy : y ∈ S.V) : trace F h y = ∑ i : Fin S.n, traceZk (h ∘ ↑(S.A i).e.symm) (multiplicity F (S.pt i)) (↑(S.A i).e' y)

trace reads through an ARBITRARY stack S at y₀ on ALL of S.V — the consumption shape for form-trace-tower (fix one stack, transport trace through its adapted charts near y₀).

theorem RS.MTrace.trace_of_regular {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {h : X → ℂ} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) {y₀ : Y} (_hy₀ : IsRegularValue F y₀) : trace F h y₀ = ∑ᶠ (x : X) (_ : x ∈ F ⁻¹' {y₀}), h x

Sanity anchor (design §4.5): at a regular value, trace reduces to the naive sum-over-the-sheets formula. The regularity hypothesis is kept for interface stability with the design even though trace_eq_finsum' proves the identity at every point.

Meromorphy of the trace (P7)

theorem RS.MTrace.meromorphicAtX_trace {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {h : X → ℂ} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (hh : MeromorphicOnX h Set.univ) (y₀ : Y) : MeromorphicAtX (trace F h) y₀

Meromorphy of the fibre trace (P7, the design's centerpiece for this file): for holomorphic nonconstant F : X → Y and h meromorphic everywhere on X, Tr_F h is meromorphic at every point of Y. Route: fix ONE stack S at y₀; on S.V the trace IS the stack formula (trace_eq_stack_sum), a finite sum of planar traceZks — each meromorphic at 0 by P5 (meromorphicAt_traceZk) — composed with the target charts (S.A i).e'; transport through the charts by CC3 chart invariance (meromorphicAtX_iff_of_mem_source).