Homotopy infrastructure for FD boundary → polygon deformation

Defines the segment helper functions HSeg1..HSeg5, proves their continuity and matching at breakpoints, and establishes the main results:

• fdBoundaryToPolygonHomotopy_continuous
• fdBoundaryToPolygonHomotopy_avoids
• fdBoundaryToPolygonHomotopy_closed
• fdBoundaryToPolygon_homotopy_avoids_interior
• circleAround and polygonToCircleHomotopy

noncomputable def RectHomotopyProof.HSeg1 (p : ℝ × ℝ) : ℂ

The homotopy on the first segment of the fundamental-domain boundary.

Equations

• RectHomotopyProof.HSeg1 p = 1 / 2 + (↑RectHomotopyProof.HHeight - ↑p.1 * (↑RectHomotopyProof.HHeight - ↑√3 / 2)) * Complex.I

noncomputable def RectHomotopyProof.HSeg2 (p : ℝ × ℝ) : ℂ

The homotopy on the second segment, interpolating an arc and its chord.

Equations

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

noncomputable def RectHomotopyProof.HSeg3 (p : ℝ × ℝ) : ℂ

The homotopy on the third segment, interpolating an arc and its chord.

Equations

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

noncomputable def RectHomotopyProof.HSeg4 (p : ℝ × ℝ) : ℂ

The homotopy on the fourth segment of the fundamental-domain boundary.

Equations

• RectHomotopyProof.HSeg4 p = -1 / 2 + (↑√3 / 2 + (↑p.1 - 3) * (↑RectHomotopyProof.HHeight - ↑√3 / 2)) * Complex.I

noncomputable def RectHomotopyProof.HSeg5 (p : ℝ × ℝ) : ℂ

The homotopy on the fifth segment of the fundamental-domain boundary.

Equations

• RectHomotopyProof.HSeg5 p = ↑p.1 - 9 / 2 + ↑RectHomotopyProof.HHeight * Complex.I

theorem RectHomotopyProof.H_seg1_continuous : Continuous HSeg1

theorem RectHomotopyProof.H_seg2_continuous : Continuous HSeg2

theorem RectHomotopyProof.H_seg3_continuous : Continuous HSeg3

theorem RectHomotopyProof.H_seg4_continuous : Continuous HSeg4

theorem RectHomotopyProof.H_seg5_continuous : Continuous HSeg5

theorem RectHomotopyProof.hasDerivAt_arc_exp (α β c t : ℝ) : HasDerivAt (fun (t' : ℝ) => Complex.exp ((↑α + (↑t' - ↑c) * ↑β) * Complex.I)) (↑β * Complex.I * Complex.exp ((↑α + (↑t - ↑c) * ↑β) * Complex.I)) t

Derivative of an affine-angle complex exponential t' ↦ exp((α + (t' - c)·β)·I).

theorem RectHomotopyProof.hasDerivAt_chordSegment_shift (a b : ℂ) (c t : ℝ) : HasDerivAt (fun (t' : ℝ) => chordSegment a b (t' - c)) (b - a) t

Derivative of the chord segment t' ↦ chordSegment a b (t' - c) is b - a.

theorem RectHomotopyProof.exp_pi_div_three_eq_rho' : Complex.exp (↑(Real.pi / 3) * Complex.I) = rho'

theorem RectHomotopyProof.exp_pi_div_two_eq_I : Complex.exp (↑(Real.pi / 2) * Complex.I) = Complex.I

theorem RectHomotopyProof.exp_two_pi_div_three_eq_rho : Complex.exp (↑(2 * Real.pi / 3) * Complex.I) = rho

theorem RectHomotopyProof.H_match_at_t1 (p : ℝ × ℝ) (hp : p.1 = 1) : HSeg1 p = HSeg2 p

theorem RectHomotopyProof.H_match_at_t2 (p : ℝ × ℝ) (hp : p.1 = 2) : HSeg2 p = HSeg3 p

theorem RectHomotopyProof.H_match_at_t3 (p : ℝ × ℝ) (hp : p.1 = 3) : HSeg3 p = HSeg4 p

theorem RectHomotopyProof.H_match_at_t4 (p : ℝ × ℝ) (hp : p.1 = 4) : HSeg4 p = HSeg5 p

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_continuous : Continuous fdBoundaryToPolygonHomotopy

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_at_zero (t : ℝ) (_ht : t ∈ Set.Icc 0 5) : fdBoundaryToPolygonHomotopy (t, 0) = fdBoundary t

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_at_one (t : ℝ) (_ht : t ∈ Set.Icc 0 5) : fdBoundaryToPolygonHomotopy (t, 1) = fdPolygon t

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_avoids (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) (t : ℝ) (_ht : t ∈ Set.Icc 0 5) (s : ℝ) (hs : s ∈ Set.Icc 0 1) : fdBoundaryToPolygonHomotopy (t, s) ≠ p

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_closed (s : ℝ) (_hs : s ∈ Set.Icc 0 1) : fdBoundaryToPolygonHomotopy (0, s) = fdBoundaryToPolygonHomotopy (5, s)

noncomputable def RectHomotopyProof.circleAround (p : ℂ) (ε : ℝ) : ℝ → ℂ

The counterclockwise circle of radius ε centred at p.

Equations

• RectHomotopyProof.circleAround p ε t = p + ↑ε * Complex.exp (2 * ↑Real.pi * Complex.I * ↑t / 5)

theorem RectHomotopyProof.circleAround_closed (p : ℂ) (ε : ℝ) : circleAround p ε 0 = circleAround p ε 5

theorem RectHomotopyProof.circleAround_continuous (p : ℂ) (ε : ℝ) : Continuous (circleAround p ε)

theorem RectHomotopyProof.circleAround_dist (p : ℂ) (ε : ℝ) (hε : 0 ≤ ε) (t : ℝ) : ‖circleAround p ε t - p‖ = ε

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

The homotopy contracting the boundary polygon onto a small circle around p.

Equations

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

theorem RectHomotopyProof.fdPolygon_avoids_interior (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) (t : ℝ) (_ht : t ∈ Set.Icc 0 5) : fdPolygon t ≠ p

theorem RectHomotopyProof.fdBoundaryToPolygon_homotopy_avoids_interior (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) (t : ℝ) : t ∈ Set.Icc 0 5 → ∀ s ∈ Set.Icc 0 1, fdBoundaryToPolygonHomotopy (t, s) ≠ p

theorem RectHomotopyProof.fdBoundaryToPolygon_homotopy_closed (s : ℝ) : s ∈ Set.Icc 0 1 → fdBoundaryToPolygonHomotopy (0, s) = fdBoundaryToPolygonHomotopy (5, s)

theorem RectHomotopyProof.fdBoundaryToPolygon_homotopy_continuous : Continuous fdBoundaryToPolygonHomotopy

theorem RectHomotopyProof.winding_number_one_summary (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) : (∀ t ∈ Set.Icc 0 5, ∀ s ∈ Set.Icc 0 1, fdBoundaryToPolygonHomotopy (t, s) ≠ p) ∧ Continuous fdBoundaryToPolygonHomotopy ∧ ∀ s ∈ Set.Icc 0 1, fdBoundaryToPolygonHomotopy (0, s) = fdBoundaryToPolygonHomotopy (5, s)