Common ancestors along contour intervals #
Between the first contour visits to two DFS vertices, the contour visits their longest common prefix and stays among its descendants. Consequently the least discrete height on that interval is the depth of their lowest common ancestor.
The proof works with the existing address lists. Each child contributes one contiguous block and distinct child blocks are separated by a root visit. The internal induction applies to arbitrary contour visits, including repeated visits to the same address; the public statements use the established first-visit times.
theorem
BGW.PlaneTree.lca_prefix_vertexContour_between_visits
{t : PlaneTree}
{a b k : ℕ}
{u v w : List ℕ}
(ha : t.vertexContour[a]? = some u)
(hb : t.vertexContour[b]? = some v)
(hlo : min a b ≤ k)
(hhi : k ≤ max a b)
(hkw : t.vertexContour[k]? = some w)
:
Between any two actual visits, every address remains below their common ancestor.
theorem
BGW.PlaneTree.lca_prefix_vertexContour_between_first_visits
{t : PlaneTree}
{i j k : ℕ}
{u v w : List ℕ}
(hi : t.vertices[i]? = some u)
(hj : t.vertices[j]? = some v)
(hlo : min (2 * i - u.length) (2 * j - v.length) ≤ k)
(hhi : k ≤ max (2 * i - u.length) (2 * j - v.length))
(hkw : t.vertexContour[k]? = some w)
:
Every visit between these first visits remains in the subtree of their LCA.