Proposition 3.7.1 (degree via Prüfer occurrence count)

Read-back. For every natural number $n$ with $n \ge 2$, every simple graph $T$ on the vertex set $\mathrm{Fin}\,n = \{0,1,\dots,n-1\}$ that is a tree (i.e. $T$ is connected and acyclic, per Mathlib's SimpleGraph.IsTree), and every vertex $k \in \mathrm{Fin}\,n$, the statement asserts $T.\mathrm{degree}(k) = \big(\text{Prüfer sequence of } T\big).\mathrm{count}(k) + 1$, where "Prüfer sequence of $T$" is the explicit length-$(n-2)$ list produced as follows. Build a sequence of pairs (active vertex set, accumulated list) starting from $S_0=\mathrm{Fin}\,n$ (all vertices), $L_0=[\,]$; at each step $j\mapsto j+1$, among $v\in S_j$ let $N_j(v):=\{w\in S_j : v\sim_T w\}$ (its "active neighbors"), call $v$ an active leaf of $S_j$ if $v\in S_j$ and $|N_j(v)|=1$, let $\ell_j$ be the least active leaf of $S_j$ in the standard order on $\mathrm{Fin}\,n$ (or the junk value $0$ if no active leaf of $S_j$ exists), let $m_j$ be the least element of $N_j(\ell_j)$ (again $0$ by convention if that set is empty), and set $S_{j+1}=S_j\setminus\{\ell_j\}$, $L_{j+1}=L_j\mathbin{+\!\!+}[m_j]$; the Prüfer sequence is then $[m_0,m_1,\dots,m_{n-3}]$ (the entry at position $i$ is literally the last, and only newly-appended, element of $L_{i+1}$, so the getD 0 fallback used in pruferEncode is never actually triggered on this indexing). The right-hand side counts how many times the fixed vertex $k$ occurs among $m_0,\dots,m_{n-3}$, and the left-hand side is the ordinary graph degree of $k$ in $T$ (the cardinality of its neighbor set). No claim is made about existence/uniqueness of active leaves at each stage beyond what the hypothesis $T.\mathrm{IsTree}$ and the definitions force; in the boundary case $n=2$, $\mathrm{Fin}(n-2)=\mathrm{Fin}\,0$ is empty, so the Prüfer sequence is the empty list, every count is $0$, and the statement reduces to asserting $T.\mathrm{degree}(k)=1$ for each of the two vertices $k$.