Unit Arc Winding Number

Proves generalizedWindingNumber' (fdBoundaryH H) 0 5 s = -1/2 for points s on the unit circle arc (‖s‖ = 1, |s.re| < 1/2, s.im > 0).

Uses the helper lemmas from UnitArcHelpers together with log ratio/diff tendsto and strict norm monotonicity on the arc.

Helper 1: Arc outside points have norm > ε

Helper 2: Arc inside points have norm ≤ ε

Helper 3: Norm classification — left of crossing

Helper 4: Norm classification — right of crossing

Helper 5: h_near — arc points within δ have norm ≤ ε

Main tendsto lemma, wired through pv_tendsto_of_crossing_limit

theorem gWN_fdBoundary_H_eq_neg_half_of_unitArc (H : ℝ) (hH : 1 < H) (s : ℂ) (hs_norm : ‖s‖ = 1) (hs_re : |s.re| < 1 / 2) (hs_im_pos : 0 < s.im) : generalizedWindingNumber' (fdBoundaryH H) 0 5 s = -1 / 2

Main theorem: gWN = −1/2 at smooth arc points.