A machine-checked solution to the Jacobians challenge

12.6. MeromorphicTrace.TracePullback🔗

Jacobians.MeromorphicTrace.TracePullback — source

ambientTrace

Coordinate form of the trace f₊, parallel to ambientPsi for pullbackForm: ambientTrace = (ambientIso Y)⁻¹ ∘ traceFormTotal f hf ∘ (ambientIso X) (matrix T, direction gX → gY; zero on the unused off-genus branch). Built from the genuine geometric trace traceFormTotal (which is traceForm off the constant locus and 0 on constant maps).

noncomputable def ambientTrace {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] {gX gY : ℕ}
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) :
    (Fin gX → ℂ) →L[ℂ] (Fin gY → ℂ)

ambientPullbackJac

The genuine Jacobian pullback in ambient coordinates: Tᵀ, the transpose of ambientTrace (via the standard Pi basis). Direction gY → gX. By the projection formula this realises periodVec δ ↦ periodVec(preimage cycle); it replaces the misformalized ambientPsi-as-pullback. As with ambientPhi, the transpose makes contravariant ambientPullbackJac_comp automatic from covariant ambientTrace_comp.

noncomputable def ambientPullbackJac {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] {gX gY : ℕ}
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) :
    (Fin gY → ℂ) →L[ℂ] (Fin gX → ℂ)

ambientTrace_id

ambientTrace id = id. Via traceFormTotal_id.

theorem ambientTrace_id {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (x : Fin (genus X) → ℂ)
    :
    ambientTrace (X := X) (Y := X) (gX := genus X) (gY := genus X) id contMDiff_id x = x

ambientTrace_comp

Covariant composition: ambientTrace (g ∘ f) = ambientTrace g ∘ ambientTrace f. Via traceFormTotal_comp.

theorem ambientTrace_comp {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] {Z : Type*} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z]
    [ConnectedSpace Z] [Nonempty Z] [ChartedSpace ℂ Z] [IsManifold 𝓘(ℂ) ω Z]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω g)
    (hgf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω (g ∘ f))
    (x : Fin (genus X) → ℂ) :
    ambientTrace (gX := genus X) (gY := genus Z) (g ∘ f) hgf x =
      ambientTrace (gX := genus Y) (gY := genus Z) g hg
        (ambientTrace (gX := genus X) (gY := genus Y) f hf x)

ambientPullbackJac_id

ambientPullbackJac id = id — transpose of the identity matrix is the identity, via ambientTrace_id.

theorem ambientPullbackJac_id {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (y : Fin (genus X) → ℂ)
    :
    ambientPullbackJac (X := X) (Y := X) (gX := genus X) (gY := genus X) id contMDiff_id y = y

ambientPullbackJac_comp

Contravariant composition: ambientPullbackJac (g ∘ f) = ambientPullbackJac f ∘ ambientPullbackJac g. Follows from covariant ambientTrace_comp via matrix transpose reversing order.

theorem ambientPullbackJac_comp {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] {Z : Type*} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z]
    [ConnectedSpace Z] [Nonempty Z] [ChartedSpace ℂ Z] [IsManifold 𝓘(ℂ) ω Z]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω g)
    (hgf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω (g ∘ f))
    (z : Fin (genus Z) → ℂ) :
    ambientPullbackJac (gX := genus X) (gY := genus Z) (g ∘ f) hgf z =
      ambientPullbackJac (gX := genus X) (gY := genus Y) f hf
        (ambientPullbackJac (gX := genus Y) (gY := genus Z) g hg z)

ambientTrace_eq_zero_of_const

ambientTrace of a constant map is zero, from traceFormTotal_eq_zero_of_const (mirrors ambientPsi_eq_zero_of_const).

theorem ambientTrace_eq_zero_of_const {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hconst : ∃ y₀ : Y, ∀ x, f x = y₀) :
    ambientTrace (gX := genus X) (gY := genus Y) f hf = 0

ambientPullbackJac_eq_zero_of_const

ambientPullbackJac of a constant map is zero (Tᵀ = 0 when T = 0). The constant-case input to ambientPullbackJac_preserves_truePeriodLattice.

theorem ambientPullbackJac_eq_zero_of_const {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hconst : ∃ y₀ : Y, ∀ x, f x = y₀) :
    ambientPullbackJac (gX := genus X) (gY := genus Y) f hf = 0

ambientPullbackJac_periodVec_apply_eq_lineIntegral_traceFormTotal

Algebraic bridge (projection formula, period level). The i-th component of the genuine Jacobian pullback ambientPullbackJac f hf (periodVec δ) is the line integral of the trace of the i-th basis form along δ: (Tᵀ · periodVec δ)ᵢ = ∫_δ traceFormTotal f hf (ωᵢ^X).

Pure linear algebra + linearity of lineIntegral, dual to periodVec_pushforward (PeriodLattice.lean). With w := (ambientIso Y).symm (traceFormTotal f hf ωᵢ^X): the matrix entry Tᵀ i j = (ambientTrace f hf eᵢ^X) j = w j (ambientTrace is the ambientIso-conjugate of traceFormTotal), so the LHS is ∑ⱼ wⱼ (periodVec δ)ⱼ; and traceFormTotal f hf ωᵢ^X = ambientIso Y w = ∑ⱼ wⱼ • ωⱼ^Y, so the RHS line integral is ∑ⱼ wⱼ ∫_δ ωⱼ^Y = ∑ⱼ wⱼ (periodVec δ)ⱼ by linearity. The integrability hypothesis is the per-basis-form regularity of a closed smooth loop.

theorem ambientPullbackJac_periodVec_apply_eq_lineIntegral_traceFormTotal {X Y : Type*}
    [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y]
    [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (δ : ℝ → Y) (i : Fin (genus X))
    (hint_Y : ∀ j : Fin (genus Y), IntervalIntegrable
      (fun t => (periodBasisForm Y j).toFun (δ t) (pathSpeed δ t)) MeasureTheory.volume 0 1) :
    ambientPullbackJac (gX := genus X) (gY := genus Y) f hf (periodVec δ) i =
      lineIntegral (traceFormTotal f hf (periodBasisForm X i)) δ

PreimageCycle

A preimage cycle witnessing the trace identity: a finite ℤ-combination of closed smooth loops in X whose period-vector sum realizes the genuine Jacobian pullback ambientPullbackJac f hf (periodVec δ).

Classically: for non-constant holomorphic f : X → Y between compact Riemann surfaces, f is a branched cover of some degree d ≥ 1, and the set-theoretic preimage f⁻¹(δ) of a loop δ (avoiding branch points) is d disjoint closed loops in X whose signed sum realizes Tᵀ (periodVec δ) (Forster §10.11).

Defining PreimageCycle as a bundle of (loops + coefficients + pullback/pushforward equations) lets us isolate the classical content: the theorem ambientPullbackJac_periodVec_mem_truePeriodLattice_of_preimageCycle is real and purely algebraic; only *producing* a PreimageCycle for each non-constant f, δ is content-gated.

structure PreimageCycle {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (δ : ℝ → Y) where

ambientPullbackJac_periodVec_mem_truePeriodLattice_of_preimageCycle

Pullback identity — algebraic reduction. Given a PreimageCycle witness for (f, δ), the pulled-back period vector ambientPullbackJac (periodVec δ) lies in truePeriodLattice X: each periodVec of a closed smooth loop is in the lattice, and the lattice is closed under ℤ-linear combinations.

theorem ambientPullbackJac_periodVec_mem_truePeriodLattice_of_preimageCycle {X Y : Type*}
    [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y]
    [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (δ : ℝ → Y) (c : PreimageCycle f hf δ) :
    ambientPullbackJac (gX := genus X) (gY := genus Y) f hf (periodVec δ) ∈
      truePeriodLattice X

finite_chartImage_branchLocus

The chart-coordinate image of the branch locus inside the chart at w is finite.

lemma finite_chartImage_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ y, f y = y₀) (w : Y) :
    ((chartAt (H := ℂ) w) '' (branchLocus f ∩ (chartAt (H := ℂ) w).source)).Finite

chartSymm_notMem_branchLocus

Off-branch transfer: a chart-target point off the chart-image of the branch locus pulls back to a point off the branch locus.

lemma chartSymm_notMem_branchLocus {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] {f : X → Y} {w : Y} {v : ℂ}
    (hv_target : v ∈ (chartAt (H := ℂ) w).target)
    (hvB : v ∉ (chartAt (H := ℂ) w) '' (branchLocus f ∩ (chartAt (H := ℂ) w).source)) :
    (chartAt (H := ℂ) w).symm v ∉ branchLocus f

exists_offBranch_detour_piece

Per-piece off-branch detour (geometric kernel). Given a chart anchor w, a sub-ball Metric.ball c r ⊆ (chartAt w).target, and two points P, Q off branchLocus f whose chart images lie in the sub-ball, there is a flat-ended smooth path γ : P → Q that

  • avoids branchLocus f on all of [0,1],

  • stays in (chartAt w).source,

  • has chart-w image inside Metric.ball c r on [0,1],

  • has matching chart endpoints chart (γ 0) = chart P, chart (γ 1) = chart Q,

  • has vanishing endpoint velocities.

The relay is OfCurveSkeleton.exists_relay_dodge_finite (planar dodge of the finite chart-image of the branch locus); the arc is the concatenation of two OfCurveSkeleton.ChartBallPathSmooth3 hops P → relay, relay → Q.

lemma exists_offBranch_detour_piece {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ y, f y = y₀)
    (w P Q : Y) (c : ℂ) (r : ℝ)
    (hball : Metric.ball c r ⊆ (chartAt (H := ℂ) w).target)
    (hP_src : P ∈ (chartAt (H := ℂ) w).source) (hQ_src : Q ∈ (chartAt (H := ℂ) w).source)
    (hP_ball : (chartAt (H := ℂ) w) P ∈ Metric.ball c r)
    (hQ_ball : (chartAt (H := ℂ) w) Q ∈ Metric.ball c r)
    (hP_off : P ∉ branchLocus f) (hQ_off : Q ∉ branchLocus f) :
    ∃ γ : ℝ → Y, IsSmoothPath P Q γ ∧
      (∀ t : ℝ, γ t ∉ branchLocus f) ∧
      (∀ t ∈ Set.Icc (0:ℝ) 1, (chartAt (H := ℂ) w) (γ t) ∈ Metric.ball c r) ∧
      (∀ t ∈ Set.Icc (0:ℝ) 1, γ t ∈ (chartAt (H := ℂ) w).source) ∧
      pathSpeed γ 0 = 0 ∧ pathSpeed γ 1 = 0

exists_offBranch_overlap_connector

[OVERLAP CONNECTOR — the off-branch breakpoint perturbation]. Let P be a point lying in the sources of two chart anchors w₁, w₂ (the anchors of two adjacent cover pieces sharing the breakpoint P = δ(k/n)), with chart-image inside each anchor's sub-ball ball (c\_j) (r\_j) ⊆ target(w\_j). Then there is a point p off branchLocus f, together with a flat-ended smooth connecting path c : P → p, whose chart-image stays inside *both* sub-balls (and whose body stays in both chart sources) on all of [0,1].

This is the perturbation that a stronger cover statement would have needed (and failed) to do at the level of δ itself: δ(k/n) may sit on the branch locus, but we dodge to a nearby off-branch p and record the short connecting path c. Because c lies in the *overlap* of the two sub-balls, the line integral of any period form along c is the same primitive-difference whether computed in ball 1 or ball 2 — which is exactly the intrinsic correction term that makes the telescope in exists_loop_off_branchLocus close.

Construction: a small ball D around chart₂ P inside ball (c₂) (r₂) whose chart₂.symm-image is in source w₁ with chart₁-image in ball (c₁) (r₁) (continuity of the transition chart₁ ∘ chart₂.symm at chart₂ P, where chart₁ P ∈ ball (c₁) (r₁) is open). Any p with chart₂ p ∈ D then lies in both balls; pick p ∈ chart₂.symm '' D off the finite branchLocus (open-minus-finite). The connector is the chart-2 straight segment ChartBallPathSmooth3 w₂ P p, confined to the convex D (so to ball 2), hence to ball 1 via the transition.

lemma exists_offBranch_overlap_connector {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ y, f y = y₀)
    (w₁ w₂ P : Y) (c₁ c₂ : ℂ) (r₁ r₂ : ℝ)
    (_hball₁ : Metric.ball c₁ r₁ ⊆ (chartAt (H := ℂ) w₁).target)
    (hball₂ : Metric.ball c₂ r₂ ⊆ (chartAt (H := ℂ) w₂).target)
    (hP₁_src : P ∈ (chartAt (H := ℂ) w₁).source) (hP₂_src : P ∈ (chartAt (H := ℂ) w₂).source)
    (hP₁_ball : (chartAt (H := ℂ) w₁) P ∈ Metric.ball c₁ r₁)
    (hP₂_ball : (chartAt (H := ℂ) w₂) P ∈ Metric.ball c₂ r₂) :
    ∃ (p : Y) (c : ℝ → Y),
      p ∉ branchLocus f ∧ IsSmoothPath P p c ∧
      pathSpeed c 0 = 0 ∧ pathSpeed c 1 = 0 ∧
      (∀ t ∈ Set.Icc (0:ℝ) 1, c t ∈ (chartAt (H := ℂ) w₁).source) ∧
      (∀ t ∈ Set.Icc (0:ℝ) 1, c t ∈ (chartAt (H := ℂ) w₂).source) ∧
      (∀ t ∈ Set.Icc (0:ℝ) 1, (chartAt (H := ℂ) w₁) (c t) ∈ Metric.ball c₁ r₁) ∧
      (∀ t ∈ Set.Icc (0:ℝ) 1, (chartAt (H := ℂ) w₂) (c t) ∈ Metric.ball c₂ r₂)

exists_overlap_connectors

Batch of off-branch overlap connectors, one per breakpoint. From the sub-ball cover of δ (uniform n-partition, per-piece anchor x k, sub-ball ball (c k) (r k) ⊆ target(x k), confining δ's chart-image on piece k), produce, for every breakpoint k : Fin n (sitting at parameter k/n), an off-branch point p k and a flat-ended smooth connector cc k : δ(k/n) → p k whose body and chart-image are confined to *both* adjacent sub-balls: the "this" ball k (left end of piece k) and the "previous" ball k-1 (right end of piece k-1, with the wrap 0-1 = n-1 handled via δ 1 = δ 0).

The endpoint p k thus lies in source(x k) ∩ source(x (k-1)) with chart-images in both balls — so adjacent detours can be built between the p's — and the connector lies in the overlap, so the line integral of any period form along cc k is the same primitive-difference in either ball (the intrinsic correction term corr of the telescope). Single application of exists_offBranch_overlap_connector per breakpoint.

lemma exists_overlap_connectors {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ y, f y = y₀)
    (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ)
    (n : ℕ) [NeZero n] (hn : 0 < n) (x : Fin n → Y) (c : Fin n → ℂ) (r : Fin n → ℝ)
    (hconf : ∀ (k : Fin n) (s : ℝ), (k : ℝ) / n ≤ s → s ≤ ((k : ℝ) + 1) / n →
      Metric.ball (c k) (r k) ⊆ (chartAt (H := ℂ) (x k)).target ∧
      δ s ∈ (chartAt (H := ℂ) (x k)).source ∧
      (chartAt (H := ℂ) (x k)) (δ s) ∈ Metric.ball (c k) (r k)) :
    ∃ (p : Fin n → Y) (cc : Fin n → ℝ → Y),
      ∀ k : Fin n,
        p k ∉ branchLocus f ∧
        IsSmoothPath (δ ((k : ℝ) / n)) (p k) (cc k) ∧
        pathSpeed (cc k) 0 = 0 ∧ pathSpeed (cc k) 1 = 0 ∧
        (∀ t ∈ Set.Icc (0:ℝ) 1, cc k t ∈ (chartAt (H := ℂ) (x (k - 1))).source) ∧
        (∀ t ∈ Set.Icc (0:ℝ) 1, cc k t ∈ (chartAt (H := ℂ) (x k)).source) ∧
        (∀ t ∈ Set.Icc (0:ℝ) 1,
          (chartAt (H := ℂ) (x (k - 1))) (cc k t) ∈ Metric.ball (c (k - 1)) (r (k - 1))) ∧
        (∀ t ∈ Set.Icc (0:ℝ) 1, (chartAt (H := ℂ) (x k)) (cc k t) ∈ Metric.ball (c k) (r k))

exists_loop_off_branchLocus

[off-branch surgery, period-preserving — the discharge of #6]. A closed smooth loop δ in Y can be deformed off the finite branchLocus f *without changing its period vector*.

This is proved directly (an intermediate off-branch-breakpoint cover would be false, since a C¹ loop may linger on a branch value, so a uniform breakpoint δ(k/n) can be forced onto the locus). Instead we *perturb the breakpoints*:

  1. Cover. OfCurveSkeleton.exists_subBallChartCover gives a uniform n-partition with, per piece k, a chart anchor x k and a sub-ball ball (c k) (r k) ⊆ target(x k) confining δ's chart-image on [k/n,(k+1)/n]. (No off-branch claim.)

  2. Perturb. exists_overlap_connectors dodges each breakpoint δ(k/n) to a nearby off-branch p k, with a flat-ended connector cc k : δ(k/n) → p k confined to *both* adjacent sub-balls.

  3. Detour + glue. exists_offBranch_detour_piece builds, per piece, an off-branch detour p k → p(k+1) confined to ball k; OfCurveSkeleton.uniformGlue glues them into a closed smooth loop δ' avoiding branchLocus f (wrap p n = p 0 from δ 1 = δ 0).

  4. Period equality. On piece k, working with the *single* ball-k holomorphic primitive F of chartFormCoeff (x k) i (intervalIntegral_form_pathSpeed_eq_primitive_diff_of_primitive): ∫δ'|ₖ − ∫δ|ₖ = corr(k+1) − corr(k), where corr(j) := ∫₀¹ ωᵢ(cc j) is the intrinsic line integral of the connector (the same value in either adjacent ball, since cc j lies in the overlap). The corrections telescope to corr(n) − corr(0) = 0 (cc n = cc 0), giving periodVec δ' = periodVec δ via periodVec_eq_of_partition_integral_telescope.

NO global manifold Stokes / de Rham / homotopy is involved — only the 1-dimensional chart-disk FTC, ball-confined path-independence, and a telescoping sum. Consumers (exists_preimageCycle_of_nonconstant, …sheets_eq_fibreCard_…) require the period vector *literally* equal (threaded through PreimageCycle.congr_periodVec), which this provides.

theorem exists_loop_off_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ) :
    ∃ δ', IsClosedSmoothLoop δ' ∧ periodVec δ' = periodVec δ ∧
      (∀ t : ℝ, δ' t ∉ branchLocus f)

exists_continuous_lift_off_branchLocus

Continuous path-lift off the branch locus. A path δ in Y that avoids the branch locus lifts, through the covering (univ \ branchLocus f).restrictPreimage f, to a continuous path Γ in X with f (Γ t) = δ t on [0,1] and prescribed start Γ 0 = e (any fibre point over δ 0). The lift is Mathlib's IsCoveringMap.liftPath, repackaged from the unit interval to ℝ → X via Set.projIcc. Foundation for the smooth-loop assembly (§3 sub-piece A).

The lift is Set.projIcc-clamped, so it is constant outside [0,1] (= e on (-∞,0], = Γ 1 on [1,∞)); these two facts are exposed in the conclusion — they give the two-sided endpoint control the seam-flattening construction needs.

theorem exists_continuous_lift_off_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (δ : ℝ → Y) (hδ_cont : Continuous δ) (havoid : ∀ t : ℝ, δ t ∉ branchLocus f)
    {e : X} (he : f e = δ 0) :
    ∃ Γ : ℝ → X, Continuous Γ ∧ (∀ t ∈ Set.Icc (0:ℝ) 1, f (Γ t) = δ t) ∧ Γ 0 = e ∧
      (∀ t : ℝ, t ≤ 0 → Γ t = e) ∧ (∀ t : ℝ, 1 ≤ t → Γ t = Γ 1)

flatEndReparam

A smooth reparametrization of the unit interval, constant near the endpoints: flatEndReparam t = Real.smoothTransition (2 t - 1/2). It is ≡ 0 on (-∞, 1/4], ≡ 1 on [3/4, ∞), smooth, monotone, maps [0,1] into [0,1], and fixes the endpoints (0 ↦ 0, 1 ↦ 1). The end plateaus are what make a lift of δ ∘ flatEndReparam constant near the seam.

noncomputable def flatEndReparam (t : ℝ) : ℝ

flatEndReparam_zero

@[simp] theorem flatEndReparam_zero : flatEndReparam 0 = 0

flatEndReparam_one

@[simp] theorem flatEndReparam_one : flatEndReparam 1 = 1

flatEndReparam_eqZero_of_le

flatEndReparam is ≡ 0 on the left plateau (-∞, 1/4].

theorem flatEndReparam_eqZero_of_le {t : ℝ} (ht : t ≤ 1 / 4) : flatEndReparam t = 0

flatEndReparam_eqOne_of_ge

flatEndReparam is ≡ 1 on the right plateau [3/4, ∞).

theorem flatEndReparam_eqOne_of_ge {t : ℝ} (ht : 3 / 4 ≤ t) : flatEndReparam t = 1

flatEndReparam_mem_unit

theorem flatEndReparam_mem_unit (t : ℝ) : flatEndReparam t ∈ Set.Icc (0 : ℝ) 1

contDiff_flatEndReparam

theorem contDiff_flatEndReparam {n : ℕ∞} : ContDiff ℝ n flatEndReparam

differentiable_flatEndReparam

theorem differentiable_flatEndReparam : Differentiable ℝ flatEndReparam

flatEndReparam_hasDerivAt

theorem flatEndReparam_hasDerivAt (t : ℝ) :
    HasDerivAt flatEndReparam (deriv flatEndReparam t) t

flatEndReparam_monotone

theorem flatEndReparam_monotone : Monotone flatEndReparam

flatEndReparam_image_Icc

theorem flatEndReparam_image_Icc : flatEndReparam '' Set.Icc (0:ℝ) 1 = Set.Icc 0 1

pathSpeed_flatEndReparam_comp_eq

Reparametrized pathSpeed (chain rule): pathSpeed (γ ∘ flatEndReparam) t = flatEndReparam'(t) · pathSpeed γ (flatEndReparam t). Mirrors pathSpeed_smoothStep01_comp_eq.

theorem pathSpeed_flatEndReparam_comp_eq {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (γ : ℝ → X) (t : ℝ)
    (hγ_diff : DifferentiableAt ℝ
      ((chartAt (H := ℂ) (γ (flatEndReparam t))).toFun ∘ γ) (flatEndReparam t)) :
    pathSpeed (γ ∘ flatEndReparam) t =
      ((deriv flatEndReparam t : ℝ) : ℂ) * pathSpeed γ (flatEndReparam t)

lineIntegral_comp_flatEndReparam

Reparametrization-invariance of the line integral (the textbook monotone change of variables). Reparametrizing a (regular, integrable) path by the monotone flatEndReparam leaves the line integral unchanged. Uses Mathlib's measure-theoretic monotone CoV integral_image_eq_integral_deriv_smul_of_monotoneOn (valid for merely *integrable* integrands — no C¹ needed), exactly the value-level companion of the smoothStep01 integrability argument in isSmoothPath_smoothPathSmooth. The key to transporting the preimage-cycle construction from δ∘flatEndReparam back to δ.

theorem lineIntegral_comp_flatEndReparam {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (α : HolomorphicOneForms X) (γ : ℝ → X)
    (hγ_diff : ∀ t ∈ Set.uIcc (0:ℝ) 1,
      DifferentiableAt ℝ ((chartAt (H := ℂ) (γ t)).toFun ∘ γ) t) :
    lineIntegral α (γ ∘ flatEndReparam) = lineIntegral α γ

periodVec_comp_flatEndReparam

Period vector is flatEndReparam-invariant. A closed smooth loop and its seam-flattened reparametrization γ ∘ flatEndReparam have the same period vector (componentwise lineIntegral_comp_flatEndReparam). This is what lets the preimage-cycle construction, carried out for δ ∘ flatEndReparam, transport back to δ (via PreimageCycle.congr_periodVec).

theorem periodVec_comp_flatEndReparam {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (γ : ℝ → X)
    (hγ : IsClosedSmoothLoop γ) :
    periodVec (γ ∘ flatEndReparam) = periodVec γ

lineIntegral_congr_of_eqOn

Line integral depends only on the path's values on [0,1]. Two paths agreeing on [0,1] have equal line integrals: the integrand (value + pathSpeed, a germ at t) agrees on the open interior (0,1) — where [0,1] is a neighborhood — hence a.e. on (0,1]. The endpoints, where the germ leaks outside [0,1], are a null set. Gives the single-lift pushforward lineIntegral α (f∘Γ) = lineIntegral α δr since a lift satisfies f∘Γ = δr on [0,1].

theorem lineIntegral_congr_of_eqOn {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (α : HolomorphicOneForms X)
    {g₁ g₂ : ℝ → X}
    (h : Set.EqOn g₁ g₂ (Set.Icc (0:ℝ) 1)) :
    lineIntegral α g₁ = lineIntegral α g₂

periodVec_congr_of_eqOn

Period vector depends only on the loop's values on [0,1]. Componentwise lineIntegral_congr_of_eqOn.

theorem periodVec_congr_of_eqOn {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {g₁ g₂ : ℝ → X}
    (h : Set.EqOn g₁ g₂ (Set.Icc (0:ℝ) 1)) : periodVec g₁ = periodVec g₂

differentiableAt_chart_lift_of_notMem_criticalSet

§3 sub-piece B — smoothness of the lift. A continuous lift Γ of δ through a non-critical point inherits δ's chart-pullback differentiability. Given Γ continuous at t₀, f ∘ Γ = δ near t₀, Γ t₀ off the critical set, and δ chart-pullback-differentiable at t₀, the lift Γ is chart-pullback differentiable at t₀.

Proof: take the two-sided local inverse g at Γ t₀ (exists_twoSided_localInverse). Near t₀, Γ = g ∘ δ directly from g∘f=id near Γ t₀ + continuity of Γ + f∘Γ=δ (no lift-uniqueness needed). In charts, (chart_Γt₀)∘Γ =ᶠ G∘d where G = (chart_Γt₀)∘g∘(chart_δt₀).symm is the chart representation of the holomorphic g and d = (chart_δt₀)∘δ. G is ℂ-, hence ℝ-differentiable (via writtenInExtChartAt + restrictScalars), so the chain rule and congr_of_eventuallyEq conclude. Mirrors IsClosedSmoothLoop.comp / pathSpeed_comp_eq_mfderiv. Foundation for assembling the lift into a smooth loop.

theorem differentiableAt_chart_lift_of_notMem_criticalSet {X Y : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [Nonempty Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (δ : ℝ → Y) (Γ : ℝ → X) {t₀ : ℝ}
    (hΓ_cont : ContinuousAt Γ t₀)
    (hfΓδ : ∀ᶠ t in 𝓝 t₀, f (Γ t) = δ t)
    (hΓcrit : Γ t₀ ∉ criticalSet f)
    (hδ_diff : DifferentiableAt ℝ ((chartAt (H := ℂ) (δ t₀)).toFun ∘ δ) t₀) :
    DifferentiableAt ℝ ((chartAt (H := ℂ) (Γ t₀)).toFun ∘ Γ) t₀

exists_smoothLift_flatEnd_off_branchLocus

§3 sub-piece C — the seam-flattened smooth lift. Lifting the *reparametrized* loop δ ∘ flatEndReparam (constant near 0,1) off the branch locus from a fibre point e yields a genuine smooth path with zero endpoint velocity:

  • Γ is constant = e near 0 and constant = Γ 1 near 1 (continuity + local injectivity of f, using the lift's projIcc clamp), so it is chart-differentiable with zero velocity at both endpoints;

  • on the interior (0,1), Γ is chart-differentiable by sub-piece B;

  • its velocity tangent-section is ContinuousOn [0,1] (velCont): off the endpoints via velContWithinAt_compOn (each interior point lies in a local two-sided inverse g's domain, where Γ =ᶠ g ∘ δr), and at the seam-flat ends via velsection_eventuallyEq_of_eventuallyEq against the constant path — so Γ is a full IsSmoothPath, not merely chart-differentiable;

  • its endpoint Γ 1 lies in the same fibre (f (Γ 1) = δ 0), the monodromy target.

This is the per-segment building block of the orbit construction: concatenating these over a monodromy orbit (zero junction velocities ⇒ IsSmoothPath.concat) closes the lift into a smooth loop. The base loop is δ ∘ flatEndReparam, a reparametrization of δ (its period vector is unchanged — recorded separately).

theorem exists_smoothLift_flatEnd_off_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ) (havoid : ∀ t : ℝ, δ t ∉ branchLocus f)
    {e : X} (he : f e = δ 0) :
    ∃ Γ : ℝ → X,
      Continuous Γ ∧ Γ 0 = e ∧
      (∀ t ∈ Set.Icc (0:ℝ) 1, f (Γ t) = δ (flatEndReparam t)) ∧
      (∀ t ∈ Set.uIcc (0:ℝ) 1, DifferentiableAt ℝ ((chartAt (H := ℂ) (Γ t)).toFun ∘ Γ) t) ∧
      ContinuousOn (fun s : ℝ => Bundle.TotalSpace.mk' ℂ
          (E := TangentSpace 𝓘(ℂ) (M := X)) (Γ s) (pathSpeed Γ s)) (Set.Icc 0 1) ∧
      pathSpeed Γ 0 = 0 ∧ pathSpeed Γ 1 = 0 ∧
      f (Γ 1) = δ 0

MonodromyLiftFamily

Interface for the §3 monodromy construction. A finite family of seam-flattened smooth lifts Γ i of δr = δ ∘ flatEndReparam, whose time-t evaluations i ↦ Γ i t sweep the fibre f⁻¹(δr t) injectively and surjectively for every t ∈ [0,1]. Carrying the whole family at once (rather than local sheets) is what turns the projection formula into a pointwise fibre-sum identity, and the t = 1 bijection is the monodromy permutation driving the orbit loops.

structure MonodromyLiftFamily {X Y : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (f : X → Y) (δ : ℝ → Y) where

MonodromyLiftFamily.n_eq_fibre_ncard

The lift count is the regular-fibre cardinality. At t = 0 the map i ↦ Γ i 0 is a bijection from Fin M.n onto the fibre f⁻¹{δ(flatEndReparam 0)} (injective by fibre_inj, onto by fibre_surj), so M.n equals that fibre's ncard. This is what pins the cycle's sheet count to a *regular* fibre.

lemma MonodromyLiftFamily.n_eq_fibre_ncard {X Y : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {f : X → Y} {δ : ℝ → Y}
    (M : MonodromyLiftFamily f δ) :
    M.n = (f ⁻¹' {δ (flatEndReparam 0)}).ncard

exists_monodromyLiftFamily

Leaf A + B — construct the monodromy lift family. Off the branch locus, the seam-flattened lifts of δ (one per fibre point, exists_smoothLift_flatEnd_off_branchLocus upgraded with velCont) assemble into a MonodromyLiftFamily: injectivity is lift uniqueness, surjectivity is constancy of the off-branch fibre cardinality along the connected [0,1] (via the local sheet system).

theorem exists_monodromyLiftFamily {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ) (havoid : ∀ t : ℝ, δ t ∉ branchLocus f) :
    Nonempty (MonodromyLiftFamily f δ)

lineIntegral_traceFormTotal_eq_sum_periodVec

Leaf D — projection formula (pointwise fibre-sum). The line integral of the trace form along δ equals the sum, over the lift family, of the lift periods: ∫_δ traceFormTotal(ωⱼ) = ∑ᵢ periodVec(Γ i) j. Reparametrize to δr, then integrate the pointwise identity traceFun f ωⱼ (δr t)(δr' t) = ∑ᵢ ωⱼ(Γ i t)(Γ i' t) (the trace fibre-sum reindexed by the time-t bijection i ↦ Γ i t, each summand the pullback covector with (mfderiv f)⁻¹ (δr' t) = pathSpeed (Γ i) t).

theorem lineIntegral_traceFormTotal_eq_sum_periodVec {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ) (havoid : ∀ t : ℝ, δ t ∉ branchLocus f)
    (M : MonodromyLiftFamily f δ) (j : Fin (genus X)) :
    lineIntegral (traceFormTotal f hf (periodBasisForm X j)) δ
      = ∑ i, periodVec (M.Γ i) j

IsSmoothPath.comp

Push a smooth path forward by a global C^ω map. f ∘ γ is a smooth path from f P to f Q: continuity by composition; chart-pullback differentiability via the chart-local representation f_loc = chartY ∘ f ∘ chartX.symm (holomorphic ⟹ ℝ-diff by restrictScalars, as in differentiableAt_chart_lift_of_notMem_criticalSet); velCont by velCont_comp. The orbit loops push to multiples of δ, so f ∘ (orbit loop) must be a smooth path for the period accounting.

theorem IsSmoothPath.comp {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    {P Q : X} {γ : ℝ → X} (hγ : IsSmoothPath P Q γ) :
    IsSmoothPath (f P) (f Q) (f ∘ γ) where

exists_orbitLoops_of_monodromyLiftFamily

Leaf E — orbit loops. Group the lift family into closed smooth loops along the orbits of the monodromy permutation σ i := the index with Γ (σ i) 0 = Γ i 1 (bijective by fibre_inj/fibre_surj at t = 1): each orbit gives the iterated concat of its lifts (a closed loop — junction velocities 0 — smooth by velCont_concat). With all coeffs = 1 and sheets = M.n, period accounting gives the two identities: ∑ orbit-periods = ∑ᵢ periodVec(Γ i) (orbit partition + periodVec_concat_of_smooth), and ∑ periodVec(f ∘ loop) = M.n • periodVec δ (each f ∘ Γ i = δr so each orbit pushes to (orbit length) • periodVec δ).

theorem exists_orbitLoops_of_monodromyLiftFamily {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ)
    (M : MonodromyLiftFamily f δ) :
    ∃ (m : ℕ) (loops : Fin m → ℝ → X) (coeffs : Fin m → ℤ),
      (∀ i, IsClosedSmoothLoop (loops i)) ∧
      (∑ i, coeffs i • periodVec (loops i) = ∑ i, periodVec (M.Γ i)) ∧
      (∑ i, coeffs i • periodVec (f ∘ loops i) = (M.n : ℤ) • periodVec δ)

exists_preimageLoopFamily

[open] — geometric heart of the preimage-cycle lift. The monodromy/orbit construction, stated purely in elementary line-integral / period-vector terms (no ambient-coordinate ambientPullbackJac): off the branch locus, δ lifts to a finite ℤ-family of closed smooth loops realizing

  • the projection identity ∫_δ traceFormTotal(ωⱼ^X) = ∑ᵢ coeffsᵢ • periodVec(loopsᵢ)ⱼ (the per-component pullback, before coordinatization), and

  • the pushforward identity ∑ᵢ coeffsᵢ • periodVec(f∘loopsᵢ) = sheets • periodVec δ.

The reduction exists_preimageCycle_of_off_branchLocus below turns this into a PreimageCycle via the coordinate bridge ambientPullbackJac_periodVec_apply_eq_lineIntegral_traceFormTotal — so this lemma isolates exactly the geometry.

Ingredients:

  • the seam-flattened smooth lifts exists_smoothLift_flatEnd_off_branchLocus, one per fibre point (fiber_finite_off_branchLocus ⇒ Fintype), assembled into a monodromy permutation via lift uniqueness (IsCoveringMap.eq_liftPath_iff) and concatenated over its orbits (IsSmoothPath.concat, junction velocities zero);

  • the partition/sheet-reassembly projection formula (exists_nbhd_cover + exists_localSheetSystem_traceForm_eq_sum + lineIntegral_pullback_section);

  • the line-integral reparametrization-invariance periodVec (δ∘flatEndReparam) = periodVec δ (periodVec_comp_flatEndReparam, monotone change-of-variables for *integrable* integrands), with the lifts' integrability from the C¹ loop predicate (IsClosedSmoothLoop carries velCont; a local-section lift g∘δr gets its velCont from velCont_compOn, whence integrable).

theorem exists_preimageLoopFamily {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ) (havoid : ∀ t : ℝ, δ t ∉ branchLocus f) :
    ∃ (m : ℕ) (loops : Fin m → ℝ → X) (coeffs : Fin m → ℤ) (sheets : ℕ),
      (∀ i, IsClosedSmoothLoop (loops i)) ∧
      (fun j => lineIntegral (traceFormTotal f hf (periodBasisForm X j)) δ) =
        ∑ i, coeffs i • periodVec (loops i) ∧
      ∑ i, coeffs i • periodVec (f ∘ loops i) = (sheets : ℤ) • periodVec δ

exists_preimageCycle_of_off_branchLocus

A closed smooth loop off the branch locus lifts to a preimage cycle. Takes the elementary geometric loop family exists_preimageLoopFamily and packages it as a PreimageCycle; the only nontrivial step is the projection identity's conversion from the line-integral form ∫_δ trace(ωⱼ) to the ambient pullback (ambientPullbackJac f hf (periodVec δ))ⱼ via the bridge ambientPullbackJac_periodVec_apply_eq_lineIntegral_traceFormTotal (integrability supplied by hδ.integrable).

theorem exists_preimageCycle_of_off_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ) (havoid : ∀ t : ℝ, δ t ∉ branchLocus f) :
    Nonempty (PreimageCycle f hf δ)

PreimageCycle.congr_periodVec

A PreimageCycle depends on δ only through periodVec δ (the only places δ enters the data are the pullback/pushforward identities, whose δ-dependence is exactly through periodVec δ). Transporting along a period-vector equality reuses the same loops/coeffs.

def PreimageCycle.congr_periodVec {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] {f : X → Y} {hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f}
    {δ δ' : ℝ → Y} (h : periodVec δ = periodVec δ') (c : PreimageCycle f hf δ') :
    PreimageCycle f hf δ where

exists_preimageCycle_of_nonconstant

exists_preimageCycle_of_nonconstant, assembled: homotope δ off the branch locus, lift it to a preimage cycle, and transport back along the period-vector equality (congr_periodVec).

theorem exists_preimageCycle_of_nonconstant {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ) :
    Nonempty (PreimageCycle f hf δ)

notMem_criticalValuesGeneral_of_notMem_branchLocus

A value off the branch locus is off the (defeq) general critical-value set criticalValuesGeneral. (branchLocus f = f '' criticalSet f = f '' criticalSetGeneral f = criticalValuesGeneral f by definition.)

theorem notMem_criticalValuesGeneral_of_notMem_branchLocus {X Y : Type*} [TopologicalSpace X]
    {f : X → Y} {y : Y}
    (h : y ∉ branchLocus f) :
    y ∉ Jacobians.Discharge.Manifold.criticalValuesGeneral f

exists_preimageCycle_sheets_eq_fibreCard_of_off_branchLocus

Strengthened off-branch cycle. Beyond the PreimageCycle, returns a *regular value* y₀ (off the branch locus) whose fibre has cardinality equal to the cycle's sheets. This exposes sheets = #(regular fibre), the bridge identifying sheets with the analytic degree degreeFiber. Built exactly like exists_preimageCycle_of_off_branchLocus, but keeping the monodromy family M in scope so its n = #fibre (M.n_eq_fibre_ncard) can be read off.

theorem exists_preimageCycle_sheets_eq_fibreCard_of_off_branchLocus {X Y : Type*}
    [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y]
    [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ) (havoid : ∀ t : ℝ, δ t ∉ branchLocus f) :
    ∃ (c : PreimageCycle f hf δ) (y₀ : Y),
      y₀ ∉ branchLocus f ∧ c.sheets = (f ⁻¹' {y₀}).ncard

exists_preimageCycle_sheets_eq_fibreCard_of_nonconstant

Strengthened cycle for any non-constant f. Combines exists_preimageCycle_sheets_eq_fibreCard_of_off_branchLocus with the off-branch homotopy; congr_periodVec carries sheets (and hence the fibre-cardinality identity) across.

theorem exists_preimageCycle_sheets_eq_fibreCard_of_nonconstant {X Y : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [Nonempty Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ) :
    ∃ (c : PreimageCycle f hf δ) (y₀ : Y),
      y₀ ∉ branchLocus f ∧ c.sheets = (f ⁻¹' {y₀}).ncard

ambientPullbackJac_periodVec_mem_truePeriodLattice

Pullback identity — member case. For a closed smooth loop δ in Y, the genuine pullback ambientPullbackJac (periodVec δ) lies in truePeriodLattice X. Case-splits on constancy of f:

  • If f is constant, ambientPullbackJac f hf = 0 (ambientPullbackJac_eq_zero_of_const), so the image is 0.

  • If f is non-constant, extract a preimage cycle witness via exists_preimageCycle_of_nonconstant, then apply the algebraic reduction ambientPullbackJac_periodVec_mem_truePeriodLattice_of_preimageCycle.

theorem ambientPullbackJac_periodVec_mem_truePeriodLattice {X Y : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [Nonempty Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (δ : ℝ → Y) (hδ : IsClosedSmoothLoop δ) :
    ambientPullbackJac (gX := genus X) (gY := genus Y) f hf (periodVec δ) ∈
      truePeriodLattice X

ambientPullbackJac_preserves_truePeriodLattice

ambientPullbackJac (the genuine Jacobian pullback Tᵀ) preserves the period lattice. Reduces to ambientPullbackJac_periodVec_mem_truePeriodLattice on closed-loop generators, extended to the ℤ-span by Submodule.span_induction and ℤ-linearity. Discharges Jacobian.ambientPullbackJac_preserves_lattice.

theorem ambientPullbackJac_preserves_truePeriodLattice {X Y : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [Nonempty Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) :
    (truePeriodLattice Y).toAddSubgroup ≤
      (truePeriodLattice X).toAddSubgroup.comap
        (ambientPullbackJac (gX := genus X) (gY := genus Y) f hf).toAddMonoidHom