The contour as a walk on vertex addresses

The contour starts at the root, traverses the children in order, and returns to the root after each child. Both endpoint visits are included. Projecting an address to its length gives the existing discrete height contour. Consecutive addresses are adjacent in the graph metric. The first occurrence of the vertex at DFS index i is at contour index 2 * i - depth; this refers to the address itself, not merely to its height.

def BGW.PlaneTree.vertexContour : PlaneTree → List (List ℕ)

Vertex addresses along the complete contour, including both endpoint visits.

Equations

• BGW.PlaneTree.vertexContour = BGW.PlaneTree.fold fun (cs : List (List (List ℕ))) => [] :: (List.mapIdx (fun (i : ℕ) (c : List (List ℕ)) => List.map (List.cons i) c ++ [[]]) cs).flatten

@[simp]

theorem BGW.PlaneTree.vertexContour_node (ts : List PlaneTree) : (node ts).vertexContour = [] :: (List.mapIdx (fun (i : ℕ) (t : PlaneTree) => List.map (List.cons i) t.vertexContour ++ [[]]) ts).flatten

@[simp]

theorem BGW.PlaneTree.vertexContour_leaf : leaf.vertexContour = [[]]

theorem BGW.PlaneTree.vertexContour_ne_nil (t : PlaneTree) : t.vertexContour ≠ []

@[simp]

theorem BGW.PlaneTree.head?_vertexContour (t : PlaneTree) : t.vertexContour.head? = some []

@[simp]

theorem BGW.PlaneTree.getLast?_vertexContour (t : PlaneTree) : t.vertexContour.getLast? = some []

theorem BGW.PlaneTree.map_length_vertexContour (t : PlaneTree) : List.map List.length t.vertexContour = t.contour

Address depth is exactly the height recorded by the discrete contour.

@[simp]

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

Each edge is traversed twice and the initial root visit is also listed.

theorem BGW.PlaneTree.length_vertexContour_add_one (t : PlaneTree) : t.vertexContour.length + 1 = 2 * t.size

An addition-only form of the contour length formula.

theorem BGW.PlaneTree.mem_vertexContour_iff (t : PlaneTree) (u : List ℕ) : u ∈ t.vertexContour ↔ t.IsVertex u

The contour visits precisely the present vertex addresses.

theorem BGW.PlaneTree.isChain_vertexContour (t : PlaneTree) : List.IsChain (fun (u v : List ℕ) => graphDist u v = 1) t.vertexContour

Successive contour visits are joined by one parent-child edge.

theorem BGW.PlaneTree.idxOf_vertexContour_add_length (t : PlaneTree) (u : List ℕ) (hu : t.IsVertex u) : List.idxOf u t.vertexContour + u.length = 2 * List.idxOf u t.vertices

The first contour visit plus vertex depth is twice the DFS index. This addition-only form certifies that the first-visit subtraction never truncates.

theorem BGW.PlaneTree.idxOf?_vertexContour_of_getElem?_vertices {t : PlaneTree} {i : ℕ} {u : List ℕ} (hi : t.vertices[i]? = some u) : List.idxOf? u t.vertexContour = some (2 * i - u.length)

The first visit to the address at DFS index i occurs at 2 * i - depth. idxOf? specifies both this occurrence and the absence of every earlier occurrence.

theorem BGW.PlaneTree.getElem?_contour_first_visit {t : PlaneTree} {i : ℕ} {u : List ℕ} (hi : t.vertices[i]? = some u) : t.contour[2 * i - u.length]? = some u.length

At the first visit to a DFS vertex, the height contour records its depth.