The discrete contour of a finite plane tree

The contour records heights during the complete depth-first traversal, starting and ending at the root. Each child contributes its own contour raised by one, followed by a return to height zero. The root-only tree has contour [0]; a tree with n vertices has contour length 2 * (n - 1) + 1, hence traversal duration 2 * (n - 1). Vertex addresses and their lengths identify exactly the heights encountered. This is a list of discrete heights, without any continuous interpolation.

def BGW.PlaneTree.contour : PlaneTree → List ℕ

Heights along the complete depth-first contour, including both endpoint visits.

Equations

• BGW.PlaneTree.contour = BGW.PlaneTree.fold fun (cs : List (List ℕ)) => 0 :: (List.map (fun (c : List ℕ) => List.map Nat.succ c ++ [0]) cs).flatten

@[simp]

theorem BGW.PlaneTree.contour_node (ts : List PlaneTree) : (node ts).contour = 0 :: (List.map (fun (t : PlaneTree) => List.map Nat.succ t.contour ++ [0]) ts).flatten

@[simp]

theorem BGW.PlaneTree.contour_leaf : leaf.contour = [0]

theorem BGW.PlaneTree.contour_ne_nil (t : PlaneTree) : t.contour ≠ []

@[simp]

theorem BGW.PlaneTree.head?_contour (t : PlaneTree) : t.contour.head? = some 0

@[simp]

theorem BGW.PlaneTree.getLast?_contour (t : PlaneTree) : t.contour.getLast? = some 0

theorem BGW.PlaneTree.isChain_contour (t : PlaneTree) : List.IsChain (fun (a b : ℕ) => a + 1 = b ∨ b + 1 = a) t.contour

Every contour step changes height by exactly one; for the root-only tree this is vacuous.

theorem BGW.PlaneTree.length_contour_add_one (t : PlaneTree) : t.contour.length + 1 = 2 * t.size

An addition-only form of the contour length formula.

@[simp]

theorem BGW.PlaneTree.length_contour (t : PlaneTree) : t.contour.length = 2 * (t.size - 1) + 1

The contour has one more entry than its traversal duration.

theorem BGW.PlaneTree.mem_contour_iff (t : PlaneTree) (h : ℕ) : h ∈ t.contour ↔ ∃ (u : List ℕ), t.IsVertex u ∧ u.length = h

The contour visits exactly the depths of the tree's vertex addresses.