\section{A certified rigidity theorem for the thirteen-cycle}
\label{sec:cycle-certificate}

This section gives a finite, exact certificate for the only additional
geometric obstruction needed in our proof of the main theorem.
The computation uses integer arithmetic throughout; numerical root finding
is not a proof input.  In particular, the assertions below concern all real
configurations satisfying the hypotheses, not a bounded coordinate search.

\begin{lemma}\label{lem:cycle}
Let $Y\subset\mathbb R^2$ have thirteen points.  If its diameter graph is
$C_{13}$ and $Y$ determines at most seven distances, then $Y$ is similar to
the vertex set of a regular thirteen-gon.
\end{lemma}

We first give the geometric reduction, then specify and verify the finite
algebraic assertion on which the lemma depends.

\subsection{The order of the diameter edges and the two side lengths}

The endpoints of diameters are in strictly convex position.  Write them
as $p_0,\ldots,p_{12}$ in counterclockwise order, with subscripts modulo
thirteen, and normalize the diameter to one.  Every two vertex-disjoint
diameter segments cross.  Fix one diameter edge and delete its endpoints
from the diameter cycle.  The remaining eleven vertices form a path, all
of whose edges cross the fixed diameter.  Its vertices consequently
alternate between the two open half-planes bounded by that diameter's
line.  The two boundary arcs between its endpoints therefore contain five
and six vertices.  Thus every diameter edge joins indices differing by
six or seven.  Each vertex has two diameter neighbors, so both such
edges occur.  The diameter cycle is exactly the step-six star.

For a boundary side $p_jp_{j+1}$, the perpendicular bisector passes through
$p_{j+7}$: this vertex is at distance one from both endpoints.  The line
through the side midpoint and $p_{j+7}$ meets the convex polygon exactly
in the segment between these two points.  Hence the two boundary arcs
between them lie strictly in the two respective open half-planes.
Applying the resulting comparison of distances to successive sides gives
\begin{equation}\label{eq:cycle-chains}
 |p_i-p_{i+1}|<|p_i-p_{i+2}|<\cdots<|p_i-p_{i+6}|=1
 \qquad (i\in\mathbb Z/13\mathbb Z).
\end{equation}
In particular, there are at least six distances.  If there are only six,
every boundary side has the shortest length.  If there are seven, every
boundary side is one of the two shortest lengths.

Traverse the diameter star in steps of six.  At each star vertex the two
neighbors are consecutive in the convex order, so the angle between the
two incident diameter segments is the apex angle of an isosceles triangle
with two sides of length one and a boundary side as its base.  If just
one boundary-side length occurs, these angles are all equal.  The star
then has equal edge lengths and equal turns and is regular, proving the
lemma in this case.

Suppose the boundary sides have two distinct lengths $a<b$.
Their apex angles are
\begin{equation}\label{eq:two-apex-angles}
 \alpha=2\arcsin(a/2),\qquad \beta=2\arcsin(b/2),
 \qquad 0<\alpha<\beta.
\end{equation}
Let $\nu$ of the thirteen successive star angles equal $\beta$, and the
other $u=13-\nu$ equal $\alpha$.  The signed exterior turn at a star vertex
is $\pi-\alpha$ or $\pi-\beta$.  The step-six star on convexly ordered
vertices has rotation index six.  Therefore
\begin{equation}\label{eq:angle-sum}
 u\alpha+\nu\beta=\pi,
 \qquad 1\le\nu\le12,
 \qquad 0<\alpha<\frac{\pi}{13}.
\end{equation}

For completeness, the rotation-index assertion does not depend on any
metric regularity.  During a deformation through strictly convex labeled
polygons, each successive star triple remains counterclockwise and
noncollinear.  Its exterior turn consequently varies continuously in
$(0,\pi)$, and the rotation index remains an integer-valued constant.
The space of strictly convex labeled polygons is connected.  One explicit
way to deform a polygon containing the origin to a cyclic polygon is to
interpolate its Minkowski functional with the Euclidean norm and move
each vertex along its ray to the corresponding unit level set; for
positive interpolation parameter these level sets are strictly convex.
The points on the resulting circle can then be moved to equally spaced
positions while preserving their order.  For the regular step-six star
the sum of exterior turns is $12\pi$, as asserted.

\subsection{The closure polynomial}

Encode the successive star angles by a binary word
$b=(b_0,\ldots,b_{12})$, taking $b_k=1$ at an angle $\beta$ and $b_k=0$
at an angle $\alpha$.  Set
\begin{equation}\label{eq:closure-parameters}
 B_k=\sum_{j<k}b_j,\qquad
 \theta=\frac{\alpha}{\nu},\qquad
 \omega=e^{-\pi i/\nu},\qquad z=e^{-i\theta}.
\end{equation}
Equation~\eqref{eq:angle-sum} gives
$\beta=\pi/\nu-u\theta$.  After rotating the first unit edge to the
positive real axis, the successive edge vectors are
\begin{equation}\label{eq:edge-vectors}
 e_k=(-1)^k\omega^{B_k}z^{\nu k-13B_k}
 \qquad(0\le k\le12).
\end{equation}
Indeed, the direction of the $k$th edge is
$k\pi-\sum_{j<k}((1-b_j)\alpha+b_j\beta)$.
The required closure condition is therefore
\begin{equation}\label{eq:laurent-closure}
 P_b(z):=\sum_{k=0}^{12}(-1)^k\omega^{B_k}
              z^{\nu k-13B_k}=0,
 \qquad 0<\theta<\frac{\pi}{13\nu}.
\end{equation}
Multiplication by a power of $z$ changes $P_b$ into an ordinary polynomial
$\widetilde P_b\in\mathbb Z[\omega][z]$ without changing its zeros on the
unit circle.  The exponents are positions in an integer walk whose
successive increments are $\nu$ or $-u$.  Its total positive increment is
$u\nu$, so
\begin{equation}\label{eq:degree-bound}
 \deg\widetilde P_b\le u\nu\le42.
\end{equation}

There are $2^{13}-2=8190$ nonconstant binary words.  Alternatively, cyclic
shifts and reversals give 378 classes.  The verifier supports both the
reduced enumeration and an enumeration of all 8190 words.  The latter
avoids any reliance on the symmetry reduction.

\subsection{Exact removal of regular and degenerate solutions}

Let $r$ be the inverse of thirteen modulo $2\nu$ and set
$\eta=\omega^r$.  The inverse exists because $1\le\nu\le12$.
Define the monic degree-twelve polynomial
\begin{equation}\label{eq:regular-factor}
 F_\nu(z)=\frac{z^{13}-\omega}{z-\eta}
       =\sum_{j=0}^{12}\eta^{12-j}z^j.
\end{equation}
Every $\widetilde P_b$ is divisible by $F_\nu$ in $\mathbb Z[\omega][z]$.
To see this, at a root of $z^{13}=\omega$ equation~\eqref{eq:laurent-closure}
reduces to
\[
 \sum_{k=0}^{12}(-z^\nu)^k.
\]
Here $(-z^\nu)^{13}=-\omega^\nu=1$.  The geometric sum vanishes unless
$z^\nu=-1$.  Among the thirteen roots of $z^{13}=\omega$, the latter
condition holds precisely at $\eta$, since $\gcd(13,\nu)=1$.
The divisor is monic, and its division into $\widetilde P_b$ is also
checked directly by the verifier with a zero remainder.

On the closed arc
\begin{equation}\label{eq:closed-arc}
 z=e^{-i\theta},\qquad 0\le\theta\le\frac{\pi}{13\nu},
\end{equation}
the polynomial $F_\nu$ can vanish only at the upper endpoint.  This is
the regular solution $\alpha=\beta=\pi/13$.  Its removed roots therefore
include no nonregular admissible solution.  Write
\begin{equation}\label{eq:remaining-quotient}
 \widetilde P_b(z)=F_\nu(z)(z-1)^{h_b}Q_b(z),
 \qquad Q_b(1)\ne0,
\end{equation}
where the maximal integer $h_b\ge0$ is found by exact evaluation and
synthetic division.  The removed factor $z-1$ corresponds only to the
excluded endpoint $\theta=0$.  All coefficient operations in this step
take place in
\[
 \mathbb Z[\omega]\cong\mathbb Z[T]/(\Phi_{2\nu}(T)),
\]
where $\Phi_{2\nu}$ is constructed by exact monic divisions of $T^j-1$.
No algebraic-number approximation is used for factor removal.

\begin{proposition}\label{prop:cycle-finite-certificate}
For each of the 8190 nonconstant binary words $b$ of length thirteen,
the quotient $Q_b$ in~\eqref{eq:remaining-quotient} is nonzero throughout
the closed arc~\eqref{eq:closed-arc}.
\end{proposition}

The following gives the complete certification procedure for this finite
assertion, rather than treating a numerical root computation as evidence
of nonexistence.

\subsection{The integer interval certificate}

Fix the common scale $S=10^{50}$.  An integer pair $(L,U)$ represents the
real interval $[L/S,U/S]$.  Addition, negation and integer scaling are
exact.  For multiplication, form the four integer products of endpoints
and round the least product down and the greatest product up after
dividing by $S$.  Division by a positive integer is rounded in the same
way.  Thus every arithmetic operation encloses all possible real inputs
from its operand intervals.  A complex interval is a pair of such real
intervals, and complex multiplication uses
$(a+ib)(c+id)=(ac-bd)+i(ad+bc)$.

A rational enclosure for $\pi$ is obtained from Machin's identity
\begin{equation}\label{eq:machin}
 \pi=16\arctan(1/5)-4\arctan(1/239).
\end{equation}
For each arctangent the verifier takes the first one hundred terms of
its alternating power series and encloses the remainder by the next
term.  The resulting rational endpoints are rounded outward to scale
$S$.

Sine and cosine are evaluated by the Taylor polynomials through degrees
121 and 120 respectively, using outward-rounded interval operations.
Every argument used for a coefficient lies in $[0,\pi)$: in the power
basis of $\mathbb Z[\omega]$ it is $j\pi/\nu$ with
$0\le j<\varphi(2\nu)\le\nu$.  Every arc argument lies in
$[0,\pi/(13\nu)]$.  All arguments are therefore in $[0,4]$.
Taylor's theorem supplies the common conservative error bound
\begin{equation}\label{eq:taylor-error}
 \frac{4^{121}}{121!}<\frac1S.
\end{equation}
The displayed integer inequality $4^{121}S<121!$ is itself asserted in
the verifier.  One unit is added outward to each Taylor interval, in
addition to all rounding enclosures already accumulated by the arithmetic.

For a dyadic parameter interval
\[
 I=\left[\frac{a\pi}{13\nu\,2^d},
          \frac{(a+1)\pi}{13\nu\,2^d}\right],
\]
monotonicity of sine and cosine on $[0,\pi/2]$ gives an enclosing complex
interval $Z_I$ for $e^{-i\theta}$, $\theta\in I$.  Complex interval
Horner evaluation gives an enclosure $Q_b(Z_I)$.  The interval is
accepted only if either the real or the imaginary component strictly
excludes zero.  If it is not accepted, it is replaced by its two equal
halves.  Starting with the full closed arc, every subdivision preserves
coverage, including both endpoints.  Failure to certify an interval by
depth thirty raises an exception; it is never treated as success.

In pseudocode, with every indicated polynomial operation exact, the
complete proof check is:
\begin{enumerate}
\item Enumerate every nonconstant binary word $b$ of length thirteen.
\item Compute $\nu,B_k,\widetilde P_b$ and $F_\nu$; divide by $F_\nu$
and assert that the remainder is zero.
\item Remove all exact factors $z-1$, obtaining $Q_b$ with $Q_b(1)\ne0$.
\item Enclose its coefficients at the specified embedding
$\omega=e^{-\pi i/\nu}$ by the integer interval procedure above.
\item Start with the full interval $[0,\pi/(13\nu)]$.  Repeatedly accept
an interval whose Horner enclosure excludes zero, or bisect it.
\item Assert that every interval has been accepted.  Record the finite
partition, its size and its greatest depth.
\end{enumerate}

The supplied verifier \texttt{certify\_cycle13.py}, which uses only the
Python standard library, completes this check.  The observed exact
certificate sizes are
\begin{center}
\begin{tabular}{lrrr}
Enumeration & Words & Accepted intervals & Greatest depth\\\hline
Dihedral representatives & 378 & 393 & 3\\
All nonconstant words & 8190 & 8459 & 3
\end{tabular}
\end{center}
The full enumeration is reproduced by
\begin{verbatim}
python3 certify_cycle13.py --all-words
\end{verbatim}
The implementation, including every interval primitive, is short enough
to be printed with the paper.  The recorded partitions provide an
additional check on complete coverage; the verifier also constructs and
checks them anew, so trusting a precomputed data file is unnecessary.

\begin{proof}[Proof of Lemma~\ref{lem:cycle}]
The preceding geometric reduction proves regularity if only one
boundary-side length occurs.  Otherwise it gives a nonconstant binary
word and a zero of its closure polynomial at
$0<\theta<\pi/(13\nu)$.  The factors removed in
\eqref{eq:remaining-quotient} have no zeros on this open arc.
Proposition~\ref{prop:cycle-finite-certificate}, verified by the finite
integer interval certificate, excludes a zero of $Q_b$ there as well.
This contradiction proves the lemma.
\end{proof}