Binary codes that do not preserve primitivity

Abstract

A code $X$ is not primitivity preserving if there is a primitive list $\mathbf{w}\in \mathtt{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|\le |x|$. We also provide a formalized parametric solution of the related equation $x^j{y}^k=z^{\ell }$.

References in corpus (1)

• Binary codes that do not preserve primitivity

Cited by in corpus (1)

• Binary codes that do not preserve primitivity