Winding number base lemmas

Establishes that the straight line from any interior point to the reference point refP₀ avoids the fdPolygon boundary, derives slitPlane membership for the translated curve, and proves continuity and limit behavior of the argument function near the branch cut crossing point tL. These results underpin the winding number computation for the fundamental domain boundary.

• fdPolygon_avoids_line_to_ref — line from p to refP₀ avoids fdPolygon
• rc_sub_ref_p₀_mem_slitPlane — radial circle minus refP₀ is in slitPlane
• fdPolygon_sub_ref_p₀_mem_slitPlane — fdPolygon minus refP₀ is in slitPlane
• continuousOn_arg_w — arg of translated curve is continuous away from tL
• tendsto_arg_w_left, tendsto_arg_w_right — limits of arg at tL from left/right

theorem RectHomotopyProof.fdPolygon_avoids_line_to_ref (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) (s : ℝ) : s ∈ Set.Icc 0 1 → ∀ t ∈ Set.Icc 0 5, fdPolygon t ≠ (1 - ↑s) * p + ↑s * refP₀

The straight line from any valid interior point p to refP₀ = I*Y₀ avoids all points on the fdPolygon boundary.

theorem RectHomotopyProof.rc_sub_ref_p₀_mem_slitPlane (t : ℝ) (ht : t ∈ Set.Icc 0 5) (htL : t ≠ tL refP₀) : fdPolygonRadialCircle refP₀ t - refP₀ ∈ Complex.slitPlane

rc(t) - refP₀ lies in slitPlane for t ∈ [0, 5] with t ≠ tL refP₀. Note: CurveAvoidance.curve_sub_in_slitPlane does not apply here because its hpos hypothesis requires 0 < im ∨ 0 < re uniformly on all of Icc 0 5, whereas at tL the vector has re < 0 and im = 0 (a branch-cut crossing). slitPlane membership at non-tL points relies on im ≠ 0 (not im > 0), which is outside the API's scope.

theorem RectHomotopyProof.fdPolygon_sub_ref_p₀_mem_slitPlane (t : ℝ) (ht : t ∈ Set.Icc 0 5) (htL : t ≠ tL refP₀) : fdPolygon t - refP₀ ∈ Complex.slitPlane

fdPolygon t - refP₀ is in slitPlane for t ∈ [0, 5] with t ≠ tL refP₀. Derived from rc_sub_ref_p₀_mem_slitPlane via positive-scaling; the same curve_sub_in_slitPlane incompatibility applies (see above).

theorem RectHomotopyProof.continuous_w : Continuous fun (t : ℝ) => fdPolygon t - refP₀

w = fdPolygon · - refP₀ is continuous.

theorem RectHomotopyProof.continuousOn_arg_w : ContinuousOn (fun (t : ℝ) => (fdPolygon t - refP₀).arg) (Set.Icc 0 5 \ {tL refP₀})

arg ∘ w is continuous on Icc 0 5 \ {tL refP₀}.

theorem RectHomotopyProof.w_tL_re_neg : (fdPolygon (tL refP₀) - refP₀).re < 0

At tL: w has re < 0 and im = 0.

theorem RectHomotopyProof.w_tL_im_zero : (fdPolygon (tL refP₀) - refP₀).im = 0

theorem RectHomotopyProof.w_im_neg_near_tL_left : ∀ᶠ (t : ℝ) in nhdsWithin (tL refP₀) (Set.Iio (tL refP₀)), (fdPolygon t - refP₀).im < 0

For t near tL from below, w(t).im < 0.

theorem RectHomotopyProof.w_im_pos_near_tL_right : ∀ᶠ (t : ℝ) in nhdsWithin (tL refP₀) (Set.Ioi (tL refP₀)), 0 < (fdPolygon t - refP₀).im

For t near tL from above, w(t).im > 0.

theorem RectHomotopyProof.tendsto_arg_w_left : Filter.Tendsto (fun (t : ℝ) => (fdPolygon t - refP₀).arg) (nhdsWithin (tL refP₀) (Set.Iio (tL refP₀))) (nhds (-Real.pi))

Tendsto arg(w(t)) from the left of tL to -π.

theorem RectHomotopyProof.tendsto_arg_w_right : Filter.Tendsto (fun (t : ℝ) => (fdPolygon t - refP₀).arg) (nhdsWithin (tL refP₀) (Set.Ioi (tL refP₀))) (nhds Real.pi)

Tendsto arg(w(t)) from the right of tL to π.