\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{microtype}
\usepackage{booktabs}
\usepackage{xurl}
\usepackage[colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref}
\hypersetup{pdftitle={Set Cover by Cyclic Rotations Is NP-Complete},pdfauthor={Yuran Xiu}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newcommand{\Z}{\mathbb Z}
\newcommand{\N}{\mathbb N}
\newcommand{\NP}{\mathsf{NP}}
\newcommand{\FP}{\mathsf{FP}}
\newcommand{\CC}{\mathsf{CyclicCover}}
\newcommand{\bits}{\operatorname{bits}}
\newcommand{\pair}{\operatorname{pair}}
\newcommand{\wt}{\operatorname{wt}}
\newcommand{\cl}{\operatorname{cl}}
\newcommand{\res}[1]{\overline{#1}}
\title{Set Cover by Cyclic Rotations Is NP-Complete}
\author{Yuran Xiu\\
Institute for Interdisciplinary Information Sciences, Tsinghua University\\
\texttt{xiuyr23@mails.tsinghua.edu.cn}}
\date{October 15, 2026}

\begin{document}
\maketitle

\begin{abstract}
Given an explicitly listed binary pattern of positive length $n$ and a
nonnegative integer $b$ in binary, can at most $b$ cyclic rotations of the
pattern cover all $n$ positions? We prove that this decision problem is
NP-complete. The reduction constructs a pattern in a cyclic group of
polynomial order and outputs its entire indicator word. Its principal
ingredient is a replicated-marker construction: a cover within the budget
must choose one translate in every layer, and each failed difference
constraint leaves a block of more holes than the remaining translates can
cover. Combining this construction with the known embedding of graph
cliques into circulant graphs using distinct three-term sums gives a
polynomial-time reduction from $3$SAT. The theorem allows every subset,
including the empty pattern, and every binary budget. A Lean formalization
checks the mathematical reduction, the full-word polynomial-time programs,
NP membership, and the unconditional NP-hardness foundation.
\end{abstract}

\section{Introduction}
\label{sec:introduction}

Let $S$ be a subset of the cyclic group $\Z_n=\Z/n\Z$, where $n\geq 1$.
Its translates are $S+t=\{s+t:s\in S\}$, for $t\in\Z_n$. The covering
number is
\[
 \tau(S,\Z_n)=\min\{|T|:T\subseteq\Z_n,\ S+T=\Z_n\},
\]
with value $+\infty$ if there is no cover. Thus the only pattern without a
cover is $S=\varnothing$. All of the sets available to the covering
algorithm are rotations of a single input pattern. This restriction is
substantial: deleting a chosen set and the positions it covers generally
does not leave an instance of the same form.

Wirth introduced this problem as \emph{pattern rotation} in
Section~2.7 of his dissertation~\cite{wirth}. He asked about its
computational complexity and distinguished finding a minimum covering
family from deciding a covering-number bound. The problem appeared again
as Open Problem~4, \emph{Set-Cover by Rotations}, attributed to Anthony
Wirth in the WADS 2023 open-problems collection~\cite{wads}.
Covering numbers of this kind also form part of the broader study of
covering groups by translates of a set; see Bollob\'as, Janson, and
Riordan~\cite{bjr}. We settle the decision classification for an explicitly
given pattern.

\begin{theorem}\label{thm:main}
The following language is NP-complete under polynomial-time many-one
reductions: an instance consists of an explicitly listed word
$s\in\{0,1\}^n$, with $n\geq1$, and a nonnegative integer $b$ encoded in
binary; it is accepted precisely when, for
$S=\{i\in\Z_n:s_i=1\}$, there exists $T\subseteq\Z_n$ such that
\[
 |T|\leq b \qquad\text{and}\qquad S+T=\Z_n.
\]
NP-hardness already holds for nonempty patterns and budgets $b\leq n$.
\end{theorem}

The pattern in this statement is the complete $n$-bit word. Its length is
part of the input size; the theorem does not concern a succinct description
of an exponentially long pattern. Neither nonemptiness of $S$ nor an upper
bound on $b$ is a promise in the unrestricted language.

The central construction is a reduction from cyclic difference constraints
to translate covering. In $\Z_m\times\Z_L$, the template has one dense
slice and $m-1$ sparse slices. The dense slice has blocks of $m$ holes.
Each block represents a constraint between two chosen phases. A sufficiently
large $L$ forces a cover of size at most $m$ to select exactly one translate
in every layer. The markers are spaced so that a sparse slice covers either
its entire intended block or at most one marker of a block. Consequently,
$m-1$ unintended contributions cannot cover a failed block of $m$ holes.
We choose $L\equiv1\pmod m$, so the product group is an ordinary cyclic
group of order $mL$.

To supply the difference constraints, we use the established
three-sum-distinct clique embedding. Codenotti, Gerace, and Vigna used this
method for circulant graphs~\cite{cgv}; Godsil and Rooney state and prove
the corresponding finite abelian-group lemma~\cite[Lemma~6.1]{gr}.
We give the required proof, including an explicit polynomial-size family of
labels. The replicated-marker covering construction is the contribution
of this paper; the clique embedding and the $3$SAT occurrence-graph
reduction are credited ingredients.

Sections~\ref{sec:language}--\ref{sec:reduction} give a mathematical proof
and an explicit polynomial-time algorithm. Section~\ref{sec:formal}
describes the checked language, its correspondence with the set formulation,
and the formal reproduction evidence.

\section{The encoded problem and NP membership}
\label{sec:language}

We fix a binary encoding to include malformed inputs and arbitrarily large
budgets in the statement. For words $s$ and $\beta$, define
$\pair(s,\beta)$ by doubling every bit of $s$ ($0\mapsto00$ and
$1\mapsto11$), appending the separator $01$, and then appending $\beta$
verbatim. Its length is $2|s|+2+|\beta|$. Reading consecutive pairs from
the start identifies the first field and separator uniquely. A word without
this form is rejected. The second field is a little-endian binary numeral:
\[
 b(\beta)=\sum_{j=0}^{|\beta|-1}\beta_j2^j.
\]
The empty numeral represents zero, and redundant high zero bits are
allowed. Reversing the numeral or using a conventional nonempty encoding
of zero gives polynomial-time equivalent ordinary binary encodings.

\begin{definition}\label{def:language}
The language $\CC$ consists of the words $\pair(s,\beta)$ for which
$n=|s|>0$ and there is a word $t\in\{0,1\}^n$ satisfying
\begin{gather}
 \wt(t)\leq b(\beta),\label{eq:budget}\\
 \forall x\in\{0,\ldots,n-1\}\ \exists i\in\{0,\ldots,n-1\}:
 \quad t_i=s_{(x+n-i)\bmod n}=1.
 \label{eq:bitcoverage}
\end{gather}
Here $\wt(t)$ denotes the number of ones in $t$.
\end{definition}

The word $t$ is the indicator of a set $T\subseteq\Z_n$. Its weight is
$|T|$, and $(x+n-i)\bmod n$ represents $x-i$ in $\Z_n$. Therefore
\eqref{eq:bitcoverage} is exactly $S+T=\Z_n$. A list of shifts with
repetitions gives no stronger notion: deleting repetitions preserves its
union and can only decrease its size.

\begin{lemma}\label{lem:cap}
For every $n\geq1$, $S\subseteq\Z_n$, and $b\in\N$, a cover with at most
$b$ shifts exists if and only if one with at most $\min(b,n)$ shifts
exists. The empty pattern is rejected at every budget, budget zero is
rejected for every pattern, and every nonempty pattern is accepted when
$b\geq n$.
\end{lemma}
\begin{proof}
Every subset of $\Z_n$ has at most $n$ elements, which proves the first
claim. If $S=\varnothing$ or $T=\varnothing$, then $S+T=\varnothing$,
whereas $\Z_n\ne\varnothing$. If $s_0\in S$, every $x\in\Z_n$ belongs
to $S+(x-s_0)$. Thus taking all $n$ shifts covers $\Z_n$.
\end{proof}

\begin{proposition}\label{prop:np}
$\CC\in\NP$.
\end{proposition}
\begin{proof}
Use the $n$-bit word $t$ as the certificate. Parse the two fields, reject
malformed inputs and $n=0$, count $\wt(t)$, and test
\eqref{eq:bitcoverage} for all $n^2$ pairs $(x,i)$. These operations have
polynomial running time in the input length on a multitape Turing machine:
indices have $O(\log(n+1))$ bits, and even sequential scans to access the
specified bits incur only a polynomial overhead.

The binary budget causes no large-integer expansion. Read its bits from
most significant to least significant, starting with $q=0$, and update
\[
 q\longleftarrow\min(n,2q+c)
\]
when the next bit is $c$. Inductively $q$ is the decoded prefix capped at
$n$, since
$\min(n,2\min(n,u)+c)=\min(n,2u+c)$ for every $u\in\N$ and
$c\in\{0,1\}$. All intermediate states have $O(\log(n+1))$ bits.
The final comparison with $\wt(t)$ is correct by Lemma~\ref{lem:cap}.
The certificate length is at most the input length, and all verification
steps are polynomial in $n+|\beta|$.
\end{proof}

\section{Replicated markers realize difference constraints}
\label{sec:markers}

Fix integers $m\geq2$ and $D\geq0$. For each nonzero $d\in\Z_m$, let
$A_d\subseteq[-D,D]\cap\Z$ be a given finite set. We will construct a
single cyclic pattern whose covers of size at most $m$ are equivalent to
assignments of phases $x_r$ satisfying
\begin{equation}\label{eq:constraints}
 x_r-x_{r-d}\in\res{A_d}\quad
 (r\in\Z_m,\ d\in\Z_m\setminus\{0\}).
\end{equation}
Here and below a bar denotes reduction of an integer or integer set modulo
the chosen positive integer $L$.

\subsection{Construction and marker spacing}

Set
\begin{equation}\label{eq:markers}
 h=m(m-1),\qquad u_j=j+2hj^2\quad(0\leq j<h),\qquad
 M=2D+1,\qquad H_{\max}=Mu_{h-1}.
\end{equation}
The marker with index $j$ is the integer $Mu_j$. Partition the markers into
$m-1$ blocks of size $m$: using representatives $1\leq d<m$, put
\begin{equation}\label{eq:blocks}
 H_d=\{\res{Mu_j}:(d-1)m\leq j<dm\},\qquad
 H=\bigcup_{d=1}^{m-1}H_d.
\end{equation}
Choose
\begin{align}
 Q&=\max\{2H_{\max}+2D,\ m^2(2D+1),\ 3D\},\label{eq:Q}\\
 L&=m\bigl(\lfloor Q/m\rfloor+1\bigr)+1,
 \qquad N=mL.\label{eq:L}
\end{align}
Then
\begin{equation}\label{eq:Lbounds}
 L>2H_{\max}+2D,\qquad L>m^2(2D+1),\qquad L>3D,
 \qquad L\equiv1\pmod m.
\end{equation}
Indeed, writing $Q=ma+r$ with $0\leq r<m$ gives $L-Q=m+1-r>0$.
The markers are distinct in $\Z_L$: the $u_j$ increase strictly and all
$Mu_j$ lie in $[0,H_{\max}]\subset[0,L)$. Thus the blocks in
\eqref{eq:blocks} are disjoint and each has exactly $m$ elements.

Define the template $S^*$ in $G=\Z_m\times\Z_L$ by its slices:
\begin{equation}\label{eq:template}
 S_0=\Z_L\setminus H,\qquad
 S_d=H_d+\res{A_d}\quad(d\ne0),\qquad
 S^*=\{(d,y):y\in S_d\}.
\end{equation}
The slice $S_0$ is dense and the other slices are sparse. In particular,
\begin{equation}\label{eq:sparsebound}
 |S_d|\leq m|A_d|\leq m(2D+1)\qquad(d\ne0).
\end{equation}
The template is nonempty, since $|H|=h<m^2<L$.

\begin{lemma}[Unique marker differences]\label{lem:ruler}
The nonzero ordered differences $u_j-u_i$, for $0\leq i,j<h$ and
$i\ne j$, determine $(i,j)$ uniquely.
\end{lemma}
\begin{proof}
First suppose $i<j$, $k<\ell$, and $u_j-u_i=u_\ell-u_k$. Reducing
modulo $2h$ gives $j-i\equiv\ell-k\pmod{2h}$. Both differences are
between $1$ and $h-1$, so they are equal to a common positive integer $t$.
The original equality now reads
\[
 t+2ht(i+j)=t+2ht(k+\ell).
\]
Canceling $2ht\ne0$ gives $i+j=k+\ell$. Equal sums and differences give
$i=k$ and $j=\ell$. Since $u_j$ is strictly increasing, the sign of a
nonzero difference identifies its orientation. Reversing both pairs
therefore proves the negative-difference case as well.
\end{proof}

\begin{lemma}[Overlap for every phase]\label{lem:overlap}
Let $d,e\in\Z_m\setminus\{0\}$ and $\delta\in\Z_L$. Then
\[
 \bigl|\{z\in H_e:z+\delta\in H_d+\res{A_d}\}\bigr|
 =m\quad\text{if }e=d\text{ and }\delta\in\res{A_d},
\]
and this cardinality is at most one in every other case.
\end{lemma}
\begin{proof}
A covered marker has an index $i$ in block $e$, and there are an index
$j$ in block $d$ and $a\in A_d$ such that
\begin{equation}\label{eq:representation}
 \delta=\res{M(u_j-u_i)+a}.
\end{equation}
Every integer on the right before reduction lies in
$[-H_{\max}-D,H_{\max}+D]$. This interval has diameter strictly less
than $L$ by \eqref{eq:Lbounds}. Therefore two representations of
$\delta$, with indices $(i,j)$ and $(k,\ell)$ and offsets $a,a'$, are
equal as integers. Subtracting them gives
\[
 M\bigl((u_j-u_i)-(u_\ell-u_k)\bigr)=a'-a.
\]
The right side has absolute value at most $2D<M$. Since the left side is
a multiple of $M$, both sides vanish. Hence $a=a'$ and
$u_j-u_i=u_\ell-u_k$.

If the common marker difference is nonzero,
Lemma~\ref{lem:ruler} identifies the ordered index pairs; in particular
$i=k$, so the two covered markers are the same. If it is zero, strict
increase gives $i=j$ and $k=\ell$. A marker belongs to only one block,
so $e=d$, and \eqref{eq:representation} gives
$\delta=\res a\in\res{A_d}$. Outside this exceptional case, any two
covered markers must therefore coincide. In the exceptional case,
$z+\delta\in H_d+\res{A_d}$ for every $z\in H_d$, giving exactly $m$
covered markers. This reasoning makes no restriction on the representative
or size of the phase $\delta$.
\end{proof}

\subsection{Forcing the translates and the constraints}

\begin{lemma}[One translate in each layer]\label{lem:layers}
If $T\subseteq G$ satisfies $|T|\leq m$ and $S^*+T=G$, then for every
$r\in\Z_m$ there is exactly one $x_r\in\Z_L$ with $(r,x_r)\in T$.
\end{lemma}
\begin{proof}
Suppose no selected shift has first coordinate $r$. A shift $(q,x)\in T$
then has $q\ne r$ and covers, in target row $r$, precisely the positions
$x+S_{r-q}$. By \eqref{eq:sparsebound}, this set has at most $m(2D+1)$
elements. The union of at most $m$ such sets has size at most
$m^2(2D+1)<L$, and cannot cover the row. Every one of the $m$ layers
must consequently contain a selected shift. The total budget $m$ implies
there is exactly one in each layer.
\end{proof}

\begin{theorem}[Replicated-marker equivalence]\label{thm:gadget}
The template $S^*$ has a cover in $G$ of size at most $m$ if and only if
there exist $x_r\in\Z_L$, for $r\in\Z_m$, satisfying
\eqref{eq:constraints}.
\end{theorem}
\begin{proof}
Suppose first that the phases satisfy \eqref{eq:constraints}. Select
$T=\{(r,x_r):r\in\Z_m\}$. In row $r$, the shift $(r,x_r)$ covers
$\Z_L\setminus(H+x_r)$. For $d\ne0$, the constraint gives
$x_r-x_{r-d}\in\res{A_d}$ and hence
\[
 H_d+x_r\subseteq H_d+\res{A_d}+x_{r-d}=S_d+x_{r-d}.
\]
The shift $(r-d,x_{r-d})$ therefore covers the entire block $H_d+x_r$.
These blocks partition the holes of the dense slice, so every position in
every row is covered.

Conversely, a cover of size at most $m$ has the form above by
Lemma~\ref{lem:layers}. If a constraint fails for some $(r,e)$, consider
the $m$ points of $H_e+x_r$ in row $r$. The own-row shift $(r,x_r)$
misses all of them. The shift $(r-d,x_{r-d})$, for $d\ne0$, covers one
of these points $z+x_r$ precisely when
\[
 z+(x_r-x_{r-d})\in H_d+\res{A_d}.
\]
If $d\ne e$, Lemma~\ref{lem:overlap} bounds its contribution by one.
If $d=e$, the same bound holds because the constraint was assumed to
fail. The $m-1$ other shifts thus cover at most $m-1$ of the $m$ points,
a contradiction. Every constraint holds.
\end{proof}

\subsection{Returning to a single cyclic group}

Since $L\equiv1\pmod m$, the integers $m$ and $L$ are coprime. The map
\[
 \phi:\Z_{mL}\longrightarrow\Z_m\times\Z_L,
 \qquad \phi(z)=(z\bmod m,z\bmod L)
\]
is an additive bijection. For completeness, if $0\leq r<m$ and
$0\leq y<L$, its inverse is represented by
\begin{equation}\label{eq:CRT}
 \psi(r,y)=y+L\bigl((r-y)\bmod m\bigr).
\end{equation}
The last remainder lies in $\{0,\ldots,m-1\}$, so
$0\leq\psi(r,y)<mL$. The expression has residue $y$ modulo $L$ and,
using $L\equiv1\pmod m$, residue $r$ modulo $m$. Uniqueness follows
because an integer divisible by both coprime factors is divisible by their
product. Define
\begin{equation}\label{eq:cyclictemplate}
 P=\phi^{-1}(S^*)\subseteq\Z_N,\qquad N=mL.
\end{equation}
An additive bijection preserves translates, unions, and cardinalities.
Thus Theorem~\ref{thm:gadget} holds with $P$ in $\Z_N$ in place of
$S^*$ in $G$. Only the two polynomial-size factors $m$ and $L$ will be
used; there is no product of an unbounded family of moduli.

\section{The credited circulant clique embedding}
\label{sec:labels}

Let $X$ be a finite simple undirected graph with vertices
$\{1,\ldots,v\}$, where $v\geq2$. Put
\begin{equation}\label{eq:labels}
 B=3v^3+1,\qquad g_i=i+Bi^2+B^2i^3,\qquad D=g_v,
\end{equation}
and let
\begin{equation}\label{eq:A}
 A=\{g_i-g_j:\{i,j\}\in E(X)\},
\end{equation}
including both orientations of every edge. All elements of $A$ lie in
$[-D,D]$, and $A$ is symmetric and does not contain zero. Let $L>3D$,
and write the labels also for their residues when the group is clear.

\begin{lemma}[Distinct three-term sums]\label{lem:b3}
If $a,b,c,d,e,f\in\{1,\ldots,v\}$ and
\[
 g_a+g_b+g_c=g_d+g_e+g_f\quad\text{in }\Z_L,
\]
then the multisets $\{a,b,c\}$ and $\{d,e,f\}$ are equal. Repeated
indices are allowed.
\end{lemma}
\begin{proof}
All integer sums in question lie in $[0,3D]$, whose diameter is less than
$L$. Their congruence is therefore an equality of integers. For each
$r\in\{1,2,3\}$, a sum of three $r$th powers of indices is at most
$3v^r\leq3v^3<B$. There are no carries between the three base-$B$
coordinates in \eqref{eq:labels}. Uniqueness of the base-$B$ expansion
implies that the two triples have the same first three power sums
$p_1,p_2,p_3$. If $e_1,e_2,e_3$ denote their elementary symmetric
polynomials, the identities
\[
 e_1=p_1,\qquad 2e_2=p_1^2-p_2,\qquad
 6e_3=p_1^3-3p_1p_2+2p_3
\]
show that these also agree. The two monic cubics
$z^3-e_1z^2+e_2z-e_3$ are consequently identical. Their roots, counted
with multiplicity, are the respective index triples, proving the assertion.
\end{proof}

Appending the same label to two equal two-term sums and canceling it from
the resulting equal multisets shows that two-term sums are also distinct
up to order. In particular,
\begin{equation}\label{eq:diffunique}
 g_a-g_b=g_c-g_d\text{ in }\Z_L,\quad a\ne b
 \quad\Longrightarrow\quad a=c\text{ and }b=d.
\end{equation}
Indeed, equality gives $\{a,d\}=\{c,b\}$; the matching $a=b$, $d=c$
is excluded. The labels themselves are distinct modulo $L$, since they
increase strictly in $[1,D]\subset[0,L)$. Thus
$0\notin\res A$.

Let $Y$ be the undirected Cayley graph on $\Z_L$ with connection set
$\res A$: distinct $x,y$ are adjacent when $x-y\in\res A$.

\begin{lemma}[Codenotti--Gerace--Vigna; Godsil--Rooney]
\label{lem:clique}
The graphs $X$ and $Y$ have the same clique number. More precisely, every
clique of $Y$ has a clique of the same size in $X$, and conversely.
\end{lemma}
\begin{proof}
The map $i\mapsto g_i$ is injective and sends every edge of $X$ to an
edge of $Y$. In fact \eqref{eq:diffunique} shows that it is an induced
embedding. This proves one direction.

For the other direction, let $C$ be a nonempty clique of $Y$. Translate
it so that $0\in C$. Each $x\in C\setminus\{0\}$ has a unique
representation $x=g_a-g_b$ with $(a,b)$ an oriented edge of $X$, by
\eqref{eq:diffunique}. Consider two distinct such points
$x=g_a-g_b$ and $y=g_c-g_d$. Since they are adjacent, write
$y-x=g_e-g_f$ for another oriented edge. Rearrangement gives
\[
 g_a+g_e+g_d=g_c+g_b+g_f.
\]
Lemma~\ref{lem:b3} implies equality of the multisets
$\{a,d,e\}=\{b,c,f\}$. Also $a\ne b$, $c\ne d$, and $e\ne f$.
To spell out the matching argument, $a$ must match either $c$ or $f$.
If it matches $c$, the matching $d=b,e=f$ is forbidden, leaving
$d=f,e=b$. If it matches $f$, the matching $d=c,e=b$ is forbidden,
leaving $d=b,e=c$. Hence
\begin{equation}\label{eq:commonpair}
 a=c\qquad\text{or}\qquad b=d.
\end{equation}
This argument applies even when some indices on the same side repeat:
multiset equality always admits a matching of the three occurrences.

A family of distinct ordered pairs satisfying \eqref{eq:commonpair}
pairwise must have a coordinate common to the whole family. If some two
pairs have the same first coordinate and different second coordinates,
any third pair with a different first coordinate would have to agree with
both distinct second coordinates, which is impossible. Otherwise, either
all first coordinates agree already or a pair with distinct first
coordinates forces all second coordinates to agree by the symmetric
argument. For a family of one pair the assertion is immediate.

Suppose the common first coordinate is $a$. Then the pairs have the form
$(a,b_x)$ with distinct $b_x$, each adjacent to $a$ in $X$. For two of
them, adjacency of the corresponding points implies
$g_{b_y}-g_{b_x}\in\res A$. By \eqref{eq:diffunique},
$\{b_x,b_y\}$ is an edge of $X$. Thus
$\{a\}\cup\{b_x:x\in C\setminus\{0\}\}$ is a clique of size
$|C|$. If the second coordinate is common, the same reasoning applies
to the distinct first coordinates. A singleton $C$ is realized by any
vertex of $X$, and the empty clique is realized by the empty set.
\end{proof}

The preceding lemma is the known three-sum-distinct embedding
from~\cite{cgv,gr}. Its proof is included to make the extraction of a
source clique from arbitrary target phases explicit.

\section{The reduction and its running time}
\label{sec:reduction}

\subsection{From a graph to a cyclic pattern}

For a graph $X$ on $v$ vertices and an integer $k$ with $2\leq k\leq v$,
take the labels and $D$ from \eqref{eq:labels}, set $m=k$, and use
$A_d=A$ for every nonzero $d\in\Z_k$ in the construction of
Section~\ref{sec:markers}. Let $P_X\subseteq\Z_N$ be the pattern
in \eqref{eq:cyclictemplate}. Its budget is $k$.

\begin{theorem}\label{thm:graphreduction}
For every finite simple undirected graph $X$ and $2\leq k\leq v$,
\[
 X\text{ has a clique of size }k
 \quad\Longleftrightarrow\quad \tau(P_X,\Z_N)\leq k.
\]
The constructed pattern is nonempty.
\end{theorem}
\begin{proof}
If $i_0,\ldots,i_{k-1}$ are the vertices of a clique, assign
$x_r=g_{i_r}\in\Z_L$ to the $k$ rows. The difference between any two
distinct assigned phases lies in $\res A$, so all constraints
\eqref{eq:constraints} hold. Theorem~\ref{thm:gadget} and the additive
bijection $\phi$ give a cover with $k$ shifts.

Conversely, a cover within the budget yields phases satisfying
\eqref{eq:constraints}. Every pair of distinct rows is of the form
$(r,r-d)$ for a nonzero $d$. Thus all pairwise phase differences lie in
$\res A$. They are nonzero, so the phases are distinct and form a
$k$-clique in $Y$. Lemma~\ref{lem:clique} produces a $k$-clique in
$X$. Nonemptiness was proved just after \eqref{eq:sparsebound}.
\end{proof}

To define the reduction on all graph instances, let the fixed YES instance
be the length-one pattern $S=\{0\}$ with budget $1$, and the fixed NO
instance the same pattern with budget $0$. For $k=0$ output YES. For
$k=1$ output YES if $v\geq1$ and NO otherwise. For $k>v$ output NO.
Use Theorem~\ref{thm:graphreduction} in all remaining cases. These
branches cover the empty graph and every natural $k$. An edgeless graph
with $2\leq k\leq v$ has $A=\varnothing$ and is handled by the same
construction: its difference constraints are impossible. Malformed graph
encodings can be sent to the fixed NO instance after an explicit
validity check. All outputs in this graph reduction have a positive-length,
nonempty pattern and a budget no larger than their length.

\subsection{Polynomial output and an explicit emitter}

\begin{lemma}\label{lem:size}
In the nontrivial branch $2\leq k\leq v$, the output length satisfies
$N\leq422v^{16}$.
\end{lemma}
\begin{proof}
Since $v\geq1$,
\[
 B\leq4v^3,\qquad
 D=v+Bv^2+B^2v^3\leq v+4v^5+16v^9\leq21v^9.
\]
Also $h=k(k-1)\leq v^2$ and $u_{h-1}<3h^3$. Since $D\geq1$,
$M=2D+1\leq3D$ and
\[
 H_{\max}\leq9Dh^3\leq189v^{15}.
\]
The three terms in \eqref{eq:Q} are bounded respectively by
$420v^{15}$, $63v^{11}$, and $63v^9$. Consequently
\[
 Q\leq420v^{15},\qquad
 L\leq Q+k+1\leq422v^{15},\qquad
 N=kL\leq422v^{16}.
\]
\end{proof}

This length bound is accompanied by an actual algorithm for writing the
full indicator. Use an explicit graph representation, for example a
$v\times v$ adjacency matrix with its vertex count, so that $v$ is
polynomially bounded by the source length. First check symmetry and the
zero diagonal and handle the branches above. In the nontrivial branch,
compute $B,D,h,M,Q,L,N$. For each integer $z=0,\ldots,N-1$, compute
$r=z\bmod k$ and $y=z\bmod L$ and write the following bit:
\begin{equation}\label{eq:emitter}
 \begin{cases}
 1\ \Longleftrightarrow\ y\not\equiv Mu_j\pmod L
       \text{ for all }0\leq j<h, &r=0,\\[2pt]
 1\ \Longleftrightarrow\ y\equiv Mu_j+g_a-g_b\pmod L
       \text{ for some }(r-1)k\leq j<rk\text{ and }\{a,b\}\in E(X),
       &r\ne0.
 \end{cases}
\end{equation}
Equation~\eqref{eq:template} proves that this is exactly the indicator of
$P_X$ under $\phi$. Finally pair the entire indicator word with the
binary encoding of $k$. The pattern field has exactly $N$ bits; the
encoded output has length $2N+2+O(\log(k+1))$.

For clarity, the emitter is polynomial-time without unit-cost arithmetic
or random access. There are $N$ output iterations. A dense-row test
examines at most $h$ markers, and a sparse-row test examines at most
$k v^2$ marker/ordered-vertex pairs. These are polynomially many tests by
Lemma~\ref{lem:size}. Every numerical quantity involved, including a
signed edge difference, has $O(\log(v+2))$ bits. Schoolbook addition,
multiplication, comparison, and division with remainder have polynomial
bit cost on these operands. One may implement every adjacency lookup by
scanning the explicit $v^2$-bit matrix, and compute labels and marker
values directly from their indices. Binary loop counters and sequential
output therefore give a deterministic multitape algorithm with a
polynomial running time. If $k$ is supplied in binary, comparison with
$v$ and the exceptional branches take polynomial time in the length of
that field; only $k\leq v$ reaches the large emitter. This proves a
runtime bound separately from the numerical output bound. No particular
optimal exponent for the Turing-machine running time is asserted.

\subsection{A complete source reduction}

We recall the standard occurrence-graph reduction to specify every source
witness. A $3$CNF formula has clauses $C_1,\ldots,C_q$, each with
exactly three literal occurrences; repeated literals are permitted. Make
one vertex $(i,j)$ for each of the three occurrences $j$ in clause $i$.
Join two vertices exactly when they belong to different clauses and their
literals are not complementary. The graph $X_F$ has $v=3q$ vertices.

\begin{lemma}\label{lem:satclique}
The formula $F$ is satisfiable if and only if $X_F$ has a clique of size
$q$.
\end{lemma}
\begin{proof}
A satisfying assignment permits the choice of one true occurrence in
each clause. Two such occurrences are never complementary, so the chosen
$q$ vertices form a clique. Conversely, a clique contains at most one
vertex from each clause, because there are no within-clause edges. A
$q$-clique consequently contains exactly one from each of the $q$ clauses.
Its selected literals are pairwise compatible. Set each variable that
appears among them to the truth value making its selected sign true;
pairwise compatibility guarantees that this is well defined. Give all
other variables any value. Every clause contains its selected true literal,
so the assignment satisfies $F$. When $q=0$, the empty conjunction is
true and the empty graph has the required zero-clique.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:main}]
The NP-completeness of $3$SAT is the standard source theorem, also proved
in the formal foundation used here~\cite{complexitylib}. Given a valid
$3$CNF formula, construct $X_F$ and use the total graph reduction with
budget $k=q$. Lemma~\ref{lem:satclique} and
Theorem~\ref{thm:graphreduction}, together with its exceptional branches,
give the required equivalence for every formula. In particular, an empty
formula produces the fixed YES instance and a one-clause formula does
also. Constructing the graph requires only polynomially many literal
comparisons; its adjacency matrix has $(3q)^2$ bits. The full cyclic
indicator is emitted in polynomial time as proved above, with
$N\leq422(3q)^{16}$ in the nontrivial branch. Source words that fail the
chosen $3$CNF syntax are detected in polynomial time and mapped to NO.
Thus this is a total polynomial-time many-one reduction. It outputs only
nonempty patterns and budgets at most their lengths, proving the stronger
NP-hardness statement. Proposition~\ref{prop:np} supplies NP membership
both for the unrestricted language and for that restriction.
\end{proof}

\section{Lean formalization and reproduction}
\label{sec:formal}

The associated Lean development checks the complete decision theorem,
including its computational interpretation. Its final theorem is
\begin{center}
\path{CyclicCover.BinaryCover.NPComplete_language}.
\end{center}
The language is defined on finite Boolean lists with the pairing and
binary-budget conventions in Section~\ref{sec:language}. The exact
semantic correspondence is
\begin{center}
\path{CyclicCover.BinaryCover.mem_encode_indicator_iff}.
\end{center}
It states, for every natural $n$ with \texttt{NeZero n}, every finite set
$S\subseteq\mathrm{ZMod}\,n$, and every natural $b$, that encoding the
$n$-bit indicator of $S$ and the ordinary binary numeral of $b$ belongs
to the language if and only if
\[
 \exists T\subseteq\mathrm{ZMod}\,n,\qquad
 |T|\leq b\ \land
 (\forall x,\ \exists t\in T,\ x-t\in S).
\]
There is no nonempty-pattern or $b\leq n$ hypothesis.
The theorem \path{CyclicCover.BinaryCover.mem_pair_iff} extends this
interpretation to arbitrary binary budget words, including redundant high
zero bits. Zero-length patterns and malformed pairs are rejected.

\subsection{Correspondence with the mathematical proof}

The arithmetic and set-theoretic core is organized as follows.
\path{CyclicCover.marker_representation_unique} supplies the
short-interval and scaled-difference argument of
Lemma~\ref{lem:overlap}.
\path{CyclicCover.Concrete.overlap_bound} instantiates it with the
explicit marker blocks. The layer argument and counting contradiction
are assembled in
\path{CyclicCover.Concrete.concrete_cover_iff}; the transport to
$\Z_{mL}$ is
\path{CyclicCover.Concrete.cyclic_cover_iff}.
The repeated-summand label property and the clique extraction are checked
in the label and graph modules, culminating in
\path{CyclicCover.GraphEncoding.clique_iff_assignment}.
The total graph reduction is verified by
\path{CyclicCover.GraphEncoding.reduceGraph_correct}, and its full
indicator length by
\path{CyclicCover.GraphEncoding.reduceGraph_indicator_length}.

The word-level reduction is checked separately. In particular,
\path{CyclicCover.GraphEncoding.GraphString.emit_mem_FP} proves that the graph-word
emitter computes its entire output in polynomial time, and
\path{CyclicCover.GraphEncoding.GraphString.emit_correct} proves its semantic
equivalence on every input word. The source parser preserves individual
literal occurrences and checks the exact $3$CNF syntax. The theorem
\path{CyclicCover.SourceReduction.threeSAT_reduction} composes its
explicit adjacency emitter with the graph-to-cover program. The
\texttt{GeneralCover} and \texttt{BinaryCover} modules then remove
intermediate nonemptiness, capped-budget, and unary-budget restrictions.
In particular,
\path{CyclicCover.BinaryCover.budget_fp} certifies capped parsing of an
arbitrary binary budget, and
\path{CyclicCover.BinaryCover.fromUnary_fp} together with
\path{CyclicCover.BinaryCover.fromUnary_correct} supplies the total
binary-output reduction. The final semantics therefore cover every input
pattern and every natural budget, not just outputs of the hardness gadget.

The complexity definitions come from the pinned
\texttt{complexitylib} library~\cite{complexitylib}. Its $\FP$
functions are computed by finite-control deterministic multitape Turing
machines with polynomial running-time bounds and exact output-tape
semantics. Its NP class is nondeterministic polynomial time, requiring
all computation paths to halt within the time bound. Polynomial
many-one reductions quantify over all input words. The source
NP-hardness is derived from the library's proved Cook--Levin and $3$SAT
theorems; it is not an additional axiom. NP membership uses the library's
verifier-to-machine theorem with the linear-size translate indicator.
The bound $422v^{16}$ is an output-size bound; the formal machine-time
certificates are separate theorems.

\subsection{Versions, trust, and commands}

The checked environment uses Lean \texttt{v4.35.0-rc3}. The principal
dependency commits are:
\begin{center}
\begin{tabular}{ll}
\toprule
Dependency & Pinned commit\\
\midrule
\texttt{complexitylib} & \texttt{add0aca8ee0d71e68969f2cb45cf91554a50f787}\\
\texttt{mathlib} & \texttt{728a93eeff833da3173895bb0575752fdc24edb0}\\
\texttt{cslib} & \texttt{311d27ad8458b61e9b7461fc83a480e4be97aef2}\\
\bottomrule
\end{tabular}
\end{center}
The successful reproduction snapshot is identified by
\texttt{20261014T124120Z}. It preserves the sources, dependency manifests,
compiler and source fingerprints, compile commands, exit statuses, and
axiom-audit logs. From that snapshot directory, the command
\begin{verbatim}
python3 reproduce_fresh.py
\end{verbatim}
creates a new output directory and rebuilds the saved source sequence;
an optional argument supplies a fresh destination directory. The
\texttt{REPRODUCE.txt} file records the setup requirements. The expected
base status is \texttt{all\_compiled\_audited}, followed by
\texttt{compiled\_and\_audited=true} in the binary-extension status.
The saved run compiled 307 modules, including all 24 authored modules and
283 selected foundation modules, and recorded 110 axiom queries. The
final source and statement audit is saved as
\texttt{PARENT\_FINAL\_AUDIT.json}; the manuscript-to-theorem mapping
and source hashes are in \texttt{PAPER\_AUDIT.json}.

The transitive axiom reports for the main theorem and semantic endpoint
contain only \texttt{propext}, \texttt{Classical.choice}, and
\texttt{Quot.sound}. No unfinished proof, new mathematical axiom, native
evaluation certificate, or externally asserted hardness result is used.
All authored, \texttt{complexitylib}, and selected \texttt{cslib} modules
in the build closure were recompiled from copied source. The pinned
official Lean and mathlib package caches were reused and fingerprinted;
their complete sources were not rebuilt. The reproduction script checks
the recorded compiler and cache locations, so a new machine must restore
the pinned environment and adjust those locations as documented. The
saved successful run does not assert portability to arbitrary library
versions.

\section{Consequences and scope}
\label{sec:scope}

Theorem~\ref{thm:main} answers the decision version of Set-Cover by
Rotations. Computing the exact covering number, or producing a minimum
cover, is consequently NP-hard, since either task decides the budget
question. For a nonempty pattern the optimum lies between $1$ and $n$;
a decision oracle therefore determines its value by binary search. The
proof does not provide a self-reduction that recovers an optimal set of
shifts while keeping all oracle queries within the single-pattern cyclic
problem, the distinction already raised by Wirth~\cite{wirth}.

The reduction is intended to establish exact complexity. Its polynomial
order bound is deliberately generous, and no approximation-hardness
factor follows from the argument. Succinctly encoded patterns, restricted
families of patterns, and improved quantitative bounds on the reduction
remain separate questions.

\begin{thebibliography}{9}

\bibitem{wads}
\emph{Open Problems from WADS 2023}.
Problem 4: Set-Cover by Rotations, contributed by Anthony Wirth, 2023.
\url{https://wadscccg2023.encs.concordia.ca/assets/pdf/wads_open_problems.pdf}.

\bibitem{wirth}
Anthony Ian Wirth.
\emph{Approximation Algorithms for Clustering}.
Ph.D. dissertation, Princeton University, January 2005.
Section 2.7, ``Pattern rotation,'' pp.~34--37.
\url{https://www.cs.princeton.edu/techreports/2004/716.pdf}.

\bibitem{bjr}
B\'ela Bollob\'as, Svante Janson, and Oliver Riordan.
\emph{On covering by translates of a set}.
arXiv:0910.3815v2, 2010.
\url{https://arxiv.org/abs/0910.3815v2}.

\bibitem{cgv}
Bruno Codenotti, Ivan Gerace, and Sebastiano Vigna.
Hardness results and spectral techniques for combinatorial problems on
circulant graphs.
\emph{Linear Algebra and its Applications}, 285(1--3):123--142, 1998.

\bibitem{gr}
Chris Godsil and Brendan Rooney.
\emph{Hardness of Computing Clique Number and Chromatic Number For
Cayley Graphs}.
arXiv:1502.00965v5, 2016. Section 6, especially Lemma 6.1.
\url{https://arxiv.org/abs/1502.00965v5}.

\bibitem{complexitylib}
The complexitylib contributors.
\emph{Complexitylib: a Lean 4 formalization of computational complexity
theory}.
Source revision \texttt{add0aca8ee0d71e68969f2cb45cf91554a50f787}.
\url{https://github.com/SamuelSchlesinger/complexitylib/tree/add0aca8ee0d71e68969f2cb45cf91554a50f787}.

\end{thebibliography}
\end{document}