 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.