Heights along a closed chain with monotone turning

Consider a closed planar chain whose step directions turn monotonically through less than one full turn and whose last two steps point in direction 0. Measure the height of each point of the chain after rotating the direction of one of its steps to the positive real axis. Along the chain the height first rises and then falls, and since the chain closes up the height is nonnegative throughout: the line through that step supports the whole chain.

The statement only records the heights: a step of length d ≥ 0 and direction ψ, measured from a reference direction θ, raises the height by d * sin (ψ - θ).

Main results

• TauCeti.heights_nonneg_of_monotone_turning -- every height of such a chain, measured from the line through one of its steps, is nonnegative.

theorem TauCeti.heights_nonneg_of_monotone_turning {n i : ℕ} (hi : i < n) {H φ : ℕ → ℝ} {Hinf : ℝ} (hmono : ∀ (l m : ℕ), l ≤ m → m ≤ n → φ l ≤ φ m) (hlow : ∀ l ≤ n, -2 * Real.pi < φ l) (hlast : φ n = 0) (hstep : ∀ l < n, ∃ (d : ℝ), 0 ≤ d ∧ H (l + 1) - H l = d * Real.sin (φ l - φ i)) (hclose₁ : ∃ (r : ℝ), 0 ≤ r ∧ Hinf - H n = r * Real.sin (-φ i)) (hclose₂ : ∃ (r : ℝ), 0 ≤ r ∧ H 0 - Hinf = r * Real.sin (-φ i)) (hHi : H i = 0) : (∀ k ≤ n, 0 ≤ H k) ∧ 0 ≤ Hinf

Heights along a closed chain with monotone turning are nonnegative. A closed chain of n + 2 steps starts and ends at height zero: n steps H l ↦ H (l + 1) whose directions φ l are monotone in (-2π, 0] with φ n = 0, followed by two steps through Hinf in direction 0. All heights are measured after rotating the direction φ i of a step i < n to zero, so a step of length d and direction ψ raises the height by d * sin (ψ - φ i). Then every height is nonnegative.