Uniform derivative bound for the homotopy

Proves a uniform bound ‖deriv_t H(t,s)‖ ≤ 5 for all (t,s) ∈ [0,5] × [0,1], handling each segment case and the non-differentiable fallback.

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_deriv_bound : ∃ (M : ℝ), ∀ t ∈ Set.Icc 0 5, ∀ s ∈ Set.Icc 0 1, ‖deriv (fun (t' : ℝ) => fdBoundaryToPolygonHomotopy (t', s)) t‖ ≤ M