Discrete height and ancestral minima of the Łukasiewicz path

Height is the length of a valid DFS vertex address, with the root at index zero. The path is the integer sum of increments strictly before its time index. The finite-height domain excludes the terminal path time. A fringe occupies one contiguous address block, and its path first falls below its starting value at the end of that block.

These are the discrete conventions used in Le Gall, Random trees and applications, Proposition 1.2, and in the height/Łukasiewicz definitions of Kortchemski, A simple proof of Duquesne's theorem on contour processes of conditioned Galton–Watson trees, Section 1.1 (local source lines 424–445).

def BGW.PlaneTree.height (t : PlaneTree) (i : Fin t.size) : ℕ

Height at an actual DFS vertex index; the terminal path index is excluded.

Equations

• t.height i = t.vertices[↑i].length

def BGW.PlaneTree.lukasiewicz (t : PlaneTree) (k : ℕ) : ℤ

Integer prefix sums of the DFS increments. This total function saturates after tree size.

Equations

• t.lukasiewicz k = (List.take k t.increments).sum

theorem BGW.PlaneTree.vertices_fringe_prefix {t s : PlaneTree} {u : List ℕ} {i : ℕ} (hi : t.vertices[i]? = some u) (hs : t.fringe? u = some s) : List.map (fun (v : List ℕ) => u ++ v) s.vertices <+: List.drop i t.vertices

The reattached DFS addresses of a fringe form a contiguous block at its root index.

theorem BGW.PlaneTree.isPrefix_iff_dfs_in_fringe {t s : PlaneTree} {u v : List ℕ} {j i : ℕ} (hj : t.vertices[j]? = some u) (hi : t.vertices[i]? = some v) (hs : t.fringe? u = some s) : u <+: v ↔ j ≤ i ∧ i < j + s.size

An address is a descendant exactly when its DFS index lies in the fringe block.

theorem BGW.PlaneTree.fringe_end_le_size {t s : PlaneTree} {u : List ℕ} {i : ℕ} (hi : t.vertices[i]? = some u) (hs : t.fringe? u = some s) : i + s.size ≤ t.size

The complete fringe block ends no later than the tree's terminal path time.

theorem BGW.PlaneTree.lukasiewicz_fringe_end {t s : PlaneTree} {u : List ℕ} {i : ℕ} (hi : t.vertices[i]? = some u) (hs : t.fringe? u = some s) : t.lukasiewicz (i + s.size) = t.lukasiewicz i - 1

At the end of a fringe block, the path is one below its value at the fringe root.

theorem BGW.PlaneTree.lukasiewicz_ge_at_fringe {t s : PlaneTree} {u : List ℕ} {i k : ℕ} (hi : t.vertices[i]? = some u) (hs : t.fringe? u = some s) (hik : i ≤ k) (hk : k < i + s.size) : t.lukasiewicz i ≤ t.lukasiewicz k

Before the fringe ends, every path value is at least its value at the fringe root.

theorem BGW.PlaneTree.lukasiewicz_recordMin_iff_before_fringe_end {t s : PlaneTree} {u : List ℕ} {j i : ℕ} (hj : t.vertices[j]? = some u) (hs : t.fringe? u = some s) (_hji : j ≤ i) : (∀ (k : ℕ), j ≤ k → k ≤ i → t.lukasiewicz j ≤ t.lukasiewicz k) ↔ i < j + s.size

The weak running-minimum condition stops exactly at the end of the fringe block.

theorem BGW.PlaneTree.isPrefix_iff_lukasiewicz_recordMin {t : PlaneTree} {u v : List ℕ} {j i : ℕ} (hj : t.vertices[j]? = some v) (hi : t.vertices[i]? = some u) (hji : j ≤ i) : v <+: u ↔ ∀ (k : ℕ), j ≤ k → k ≤ i → t.lukasiewicz j ≤ t.lukasiewicz k

Among preceding vertices, ancestry is exactly a weak running-minimum condition. The interval includes both the candidate ancestor and the target vertex.

theorem BGW.PlaneTree.length_eq_card_recordMin_of_getElem?_vertices {t : PlaneTree} {u : List ℕ} {i : ℕ} (hi : t.vertices[i]? = some u) : u.length = {j ∈ Finset.range i | ∀ (k : ℕ), j ≤ k → k ≤ i → t.lukasiewicz j ≤ t.lukasiewicz k}.card

The length of a DFS address counts the strict preceding weak record minima. The target index itself is excluded from the count and included in each tested interval.

theorem BGW.PlaneTree.height_eq_card_recordMin (t : PlaneTree) (i : Fin t.size) : t.height i = {j ∈ Finset.range ↑i | ∀ (k : ℕ), j ≤ k → k ≤ ↑i → t.lukasiewicz j ≤ t.lukasiewicz k}.card

The discrete height process is recovered from the Łukasiewicz path by counting ancestors.