Polygonal contours and the library clock

The unnormalized polygonal contour agrees with the library's hat-function interpolation when time is multiplied by the number of contour steps.

theorem BGW.PlaneTree.contourAt_zero (t : PlaneTree) : t.contourAt 0 = 0

The first contour value is zero.

theorem BGW.PlaneTree.contourAt_end (t : PlaneTree) : t.contourAt (2 * (t.size - 1)) = 0

The contour value at its final listed time is zero.

theorem BGW.PlaneTree.contourLin_of_end_le (t : PlaneTree) {s : ℝ} (hs : ↑(2 * (t.size - 1)) ≤ s) : t.contourLin s = 0

The polygonal contour vanishes at and after the final listed time.

theorem BGW.PlaneTree.contourFunction_eq_contourLin (t : PlaneTree) (s : ↑unitInterval) : t.contourFunction s = t.contourLin (↑(2 * (t.size - 1)) * ↑s)

The library contour is the same interpolation at duration times the unit parameter.

theorem BGW.PlaneTree.abs_contourAt_succ_sub_le (t : PlaneTree) (m : ℕ) : |↑(t.contourAt (m + 1)) - ↑(t.contourAt m)| ≤ 1

Consecutive totalized contour values differ by at most one.

theorem BGW.PlaneTree.abs_contourLin_sub_le (t : PlaneTree) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : |t.contourLin x - t.contourLin y| ≤ |x - y|

The polygonal contour, continued by zero, has speed at most one at nonnegative times.

theorem BGW.PlaneTree.paperContourFunction_eq_contourLin (t : PlaneTree) (s : ↑unitInterval) : t.paperContourFunction s = t.contourLin (2 * ↑t.size * ↑s)

The paper-clock contour evaluates the original polygonal contour at 2 * size * s.