\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage{lmodern,amsmath,amssymb,amsthm,geometry,microtype}
\usepackage{enumitem,booktabs,listings,xcolor}
\usepackage[hidelinks]{hyperref}
\geometry{margin=1in}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{remark}\newtheorem{remark}[theorem]{Remark}
\newcommand{\R}{\mathbb R}
\newcommand{\Z}{\mathbb Z}
\newcommand{\diam}{\operatorname{diam}}
\newcommand{\conv}{\operatorname{conv}}
\newcommand{\dist}{\Delta}
\title{The maximum cardinality of a planar seven-distance set}
\author{Alon Amit and GPT-6 Astra}
\hypersetup{pdfauthor={Alon Amit and GPT-6 Astra}}
\date{24 October 2026}
\begin{document}
\maketitle
\begin{abstract}
We give a computer-assisted proof that the maximum cardinality of a planar
set determining at most seven distinct positive distances is sixteen.
A diameter-graph argument reduces a hypothetical seventeen-point example
to an eleven-point set with at most six distances, except for a
thirteen-cycle obstruction. We exclude the cycle by an exact interval
certificate. Using a published exhaustive count of sixty-two candidate
distance patterns, we classify the eleven-point cores by exact
Gr\"obner-basis calculations and prove that none can have the required
seventeen-point extension. All extension calculations use rational or
algebraic arithmetic. An explicit sixteen-point triangular-lattice set
attains the bound.
\end{abstract}

\section{Introduction}
For a finite set $X\subset\R^2$, put
\[
 \dist(X)=\{\|x-y\|:x,y\in X,\ x\ne y\},\qquad
 g_2(s)=\max\{|X|:|\dist(X)|\le s\}.
\]
All distances are Euclidean and positive. We use ``at most'' so the
property is hereditary.
\begin{theorem}\label{thm:main}
Every finite subset of $\R^2$ determining at most seven distances has
cardinality at most sixteen. This bound is attained; hence $g_2(7)=16$.
\end{theorem}
Erd\H{o}s and Fishburn~\cite{EF} established the planar maxima through
five distances and exhibited sixteen-point seven-distance sets.
Wei~\cite{Wei} proved $g_2(6)=13$; Sz\"oll\H{o}si and
\"Osterg\aa rd~\cite{SO} completed the classification at cardinality
thirteen. Budianto~\cite{Budianto} obtained partial exclusions for a
hypothetical seventeen-point seven-distance set using diameter graphs.
Bao and Yu~\cite{BY} studied specified triangular-lattice palettes and
conjectured the unrestricted value sixteen.

Our proof uses the exhaustive candidate count at order eleven in
\cite[Table 9]{SO}, rather than repeating the large combinatorial
search that produced it. We reconstruct all sixty-two candidate patterns
by exhibiting that many inequivalent realizable patterns. Exact algebra
then exhausts their metrics. This distinction matters: a count of colored
patterns alone is not a classification of geometric realizations.
The remaining extension and cycle obstructions are finite computations
whose coverage is justified geometrically. The proof is computer-assisted,
not a proof-assistant formalization.

\section{Published inputs and notation}
Write $D=\diam X$ and let $X_D$ be the endpoints of pairs at distance
$D$. The diameter graph $G_D(X)$ has vertex set $X$ and an edge $xy$
exactly when $\|x-y\|=D$. Its induced graph on $X_D$ has no isolated
vertices. Write $m=|X_D|$. A set independent in $G_D(X)$ has at most six
distances when $X$ has at most seven.

We use the following published facts.
\begin{enumerate}[label=(\roman*)]
\item A convex $h$-gon determines at least $\lfloor h/2\rfloor$
distances. An odd convex $(2k+1)$-gon determining $k$ distances is regular.
For even $h\ge8$, a convex $h$-gon determining $h/2$ distances is regular
or is obtained by deleting one vertex from a regular $(h+1)$-gon.
See~\cite[Lemma 2]{EF}.
\item Diameter endpoints are extreme vertices, and disjoint diameter
segments cross. A planar diameter graph has no even cycle and at most one
cycle. If its graph on $m$ nonisolated vertices is not $C_m$, its
independence number is at least $\lceil m/2\rceil$.
See~\cite[Lemmas 3--5 and 9]{Wei}.
\item A set with at most six distances has at most thirteen points
\cite{Wei,SO}.
\item The exhaustive generation of~\cite[Sections 3.1 and 4, Table 9]{SO}
leaves exactly sixty-two candidate distance patterns at order eleven,
using at most six colors, modulo permutations of vertices and colors.
Every eleven-point planar set with at most six distances is represented among these
candidates. This finite-generation result is an external input to our proof.
\end{enumerate}
All references to a convex polygon mean its extreme vertices, in cyclic
boundary order. We write $R_n$ for the vertices of a regular $n$-gon and
$O$ for its center.
\section{Relation to Budianto's reductions}\label{sec:budianto}
Budianto's thesis~\cite{Budianto} studies a hypothetical seventeen-point
seven-distance set by the number $m$ of endpoints of diameter pairs.
He excludes $m\le8$ and $m\ge14$, and leaves $9\le m\le13$ partially
unresolved. In particular, pages 9--13 establish that when $m=13$, the
maximum degree of the diameter graph is two; its remaining forms are
$C_{13}$ and unions of paths. The tables for $9\le m\le12$ are expressly
incomplete, and are not used here as classification theorems.

The larger-diameter extension obstruction for the three thirteen-point
six-distance configurations already appears in Budianto's argument on
pages 15--19. For the hexagram, he obtains six possible additional points
and three incompatible opposite pairs; the two circular configurations
admit no addition introducing a larger diameter. These obstructions already explain why a thirteen-point core is useful.
The present proof goes further by classifying and extending eleven-point cores. His exclusion of fourteen and fifteen diameter
endpoints on pages 7--9 also precedes our hull reduction; the squared-distance
sum proof gives a direct argument for the stronger bound on all hull
vertices. The full thirteen-point classification is supplied by
Sz\"oll\H{o}si and \"Osterg\aa rd~\cite[Theorem 16]{SO}.

These conclusions do not give a bound of eighteen in the thesis.
The exceptional thirteen-cycle remains explicitly unresolved there.
The following route through smaller distance sets is a separate finite
classification and extension argument.

\section{A bound on the number of hull vertices}
\begin{lemma}\label{lem:hull}
If $|X|\ge16$ and $|\dist(X)|\le7$, then $\conv X$ has at most thirteen
vertices. In particular, $|X_D|\le13$.
\end{lemma}
\begin{proof}
The convex-polygon bound gives at most fifteen hull vertices. If there
are fifteen, they form $R_{15}$. A noncentral point has any given distance
to at most two vertices of $R_{15}$, since two distinct circles intersect
in at most two points. It therefore sees at least eight distances.
The center sees the circumradius, which is not an existing chord length:
$2\sin(\pi j/15)=1$ has no integral solution $1\le j\le7$.
Thus there is no additional point.

If there are fourteen hull vertices, they form $R_{14}$ or $R_{15}$ with
one vertex $v$ deleted. Normalize the circumcenter to $0$ and radius to
$1$. An additional point $q$ is in their convex hull and has $r=\|q\|<1$.
The center is again excluded because neither $14$ nor $15$ is divisible
by $6$. Otherwise the fourteen distances from $q$ must realize all seven
old distances exactly twice.

For $R_{14}$ the sum of its seven distinct squared chord lengths is
\[
 \sum_{j=1}^{7}(2-2\cos(2\pi j/14))=16.
\]
Since the vertices sum to zero, summing the fourteen squared distances
from $q$ gives $14(1+r^2)=32$, contrary to $r<1$.

For $R_{15}\setminus\{v\}$ the distinct squared chord lengths sum to
$15$, and the fourteen vertices sum to $-v$. The same calculation gives
\[
 14(1+r^2)+2q\cdot v=30,\qquad 7r^2+q\cdot v=8.
\]
But $7r^2+q\cdot v\le7r^2+r<8$. This excludes fourteen vertices as well.
\end{proof}

\section{Extensions of a regular thirteen-gon}
\begin{lemma}\label{lem:regular}
If $X$ contains $R_{13}$ and determines at most seven distances, then
$X\subseteq R_{13}\cup\{0\}$, where $0$ is the center of $R_{13}$.
\end{lemma}
\begin{proof}
Normalize the circumradius to $1$. Set $a=\pi/13$, $c_j=\cos(2ja)$ for
$0\le j\le6$, and $\beta_j=2-2c_j$ for $1\le j\le6$.
Let $q\notin R_{13}\cup\{0\}$. Each distance from $q$ occurs at most
twice among the thirteen vertices, so there are exactly seven distinct
values. There is an equal-distance pair; its perpendicular bisector is
a reflection axis of the regular polygon and contains both $0$ and $q$.
As the polygon has odd order, we may write $q=t v_0$ for some vertex
$v_0$ and nonzero real $t$. The seven distinct squared distances are
\[
 f_j=t^2+1-2tc_j\quad(0\le j\le6).
\]
Their set must contain all six $\beta_j$, since their union with those
six values has size at most seven. Equivalently, the affine map
$F(z)=(1-t^2)/2+tz$ maps six of $c_0,\ldots,c_6$ onto
$c_1,\ldots,c_6$. Let $c_h$ be the omitted argument.

Put $K=2\sin a$ and $g_j=c_j-c_{j+1}=K\sin((2j+1)a)$ for $0\le j\le5$.
The following strict inequalities follow by product-to-sum identities:
\begin{align}
 g_1^2-g_0g_2&=K^2\sin^2(2a)>0,\label{eq:gap1}\\
 g_1g_4-g_2g_5&=K^2\sin a\sin(2a)>0,\label{eq:gap2}\\
 g_0g_4-g_1g_5&=-K^2\sin a\sin(2a)<0.\label{eq:gap3}
\end{align}
If $t>0$, order is preserved. For $h=0$, $F$ fixes the endpoints of
$\{c_1,\ldots,c_6\}$ and is the identity. For $1\le h\le4$, it fixes
$c_5,c_6$ and is again the identity, now an impossibility since $c_0$
is retained. For $h=5$ or $6$, the first three arguments map to
$c_1,c_2,c_3$, forcing $g_1/g_0=g_2/g_1$, contrary to~\eqref{eq:gap1}.
The identity case gives $t=1$, an existing vertex.

If $t<0$, the five consecutive gaps in the retained six-element
argument set must be proportional to $(g_5,g_4,g_3,g_2,g_1)$.
For $h=0$ this forces $g_1g_4=g_2g_5$, contradicting~\eqref{eq:gap2}.
For $h=1$ it forces $(g_0+g_1)g_4=g_2g_5$, an even stronger
contradiction. For $h=2$, the last two gaps force
$g_1g_4=g_2g_5$ again. For $3\le h\le6$, the first two gaps force
$g_0g_4=g_1g_5$, contradicting~\eqref{eq:gap3}.
Thus no such $q$ exists.
\end{proof}


\input{algebraic_section.tex}
\input{core_method_section.tex}
\input{eleven_extensions_section.tex}

\section{Proof of the main theorem}
\begin{proof}[Proof of Theorem~\ref{thm:main}, upper bound]
Suppose $X$ has seventeen points and at most seven distances. It has
exactly seven distances because $g_2(6)=13$.
By Lemma~\ref{lem:hull}, $m=|X_D|\le13$.
If the graph on $X_D$ is not $C_m$, it has an independent set of size
at least $\lceil m/2\rceil$. Together with the $17-m$ isolated vertices,
this gives an independent set of size at least
\[
 17-m+\lceil m/2\rceil=17-\lfloor m/2\rfloor\ge11.
\]
If the graph on $X_D$ is $C_m$ with $m\le11$, then $m$ is odd and the
corresponding bound is
\[
 17-m+(m-1)/2=17-(m+1)/2\ge11.
\]
In either case choose eleven independent points $A$. Their distances
omit the global diameter, so $|\dist(A)|\le6$ and $\diam A<\diam X$.
Lemma~\ref{lem:eleven-extension} gives $|X|\le16$, a contradiction.

The only remaining case is $m=13$ with endpoint graph $C_{13}$.
Lemma~\ref{lem:cycle} makes these points a regular thirteen-gon.
Lemma~\ref{lem:regular} then gives $|X|\le14$, again a contradiction.
Every larger set contains a seventeen-point subset, so all cardinalities
above sixteen are excluded.
\end{proof}

\section{An attaining configuration}\label{sec:lower}
In triangular coordinates, with $Q(a,b)=a^2+ab+b^2$, let
\[
 H=\{(a,b)\in\Z^2:Q(a,b)\in\{0,1,3\}\},\qquad
 X=H\cup\{(-2,0),(0,2),(2,-2)\}.
\]
There are sixteen points and exactly seven squared distances,
\[
 \{1,3,4,7,9,12,13\}.
\]
Their multiplicities are $33,24,18,24,9,6,6$, respectively, summing to
$\binom{16}{2}=120$. Direct integer calculation verifies these claims.
This supplies the lower bound and completes Theorem~\ref{thm:main}.

\section*{Computational provenance and reproduction}
The argument depends on the published candidate count in~\cite{SO} and
on the exact computations described here. The new computations were
performed and audited using independently written verification routines.
In particular, all sixty-two metric elimination bases were recomputed
from the original Gram minors in two runs and compared exactly; all
lattice compatibility maxima were also independently checked by exhaustive
subset enumeration. This is not a formal verification in a proof assistant.

This work is jointly authored by Alon Amit and GPT-6 Astra, an OpenAI
AI model. Alon Amit proposed the problem, guided the research, and supplied
Budianto's thesis. GPT-6 Astra, working through OpenAI Codex with parallel
research and audit agents, contributed to the literature analysis,
mathematical arguments, verification code, computational checks, and
manuscript preparation. The computational audits described above were
carried out in separate AI-agent sessions; they do not constitute external
human peer review. No human review beyond that actually performed is
implied by these audits.

The accompanying verification package contains the input coordinates,
pattern reconstruction, exact metric and extension checks, cycle verifier,
and independent audit records. From its root, with Python 3 and SymPy
installed, run
\begin{verbatim}
python3 verify_all.py
\end{verbatim}
Run without optimization: assertions are part of the certificate.
The metric stage recomputes the algebra from the Gram minors rather than
trusting cached bases. Its expected result is fifty-two forced lattice
metrics and ten exhausted circular pattern families. The extension stage
checks all fifty-two lattice cores and all circular families. The cycle
stage checks all $8190$ nonconstant words with $8459$ accepted intervals
and maximum subdivision depth three. The reference code and input data
are printed in Appendix~\ref{app:code} to preserve reproducibility of the
mathematical record without depending on a mutable external URL.
\begin{thebibliography}{9}
\bibitem{EF}
P. Erd\H{o}s and P. Fishburn,
Maximum planar sets that determine $k$ distances,
\emph{Discrete Mathematics} \textbf{160} (1996), 115--125.
\href{https://doi.org/10.1016/0012-365X(95)00153-N}{doi:10.1016/0012-365X(95)00153-N}.
\bibitem{Wei}
X. Wei, A proof of Erd\H{o}s--Fishburn's conjecture for $g(6)=13$,
\emph{Electronic Journal of Combinatorics} \textbf{19}(4) (2012), P38.
\href{https://doi.org/10.37236/2917}{doi:10.37236/2917}.
\bibitem{SO}
F. Sz\"oll\H{o}si and P. R. J. \"Osterg\aa rd,
Constructions of maximum few-distance sets in Euclidean spaces,
\emph{Electronic Journal of Combinatorics} \textbf{27}(1) (2020), P1.23.
\href{https://doi.org/10.37236/8565}{doi:10.37236/8565}.
\bibitem{Budianto}
W. T. Budianto,
\emph{An Observation on 7-distance Set in Euclidean Plane},
master's thesis, Department of Mathematics, National Central University,
Taiwan, June 2022.
\url{https://ir.lib.ncu.edu.tw/handle/987654321/88394}.

\bibitem{BY}
L.-R. Bao and W.-H. Yu, Constructions of Large $m$-Distance Sets on
Triangular Lattice, arXiv:2509.00880v1 (2025).
\url{https://arxiv.org/abs/2509.00880}.
\end{thebibliography}


\appendix
\section{Reference verification code and data}\label{app:code}
The following files form the reference verification package. File names
at the beginning of each listing give the paths relative to its root.
The input data are explicit finite mathematical objects; all proof
checks are recomputed from them. The source distribution also includes
independent audit implementations and their records.
\lstset{basicstyle=\ttfamily\scriptsize,breaklines=true,columns=fullflexible,
 keepspaces=true,showstringspaces=false,frame=single,rulecolor=\color{gray},
 numbers=left,numberstyle=\tiny\color{gray},numbersep=5pt,tabsize=4}
\input{reference_listings.tex}
\end{document}