Non-differentiability at partition points and derivative continuity

Proves the homotopy is not differentiable at t ∈ {1, 3, 4} (left/right derivatives differ) and that the per-segment derivatives are continuous.

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_not_diffAt_134 (s : ℝ) (hs : s ∈ Set.Icc 0 1) (k : ℝ) (hk : k ∈ {1, 3, 4}) : ¬DifferentiableAt ℝ (fun (t' : ℝ) => fdBoundaryToPolygonHomotopy (t', s)) k

The homotopy is NOT differentiable at t ∈ {1, 3, 4} because left/right derivatives differ.

theorem RectHomotopyProof.deriv_seg1_continuousOn : ContinuousOn (fun (_q : ℝ × ℝ) => -((↑HHeight - ↑√3 / 2) * Complex.I)) Set.univ

Segment 1 derivative continuity: constant function is continuous.

theorem RectHomotopyProof.deriv_seg4_continuousOn : ContinuousOn (fun (_q : ℝ × ℝ) => (↑HHeight - ↑√3 / 2) * Complex.I) Set.univ

Segment 4 derivative continuity: constant function is continuous.

theorem RectHomotopyProof.deriv_seg5_continuousOn : ContinuousOn (fun (_q : ℝ × ℝ) => 1) Set.univ

Segment 5 derivative continuity: constant function is continuous.

theorem RectHomotopyProof.interval_in_segment (p₁ p₂ : ℝ) (_hp : p₁ < p₂) (h_avoid : ∀ t ∈ Set.Ioo p₁ p₂, t ∉ {1, 2, 3, 4}) (_h_sub : Set.Ioo p₁ p₂ ⊆ Set.Ioo 0 5) : p₂ ≤ 1 ∨ p₁ ≥ 1 ∧ p₂ ≤ 2 ∨ p₁ ≥ 2 ∧ p₂ ≤ 3 ∨ p₁ ≥ 3 ∧ p₂ ≤ 4 ∨ p₁ ≥ 4

An interval (p1, p2) avoiding {1,2,3,4} and inside (0,5) lies in exactly one segment.