Clusters are indexed by vertices — $X : Fin n → Set (Fin n)$, cluster $X u$ centered at $u$ — rather than given as a bare family of sets. The ordering-based construction that discharges the existence theorem produces exactly this shape (one cluster per vertex, some possibly empty, $X u$ inside the 2$r$-ball of $u$), the algorithm's cover-assignment map "read the truth of a formula at $v$ inside the cluster of $f(v)$" needs the index to point at a center, and a bare family is recovered as the image of the indexing if ever needed. Centering also makes the radius condition self-witnessing: $X u$ lies in the ball of its own index, no existential center.

The three fields quantify over all of $Fin n$, including vertices outside every cluster of interest; an empty cluster satisfies both the radius and the degree conditions vacuously, so this costs nothing. Degree is stated with $Set.ncard$, the cardinality idiom of the Lax12 concepts this submission composes with.