Angle analysis and winding number invariance

Defines angle functions for fdPolygonRadialCircle and circleParamCW, analyzes the branch cut crossing on segment 4, constructs a lifted angle that tracks the full -2π rotation, and proves center-translation invariance of the winding number.

• angleOnCircle, fdPolygonRadialCircleAngle — angle of radial projection
• tL — time when vector crosses negative real axis on seg4
• fdPolygonRadialCircleAngleLifted — lifted angle accounting for branch cut
• refP₀ — reference point on imaginary axis
• winding_fdPolygon_center_invariant — winding number preserved under center translation

noncomputable def RectHomotopyProof.angleOnCircle (p z : ℂ) : ℝ

The angle of a point on the unit circle around p.

Equations

• RectHomotopyProof.angleOnCircle p z = (z - p).arg

noncomputable def RectHomotopyProof.fdPolygonRadialCircleAngle (p : ℂ) : ℝ → ℝ

The angle function for fdPolygonRadialCircle.

Equations

• RectHomotopyProof.fdPolygonRadialCircleAngle p t = RectHomotopyProof.angleOnCircle p (RectHomotopyProof.fdPolygonRadialCircle p t)

noncomputable def RectHomotopyProof.circleParamCWAngle : ℝ → ℝ

The angle function for circleParamCW.

Equations

• RectHomotopyProof.circleParamCWAngle t = 2 * Real.pi * (5 - t) / 5

noncomputable def RectHomotopyProof.angleHomotopy (p : ℂ) : ℝ × ℝ → ℂ

S¹ angle interpolation homotopy.

Equations

• One or more equations did not get rendered due to their size.

theorem RectHomotopyProof.fdPolygon_at_zero : fdPolygon 0 = 1 / 2 + ↑HHeight * Complex.I

Polygon vertex at t=0: top-right corner (1/2 + HHeight·i).

theorem RectHomotopyProof.fdPolygon_at_one : fdPolygon 1 = rho'

Polygon vertex at t=1: rho'.

theorem RectHomotopyProof.fdPolygon_at_four : fdPolygon 4 = -1 / 2 + ↑HHeight * Complex.I

Polygon vertex at t=4: top-left corner (-1/2 + HHeight·i).

theorem RectHomotopyProof.v0_quadrant (p : ℂ) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) : (fdPolygon 0 - p).re > 0 ∧ (fdPolygon 0 - p).im > 0

Direction from p to z0 is in Q1 (re > 0, im > 0).

theorem RectHomotopyProof.interior_point_im_bound (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) : p.im > √3 / 2

For interior points with ‖p‖ > 1, |p.re| < 1/2, 0 < p.im, we have p.im > √3/2.

theorem RectHomotopyProof.v1_quadrant (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) : (fdPolygon 1 - p).re > 0 ∧ (fdPolygon 1 - p).im < 0

Direction from p to fdPolygon 1 (= rho') is in Q4 (re > 0, im < 0).

theorem RectHomotopyProof.fdPolygon_at_three : fdPolygon 3 = rho

Polygon vertex at t=3: rho.

theorem RectHomotopyProof.v3_quadrant (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) : (fdPolygon 3 - p).re < 0 ∧ (fdPolygon 3 - p).im < 0

Direction from p to fdPolygon 3 (= rho) is in Q3 (re < 0, im < 0).

theorem RectHomotopyProof.v4_quadrant (p : ℂ) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) : (fdPolygon 4 - p).re < 0 ∧ (fdPolygon 4 - p).im > 0

Direction from p to fdPolygon 4 is in Q2 (re < 0, im > 0).

theorem RectHomotopyProof.arg_Q1 (z : ℂ) (hz_re : 0 < z.re) (hz_im : 0 < z.im) : 0 < z.arg ∧ z.arg < Real.pi / 2

Q1: re > 0, im > 0 → 0 < arg < π/2.

theorem RectHomotopyProof.arg_Q4 (z : ℂ) (hz_re : 0 < z.re) (hz_im : z.im < 0) : -(Real.pi / 2) < z.arg ∧ z.arg < 0

Q4: re > 0, im < 0 → -π/2 < arg < 0.

theorem RectHomotopyProof.arg_Q3 (z : ℂ) (hz_im : z.im < 0) : -Real.pi < z.arg ∧ z.arg < 0

Q3: im < 0 → -π < arg < 0.

theorem RectHomotopyProof.arg_Q2 (z : ℂ) (hz_re : z.re < 0) (hz_im : 0 < z.im) : Real.pi / 2 < z.arg ∧ z.arg ≤ Real.pi

Q2: re < 0, im > 0 → π/2 < arg ≤ π.

noncomputable def RectHomotopyProof.tL (p : ℂ) : ℝ

The unique time on seg4 where (fdPolygon t - p) crosses the negative real axis.

Equations

• RectHomotopyProof.tL p = 3 + (p.im - √3 / 2) / (RectHomotopyProof.HHeight - √3 / 2)

theorem RectHomotopyProof.tL_mem_Ioo (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : tL p ∈ Set.Ioo 3 4

tL is in (3, 4) for interior points.

theorem RectHomotopyProof.seg4_vec_re_neg (p : ℂ) (hp_re : |p.re| < 1 / 2) (t : ℝ) (ht : t ∈ Set.Ioc 3 4) : (fdPolygon t - p).re < 0

On seg4, (fdPolygon t - p).re < 0.

theorem RectHomotopyProof.seg4_im_formula (t : ℝ) (ht : t ∈ Set.Ioc 3 4) : (fdPolygon t).im = √3 / 2 + (t - 3) * (HHeight - √3 / 2)

On seg4, the imaginary part of fdPolygon t.

theorem RectHomotopyProof.seg4_vec_im_sign (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) (t : ℝ) (ht : t ∈ Set.Ioc 3 4) : (t < tL p → (fdPolygon t - p).im < 0) ∧ (t = tL p → (fdPolygon t - p).im = 0) ∧ (tL p < t → 0 < (fdPolygon t - p).im)

Sign of (fdPolygon t - p).im on seg4: negative before tL, zero at tL, positive after.

theorem RectHomotopyProof.seg4_vec_at_tL (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : (fdPolygon (tL p) - p).re < 0 ∧ (fdPolygon (tL p) - p).im = 0

At tL, the vector fdPolygon t - p is a nonzero negative real.

theorem RectHomotopyProof.arg_at_tL_eq_pi (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : (fdPolygon (tL p) - p).arg = Real.pi

arg at tL equals π (negative real).

theorem RectHomotopyProof.arg_seg4_before (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) (t : ℝ) (ht : t ∈ Set.Ioc 3 4) (htL : t < tL p) : (fdPolygon t - p).arg < 0

Before tL on seg4: arg < 0.

theorem RectHomotopyProof.arg_seg4_after (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) (t : ℝ) (ht : t ∈ Set.Ioc 3 4) (htL : tL p < t) : 0 < (fdPolygon t - p).arg

After tL on seg4: arg > 0.

theorem RectHomotopyProof.arg_normalize_eq (z : ℂ) (hz : z ≠ 0) : (z / ↑‖z‖).arg = z.arg

arg is preserved under normalization.

theorem RectHomotopyProof.fdPolygonRadialCircle_angle_eq_arg (p : ℂ) (t : ℝ) (hne : fdPolygon t ≠ p) : fdPolygonRadialCircleAngle p t = (fdPolygon t - p).arg

fdPolygonRadialCircleAngle equals arg(fdPolygon t - p).

noncomputable def RectHomotopyProof.fdPolygonRadialCircleAngleLifted (p : ℂ) : ℝ → ℝ

Lifted angle function that accounts for branch cut crossing.

Equations

• RectHomotopyProof.fdPolygonRadialCircleAngleLifted p t = if t < RectHomotopyProof.tL p then (RectHomotopyProof.fdPolygon t - p).arg else (RectHomotopyProof.fdPolygon t - p).arg - 2 * Real.pi

theorem RectHomotopyProof.fdPolygon_zero_ne_interior (p : ℂ) (hp_im : p.im < HHeight) : fdPolygon 0 ≠ p

fdPolygon 0 ≠ p for interior points.

theorem RectHomotopyProof.fdPolygon_five_ne_interior (p : ℂ) (hp_im : p.im < HHeight) : fdPolygon 5 ≠ p

fdPolygon 5 ≠ p for interior points.

theorem RectHomotopyProof.lifted_angle_at_zero (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : fdPolygonRadialCircleAngleLifted p 0 = fdPolygonRadialCircleAngle p 0

At t=0, the lifted angle equals the raw angle (0 < tL).

theorem RectHomotopyProof.lifted_angle_at_five (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : fdPolygonRadialCircleAngleLifted p 5 = fdPolygonRadialCircleAngle p 5 - 2 * Real.pi

At t=5, the lifted angle is raw angle minus 2π (5 > tL).

theorem RectHomotopyProof.fdPolygon_periodic : fdPolygon 5 = fdPolygon 0

fdPolygon is periodic with period 5.

theorem RectHomotopyProof.fdPolygonRadialCircle_angle_periodic (p : ℂ) : fdPolygonRadialCircleAngle p 5 = fdPolygonRadialCircleAngle p 0

The raw angle at 5 equals the raw angle at 0.

theorem RectHomotopyProof.fdPolygonRadialCircle_angle_lifted_change (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : fdPolygonRadialCircleAngleLifted p 5 = fdPolygonRadialCircleAngleLifted p 0 - 2 * Real.pi

The lifted angle total change is -2π.

theorem RectHomotopyProof.fdPolygonRadialCircle_angle_change (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : fdPolygonRadialCircleAngleLifted p 5 = fdPolygonRadialCircleAngleLifted p 0 - 2 * Real.pi

Equality form of wrap count.

theorem RectHomotopyProof.fdPolygonRadialCircle_wrapCount (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : ∃ (θ₀ : ℝ), fdPolygonRadialCircleAngleLifted p 0 = θ₀ ∧ fdPolygonRadialCircleAngleLifted p 5 = θ₀ - 2 * Real.pi

Wrap count for the lifted angle function.

theorem RectHomotopyProof.circleParamCW_wrapCount : circleParamCWAngle 0 = 2 * Real.pi ∧ circleParamCWAngle 5 = 0

circleParamCW also makes exactly one clockwise loop.

noncomputable def RectHomotopyProof.refY₀ : ℝ

Reference Y-coordinate on imaginary axis.

Equations

• RectHomotopyProof.refY₀ = (1 + RectHomotopyProof.HHeight) / 2

noncomputable def RectHomotopyProof.refP₀ : ℂ

The reference point p₀ = I * Y₀ on the imaginary axis.

Equations

• RectHomotopyProof.refP₀ = Complex.I * ↑RectHomotopyProof.refY₀

theorem RectHomotopyProof.ref_Y₀_pos : 0 < refY₀

theorem RectHomotopyProof.ref_Y₀_gt_one : 1 < refY₀

theorem RectHomotopyProof.ref_Y₀_lt_H : refY₀ < HHeight

theorem RectHomotopyProof.ref_p₀_norm : ‖refP₀‖ > 1

theorem RectHomotopyProof.ref_p₀_re : |refP₀.re| < 1 / 2

theorem RectHomotopyProof.ref_p₀_im_pos : 0 < refP₀.im

theorem RectHomotopyProof.ref_p₀_im : refP₀.im < HHeight

theorem RectHomotopyProof.winding_fdPolygon_center_invariant (p₁ p₂ : ℂ) (_hp₁_norm : ‖p₁‖ > 1) (_hp₁_re : |p₁.re| < 1 / 2) (_hp₁_im : p₁.im < HHeight) (_hp₂_norm : ‖p₂‖ > 1) (_hp₂_re : |p₂.re| < 1 / 2) (_hp₂_im : p₂.im < HHeight) (havoid : ∀ s ∈ Set.Icc 0 1, ∀ t ∈ Set.Icc 0 5, fdPolygon t ≠ (1 - ↑s) * p₁ + ↑s * p₂) : generalizedWindingNumber' fdPolygon 0 5 p₁ = generalizedWindingNumber' fdPolygon 0 5 p₂

Center-translation homotopy invariance of winding number.