On-Curve PV: Infrastructure

Bridge lemmas, elliptic point CPV, segment geometry helpers, arc injectivity, and CPV helper lemmas (avoidance, concatenation, sub-interval extension, integrability).

theorem cpv_exists_at_rho (H : ℝ) (hH : √3 / 2 < H) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - ellipticPointRho)⁻¹) (fdBoundaryH H) 0 5 ellipticPointRho

CPV of (z - rho)^{-1} exists along fdBoundaryH H for H > sqrt(3)/2.

theorem cpv_exists_at_rho_plus_one (H : ℝ) (hH : √3 / 2 < H) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - ellipticPointRhoPlusOne)⁻¹) (fdBoundaryH H) 0 5 ellipticPointRhoPlusOne

CPV of (z - rho')^{-1} exists along fdBoundaryH H for H > sqrt(3)/2.

theorem cpv_exists_at_i (H : ℝ) (hH : 1 < H) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - Complex.I)⁻¹) (fdBoundaryH H) 0 5 Complex.I

CPV of (z - I)^{-1} exists along fdBoundaryH H for H > 1.

theorem fdBoundary_H_seg1_re' (H : ℝ) {t : ℝ} (_ht0 : 0 ≤ t) (ht1 : t ≤ 1) : (fdBoundaryH H t).re = 1 / 2

theorem fdBoundary_H_seg4_re' (H : ℝ) {t : ℝ} (ht3 : 3 < t) (ht4 : t ≤ 4) : (fdBoundaryH H t).re = -1 / 2

theorem fdBoundary_H_seg5_re' (H : ℝ) {t : ℝ} (ht4 : 4 < t) (_ht5 : t ≤ 5) : (fdBoundaryH H t).re = t - 9 / 2

theorem fdBoundary_H_seg5_im' (H : ℝ) {t : ℝ} (ht4 : 4 < t) (_ht5 : t ≤ 5) : (fdBoundaryH H t).im = H

theorem fdBoundary_H_arc_re' (H : ℝ) {t : ℝ} (ht1 : 1 < t) (ht3 : t < 3) : (fdBoundaryH H t).re = Real.cos (Real.pi * (1 + t) / 6)

theorem fdBoundary_H_arc_im' (H : ℝ) {t : ℝ} (ht1 : 1 < t) (ht3 : t < 3) : (fdBoundaryH H t).im = Real.sin (Real.pi * (1 + t) / 6)

theorem cpv_exists_on_smooth_subinterval (H : ℝ) (_hH : √3 / 2 < H) {t₀ a' b' : ℝ} (s : ℂ) (hat₀ : t₀ ∈ Set.Ioo a' b') (hs : fdBoundaryH H t₀ = s) (hγ_C2 : ContDiffAt ℝ 2 (fdBoundaryH H) t₀) (hL_ne : deriv (fdBoundaryH H) t₀ ≠ 0) (hγ_cont_deriv : ContinuousOn (deriv (fdBoundaryH H)) (Set.Icc a' b')) (h_inj : ∀ t ∈ Set.Icc a' b', fdBoundaryH H t = fdBoundaryH H t₀ → t = t₀) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - s)⁻¹) (fdBoundaryH H) a' b' s

theorem fdBoundary_H_cutout_ii (H : ℝ) (hH : √3 / 2 < H) (s : ℂ) (ε : ℝ) (hε : 0 < ε) : IntervalIntegrable (fun (t : ℝ) => if ε < ‖fdBoundaryH H t - s‖ then (fdBoundaryH H t - s)⁻¹ * deriv (fdBoundaryH H) t else 0) MeasureTheory.volume 0 5

The cutout integrand for (z - s)⁻¹ along fdBoundaryH H is interval-integrable on [0, 5]. Uses ae-measurability from piecewise C1 structure + uniform bound.

theorem cpv_extend_to_full_interval (H : ℝ) (hH : √3 / 2 < H) (s : ℂ) (a' b' : ℝ) (ha' : 0 ≤ a') (hb' : b' ≤ 5) (hab' : a' < b') (h_sub : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - s)⁻¹) (fdBoundaryH H) a' b' s) (h_avoid_left : ∀ t ∈ Set.Icc 0 a', fdBoundaryH H t ≠ s) (h_avoid_right : ∀ t ∈ Set.Icc b' 5, fdBoundaryH H t ≠ s) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - s)⁻¹) (fdBoundaryH H) 0 5 s

If CPV exists on a sub-interval [a', b'] ⊆ [0, 5] containing the sole crossing point, and the curve avoids s on [0, a'] and [b', 5], then CPV exists on [0, 5]. This combines cpv_avoidance on the complement and cpv_concat to glue.