Cutoff zpow Infrastructure

Direction rate from flatness, cutoff integral splitting, and the FTC-based proof infrastructure for per-term PV vanishing. Builds on the boundary vanishing foundations to provide the cutoff_zpow_infrastructure lemma.

Main Results

• direction_rate_from_flatness_right — direction rate for right exit
• direction_rate_from_flatness_left — direction rate for left exit
• cutoff_zpow_infrastructure — combined FTC + direction infrastructure

theorem GeneralizedResidueTheory.cutoff_zpow_infrastructure (γ : PiecewiseC1Immersion) (s : ℂ) (m : ℕ) (hm : 2 ≤ m) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = s) (h_unique : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = s → t = t₀) (hγ_closed : γ.IsClosed) (h_flat : IsFlatOfOrder γ.toFun t₀ m) : ∃ (wR : ℝ → ℂ) (wL : ℝ → ℂ) (uR : ℂ) (uL : ℂ), (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖wR ε‖ = ε) ∧ (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖wL ε‖ = ε) ∧ (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), wR ε ≠ 0) ∧ (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), wL ε ≠ 0) ∧ ‖uR‖ = 1 ∧ ‖uL‖ = 1 ∧ (∃ (n_angle : ℤ), uR.arg - uL.arg = angleAtCrossing γ t₀ ht₀ + ↑n_angle * (2 * Real.pi)) ∧ ((fun (ε : ℝ) => ‖wR ε / ↑‖wR ε‖ - uR‖) =o[nhdsWithin 0 (Set.Ioi 0)] fun (ε : ℝ) => ε ^ (m - 1)) ∧ ((fun (ε : ℝ) => ‖wL ε / ↑‖wL ε‖ - uL‖) =o[nhdsWithin 0 (Set.Ioi 0)] fun (ε : ℝ) => ε ^ (m - 1)) ∧ ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), (∫ (t : ℝ) in γ.a..γ.b, if ‖γ.toFun t - s‖ > ε then (γ.toFun t - s) ^ (-↑m) * deriv γ.toFun t else 0) = (wL ε ^ (1 - ↑m) - wR ε ^ (1 - ↑m)) / (1 - ↑↑m)

Infrastructure for the FTC-based proof of L4. Given a piecewise C¹ immersion crossing s at t₀ with flatness of order m, this provides:

• Exit time functions wR, wL with ‖w(ε)‖ = ε on the ε-sphere
• Direction limits uR, uL on the unit circle related to angleAtCrossing
• Direction convergence rates o(ε^{m-1}) from flatness
• FTC reduction: the cutoff integral equals (wL^{1-m} - wR^{1-m}) / (1-m)