Contour bracketing using only a strict height prefix

A height bound at the right endpoint excludes bracket indices beyond that endpoint. The resulting comparison uses heights and their oscillations only on the larger prefix.

theorem BGW.PlaneTree.heightSeq_add_le (t : PlaneTree) (m d : ℕ) : t.heightSeq (m + d) ≤ t.heightSeq m + d

Along the DFS order, the height can increase by at most the number of steps.

theorem BGW.PlaneTree.contourLin_bracket_prefix (t : PlaneTree) {m : ℕ} {u : ℝ} (hu0 : 0 ≤ u) (hu : u ≤ ↑t.size) (hbuffer : 2 * u + ↑(t.heightSeq m) ≤ 2 * ↑m) : ∃ i < t.size, i ≤ m ∧ u - 1 ≤ ↑i ∧ ↑i ≤ u + ↑(t.heightSeq i) / 2 ∧ |t.contourLin (2 * u) - ↑(t.heightSeq i)| ≤ |↑(t.heightSeq (i + 1)) - ↑(t.heightSeq i)| + 1

A height bound at m prevents a contour bracket for time 2u from passing m.

theorem BGW.PlaneTree.contourLin_two_mul_sub_heightLin_le_prefix (t : PlaneTree) {m : ℕ} {u ω δ : ℝ} (hu0 : 0 ≤ u) (hu : u ≤ ↑m + 1) (hm : m + 1 ≤ t.size) (hbuffer : 2 * u + ↑(t.heightSeq m) ≤ 2 * ↑m) (hω1 : 1 ≤ ω) (hω2 : ∀ j ≤ m, ↑(t.heightSeq j) / 2 ≤ ω) (hδ : ∀ (x y : ℝ), 0 ≤ x → x ≤ ↑m + 1 → 0 ≤ y → y ≤ ↑m + 1 → |x - y| ≤ ω → |t.heightLin x - t.heightLin y| ≤ δ) : |t.contourLin (2 * u) - t.heightLin u| ≤ 2 * δ + 1

Prefix-local contour/height comparison: all height and modulus hypotheses stop at m+1.