Winding number computation

Proves that the winding number of fdPolygon around interior points equals -1, using FTC with lifted angle functions and S1 curve comparisons.

• angle_lifted_ref_p₀_continuousOn — lifted angle is continuous on [0, 5]
• rc_integral_eq_neg_two_pi_I_ref_p₀ — S1 integral equals -2piI
• winding_fdPolygon_at_ref_eq_neg_one — base case at reference point
• winding_fdPolygon_eq_neg_one — general case for all interior points
• winding_fdPolygon_eq_circleParamCW — matches circleParamCW winding

theorem RectHomotopyProof.angle_lifted_ref_p₀_continuousOn : ContinuousOn (fun (t : ℝ) => ↑(fdPolygonRadialCircleAngleLifted refP₀ t)) (Set.Icc 0 5)

The lifted angle function is continuous on [0, 5] for the reference point ref_p0.

theorem RectHomotopyProof.rc_integral_eq_neg_two_pi_I_ref_p₀ : ∫ (t : ℝ) in 0..5, (fdPolygonRadialCircle refP₀ t - refP₀)⁻¹ * deriv (fdPolygonRadialCircle refP₀) t = -2 * ↑Real.pi * Complex.I

The S1 integral for the radial circle around ref_p0 equals -2piI.

theorem RectHomotopyProof.winding_fdPolygon_at_ref_eq_neg_one : generalizedWindingNumber' fdPolygon 0 5 refP₀ = -1

Winding number of fdPolygon at the reference point ref_p0 is -1.

theorem RectHomotopyProof.winding_fdPolygon_eq_neg_one (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : generalizedWindingNumber' fdPolygon 0 5 p = -1

The winding number of fdPolygon around any valid interior point is -1.

theorem RectHomotopyProof.winding_radialCircle_eq_neg_one (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : generalizedWindingNumber' (fdPolygonRadialCircle p) 0 5 p = -1

Winding number of fdPolygonRadialCircle around p equals -1.

theorem RectHomotopyProof.winding_radialCircle_eq_circleParamCW (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : generalizedWindingNumber' (fdPolygonRadialCircle p) 0 5 p = generalizedWindingNumber' (circleParamCW p 1 0 5) 0 5 p

Winding numbers of fdPolygonRadialCircle and circleParamCW are equal.

theorem RectHomotopyProof.winding_fdPolygon_eq_circleParamCW (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : generalizedWindingNumber' fdPolygon 0 5 p = generalizedWindingNumber' (circleParamCW p 1 0 5) 0 5 p

Winding number of fdPolygon equals winding number of circleParamCW.