= Excursion coding theorem for compact real trees
Every compact <real tree> is <isometric> to a <real tree encoded by an excursion>. One construction takes finite subtrees spanning successively finer finite nets, performs depth-first contour traversals of those subtrees, and chooses compatible time parameterizations. The contour functions have a uniformly convergent subsequence, and continuity of excursion coding in the <Gromov-Hausdorff distance> identifies the limiting coded tree with the original tree.
Back to article page