  A code $X$ is not primitivity preserving if there is a primitive list
${\mathbf w} \in {\tt lists} X$ whose concatenation is imprimitive. We
formalize a full characterization of such codes in the binary case in the proof
assistant Isabelle/HOL. Part of the formalization, interesting on its own, is a
description of $\{x,y\}$-interpretations of the square $xx$ if $|y| \leq |x|$.
We also provide a formalized parametric solution of the related equation
$x^jy^k = z^\ell$.
