The deterministic shifted-height identity

Separate records preceding the shift from records inside the shifted interval. The former attain their final count at the first minimum of the intervening walk.

theorem BGW.StableTrees.DiscreteForest.shiftedHeight_eq (ω : ℕ → ℕ) (m k : ℕ) : shiftedHeight ω m k = ↑(forestHeight (shiftSeq m ω) k)

(Finding 3, deterministic) H_{m+k} - min_{m≤j≤m+k} H_j = H_k of the shifted sequence, for every ω, m, k.