Joint height and contour convergence at exact size

The contour limit and the global height/contour error give the diagonal joint limit. The deterministic clock comparison transfers it to the library contour convention.

theorem BGW.StableTrees.ExactContour.tendsto_exactHeightContourLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : Filter.Tendsto (fun (k : ℕ) => exactHeightContourLaw μ B (q k) ⋯) Filter.atTop (nhds ((excLaw θ).map fun (p : Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ)) => (p.2, p.2)))

C29 (joint height/contour, exact size): along every unbounded sequence of admissible sizes, the rescaled height (time nt) and contour (time 2nt) of the exact-size BGW tree converge jointly to the excursion height H^exc in BOTH coordinates.

theorem BGW.StableTrees.ExactContour.tendsto_exactHeightLibContourLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : Filter.Tendsto (fun (k : ℕ) => exactHeightLibContourLaw μ B (q k) ⋯) Filter.atTop (nhds ((excLaw θ).map fun (p : Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ)) => (p.2, p.2)))

C29 in the library contour convention (2(n-1)t): the same limit.