The graph metric coded by the interpolated finite-tree contour

Between grid times, the polygonal contour is a convex combination of its two endpoint heights. A discrete lower bound and an attaining grid point therefore identify its continuous interval minimum. Applied between the first visits to two vertices, this minimum is the depth of their lowest common ancestor, so the continuous coding distance is their graph distance.

The first-visit grid indices are explicit Fin arguments. Equal indices include the singleton tree; the upper endpoint of each interval is treated before taking a natural floor, so every interpolation cell used has two valid endpoints.

theorem BGW.ContinuumTrees.ContourCoding.intervalMin_contourTime_of_vertices {t : PlaneTree} (a b : Fin t.contour.length) {u v : List ℕ} (ha : t.vertexContour[↑a]? = some u) (hb : t.vertexContour[↑b]? = some v) : Coding.intervalMin t.contourFunction (t.contourTime a) (t.contourTime b) = ↑(PlaneTree.lca u v).length

Arbitrary grid visits have continuous interval minimum equal to their LCA depth.

theorem BGW.ContinuumTrees.ContourCoding.codingDist_contourTime_of_vertices {t : PlaneTree} (a b : Fin t.contour.length) {u v : List ℕ} (ha : t.vertexContour[↑a]? = some u) (hb : t.vertexContour[↑b]? = some v) : Coding.codingDist t.contourFunction (t.contourTime a) (t.contourTime b) = ↑(PlaneTree.graphDist u v)

Coding distance at any pair of grid visits equals the distance of their addresses.

theorem BGW.ContinuumTrees.ContourCoding.intervalMin_first_visits {t : PlaneTree} {i j : ℕ} {u v : List ℕ} (hi : t.vertices[i]? = some u) (hj : t.vertices[j]? = some v) (a b : Fin t.contour.length) (ha : ↑a = 2 * i - u.length) (hb : ↑b = 2 * j - v.length) : Coding.intervalMin t.contourFunction (t.contourTime a) (t.contourTime b) = ↑(PlaneTree.lca u v).length

The continuous contour minimum between first visits is the depth of the LCA.

theorem BGW.ContinuumTrees.ContourCoding.codingDist_first_visits {t : PlaneTree} {i j : ℕ} {u v : List ℕ} (hi : t.vertices[i]? = some u) (hj : t.vertices[j]? = some v) (a b : Fin t.contour.length) (ha : ↑a = 2 * i - u.length) (hb : ↑b = 2 * j - v.length) : Coding.codingDist t.contourFunction (t.contourTime a) (t.contourTime b) = ↑(PlaneTree.graphDist u v)

The distance coded by the interpolated contour agrees with the vertex graph metric.