An unbounded gap between domination parameters in two graph products

We refute Conjecture 3 in Davila’s Automated Conjecturing with TxGraffiti, which compares ordinary domination in a direct product with total domination in a Cartesian product. A connected bipartite graph H on twelve vertices satisfies γ(P₅×H)=15 and γₜ(P₅□H)=14. Joining copies gives connected bipartite partners on 12m vertices, of maximum degree at most six, with exact values 15m and 14m. Thus the additive gap is unbounded with P₅ fixed. We prove that five is the minimum failing connected factor order; a computer-assisted exclusion proves that twelve is the minimum connected partner order against P₅. The same partner fails against every once-subdivided star, and every connected graph embeds as an induced subgraph of a failing connected factor. For the supremum R₅ of the product-value ratio with P₅ fixed, we prove 9/8≤R₅≤43/38; whether R₅=9/8 remains open. The upper bound combines a Hall assignment with finite exact inequalities. The fractional comparison also fails, with sharp ratio between 17/16 and 10/9. Both lower ratio limits persist with arbitrarily high partner vertex connectivity. A separate computer-assisted theorem gives the sharp tree-partner ratio 43/42, including a failing pair of trees. The twelve-vertex construction, its chains and the subdivided-star values have hand proofs and Lean formalizations. This preprint includes a mathematical supplement and a verification archive specifying the proofs, computational trust and reproduction commands. It has not undergone external peer review. Substantial AI assistance is disclosed in the manuscript.