Sector-even cancellation at a flat crossing

For a curve crossing a pole s of the Laurent term c / (z - s)^k (k ≥ 2), the two branch contributions to the principal value cancel when the one-sided tangent directions satisfy the power identity (L₊ / ‖L₊‖)^(k-1) = (-L₋ / ‖L₋‖)^(k-1) — condition (B) of Hungerbühler–Wasem, their equation 3.4: PV ∮ dz/zⁿ = lim (1 - e^{-i(n-1)α}) / ((n-1)ε^{n-1}), which vanishes whenever (n-1)α ∈ 2πℤ.

This file contributes the antiderivative-difference half of that mechanism, for the antiderivative F(z) = -1/((k-1)(z-s)^(k-1)) of z ↦ (z - s)^(-k):

Main results

• Contour.smul_pow_eq_of_div_norm_pow_eq — under the power identity, the radius-ε chords ε • (L₊ / ‖L₊‖) and ε • (-L₋ / ‖L₋‖) have equal (k-1)-th powers.
• Contour.antiderivative_diff_across_crossing_tendsto_zero — for a curve flat of order n ≥ k at the crossing with one-sided tangents L₋, L₊, the difference of F along the curve across the crossing, evaluated at exit times from the ε-disc on each side, tends to 0 as ε → 0⁺.

Provenance

Migrated from F_line_diff_eq_zero_under_conditionB (here pared to the underlying chord power identity) and F_curve_diff_tendsto_zero_under_conditionB of SectorCancellation.lean in the AINTLIB LeanModularForms development. There the flatness hypothesis is tangent-indexed (IsFlatOfOrder), so the deviation bounds feed in directly; here Contour.FlatOfOrder quantifies its witness directions existentially, and the tangent-forcing bridge (FlatOfOrder.tangentDeviation_isLittleO_right/left) recovers them. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.smul_pow_eq_of_div_norm_pow_eq (L_minus L_plus : ℂ) (k : ℕ) (h_B : (L_plus / ↑‖L_plus‖) ^ (k - 1) = (-L_minus / ↑‖L_minus‖) ^ (k - 1)) (ε : ℝ) : ((ε / ‖L_plus‖) • L_plus) ^ (k - 1) = ((ε / ‖L_minus‖) • -L_minus) ^ (k - 1)

Equal chord powers under condition (B). For tangent directions L₊ (rightward) and -L₋ (the left tangent, used inward), the radius-ε chords have equal (k-1)-th powers under the power identity (L₊ / ‖L₊‖)^(k-1) = (-L₋ / ‖L₋‖)^(k-1) — condition (B) of Hungerbühler–Wasem. When the curve is C¹ at the crossing (L₋ = L₊), condition (B) holds automatically for k odd, since (-1)^(k-1) = 1.

theorem TauCeti.Contour.antiderivative_diff_across_crossing_tendsto_zero {γ : ℝ → ℂ} {t₀ : ℝ} {s L_minus L_plus : ℂ} {n k : ℕ} (h_flat : FlatOfOrder γ t₀ n) (hL_minus : L_minus ≠ 0) (hL_plus : L_plus ≠ 0) (h_deriv_right : HasDerivWithinAt γ L_plus (Set.Ioi t₀) t₀) (h_deriv_left : HasDerivWithinAt γ L_minus (Set.Iio t₀) t₀) (h_s : γ t₀ = s) (hk : 2 ≤ k) (hkn : k ≤ n) (h_B : (L_plus / ↑‖L_plus‖) ^ (k - 1) = (-L_minus / ↑‖L_minus‖) ^ (k - 1)) {t_eps_plus t_eps_minus : ℝ → ℝ} (h_plus_to : Filter.Tendsto t_eps_plus (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin t₀ (Set.Ioi t₀))) (h_plus_radius : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖γ (t_eps_plus ε) - s‖ = ε) (h_minus_to : Filter.Tendsto t_eps_minus (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin t₀ (Set.Iio t₀))) (h_minus_radius : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖γ (t_eps_minus ε) - s‖ = ε) : Filter.Tendsto (fun (ε : ℝ) => ‖-(↑(k - 1))⁻¹ * ((γ (t_eps_minus ε) - s) ^ (k - 1))⁻¹ - -(↑(k - 1))⁻¹ * ((γ (t_eps_plus ε) - s) ^ (k - 1))⁻¹‖) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The antiderivative difference across a flat crossing tends to zero. For a curve flat of order n at t₀ over the pole s = γ t₀, with one-sided tangents L₋ (left) and L₊ (right) satisfying the condition-(B) power identity, and exit times t_eps_plus, t_eps_minus reaching radius ε on each side: the difference of F(z) = -1/((k-1)(z-s)^(k-1)) along the curve between the two exits tends to 0 as ε → 0⁺ (2 ≤ k ≤ n). This is the cancellation half of the Hungerbühler–Wasem principal-value mechanism at a condition-(B) crossing.