Depth-first degree sequences

The degree sequence visits the root first, then each child subtree in its child order. Subtracting one in ℤ gives the Łukasiewicz increments: their sum is -1, and each strict prefix has nonnegative sum.

This is the forward coding direction used in Section 2 of Kortchemski–Vetter, Rare subtree patterns in size-conditioned Bienaymé trees. Reconstruction and the identification of fringe segments are separate results.

def BGW.PlaneTree.degrees : PlaneTree → List ℕ

Outdegrees in root-first depth-first order, counting every vertex occurrence.

Equations

• BGW.PlaneTree.degrees = BGW.PlaneTree.fold fun (ds : List (List ℕ)) => ds.length :: ds.flatten

@[simp]

theorem BGW.PlaneTree.degrees_node (ts : List PlaneTree) : (node ts).degrees = ts.length :: (List.map degrees ts).flatten

@[simp]

theorem BGW.PlaneTree.length_degrees (t : PlaneTree) : t.degrees.length = t.size

theorem BGW.PlaneTree.sum_degrees_add_one (t : PlaneTree) : t.degrees.sum + 1 = t.size

The sum of all outdegrees is one less than the number of vertices.

def BGW.PlaneTree.increments (t : PlaneTree) : List ℤ

Integer Łukasiewicz increments; subtraction is not truncated at zero.

Equations

• t.increments = List.map (fun (d : ℕ) => ↑d - 1) t.degrees

@[simp]

theorem BGW.PlaneTree.increments_node (ts : List PlaneTree) : (node ts).increments = (↑ts.length - 1) :: (List.map increments ts).flatten

@[simp]

theorem BGW.PlaneTree.length_increments (t : PlaneTree) : t.increments.length = t.size

theorem BGW.PlaneTree.sum_increments (t : PlaneTree) : t.increments.sum = -1

The Łukasiewicz path ends at -1.

theorem BGW.PlaneTree.neg_one_le_increment (t : PlaneTree) {x : ℤ} (hx : x ∈ t.increments) : -1 ≤ x

theorem BGW.PlaneTree.sum_take_increments_nonneg (t : PlaneTree) {i : ℕ} (hi : i < t.increments.length) : 0 ≤ (List.take i t.increments).sum

Before its final increment, the Łukasiewicz path stays nonnegative.

theorem BGW.PlaneTree.map_fringe?_vertices_rootDegree (t : PlaneTree) : List.map (fun (u : List ℕ) => Option.map rootDegree (t.fringe? u)) t.vertices = List.map some t.degrees

The recursive degree sequence agrees with fringe lookup at the actual DFS addresses. The Option codomain avoids assigning an artificial degree to an invalid address.

def BGW.PlaneForest.size (ts : PlaneForest) : ℕ

Total number of vertices in a finite ordered forest.

Equations

• ts.size = (List.map BGW.PlaneTree.size ts).sum

def BGW.PlaneForest.increments (ts : PlaneForest) : List ℤ

Concatenate the depth-first increment sequences in component order.

Equations

• ts.increments = (List.map BGW.PlaneTree.increments ts).flatten

@[simp]

theorem BGW.PlaneForest.length_increments (ts : PlaneForest) : ts.increments.length = ts.size

theorem BGW.PlaneForest.sum_increments (ts : PlaneForest) : ts.increments.sum = -↑(List.length ts)

Each component contributes one net downward step, including the empty forest.