The subdivision reading and the model stated here are the same notion: subdividing an edge k times replaces it by a path of length k+1, so a subdivision of H with at most 2r subdivisions per edge embeds into G exactly when the vertices of H can be sent injectively to principal vertices of G and the edges to connecting paths of length at most 2r+1 that are pairwise internally disjoint and avoid all principal vertices internally. The model carries that data directly.

Connecting walks are indexed by adjacent pairs of vertices of $H$ rather than by the edge set, which keeps $Sym2$ and its membership plumbing off the surface. The two orientations of one edge therefore each carry a walk, and the two are deliberately not required to be reverses of each other: the $disjoint$ field concludes that the two edges agree, so it never fires on the two orientations of a single edge and forces nothing between them. Either orientation's walk witnesses that edge of the subdivision, and a model in the usual edge-indexed form gives one here by sending the reversed orientation to the reversed walk.

Walks rather than paths, as everywhere in this submission: bypassing a walk to a path shortens it and shrinks its support, so it preserves both the length bound and the disjointness conditions, and the two readings define the same relation. $principal_inj$ is not derivable from the other fields — nothing constrains vertices of $H$ that share no edge — and it is exactly the notes' requirement that principal vertices be distinct.

No numeric topological grad is introduced, for the reason the ordinary-minor density concept gives: every statement of this submission supplies a concrete bound d rather than consuming a number, so a $sInf$-defined ∇̃ would be review surface that no claim uses. Edges are counted as the natural cardinality ($Set.ncard$) of $edgeSet$, and minors range over the canonical carriers $Fin m$, as in the ordinary-minor concepts.