Rect Homotopy: Geometry and Definitions

Basic geometry for the rectangle/chord homotopy proof that the winding number of fdBoundary around interior points is -1.

Main Definitions

• RectHomotopyProof.rho, rho', iPoint — elliptic points
• RectHomotopyProof.chordSegment — straight line between two points
• RectHomotopyProof.fdPolygon — FD boundary with arcs replaced by chords
• RectHomotopyProof.fdBoundary — the actual FD boundary curve
• RectHomotopyProof.HHeight — height parameter (= heightCutoff)

noncomputable def RectHomotopyProof.rho : ℂ

The elliptic point ρ = e^{2πi/3} = -1/2 + √3/2 · i

Equations

• RectHomotopyProof.rho = -1 / 2 + ↑√3 / 2 * Complex.I

noncomputable def RectHomotopyProof.rho' : ℂ

The elliptic point ρ' = e^{πi/3} = 1/2 + √3/2 · i

Equations

• RectHomotopyProof.rho' = 1 / 2 + ↑√3 / 2 * Complex.I

def RectHomotopyProof.iPoint : ℂ

The elliptic point i

Equations

• RectHomotopyProof.iPoint = Complex.I

theorem RectHomotopyProof.rho_norm : ‖rho‖ = 1

theorem RectHomotopyProof.rho'_norm : ‖rho'‖ = 1

theorem RectHomotopyProof.i_point_norm : ‖iPoint‖ = 1

theorem RectHomotopyProof.outside_closed_unit_ball (z : ℂ) (hz : ‖z‖ > 1) : z ∉ Metric.closedBall 0 1

noncomputable def RectHomotopyProof.chordSegment (z₁ z₂ : ℂ) : ℝ → ℂ

The chord (straight line segment) from z₁ to z₂.

Equations

• RectHomotopyProof.chordSegment z₁ z₂ t = (1 - t) • z₁ + t • z₂

theorem RectHomotopyProof.chordSegment_in_convex {z₁ z₂ : ℂ} {S : Set ℂ} (hS : Convex ℝ S) (hz₁ : z₁ ∈ S) (hz₂ : z₂ ∈ S) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : chordSegment z₁ z₂ t ∈ S

theorem RectHomotopyProof.convex_closedBall_zero_one : Convex ℝ (Metric.closedBall 0 1)

theorem RectHomotopyProof.chord_in_closed_unit_ball (z₁ z₂ : ℂ) (hz₁ : ‖z₁‖ = 1) (hz₂ : ‖z₂‖ = 1) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : chordSegment z₁ z₂ t ∈ Metric.closedBall 0 1

noncomputable def RectHomotopyProof.arcToChordHomotopy (arc chord : ℝ → ℂ) : ℝ × ℝ → ℂ

The straight-line homotopy interpolating between an arc and a chord.

Equations

• RectHomotopyProof.arcToChordHomotopy arc chord (t, s) = (1 - s) • arc t + s • chord t

theorem RectHomotopyProof.arcToChordHomotopy_in_closed_unit_ball (arc chord : ℝ → ℂ) (harc : ∀ t ∈ Set.Icc 0 1, arc t ∈ Metric.closedBall 0 1) (hchord : ∀ t ∈ Set.Icc 0 1, chord t ∈ Metric.closedBall 0 1) (t : ℝ) (ht : t ∈ Set.Icc 0 1) (s : ℝ) (hs : s ∈ Set.Icc 0 1) : arcToChordHomotopy arc chord (t, s) ∈ Metric.closedBall 0 1

theorem RectHomotopyProof.arcToChordHomotopy_avoids (arc chord : ℝ → ℂ) (p : ℂ) (hp : ‖p‖ > 1) (harc : ∀ t ∈ Set.Icc 0 1, arc t ∈ Metric.closedBall 0 1) (hchord : ∀ t ∈ Set.Icc 0 1, chord t ∈ Metric.closedBall 0 1) (t : ℝ) (ht : t ∈ Set.Icc 0 1) (s : ℝ) (hs : s ∈ Set.Icc 0 1) : arcToChordHomotopy arc chord (t, s) ≠ p

noncomputable def RectHomotopyProof.θRho' : ℝ

The argument of the lower-corner point ρ' on the unit circle, π / 3.

Equations

• RectHomotopyProof.θRho' = Real.pi / 3

noncomputable def RectHomotopyProof.θI : ℝ

The argument of the point i on the unit circle, π / 2.

Equations

• RectHomotopyProof.θI = Real.pi / 2

noncomputable def RectHomotopyProof.θRho : ℝ

The argument of the corner point ρ on the unit circle, 2π / 3.

Equations

• RectHomotopyProof.θRho = 2 * Real.pi / 3

noncomputable def RectHomotopyProof.arc1 (t : ℝ) : ℂ

The unit-circle arc from ρ' to i.

Equations

• RectHomotopyProof.arc1 t = Complex.exp (Complex.I * (↑RectHomotopyProof.θRho' + ↑t * (↑RectHomotopyProof.θI - ↑RectHomotopyProof.θRho')))

noncomputable def RectHomotopyProof.arc2 (t : ℝ) : ℂ

The unit-circle arc from i to ρ.

Equations

• RectHomotopyProof.arc2 t = Complex.exp (Complex.I * (↑RectHomotopyProof.θI + ↑t * (↑RectHomotopyProof.θRho - ↑RectHomotopyProof.θI)))

theorem RectHomotopyProof.arc1_on_unit_circle (t : ℝ) : ‖arc1 t‖ = 1

theorem RectHomotopyProof.arc2_on_unit_circle (t : ℝ) : ‖arc2 t‖ = 1

theorem RectHomotopyProof.arc1_in_closed_unit_ball (t : ℝ) : t ∈ Set.Icc 0 1 → arc1 t ∈ Metric.closedBall 0 1

theorem RectHomotopyProof.arc2_in_closed_unit_ball (t : ℝ) : t ∈ Set.Icc 0 1 → arc2 t ∈ Metric.closedBall 0 1

noncomputable def RectHomotopyProof.chord1 : ℝ → ℂ

The straight chord from ρ' to i.

Equations

• RectHomotopyProof.chord1 = RectHomotopyProof.chordSegment RectHomotopyProof.rho' RectHomotopyProof.iPoint

noncomputable def RectHomotopyProof.chord2 : ℝ → ℂ

The straight chord from i to ρ.

Equations

• RectHomotopyProof.chord2 = RectHomotopyProof.chordSegment RectHomotopyProof.iPoint RectHomotopyProof.rho

theorem RectHomotopyProof.chord1_in_closed_unit_ball (t : ℝ) (ht : t ∈ Set.Icc 0 1) : chord1 t ∈ Metric.closedBall 0 1

theorem RectHomotopyProof.chord2_in_closed_unit_ball (t : ℝ) (ht : t ∈ Set.Icc 0 1) : chord2 t ∈ Metric.closedBall 0 1

theorem RectHomotopyProof.exists_ball_in_polygon_interior (p : ℂ) (hp : ‖p‖ > 1) (hp_im : 0 < p.im) : ∃ ε > 0, ∀ (z : ℂ), ‖z - p‖ < ε → z.im > 0 ∧ ‖z‖ > 1

theorem RectHomotopyProof.circleIntegral_winding (p : ℂ) (ε : ℝ) (hε : 0 < ε) : ∮ (z : ℂ) in C(p, ε), (z - p)⁻¹ = 2 * ↑Real.pi * Complex.I

noncomputable def RectHomotopyProof.HHeight : ℝ

Height parameter H = √3/2 + 1 for FD boundary.

Equations

• RectHomotopyProof.HHeight = √3 / 2 + 1

theorem RectHomotopyProof.H_height_eq_heightCutoff : HHeight = heightCutoff

noncomputable def RectHomotopyProof.fdPolygon : ℝ → ℂ

Polygon: FD boundary with arcs replaced by chords.

Equations

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

noncomputable def RectHomotopyProof.fdBoundary : ℝ → ℂ

The FD boundary curve (local copy matching clean folder's fdBoundary).

Equations

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

noncomputable def RectHomotopyProof.fdBoundaryToPolygonHomotopy : ℝ × ℝ → ℂ

The homotopy from FD boundary (s=0) to polygon (s=1). Segments 1,4,5 unchanged; segments 2,3 use arc-to-chord interpolation.

Equations

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

theorem RectHomotopyProof.fdBoundary_at_zero : fdBoundary 0 = 1 / 2 + ↑HHeight * Complex.I

theorem RectHomotopyProof.fdBoundary_at_five : fdBoundary 5 = 1 / 2 + ↑HHeight * Complex.I

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_at_t_zero (s : ℝ) : fdBoundaryToPolygonHomotopy (0, s) = 1 / 2 + ↑HHeight * Complex.I

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_at_t_five (s : ℝ) : fdBoundaryToPolygonHomotopy (5, s) = 1 / 2 + ↑HHeight * Complex.I

theorem RectHomotopyProof.segment2_arc_on_unit_circle (t : ℝ) : ‖Complex.exp ((↑Real.pi / 3 + (↑t - 1) * (↑Real.pi / 2 - ↑Real.pi / 3)) * Complex.I)‖ = 1

theorem RectHomotopyProof.segment3_arc_on_unit_circle (t : ℝ) : ‖Complex.exp ((↑Real.pi / 2 + (↑t - 2) * (2 * ↑Real.pi / 3 - ↑Real.pi / 2)) * Complex.I)‖ = 1

theorem RectHomotopyProof.segment2_arc_in_closed_unit_ball (t : ℝ) : Complex.exp ((↑Real.pi / 3 + (↑t - 1) * (↑Real.pi / 2 - ↑Real.pi / 3)) * Complex.I) ∈ Metric.closedBall 0 1

theorem RectHomotopyProof.segment3_arc_in_closed_unit_ball (t : ℝ) : Complex.exp ((↑Real.pi / 2 + (↑t - 2) * (2 * ↑Real.pi / 3 - ↑Real.pi / 2)) * Complex.I) ∈ Metric.closedBall 0 1

theorem RectHomotopyProof.norm_ge_abs_im (z : ℂ) : ‖z‖ ≥ |z.im|

theorem RectHomotopyProof.H_height_gt_one : HHeight > 1