Degree prefixes determine interpolated height prefixes

Record minima recover every height through the degree-prefix index. One extra degree determines the final interpolation interval, including the test that its vertex exists.

theorem BGW.StableTrees.ExactPair.exists_treePairPath_eq_comp_treePrefix (B : ℕ → ℝ) (n : ℕ) (a : NNReal) {m : ℕ} (hm : ⌊↑a * ↑n⌋₊ + 1 ≤ m) : ∃ (G : List ℕ → Skorokhod.D ↑a ℝ × C(↑(Set.Icc 0 ↑a), ℝ)), ∀ (τ : LocallyFinite.Tree), TailPair.treePairPath B n a τ = G (DiscreteForest.treePrefix m τ)

Prefix measurability of the pair (deterministic repair): the pair on [0,a] reads the walk up to index ⌊an⌋ and the heights up to index ⌊an⌋ + 1, hence it is a function of the first m DFS degrees for every m ≥ ⌊an⌋ + 1 (in general not of the first ⌊an⌋).