Discharging the HW conditions into the per-pole hypotheses

The polar-part principal-value theorem (Contour.PolarPartDecomposition.hasCauchyPVAt_polarPart) takes raw per-crossing hypotheses: interiority of the crossings, flatness at each surviving coefficient's order, and the tangent-power sector equation. This file discharges them from the roadmap-level data: closedness with the basepoint off the pole gives interiority; condition (A′) gives the flatness through the downward restriction; condition (B) gives the sector equation through the crossing-angle resonance bridge and the uniqueness of Laurent coefficients — the decomposition's coefficients are the canonical ones, so the condition's own Laurent witness constrains them.

Main results

• Contour.PolarPartDecomposition.coeff_eq_meromorphicPolarCoeffAt — a decomposition of canonical order has the canonical coefficients.
• Contour.ConditionAprime.flatOfOrder_of_crossing — condition (A′) discharges the gated flatness hypothesis (for every index below the order; no surviving coefficient needed).
• Contour.ConditionB.pow_unit_tangent_eq_of_coeff_ne_zero — condition (B) discharges the gated sector hypothesis.
• Contour.mem_Ioo_of_closed_of_ne — on a closed curve with basepoint off z, every crossing of z is interior.

Provenance

The condition-(B) discharge corresponds to condB_to_h_B_at_crossings_corner of Crossing.lean in the AINTLIB LeanModularForms development (there through a decomposition constructed from the condition's own witness; here through coefficient uniqueness against the canonical data). See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.mem_Ioo_of_closed_of_ne {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hclosed : γ a = γ b) (hγa : γ a ≠ z) (t : ℝ) : t ∈ Set.Icc a b → γ t = z → t ∈ Set.Ioo a b

Interior crossings from a closed curve rooted off the point: if γ a = γ b ≠ z, every parameter of [a, b] where γ takes the value z is interior.

theorem TauCeti.Contour.PolarPartDecomposition.coeff_eq_meromorphicPolarCoeffAt {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) (hU : IsOpen U) (hSU : ↑S ⊆ U) (s : ↥S) (hMero : MeromorphicAt f ↑s) (h_ord : decomp.order s = meromorphicPolarOrderAt f ↑s) (k : Fin (decomp.order s)) : decomp.coeff s k = meromorphicPolarCoeffAt hMero ⟨↑k, ⋯⟩

A decomposition of canonical order has the canonical coefficients: near s ∈ S the decomposition exhibits f as its polar part at s plus a function analytic there, so by uniqueness of finite principal-part expansions its coefficients are meromorphicPolarCoeffAt.

theorem TauCeti.Contour.ConditionAprime.flatOfOrder_of_crossing {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {S' : Finset ℂ} (hA : ConditionAprime γ a b f S') {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) (s : ↥S) (hsS' : ↑s ∈ S') (h_imm : IsPwC1ImmersionOn γ a b) (hab : a ≤ b) (h_interior : ∀ t ∈ Set.Icc a b, γ t = ↑s → t ∈ Set.Ioo a b) (h_ord : decomp.order s = meromorphicPolarOrderAt f ↑s) (k : Fin (decomp.order s)) : 1 ≤ ↑k → ∀ t ∈ Set.Icc a b, γ t = ↑s → FlatOfOrder γ t (↑k + 1)

Condition (A′) discharges the flatness hypothesis of the polar-part principal-value theorem: at each crossing of s, the pole's canonical order pins meromorphicOrderAt, the condition gives flatness of the full order, and the downward restriction gives it at each surviving coefficient's order.

theorem TauCeti.Contour.ConditionB.pow_unit_tangent_eq_of_coeff_ne_zero {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} (hB : ConditionB γ a b f) {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) (hU : IsOpen U) (hSU : ↑S ⊆ U) (s : ↥S) (hMero : MeromorphicAt f ↑s) (h_imm : IsPwC1ImmersionOn γ a b) (h_interior : ∀ t ∈ Set.Icc a b, γ t = ↑s → t ∈ Set.Ioo a b) (h_ord : decomp.order s = meromorphicPolarOrderAt f ↑s) (k : Fin (decomp.order s)) : 1 ≤ ↑k → decomp.coeff s k ≠ 0 → ∀ t ∈ Set.Icc a b, γ t = ↑s → ∀ (L_R L_L : ℂ), Filter.Tendsto (deriv γ) (nhdsWithin t (Set.Ioi t)) (nhds L_R) → Filter.Tendsto (deriv γ) (nhdsWithin t (Set.Iio t)) (nhds L_L) → (L_R / ↑‖L_R‖) ^ ↑k = (-L_L / ↑‖L_L‖) ^ ↑k

Condition (B) discharges the sector hypothesis of the polar-part principal-value theorem: a surviving coefficient of index ≥ 1 makes s a pole of order > 1, the condition's sector compatibility at the crossing angle carries a Laurent witness whose coefficients are the decomposition's by uniqueness, and its resonance transfers to the unit tangent powers through the crossing-angle bridge.