The ordering is a permutation $π$ of $Fin n$, as in the coloring-number concept, and the family is indexed by $Fin k$, so its size is the parameter of the structure rather than a derived cardinality. Paths are stated as walks, as everywhere in this submission: bypassing a walk to a path shrinks its support, so a family of walks meeting only in $v$ yields a family of paths meeting only in $v$ of the same size, and the two readings define the same largest $k$.

The endpoints of a family are automatically pairwise distinct — a shared endpoint would lie on two paths and differ from $v$ — so no injectivity field is carried. $HasAdmAtMost G r k$ says that some ordering admits no family of $k$ paths anywhere, and $adm$ is the least such $k$. The set is nonempty ($k = n + 1$ always qualifies, since a family's endpoints are $k$ distinct vertices other than $v$), so $Nat.sInf ∅ = 0$ is never exercised; on the empty graph every bound holds vacuously and $adm$, $wcol$, $scol$ are all $0$.