Prüfer encoding and decoding of labeled trees

activeNeighbors. For a natural number $n$ with $n \neq 0$ (fixed throughout via the [NeZero n] assumption), a simple graph $T$ on the vertex set $\mathrm{Fin}\ n = \{0,1,\dots,n-1\}$ (so $T$'s adjacency relation $T.\mathrm{Adj}$ is symmetric and irreflexive — no vertex is adjacent to itself), a finite subset $S \subseteq \mathrm{Fin}\ n$, and a vertex $v \in \mathrm{Fin}\ n$, activeNeighbors $T\,S\,v$ is defined as the finite set $\{\, w \in S : T.\mathrm{Adj}(v,w) \,\}$ — i.e. those elements of $S$ that are $T$-adjacent to $v$. Note $v$ itself need not lie in $S$, and if $v \notin S$ or $v$ has no neighbors in $S$ this set is simply empty.

IsActiveLeaf. For the same data $T, S$ and a vertex $v$, the proposition IsActiveLeaf $T\,S\,v$ holds exactly when $v \in S$ and $|\{\, w \in S : T.\mathrm{Adj}(v,w)\,\}| = 1$, i.e. $v$ belongs to $S$ and $v$ has exactly one $T$-neighbor lying in $S$ (using activeNeighbors as defined above). This says nothing about $v$'s neighbors outside $S$, and it is a strict equality to $1$: a vertex in $S$ with zero or with two-or-more active neighbors does not satisfy this predicate.

leastActiveLeaf. For $T$ and $S$ as above, leastActiveLeaf $T\,S$ first forms the sub-finset of $S$ consisting of those $v \in S$ that are active leaves in the above sense (i.e. $\{v \in S : v \in S \text{ and } v \text{ has exactly one } T\text{-neighbor in } S\}$, which is just the set of active leaves of $S$), then takes its minimum under the standard order on $\mathrm{Fin}\ n$ ($0 < 1 < \cdots < n-1$), and if that set of active leaves is empty, returns the default/junk value $0 \in \mathrm{Fin}\ n$ instead (which is a genuine element since $n \neq 0$). So the output is: the smallest-labeled vertex of $S$ that has exactly one $T$-neighbor in $S$, when such a vertex exists; and it is the numeral $0$ — indistinguishable, by this definition alone, from a genuine leaf labeled $0$ — whenever $S$ has no active leaf at all (this is expected to happen only outside the "intended" regime $|S| \geq 2$, per the doc comment, but the definition itself imposes no such hypothesis and is total on all $S$).

leastActiveLeafNeighbor. For $T$ and $S$, this takes $v_0 :=$ leastActiveLeaf $T\,S$ (as just described, possibly the junk value $0$), computes its active-neighbor set $\{\, w \in S : T.\mathrm{Adj}(v_0,w)\,\}$, and returns the minimum element of that set under the order on $\mathrm{Fin}\ n$, again defaulting to $0$ if that set is empty. Thus the result is: the smallest-labeled $T$-neighbor of the least active leaf that also lies in $S$ — which, when $v_0$ genuinely is an active leaf, is its unique such neighbor (so "least" is redundant there, since there is only one) — and it falls back to the junk value $0$ whenever that neighbor set is empty, in particular whenever $S$ had no active leaf to begin with (so $v_0$ was already junk) or, degenerately, whenever the found $v_0$ happens to have no $T$-neighbor inside $S$.

pruferPeel. This is a function defined for every natural number $k$ (not just those in some intended range), taking values in pairs (finite subset of $\mathrm{Fin}\ n$, list of elements of $\mathrm{Fin}\ n$), by recursion on $k$, for a fixed graph $T$. At $k=0$ it is $(\mathrm{Fin}\ n{,}\ [\,])$: the full vertex set (all $n$ labels, nonempty since $n\neq0$) paired with the empty list. Given its value $(S,\mathrm{acc})$ at some $k$, its value at $k+1$ is $(S \setminus \{v_0\},\ \mathrm{acc} \,{+\!\!+}\, [w_0])$, where $v_0 =$ leastActiveLeaf $T\,S$ is removed from $S$ (erasing an element not present is a no-op, relevant if $v_0$ is the junk value $0$ and $0 \notin S$), and $w_0 =$ leastActiveLeafNeighbor $T\,S$ is appended to the accumulator list. So, informally, step $k+1$ removes the smallest-labeled active leaf of the current active set from that set and records (the smallest label of) its unique remaining neighbor — and it does this uniformly for every $k$, including $k$ far beyond $n-2$ (where $S$ may already be very small, empty, or have no active leaf, in which case the junk-value fallbacks of leastActiveLeaf/leastActiveLeafNeighbor silently kick in and the "peel" degenerates to repeatedly appending $0$).

pruferEncode. For a graph $T$ and an index $i$ ranging over $\mathrm{Fin}(n-2)$ — where $n-2$ is truncated natural-number subtraction, so this type is empty whenever $n \le 2$, making pruferEncode vacuously have no outputs to specify in that case — pruferEncode $T\,i$ is defined as the entry at position $i$ (0-indexed) of the list-component of pruferPeel $T\,(i+1)$, using List.getD with default value $0$ if that position is out of range. Since the list produced after $i+1$ applications of the peeling step (as defined above) always has exactly $i+1$ entries, the requested index $i$ always exists and refers to the last entry appended, so no default value is ever actually triggered here; concretely, pruferEncode $T\,i$ equals leastActiveLeafNeighbor $T\,S_i$, where $S_i$ is the active vertex set remaining after $i$ peeling steps from the full vertex set (i.e. the $(i+1)$-th recorded neighbor label in the peeling process). Thus pruferEncode $T$ is a function $\mathrm{Fin}(n-2) \to \mathrm{Fin}\ n$ giving, for each of the first $n-2$ peeling steps, the neighbor label recorded at that step — the usual "Prüfer sequence" of $T$ under this specific leaf-peeling rule, well-defined (non-junk) precisely to the extent that each successive active set genuinely has an active leaf; if it does not, the corresponding sequence entries silently become $0$ via the upstream junk-value defaults, with no signal in the type that this happened.

pruferDecodeAux. This is a function taking a list $P$ of elements of $\mathrm{Fin}\ n$ and a finite set $L \subseteq \mathrm{Fin}\ n$ of "available labels," returning a simple graph on $\mathrm{Fin}\ n$, defined by recursion on $P$. In the base case $P = [\,]$: let $a$ be the minimum element of $L$ (or $0$ if $L$ is empty) and $b$ the minimum element of $L$ with $a$ removed (or $0$ if that is empty, i.e. if $L$ has at most one element); the result is the graph whose only possible edge is $\{a,b\}$ — via SimpleGraph.fromEdgeSet, which automatically discards a "loop" $\{a,b\}$ with $a=b$ since simple graphs are irreflexive — so this yields the single edge joining $L$'s two smallest elements when $|L| \ge 2$ and $a \ne b$, and yields the empty graph (no edges at all) whenever $L$ has fewer than two elements, or degenerately whenever the two computed values coincide (e.g. $|L|=1$ and its element happens to be $0$, or $L=\emptyset$). In the recursive case $P = p :: ps$ (head $p$, tail $ps$): let $k$ be the minimum element of $L \setminus \{\text{labels occurring anywhere in } p::ps\}$ (or $0$ if no such element exists, i.e. if every element of $L$ already occurs in the remaining list $p::ps$); the result is the graph pruferDecodeAux $ps\,(L \setminus \{k\})$ (the recursive decoding of the tail on $L$ with $k$ removed) unioned (edge-set union, ⊔) with the single-edge graph on $\{k,p\}$ (again silently containing no edge if $k = p$). Thus, informally and when no junk case is triggered, this implements the standard Prüfer-sequence decoding: repeatedly attach an edge from the smallest currently-available label not still needed later in the sequence to the current sequence entry, shrinking the available-label pool by one each step, with a final edge joining whichever two labels remain once the sequence is exhausted; but the definition is total and silently produces missing/degenerate edges (via the described 0-fallbacks and self-loop suppression) whenever $L$ does not have the size the recursion expects at that point.

pruferDecode. For a function $s : \mathrm{Fin}(n-2) \to \mathrm{Fin}\ n$ (again vacuous data, i.e. the empty function, whenever $n \le 2$), pruferDecode $s$ is defined as pruferDecodeAux applied to the list $[s(0), s(1), \dots, s(n-3)]$ (the values of $s$ listed in increasing order of index, via List.ofFn) together with $L = \mathrm{Fin}\ n$, the full set of all $n$ vertex labels, as the initial available-label pool. It returns a simple graph on $\mathrm{Fin}\ n$, built by the recursive procedure of pruferDecodeAux described above, starting from all $n$ labels available and consuming exactly the $n-2$ entries of $s$ in order before the base-case final edge.