A counterexample to packing-domination inheritance in strong products

Abstract

The d-distance p-packing domination number of a graph is the minimum size of a set that dominates within distance d and separates distinct centers by distance at least p+1, with value infinity when no such set exists. Bujtás, Iršič Chenoweth, Klavžar and Zhang conjectured that nonexistence in one factor is inherited by every strong product containing that factor. We construct a finite connected simple graph H, with 608 vertices and 9,168 edges, for which the binary six-cube Q6 admits no 2-distance dominating 3-packing but its strong product with H admits one with 64 centers. The auxiliary graph uses singleton and distance-four pair supports in the binary six-cube. Compatibility of support unions prevents short paths between incompatible code labels, while explicit eight-label sets provide radius-two coverage at pair vertices. We give a complete proof from actual graph adjacency. A Lean formalization checks the complete existence-level counterexample on finite simple graphs and standard graph walks; two separately implemented exact checkers reconstruct and verify the finite graph and its same-center covering witness. The numerical optimum is not determined, and historical priority is not asserted.