Corollary 3.7.2 (leaves are exactly the absent labels)

Read-back of corollary_3_7_2.

Fix $n\in\mathbb N$ with $n\ge 2$ (so in particular $n\neq 0$, which is all the NeZero n instance records), a simple graph $T$ on the vertex set $\mathrm{Fin}\,n=\{0,1,\dots,n-1\}$ that is a tree (connected and acyclic), and an arbitrary vertex $k\in\mathrm{Fin}\,n$. The theorem asserts the biconditional

where $\deg_T(k)$ is the ordinary degree of $k$ in the full graph $T$ (the number of vertices of $T$ adjacent to $k$), and $L$ is a specific list of length $n-2$ built as follows. For a subset $S\subseteq\mathrm{Fin}\,n$ and a vertex $v$, let $\mathrm{activeNeighbors}(S,v)=\{w\in S: T.Adj(v,w)\}$, the neighbors of $v$ in $T$ that also lie in $S$; call $v$ an active leaf of $S$ if $v\in S$ and $|\mathrm{activeNeighbors}(S,v)|=1$ (i.e. $v$ has exactly one neighbor remaining inside $S$). Starting from $S_0=\mathrm{Fin}\,n$ and an empty accumulator, repeat for $j=0,1,2,\dots$: let $\ell_j$ be the smallest-indexed active leaf of $S_j$ under the standard order on $\mathrm{Fin}\,n$ — or, if $S_j$ happens to have no active leaf, the junk default $0$ — let $m_j$ be the smallest-indexed member of $\mathrm{activeNeighbors}(S_j,\ell_j)$ (again defaulting to $0$ if that set is empty), set $S_{j+1}=S_j\setminus\{\ell_j\}$, and append $m_j$ to the accumulator. After $i+1$ such steps the accumulator has length $i+1$ and its last entry is, by definition, $\mathrm{pruferEncode}(T)(i)$ for each $i<n-2$ (formally extracted via List.getD with a junk default $0$ that is never actually triggered, since the index $i$ is always in range of the length-$(i+1)$ accumulator); then $L=[\mathrm{pruferEncode}(T)(0),\dots,\mathrm{pruferEncode}(T)(n-3)]$, i.e. exactly this length-$(n-2)$ record of successively-peeled leaves' neighbors — the standard Prüfer-sequence construction (repeatedly strip the least-labeled degree-one vertex of the shrinking vertex set and record its unique surviving neighbor), here made total by the two getD 0 fallbacks for the edge cases where no active leaf, or no active neighbor, exists in $S_j$. In the boundary case $n=2$, $n-2=0$, so $L$ is the empty list and the left-hand side is false for every $k$; correspondingly the unique tree on two vertices is the single edge, so both vertices have degree $1$ and the right-hand side is false as well, so the iff holds trivially there. For $n\ge3$ the statement is the classical fact that a vertex occurs in the Prüfer sequence of a tree iff it is not a leaf of the tree (equivalently, its total degree is at least $2$), asserted here as an exact iff (membership in $L$, not multiplicity, versus degree being different from — not merely at most — $1$).