Four-Part Multiset Resolutions of Cylindrical Graphs

A multiset resolving partition distinguishes each vertex of a graph by the unordered multiset of its minimum distances to the partition parts. We prove that every prism formed from two corresponding cycles of length at least ten has multiset partition dimension four, using two singleton parts, one vertical pair and one residual part. Five parts suffice for cycle lengths eight and nine. More generally, we construct optimal four-part partitions of cylindrical graphs using three singleton landmarks in an end cycle and one residual part. For a family of near-antipodal landmark triples, we determine the exact number of layers at which the specified construction first fails. This number is one more than the least positive translation relating two cycle distance profiles, which we compute for odd and even circumferences with explicit collision witnesses. General transfer criteria account for the extra comparisons introduced at landmark vertices. Combining the bipartite criterion with an existing four-landmark theorem also gives a five-part upper bound at every height of at least two for even circumferences of at least twelve. The three-landmark cylinder families have ordinary multiset dimension three. Version 2 adds a public Lean 4 companion organized around 17 paper-facing endpoints. The formal source, theorem map, pinned toolchain, and signed Kernel-Only verification materials are available from the public repository and the archived software record at doi:10.5281/zenodo.22739037. The signed receipt reports only propext, Classical.choice, and Quot.sound, with no project-defined axiom. This machine-checked evidence is distinct from external peer review.