Density of vertices in the contour-coded finite tree

Every grid visit represents the same coded point as the first visit to its address, including return visits. Every interpolated contour point is within distance one of an embedded vertex: in its interpolation cell, choose the endpoint of lower height. The two endpoint heights differ by one, and the contour stays above the lower endpoint throughout that cell.

The zero-duration contour is constant zero, so the singleton case is included. No scaling, measure comparison, or convergence assertion is made here.

theorem BGW.ContinuumTrees.FiniteTree.projection_contourTime_eq_vertexEmbedding (t : PlaneTree) (k : Fin t.contour.length) (u : t.Vertex) (hk : t.vertexContour[↑k]? = some ↑u) : Coding.projection t.contourFunction (t.contourTime k) = vertexEmbedding t u

Every contour visit represents the embedded vertex at its address, even on a return.

theorem BGW.ContinuumTrees.FiniteTree.exists_vertex_dist_le_one (t : PlaneTree) (x : Coding.Space t.contourFunction) : ∃ (u : t.Vertex), dist x (vertexEmbedding t u) ≤ 1

Every point of the contour-coded tree is within one edge length of an embedded vertex.