Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Binary codes that do not preserve primitivity

Štěpán Holub, Martin Raška, Štěpán Starosta

TL;DR

This work provides a complete binary-case characterization of not primitivity-preserving codes: a code $B=\{x,y\}$ fails to preserve primitivity iff there exist integers $j,k\ge 1$ with $k=1$ or $j=1$ such that any witnessing primitive list $\mathbf w\in \mathop{\mathrm{lists}} B$ with $|\mathbf w|\ge 2$ has $\mathbf w$ conjugate to $[x]^j[y]^k$ and $\mathop{\mathrm{concat}}\mathbf w$ is imprimitive. With the additional assumption $|y|\le |x|$, the possibilities collapse to the cases $j=2,k=1$ with $x,y$ primitive, or $j=1,k\ge 2$ with $x$ primitive; the paper also gives a complete parametric solution of $x^j y^k = z^\ell$ (for $\ell\ge 2$) and establishes the uniqueness of the exponent pair $(j,k)$. The formalization in Isabelle/HOL centers on $X$-interpretations, a gluing technique for blocks of a word, and a structured collection of lemmas that render the combinatorics of words manageable and reusable for related word equations.

Abstract

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$.

Binary codes that do not preserve primitivity

TL;DR

This work provides a complete binary-case characterization of not primitivity-preserving codes: a code fails to preserve primitivity iff there exist integers with or such that any witnessing primitive list with has conjugate to and is imprimitive. With the additional assumption , the possibilities collapse to the cases with primitive, or with primitive; the paper also gives a complete parametric solution of (for ) and establishes the uniqueness of the exponent pair . The formalization in Isabelle/HOL centers on -interpretations, a gluing technique for blocks of a word, and a structured collection of lemmas that render the combinatorics of words manageable and reusable for related word equations.

Abstract

A code is not primitivity preserving if there is a primitive list 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 -interpretations of the square if . We also provide a formalized parametric solution of the related equation .
Paper Structure (3 sections, 2 theorems)

This paper contains 3 sections, 2 theorems.

Table of Contents

  1. Introduction
  2. Basic facts and notation
  3. Main theorem

Key Result

theorem 1

Let $B = \{x,y\}$ be a code that is not primitivity preserving. Then there are integers $j \geq 1$ and $k \geq 1$, with $k = 1$ or $j = 1$, such that the following conditions are equivalent for any $\mathbf w \in \mathop{\mathrm{\tt lists}}\nolimits B$ with $\left\vert \mathbf w \right\vert \geq 2$: Moreover, assuming $\left\vert y \right\vert \leq \left\vert x \right\vert$,

Theorems & Definitions (4)

  • definition 1
  • theorem 1: bin_imprim_code
  • proof
  • theorem 2: LS_parametric_solution