Proposition 3.7.3 (decoding always yields a tree)

Read‑back of GYGraphTheory.prop_3_7_3.

Fix a natural number $n$ with $n\ge 2$ and an arbitrary function $s:\mathrm{Fin}(n-2)\to\mathrm{Fin}\,n$ — no injectivity, surjectivity, or any other condition is imposed on $s$; it may repeat values or even be constant (e.g. $s\equiv 0$). Write $P=[s_0,\dots,s_{n-3}]$ for the list List.ofFn s (empty when $n=2$, since $\mathrm{Fin}(0)$ has no elements). Define a graph pruferDecodeAux P L on vertex set $\mathrm{Fin}\,n$ by recursion on the list argument, starting from $L=\{0,\dots,n-1\}$ (all of $\mathrm{Fin}\,n$): given a nonempty remaining list with head $p$ and tail $\mathit{ps}$ and current set $L$, let $k$ be the least element of $L\setminus(\{p\}\cup\{\text{elements of }\mathit{ps}\})$ — i.e. the smallest label still "available" that does not occur anywhere in the as‑yet‑unprocessed part of the sequence — defaulting to $0$ if that set happens to be empty; add the edge $\{k,p\}$ (silently dropped if $k=p$, since fromEdgeSet discards self‑loops) and recurse on $\mathit{ps}$ with $k$ removed from $L$, taking the union (of edge sets, via $\sqcup$) with this edge. When the list is exhausted, take $a=\min L$ and $b=\min(L\setminus\{a\})$ (each defaulting to $0$ if the relevant set is empty) and output the single edge $\{a,b\}$ (again dropped if $a=b$). This produces up to $n-2$ edges from the recursive steps plus one final edge from the base case — the standard Prüfer‑sequence decoding procedure. pruferDecode s is this graph run on the full input $P$ starting from $L=\mathrm{Fin}\,n$ (as a Finset). (The hypothesis hn : 2 ≤ n is used only to derive the typeclass instance NeZero n via omega, so that Fin n and the decoding are well‑formed; it contributes no separate mathematical content beyond enabling the statement to typecheck.)

The theorem asserts: for every $n\ge 2$ and for every function $s:\mathrm{Fin}(n-2)\to\mathrm{Fin}\,n$ whatsoever (with no further hypotheses), the graph pruferDecode s on the $n$‑element vertex set $\mathrm{Fin}\,n$ is a tree in Mathlib's sense — that is, it is connected (any two vertices are joined by a path) and acyclic (it contains no cycle), which in particular forces it to have exactly $n-1$ edges and forces the vertex type $\mathrm{Fin}\,n$ to be nonempty (automatic here since $n\ge 2$). No claim is made about the relationship between $s$ and the tree beyond this: the statement covers every conceivable input sequence uniformly, including degenerate ones such as $n=2$ (where $\mathrm{Fin}(0)$ is empty, so the "decoding" is forced to be the single base‑case edge $\{0,1\}$ regardless of $s$) and constant or repeated‑value sequences, and it says nothing about uniqueness of $s$ for a given tree or about any inverse (encoding) map.