Polygon slope analysis and derivative bounds

Proves slope identities for fdPolygon on each segment, tendsto at breakpoints, non-differentiability at partition points {1,2,3,4}, and global derivative bounds.

• slope_fdPolygon_segN — slope equals segment derivative on each interval
• fdPolygon_not_differentiableAt_partition — left/right slopes differ
• fdPolygon_deriv_bounded — ∃ M, ∀ t ∈ Icc 0 5, ‖deriv fdPolygon t‖ ≤ M

theorem RectHomotopyProof.slope_fdPolygon_seg1 (s t : ℝ) (hs : s < 1) (ht : t < 1) (hst : s ≠ t) : slope fdPolygon s t = -(↑HHeight - ↑√3 / 2) * Complex.I

theorem RectHomotopyProof.slope_fdPolygon_seg2 (s t : ℝ) (hs : s > 1) (ht : t > 1) (hs2 : s ≤ 2) (ht2 : t ≤ 2) (hst : s ≠ t) : slope fdPolygon s t = iPoint - rho'

theorem RectHomotopyProof.slope_fdPolygon_seg3 (s t : ℝ) (hs : s > 2) (ht : t > 2) (hs3 : s ≤ 3) (ht3 : t ≤ 3) (hst : s ≠ t) : slope fdPolygon s t = rho - iPoint

theorem RectHomotopyProof.slope_fdPolygon_seg4 (s t : ℝ) (hs : s > 3) (ht : t > 3) (hs4 : s ≤ 4) (ht4 : t ≤ 4) (hst : s ≠ t) : slope fdPolygon s t = (↑HHeight - ↑√3 / 2) * Complex.I

theorem RectHomotopyProof.slope_fdPolygon_seg5 (s t : ℝ) (hs : s > 4) (ht : t > 4) (hst : s ≠ t) : slope fdPolygon s t = 1

theorem RectHomotopyProof.fdPolygon_deriv_ne_at_t1 : -Complex.I ≠ iPoint - rho'

theorem RectHomotopyProof.fdPolygon_deriv_ne_at_t2 : iPoint - rho' ≠ rho - iPoint

theorem RectHomotopyProof.fdPolygon_deriv_ne_at_t3 : rho - iPoint ≠ Complex.I

theorem RectHomotopyProof.fdPolygon_deriv_ne_at_t4 : Complex.I ≠ 1

theorem RectHomotopyProof.slope_fdPolygon_at_t1_left (s : ℝ) (hs : s < 1) : slope fdPolygon 1 s = -(↑HHeight - ↑√3 / 2) * Complex.I

theorem RectHomotopyProof.slope_fdPolygon_at_t1_right (s : ℝ) (hs : s > 1) (hs2 : s ≤ 2) : slope fdPolygon 1 s = iPoint - rho'

theorem RectHomotopyProof.slope_fdPolygon_at_t2_left (s : ℝ) (hs1 : s > 1) (hs2 : s < 2) : slope fdPolygon 2 s = iPoint - rho'

theorem RectHomotopyProof.slope_fdPolygon_at_t2_right (s : ℝ) (hs2 : s > 2) (hs3 : s ≤ 3) : slope fdPolygon 2 s = rho - iPoint

theorem RectHomotopyProof.slope_fdPolygon_at_t3_left (s : ℝ) (hs2 : s > 2) (hs3 : s < 3) : slope fdPolygon 3 s = rho - iPoint

theorem RectHomotopyProof.slope_fdPolygon_at_t3_right (s : ℝ) (hs3 : s > 3) (hs4 : s ≤ 4) : slope fdPolygon 3 s = (↑HHeight - ↑√3 / 2) * Complex.I

theorem RectHomotopyProof.slope_fdPolygon_at_t4_left (s : ℝ) (hs3 : s > 3) (hs4 : s < 4) : slope fdPolygon 4 s = (↑HHeight - ↑√3 / 2) * Complex.I

theorem RectHomotopyProof.slope_fdPolygon_at_t4_right (s : ℝ) (hs4 : s > 4) : slope fdPolygon 4 s = 1

theorem RectHomotopyProof.slope_fdPolygon_tendsto_seg1_left : Filter.Tendsto (slope fdPolygon 1) (nhdsWithin 1 (Set.Iio 1)) (nhds (-(↑HHeight - ↑√3 / 2) * Complex.I))

theorem RectHomotopyProof.slope_fdPolygon_tendsto_seg2_right : Filter.Tendsto (slope fdPolygon 1) (nhdsWithin 1 (Set.Ioi 1)) (nhds (iPoint - rho'))

theorem RectHomotopyProof.slope_fdPolygon_tendsto_seg2_left : Filter.Tendsto (slope fdPolygon 2) (nhdsWithin 2 (Set.Iio 2)) (nhds (iPoint - rho'))

theorem RectHomotopyProof.slope_fdPolygon_tendsto_seg3_right : Filter.Tendsto (slope fdPolygon 2) (nhdsWithin 2 (Set.Ioi 2)) (nhds (rho - iPoint))

theorem RectHomotopyProof.slope_fdPolygon_tendsto_seg3_left : Filter.Tendsto (slope fdPolygon 3) (nhdsWithin 3 (Set.Iio 3)) (nhds (rho - iPoint))

theorem RectHomotopyProof.slope_fdPolygon_tendsto_seg4_right : Filter.Tendsto (slope fdPolygon 3) (nhdsWithin 3 (Set.Ioi 3)) (nhds ((↑HHeight - ↑√3 / 2) * Complex.I))

theorem RectHomotopyProof.slope_fdPolygon_tendsto_seg4_left : Filter.Tendsto (slope fdPolygon 4) (nhdsWithin 4 (Set.Iio 4)) (nhds ((↑HHeight - ↑√3 / 2) * Complex.I))

theorem RectHomotopyProof.slope_fdPolygon_tendsto_seg5_right : Filter.Tendsto (slope fdPolygon 4) (nhdsWithin 4 (Set.Ioi 4)) (nhds 1)

theorem RectHomotopyProof.fdPolygon_not_differentiableAt_partition (t : ℝ) (ht : t ∈ {1, 2, 3, 4}) : ¬DifferentiableAt ℝ fdPolygon t

theorem RectHomotopyProof.fdPolygon_deriv_bounded : ∃ (M : ℝ), ∀ t ∈ Set.Icc 0 5, ‖deriv fdPolygon t‖ ≤ M