Generalized Winding Number at Left Edge Points

Proves generalizedWindingNumber' (fdBoundaryH H) 0 5 s = -1/2 for points s on the left vertical edge of the fundamental domain (s.re = -1/2, √3/2 < s.im < H).

theorem gWN_fdBoundary_H_eq_neg_half_of_leftEdge (H : ℝ) (hH_sqrt : √3 / 2 < H) (s : ℂ) (hs_re : s.re = -1 / 2) (hs_norm : ‖s‖ > 1) (hs_im_lower : √3 / 2 < s.im) (hs_im : s.im < H) : generalizedWindingNumber' (fdBoundaryH H) 0 5 s = -1 / 2