Modular Forms — Hungerbühler–Wasem & Valence Formula in Lean

5. The Hungerbühler–Wasem generalised residue theorem🔗

In this chapter we present the dependency chain culminating in the fully discharged paper-faithful form of the Hungerbühler–Wasem generalised residue theorem (Hungerbühler–Wasem 2018, Theorem 3.3). The headline statement asserts that the multi-point Cauchy principal value of f along a closed null-homologous piecewise-C^{1} immersion equals a weighted sum of residues, where the weights are the generalised winding numbers. The proof proceeds by reducing to the per-pole problem, splitting each pole into its simple and higher-order Laurent contributions, and handling the higher-order part by the sector-cancellation identity under condition (B).

Theorem5.1
Statement uses 6
Statement dependency previews
Preview
Definition 1.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

Let U \subseteq \mathbb{C} be a non-empty open set, S \subseteq U a finite set, and f : \mathbb{C} \to \mathbb{C} a function. Assume:

  • f is holomorphic on U \setminus S and meromorphic at every point of S;

  • \gamma is a closed piecewise-C^{1} immersion based at x \in U, with x \notin S;

  • \gamma is null-homologous in U;

  • (\gamma, f) satisfies condition (B) relative to S;

  • \gamma satisfies condition (A') relative to S with \operatorname{poleOrder}(s) equal to the order of the polar part of f at s provided by the canonical polar-part decomposition.

Then the multi-point Cauchy principal value of \oint_\gamma f exists and equals \operatorname{PV}_S\!\!\int_\gamma f(z)\,\mathrm{d}z \;=\; \sum_{s \in S} 2 \pi i \, \operatorname{gWN}(\gamma, s) \, \operatorname{Res}(f, s).

Definition 1.1 Definition 1.2 Definition 2.1 Definition 3.1 Definition 4.1 Definition 4.2

Lean code for Theorem5.1●1 theorem
  • theoremdefined in LeanModularForms/ForMathlib/HungerbuhlerWasem/MultiCrossingCPV.lean
    complete
    theorem HungerbuhlerWasem.residueTheorem_crossing_paper_faithful_clean {x : ℂ}
  {U : Set ℂ} (hU_open : IsOpen U) (hU_ne : U.Nonempty) {S : Finset ℂ}
  (hS_in_U : ↑S ⊆ U) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (U \ ↑S))
  (γ : ClosedPwC1Immersion x)
  (h_null : IsNullHomologous γ.toPwC1Immersion U)
  (hMero : ∀ s ∈ S, MeromorphicAt f s)
  (hCondB : SatisfiesConditionB γ.toPwC1Immersion f S)
  (hCondA :
    SatisfiesConditionA' γ.toPwC1Immersion f S fun s ↦
      (HungerbuhlerWasem.PolarPartDecomposition.ofMeromorphicWithCondB
            hU_open hS_in_U hf hMero hCondB).order
        s)
  (hx_notin_S : x ∉ ↑S) :
  HasCauchyPVOn S f γ.toPwC1Immersion.toPiecewiseC1Path
    (∑ s ∈ S,
      2 * ↑Real.pi * Complex.I *
          generalizedWindingNumber γ.toPwC1Immersion.toPiecewiseC1Path
            s *
        residue f s)
    theorem HungerbuhlerWasem.residueTheorem_crossing_paper_faithful_clean
  {x : ℂ} {U : Set ℂ} (hU_open : IsOpen U)
  (hU_ne : U.Nonempty) {S : Finset ℂ}
  (hS_in_U : ↑S ⊆ U) {f : ℂ → ℂ}
  (hf : DifferentiableOn ℂ f (U \ ↑S))
  (γ : ClosedPwC1Immersion x)
  (h_null :
    IsNullHomologous γ.toPwC1Immersion U)
  (hMero : ∀ s ∈ S, MeromorphicAt f s)
  (hCondB :
    SatisfiesConditionB γ.toPwC1Immersion
      f S)
  (hCondA :
    SatisfiesConditionA' γ.toPwC1Immersion
      f S fun s ↦
      (HungerbuhlerWasem.PolarPartDecomposition.ofMeromorphicWithCondB
            hU_open hS_in_U hf hMero
            hCondB).order
        s)
  (hx_notin_S : x ∉ ↑S) :
  HasCauchyPVOn S f
    γ.toPwC1Immersion.toPiecewiseC1Path
    (∑ s ∈ S,
      2 * ↑Real.pi * Complex.I *
          generalizedWindingNumber
            γ.toPwC1Immersion.toPiecewiseC1Path
            s *
        residue f s)
    **HW3.3 — Corner-friendly clean spec form (T-BR-Y11c).**

The clean version of `residueTheorem_crossing_paper_faithful` admitting
BOTH multi-crossings AND corner crossings, with the eight paper spec
hypotheses plus a basepoint-off residual `hx_notin_S`. The per-pole
simple-pole CPV existence hypothesis is auto-discharged internally via
`hasCauchyPV_inv_sub_multiCrossing_corner`.
Proof for Theorem 5.1
Proof uses 3
Proof dependency previews
Preview
Theorem 5.2
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

By extracting the canonical polar-part decomposition of f over S in U from the condition-(B) data, we reduce to the compositional residue theorem (Theorem 5.2). That reduction in turn requires, for each s \in S, an explicit per-pole Cauchy principal value identity for the polar part. We split the proof of those identities into two cases:

  • if \gamma avoids the pole s on [0,1], the polar part is regular along \gamma, and the principal value coincides with the ordinary contour integral; this is Theorem 5.3;

  • otherwise the set of crossings of \gamma at s is a finite subset of (0,1) (its finiteness uses x \notin S); we then combine the corner-friendly multi-crossing CPV identity Theorem 5.4 with the canonical right/left tangent limits at each crossing.

Together these per-pole identities, applied to every s \in S, combine via the compositional theorem to yield the stated equality.

Theorem 5.2 Theorem 5.3 Theorem 5.4

Theorem5.2
Statement uses 4
Statement dependency previews
Preview
Definition 1.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

Let U \subseteq \mathbb{C} be a non-empty open set, S \subseteq U a finite set, f : \mathbb{C} \to \mathbb{C} holomorphic on U \setminus S, and \gamma a closed piecewise-C^{1} immersion based at x \in U that is null-homologous in U. Assume that f admits a polar-part decomposition f(z) = h(z) + \sum_{s \in S} P_s(z), where each P_s is the Laurent polar part at s and h is the analytic remainder, and that for each s \in S the polar part has principal value \operatorname{PV}_S\!\!\int_\gamma P_s(z)\,\mathrm{d}z \;=\; 2 \pi i \, \operatorname{gWN}(\gamma, s) \, \operatorname{Res}(f, s). Then \operatorname{PV}_S\!\!\int_\gamma f(z)\,\mathrm{d}z \;=\; \sum_{s \in S} 2 \pi i \, \operatorname{gWN}(\gamma, s) \, \operatorname{Res}(f, s).

Definition 1.1 Definition 1.2 Definition 2.1 Definition 3.1

Lean code for Theorem5.2●1 theorem
  • theoremdefined in LeanModularForms/ForMathlib/HungerbuhlerWasem/Crossing.lean
    complete
    theorem HungerbuhlerWasem.residueTheorem_crossing_compositional {x : ℂ}
  {U : Set ℂ} (hU_open : IsOpen U) (hU_ne : U.Nonempty) (S : Finset ℂ)
  (hS_in_U : ↑S ⊆ U) (f : ℂ → ℂ) (_hf : DifferentiableOn ℂ f (U \ ↑S))
  (γ : ClosedPwC1Immersion x)
  (h_null : IsNullHomologous γ.toPwC1Immersion U)
  (decomp : HungerbuhlerWasem.PolarPartDecomposition f S U)
  (h_polar_cpv :
    ∀ s ∈ S,
      HasCauchyPVOn S (decomp.polarPart s)
        γ.toPwC1Immersion.toPiecewiseC1Path
        (2 * ↑Real.pi * Complex.I *
            generalizedWindingNumber γ.toPwC1Immersion.toPiecewiseC1Path
              s *
          residue f s)) :
  HasCauchyPVOn S f γ.toPwC1Immersion.toPiecewiseC1Path
    (∑ s ∈ S,
      2 * ↑Real.pi * Complex.I *
          generalizedWindingNumber γ.toPwC1Immersion.toPiecewiseC1Path
            s *
        residue f s)
    theorem HungerbuhlerWasem.residueTheorem_crossing_compositional
  {x : ℂ} {U : Set ℂ} (hU_open : IsOpen U)
  (hU_ne : U.Nonempty) (S : Finset ℂ)
  (hS_in_U : ↑S ⊆ U) (f : ℂ → ℂ)
  (_hf : DifferentiableOn ℂ f (U \ ↑S))
  (γ : ClosedPwC1Immersion x)
  (h_null :
    IsNullHomologous γ.toPwC1Immersion U)
  (decomp :
    HungerbuhlerWasem.PolarPartDecomposition
      f S U)
  (h_polar_cpv :
    ∀ s ∈ S,
      HasCauchyPVOn S (decomp.polarPart s)
        γ.toPwC1Immersion.toPiecewiseC1Path
        (2 * ↑Real.pi * Complex.I *
            generalizedWindingNumber
              γ.toPwC1Immersion.toPiecewiseC1Path
              s *
          residue f s)) :
  HasCauchyPVOn S f
    γ.toPwC1Immersion.toPiecewiseC1Path
    (∑ s ∈ S,
      2 * ↑Real.pi * Complex.I *
          generalizedWindingNumber
            γ.toPwC1Immersion.toPiecewiseC1Path
            s *
        residue f s)
    **Hungerbühler–Wasem Theorem 3.3 — compositional crossing form.**

For `f` with a `PolarPartDecomposition` over `S ⊆ U` and a closed γ
null-homologous in `U` (which may cross poles of any order), the multi-point
Cauchy principal value of `∮f` along `γ` equals
`∑ s ∈ S, 2πi · w(γ, s) · residue f s`.

Per-pole CPV witnesses for each polar part — typically obtained from
`cpv_polarPart_at_pole_under_conditions` (T-GL-01) — are supplied as data.
The analytic-remainder CPV and integrability are derived internally from
`analyticRemainder_hasCauchyPVOn_zero` and
`cpvIntegrandOn_diff_intervalIntegrable`. The avoidance form
`residueTheorem_avoidance` is the special case where the per-pole witnesses
come from `hasCauchyPVOn_of_avoids`.

This is the *compositional* form: it consumes a `PolarPartDecomposition` and
per-pole CPV witnesses as data.
Proof for Theorem 5.2
uses 0

The analytic remainder h has principal value zero by Dixon's theorem applied to the null-homologous \gamma together with the observation that the multi-point CPV-cutoff integral of an analytic function on U along a null-homologous curve tends to the contour integral of h, which vanishes. Adding this to the assumed per-pole identities, and exchanging finite sum with the \varepsilon \to 0^{+} limit, gives the result. The exchange-of-limit step is justified by the integrability of each cutoff integrand on [0,1], which holds because the polar parts are continuous off their poles and h is continuous everywhere.

Theorem5.3
Statement uses 4
Statement dependency previews
Preview
Definition 1.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

Let U \subseteq \mathbb{C} be open, S \subseteq U finite, and f : \mathbb{C} \to \mathbb{C} with polar-part decomposition over S in U. Let \gamma be a closed piecewise-C^{1} immersion null-homologous in U, and let s \in S be a pole that \gamma avoids: \gamma(t) \ne s for every t \in [0,1]. Then the polar part at s has multi-point Cauchy principal value \operatorname{PV}_S\!\!\int_\gamma P_s(z)\,\mathrm{d}z \;=\; 2 \pi i \, \operatorname{gWN}(\gamma, s) \, \operatorname{Res}(f, s).

Definition 1.1 Definition 1.2 Definition 2.1 Definition 3.1

Lean code for Theorem5.3●1 theorem
  • theoremdefined in LeanModularForms/ForMathlib/HungerbuhlerWasem/Crossing.lean
    complete
    theorem HungerbuhlerWasem.cpv_polarPart_at_uncrossed_pole {x : ℂ} {U : Set ℂ}
  (_hU_open : IsOpen U) (_hU_ne : U.Nonempty) {S : Finset ℂ}
  (hS_in_U : ↑S ⊆ U) {f : ℂ → ℂ} (γ : ClosedPwC1Immersion x)
  (h_null : IsNullHomologous γ.toPwC1Immersion U)
  (decomp : HungerbuhlerWasem.PolarPartDecomposition f S U) (s : ℂ)
  (hs : s ∈ S)
  (h_avoid : ∀ t ∈ Set.Icc 0 1, γ.toPwC1Immersion.extendedPath t ≠ s) :
  HasCauchyPVOn S (decomp.polarPart s)
    γ.toPwC1Immersion.toPiecewiseC1Path
    (2 * ↑Real.pi * Complex.I *
        generalizedWindingNumber γ.toPwC1Immersion.toPiecewiseC1Path s *
      residue f s)
    theorem HungerbuhlerWasem.cpv_polarPart_at_uncrossed_pole
  {x : ℂ} {U : Set ℂ}
  (_hU_open : IsOpen U)
  (_hU_ne : U.Nonempty) {S : Finset ℂ}
  (hS_in_U : ↑S ⊆ U) {f : ℂ → ℂ}
  (γ : ClosedPwC1Immersion x)
  (h_null :
    IsNullHomologous γ.toPwC1Immersion U)
  (decomp :
    HungerbuhlerWasem.PolarPartDecomposition
      f S U)
  (s : ℂ) (hs : s ∈ S)
  (h_avoid :
    ∀ t ∈ Set.Icc 0 1,
      γ.toPwC1Immersion.extendedPath t ≠
        s) :
  HasCauchyPVOn S (decomp.polarPart s)
    γ.toPwC1Immersion.toPiecewiseC1Path
    (2 * ↑Real.pi * Complex.I *
        generalizedWindingNumber
          γ.toPwC1Immersion.toPiecewiseC1Path
          s *
      residue f s)
    **Per-pole CPV at an uncrossed pole.** When γ avoids the pole `s`, the polar
part `decomp.polarPart s` is regular along γ, and DCT gives that the multi-point
CPV equals the contour integral of the polar part along γ. The contour integral
in turn equals `2πi · w · res f s` by the avoidance computation
(`residueTheorem_avoidance` per-pole step).
Proof for Theorem 5.3
uses 0

Since \gamma avoids s, the distance from \gamma to s is bounded below by some \delta > 0 by compactness of the image. For \varepsilon < \delta the multi-point cutoff integrand for the polar part coincides with the ordinary integrand on all of [0,1], so the cutoff integrals are eventually constant in \varepsilon and equal to the contour integral \int_\gamma P_s(z)\,\mathrm{d}z. The dominated-convergence argument therefore reduces to evaluating the contour integral of P_s on \gamma, and the avoidance computation identifies this with 2\pi i \, \operatorname{gWN}(\gamma, s) \, \operatorname{Res}(f, s).

Theorem5.4
Statement uses 5
Statement dependency previews
Preview
Definition 1.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

Let \gamma be a closed piecewise-C^{1} immersion at x, let s \in S be a pole at which the polar part of f has order N, and let \operatorname{crossings} = \{ t \in (0,1) : \gamma(t) = s \} be a finite (corner-allowing) crossing set. Assume the following data on \operatorname{crossings}:

  • at every t \in \operatorname{crossings} the curve \gamma is flat of order N (the condition (A') witness);

  • right and left tangent limits L_+(t), L_-(t) \in \mathbb{C}^{\times} exist;

  • the angle-compatibility identity from condition (B) \bigl(L_+(t) / |L_+(t)|\bigr)^{k} = \bigl(-L_-(t) / |L_-(t)|\bigr)^{k} holds for every k \ge 1 at which the Laurent coefficient a_k at s is non-zero;

  • the simple-pole Cauchy principal value of (z - s)^{-1} along \gamma exists.

Then the polar part at s has multi-point CPV \operatorname{PV}_{\{s\}}\!\!\int_\gamma P_s(z)\,\mathrm{d}z \;=\; 2 \pi i \, \operatorname{gWN}(\gamma, s) \, \operatorname{Res}(f, s).

Definition 1.1 Definition 2.1 Definition 3.1 Definition 4.1 Definition 4.2

Lean code for Theorem5.4●1 theorem
  • theoremdefined in LeanModularForms/ForMathlib/HungerbuhlerWasem/MultiCrossingCPV.lean
    complete
    theorem HungerbuhlerWasem.cpv_polarPart_at_multiCrossed_pole_under_condB_corner
  {x : ℂ} {γ : ClosedPwC1Immersion x} {s : ℂ} {S : Finset ℂ}
  (hs : s ∈ S) {f : ℂ → ℂ} {U : Set ℂ}
  (decomp : HungerbuhlerWasem.PolarPartDecomposition f S U)
  {crossings : Finset ℝ} (h_Ioo : ∀ t ∈ crossings, t ∈ Set.Ioo 0 1)
  (h_at : ∀ t ∈ crossings, γ.toPwC1Immersion.toPath.extend t = s)
  (h_complete :
    ∀ t ∈ Set.Icc 0 1,
      γ.toPwC1Immersion.toPath.extend t = s → t ∈ crossings)
  (h_flat_at_each :
    ∀ t₀ ∈ crossings,
      IsFlatOfOrder (⇑γ.toPwC1Immersion.toPath.extend) t₀
        (decomp.order s))
  (L_plus L_minus : ℝ → ℂ) (hL_plus_ne : ∀ t ∈ crossings, L_plus t ≠ 0)
  (hL_minus_ne : ∀ t ∈ crossings, L_minus t ≠ 0)
  (hL_right :
    ∀ t ∈ crossings,
      Filter.Tendsto (deriv ⇑γ.toPwC1Immersion.toPath.extend)
        (nhdsWithin t (Set.Ioi t)) (nhds (L_plus t)))
  (hL_left :
    ∀ t ∈ crossings,
      Filter.Tendsto (deriv ⇑γ.toPwC1Immersion.toPath.extend)
        (nhdsWithin t (Set.Iio t)) (nhds (L_minus t)))
  (h_B :
    ∀ (k : Fin (decomp.order s)),
      1 ≤ ↑k →
        decomp.coeff s k ≠ 0 →
          ∀ t ∈ crossings,
            (L_plus t / ↑‖L_plus t‖) ^ ↑k =
              (-L_minus t / ↑‖L_minus t‖) ^ ↑k)
  (h_simple_cpv :
    ∃ L,
      HasCauchyPV (fun z ↦ (z - s)⁻¹)
        γ.toPwC1Immersion.toPiecewiseC1Path s L) :
  HasCauchyPVOn {s} (decomp.polarPart s)
    γ.toPwC1Immersion.toPiecewiseC1Path
    (2 * ↑Real.pi * Complex.I *
        generalizedWindingNumber γ.toPwC1Immersion.toPiecewiseC1Path s *
      residue f s)
    theorem HungerbuhlerWasem.cpv_polarPart_at_multiCrossed_pole_under_condB_corner
  {x : ℂ} {γ : ClosedPwC1Immersion x}
  {s : ℂ} {S : Finset ℂ} (hs : s ∈ S)
  {f : ℂ → ℂ} {U : Set ℂ}
  (decomp :
    HungerbuhlerWasem.PolarPartDecomposition
      f S U)
  {crossings : Finset ℝ}
  (h_Ioo :
    ∀ t ∈ crossings, t ∈ Set.Ioo 0 1)
  (h_at :
    ∀ t ∈ crossings,
      γ.toPwC1Immersion.toPath.extend t =
        s)
  (h_complete :
    ∀ t ∈ Set.Icc 0 1,
      γ.toPwC1Immersion.toPath.extend t =
          s →
        t ∈ crossings)
  (h_flat_at_each :
    ∀ t₀ ∈ crossings,
      IsFlatOfOrder
        (⇑γ.toPwC1Immersion.toPath.extend)
        t₀ (decomp.order s))
  (L_plus L_minus : ℝ → ℂ)
  (hL_plus_ne :
    ∀ t ∈ crossings, L_plus t ≠ 0)
  (hL_minus_ne :
    ∀ t ∈ crossings, L_minus t ≠ 0)
  (hL_right :
    ∀ t ∈ crossings,
      Filter.Tendsto
        (deriv
          ⇑γ.toPwC1Immersion.toPath.extend)
        (nhdsWithin t (Set.Ioi t))
        (nhds (L_plus t)))
  (hL_left :
    ∀ t ∈ crossings,
      Filter.Tendsto
        (deriv
          ⇑γ.toPwC1Immersion.toPath.extend)
        (nhdsWithin t (Set.Iio t))
        (nhds (L_minus t)))
  (h_B :
    ∀ (k : Fin (decomp.order s)),
      1 ≤ ↑k →
        decomp.coeff s k ≠ 0 →
          ∀ t ∈ crossings,
            (L_plus t / ↑‖L_plus t‖) ^
                ↑k =
              (-L_minus t /
                  ↑‖L_minus t‖) ^
                ↑k)
  (h_simple_cpv :
    ∃ L,
      HasCauchyPV (fun z ↦ (z - s)⁻¹)
        γ.toPwC1Immersion.toPiecewiseC1Path
        s L) :
  HasCauchyPVOn {s} (decomp.polarPart s)
    γ.toPwC1Immersion.toPiecewiseC1Path
    (2 * ↑Real.pi * Complex.I *
        generalizedWindingNumber
          γ.toPwC1Immersion.toPiecewiseC1Path
          s *
      residue f s)
    **Corner-friendly per-pole polar-part multi-crossing CPV (T-BR-Y11b).**

Generalises `cpv_polarPart_at_multiCrossed_pole_under_condB` to admit corner
crossings (no `h_off` per crossing). Takes the simple-pole CPV existence
`h_simple_cpv` as a hypothesis (auto-discharged by smooth-only / single-crossing
machinery for typical callers).
Proof for Theorem 5.4
uses 0

We split the polar part as P_s(z) = a_0/(z-s) + \sum_{k=1}^{N-1} a_k/(z-s)^{k+1}. The k = 0 term is the simple-pole contribution: by the assumed existence of the principal value for (z-s)^{-1}, that principal value equals 2\pi i \, \operatorname{gWN}(\gamma, s), so the k=0 contribution gives a_0 times this expression, which equals 2\pi i \, \operatorname{gWN}(\gamma, s) \, \operatorname{Res}(f, s).

For each k \ge 1, two cases. If a_k = 0 the term is identically zero. If a_k \ne 0, the flatness-of-order-N hypothesis and the angle-compatibility condition (B) hypothesis combine to give the sector-cancellation identity: the cutoff integral of a_k/(z-s)^{k+1} along \gamma vanishes in the \varepsilon \to 0^+ limit. Summing over k from 0 to N-1 yields the claim.

Theorem5.5
Statement uses 7
Statement dependency previews
Preview
Definition 1.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 2
Reverse dependency previews
Preview
Theorem 7.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let U \subseteq \mathbb{C} be a non-empty open set, S \subseteq U a finite set, and f : \mathbb{C} \to \mathbb{C} a function such that

  • f is holomorphic on U \setminus S, and

  • f is meromorphic at each s \in S.

Let \gamma be a closed piecewise-C^{1} immersion based at x \in U with x \notin S, null-homologous in U. Suppose that (\gamma, f) satisfies condition (B) and that \gamma satisfies condition (A') with pole-order data equal to the canonical polar-part orders extracted from the condition-(B) witness. Then \operatorname{PV}_S\!\!\int_\gamma f(z)\,\mathrm{d}z \;=\; \sum_{s \in S} 2 \pi i \, \operatorname{gWN}(\gamma, s) \, \operatorname{Res}(f, s). This is the maximally general paper-faithful form of Hungerbühler–Wasem 2018, Theorem 3.3, with all six oracle hypotheses of the intermediate hw_3_3_paper formulation discharged.

Theorem 5.1 Definition 1.1 Definition 1.2 Definition 2.1 Definition 3.1 Definition 4.1 Definition 4.2

Lean code for Theorem5.5●1 theorem
  • theoremdefined in LeanModularForms/ForMathlib/HW33Clean.lean
    complete
    theorem LeanModularForms.hw_3_3_clean_full_mero {x : ℂ} {U : Set ℂ}
  (hU_open : IsOpen U) (hU_ne : U.Nonempty) {S : Finset ℂ}
  (hS_in_U : ↑S ⊆ U) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (U \ ↑S))
  (γ : ClosedPwC1Immersion x)
  (h_null : IsNullHomologous γ.toPwC1Immersion U)
  (hMero : ∀ s ∈ S, MeromorphicAt f s)
  (hCondB : SatisfiesConditionB γ.toPwC1Immersion f S)
  (hCondA :
    SatisfiesConditionA' γ.toPwC1Immersion f S fun s ↦
      (HungerbuhlerWasem.PolarPartDecomposition.ofMeromorphicWithCondB
            hU_open hS_in_U hf hMero hCondB).order
        s)
  (hx_notin_S : x ∉ ↑S) :
  HasCauchyPVOn S f γ.toPwC1Immersion.toPiecewiseC1Path
    (∑ s ∈ S,
      2 * ↑Real.pi * Complex.I *
          generalizedWindingNumber γ.toPwC1Immersion.toPiecewiseC1Path
            s *
        residue f s)
    theorem LeanModularForms.hw_3_3_clean_full_mero
  {x : ℂ} {U : Set ℂ} (hU_open : IsOpen U)
  (hU_ne : U.Nonempty) {S : Finset ℂ}
  (hS_in_U : ↑S ⊆ U) {f : ℂ → ℂ}
  (hf : DifferentiableOn ℂ f (U \ ↑S))
  (γ : ClosedPwC1Immersion x)
  (h_null :
    IsNullHomologous γ.toPwC1Immersion U)
  (hMero : ∀ s ∈ S, MeromorphicAt f s)
  (hCondB :
    SatisfiesConditionB γ.toPwC1Immersion
      f S)
  (hCondA :
    SatisfiesConditionA' γ.toPwC1Immersion
      f S fun s ↦
      (HungerbuhlerWasem.PolarPartDecomposition.ofMeromorphicWithCondB
            hU_open hS_in_U hf hMero
            hCondB).order
        s)
  (hx_notin_S : x ∉ ↑S) :
  HasCauchyPVOn S f
    γ.toPwC1Immersion.toPiecewiseC1Path
    (∑ s ∈ S,
      2 * ↑Real.pi * Complex.I *
          generalizedWindingNumber
            γ.toPwC1Immersion.toPiecewiseC1Path
            s *
        residue f s)
    **HW Theorem 3.3 — fully general, multi-crossing, meromorphic, clean form.**

The maximally general paper-faithful HW 3.3 in the project: `f` may have
**higher-order** meromorphic poles at each point of `S` and γ may cross
any subset of `S` at any number of parameters.

Hypotheses (8 paper + 1 structural):

* `hU_open, hU_ne, hS_in_U, hf, h_null, hMero, hCondA, hCondB` — the 8 paper
  hypotheses, exactly matching Hungerbühler–Wasem Theorem 3.3.
* `hx_notin_S` — basepoint off `S`. The only Lean-formalization residual:
  `ClosedPwC1Immersion x` carries a typed basepoint, while the paper's "cycle"
  formulation has no basepoint. Every practical caller satisfies it.

All cancellation, integrability, CPV-existence (at crossings AND at avoided
poles), multi-pole aggregation, polar-part decomposition, higher-order Laurent
vanishing under condition (B), and corner-crossing avoidance are discharged
internally via `HungerbuhlerWasem.residueTheorem_crossing_paper_faithful_clean`.

The formal elimination of `hx_notin_S` is provided by the `cyclicShift`
infrastructure in `PaperPwC1Immersion.lean`: if `x ∈ S`, pick `τ ∈ Ioo 0 1`
with `γ(τ) ∉ S` (exists by `preimage_finite`), apply the theorem to
`γ.cyclicShift τ` whose basepoint is `γ(τ) ∉ S`, and lift back via
the corresponding invariance lemmas.
Proof for Theorem 5.5
uses 1

This is a direct invocation of the paper-faithful clean form Theorem 5.1: the hypothesis list of the present theorem matches that of the clean form term-for-term, and no additional reduction is needed.

The single structural residual x \notin S is the only Lean-formalisation artefact (the curve in our setting carries a typed basepoint, whereas the paper works with cycles). It is routinely satisfiable: if x \in S, replace \gamma by the cyclic shift \gamma(\,\cdot\, + \tau) for a parameter \tau \in (0,1) at which \gamma(\tau) \notin S, which exists since the preimage of the finite set S under \gamma is finite.

Theorem 5.1