Proposition 3.7.4 (encoding and decoding are mutually inverse)

Read-back.

For a natural number $n$ with an implicit assumption $hn : 2 \le n$ (which trivially yields $n \neq 0$, contributing no further content beyond $hn$ itself), the statement is a conjunction of two universally quantified claims about a pair of maps between simple graphs on the labeled vertex set $\mathrm{Fin}\,n = \{0,\dots,n-1\}$ and functions $\mathrm{Fin}(n-2) \to \mathrm{Fin}\,n$ (with $n-2$ truncated subtraction, so $n-2=0$ when $n=2$), where these maps are defined by a specific leaf-pruning algorithm: for a graph $T$ and a subset $S \subseteq \mathrm{Fin}\,n$, define $N_S(v) = \{w \in S : T.\mathrm{Adj}(v,w)\}$; call $v$ an active leaf of $S$ if $v \in S$ and $|N_S(v)| = 1$; let $\ell(S)$ be the least (in the standard order on $\mathrm{Fin}\,n$) active leaf of $S$, defaulting to $0$ if $S$ has no active leaf, and let $m(S)$ be the least element of $N_S(\ell(S))$, again defaulting to $0$ if that set is empty. Starting from $(S_0,\mathrm{acc}_0) = (\mathrm{Fin}\,n,\,[\,])$, iterate $(S_{k+1},\mathrm{acc}_{k+1}) = (S_k \setminus \{\ell(S_k)\},\ \mathrm{acc}_k \mathbin{+\!+} [m(S_k)])$; then $\mathrm{pruferEncode}(T)(i)$, for $i \in \mathrm{Fin}(n-2)$, is the $i$-th entry (0-indexed, defaulting to $0$ if out of range) of $\mathrm{acc}_{i+1}$ — i.e. the neighbor recorded at the $(i{+}1)$-st leaf-removal step. Conversely, given $s : \mathrm{Fin}(n-2) \to \mathrm{Fin}\,n$, form the list $[s(0),\dots,s(n-3)]$ and, starting from the full label set $L = \mathrm{Fin}\,n$, decode recursively: on an empty remaining list, take $a$ = least element of $L$ and $b$ = least element of $L \setminus \{a\}$ and output the single-edge graph on $\{a,b\}$ (which degenerates to the empty graph if $a=b$, since a simple graph has no self-loops); on a list with head $p$ and tail $\mathrm{ps}$, let $k$ be the least element of $L$ not occurring in $p :: \mathrm{ps}$, output the graph obtained by adjoining the edge $\{k,p\}$ (via graph-union $\sqcup$) to the recursive decoding of $\mathrm{ps}$ with $L$ replaced by $L \setminus \{k\}$; $\mathrm{pruferDecode}(s)$ is this recursion run on the full list with $L = \mathrm{Fin}\,n$. The theorem then asserts, first, that for every simple graph $T$ on $\mathrm{Fin}\,n$ that is a tree (connected and acyclic) in the sense of SimpleGraph.IsTree, decoding the encoding of $T$ returns $T$ exactly (same adjacency relation), with no hypothesis restricting $n$ beyond $n\ge 2$ (so this includes the case $n=2$, where the only trees are on a two-vertex set and the sequence type $\mathrm{Fin}(n-2)=\mathrm{Fin}\,0$ is empty); and second, that for every function $s : \mathrm{Fin}(n-2) \to \mathrm{Fin}\,n$ whatsoever — with no constraint that $s$ arise from any actual tree — encoding the decoding of $s$ returns $s$ exactly. Jointly these two clauses assert that $\mathrm{pruferEncode}$ and $\mathrm{pruferDecode}$, as literally defined (including their $0$-valued fallbacks whenever a Finset.min is taken of an empty set or a list index falls out of range, fallbacks whose actual invocation on the relevant inputs is not addressed one way or the other by the statement), are mutually inverse bijections between trees on $\mathrm{Fin}\,n$ and arbitrary functions $\mathrm{Fin}(n-2) \to \mathrm{Fin}\,n$.