\documentclass[11pt,a4paper]{article}
\usepackage[utf8]{inputenc}\usepackage[T1]{fontenc}
\usepackage{amsmath,amssymb,amsthm}\usepackage[margin=2.4cm]{geometry}
\usepackage[hidelinks]{hyperref}
\newtheorem{theorem}{Theorem}\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{conjecture}[theorem]{Conjecture}
\theoremstyle{remark}\newtheorem{remark}[theorem]{Remark}
\theoremstyle{definition}\newtheorem{definition}[theorem]{Definition}
\title{Every $C_4$-free graph on $49$ vertices has a vertex of degree at most $6$}
\author{David Niedbala Giraudin\\ \small ORCID 0009-0009-1526-1178}
\date{\small Technical assistance: Claude (Anthropic)}
\begin{document}\maketitle
\begin{abstract}
We prove that every graph on $49$ vertices containing no cycle of length four has a vertex of
degree at most $6$. Equivalently, $R(C_4,K_{1,42})\le 49$, hence $R(C_4,K_{1,42})=49$, a value
left open in the published tables. In the notation of Erd\H{o}s, the least integer $f(n)$ such
that every graph on $n$ vertices with minimum degree at least $f(n)$ contains a $C_4$ satisfies
$f(49)=7$, while $f(48)=f(50)=8$; the value $f(48)=8$ comes from an explicit $7$-regular
$C_4$-free Cayley graph on $48$ vertices, which is also an explicit lower-bound construction for
the tabulated value $R(C_4,K_{1,41})=49$. Hence $f$ is not non-decreasing; to our knowledge no
$n$ with $f(n+1)<f(n)$ was known before. Erd\H{o}s's
question whether $f(n+1)\ge f(n)$ for all sufficiently large $n$ (Problem~85 of
erdosproblems.com) remains open. The proof combines structural lemmas, valid for every odd $k$,
on $C_4$-free graphs with $k^2$ vertices and minimum degree at least $k$, a symmetry reduction
for $k=7$, and an exhaustive SAT search carried out by two separately written programs.
\end{abstract}

\begin{center}\begin{minipage}{0.86\textwidth}\small
\textbf{R\'esum\'e.} Nous montrons que tout graphe \`a $49$ sommets sans cycle de longueur
quatre poss\`ede un sommet de degr\'e au plus $6$~; de fa\c{c}on \'equivalente,
$R(C_4,K_{1,42})\le 49$, d'o\`u $R(C_4,K_{1,42})=49$, valeur laiss\'ee ouverte dans les tables
publi\'ees. Combin\'e avec un graphe de Cayley explicite \`a $48$ sommets, $7$-r\'egulier et sans
$C_4$, ce r\'esultat donne $f(48)=8>f(49)=7$, o\`u
$f(n)$ est le plus petit entier tel que tout graphe \`a $n$ sommets de degr\'e minimum au moins
$f(n)$ contienne un $C_4$~; ce graphe fournit aussi une construction explicite pour la valeur
tabul\'ee $R(C_4,K_{1,41})=49$, et le graphe de Hoffman--Singleton donne $f(50)=8$. Ainsi $f$ n'est pas croissante au sens large~; \`a notre
connaissance aucune valeur de $n$ v\'erifiant $f(n+1)<f(n)$ n'\'etait connue. La question d'Erd\H{o}s de savoir si $f(n+1)\ge f(n)$ pour tout $n$ assez grand
(probl\`eme~85 d'erdosproblems.com) reste ouverte. La preuve combine des lemmes structurels,
valables pour tout $k$ impair, sur les graphes sans $C_4$ \`a $k^2$ sommets de degr\'e minimum au
moins $k$, une r\'eduction par sym\'etrie pour $k=7$ et une recherche exhaustive par solveurs SAT
men\'ee par deux programmes \'ecrits s\'epar\'ement.
\end{minipage}\end{center}

\section{Introduction}
For $n\ge 4$ let $f(n)$ be the least integer such that every graph on $n$ vertices with minimum
degree at least $f(n)$ contains a cycle $C_4$, and let $h(n)=f(n)-1$ be the largest minimum
degree of a $C_4$-free graph on $n$ vertices. Erd\H{o}s asked whether $f(n+1)\ge f(n)$ for all
sufficiently large $n$, and whether at least
$f(m)>f(n)-c$ for all $m>n$ and some constant $c$ (Problem~85 of [EP], where the original
sources, among them [Er93, p.~345], are listed).

The function $f$ carries the same information as the Ramsey number $s(m)=R(C_4,K_{1,m})$:
a $C_4$-free graph on $N$ vertices whose complement contains no $K_{1,m}$ is exactly a $C_4$-free
graph with minimum degree at least $N-m$, so that
\[ h(N)\ge N-m \iff s(m)\ge N+1 . \]
Parsons [Pa75] proved $s(m)\le m+\lfloor\sqrt{m-1}\rfloor+2$ for all $m\ge2$ (see [Bo24]).
The values of $s(m)$ are known for $m\le 38$ [Bo24, Ra], and also $s(40)=47$; the values
$s(38)=45$ and $s(40)=47$ are due to Zhang, Chen and Cheng [ZCC17]. The tables of [Bo24] and [Ra]
record $s(41)=49$; we did not find a construction for the lower bound $s(41)\ge49$ in
[Bo24, Pa75, Ra]. For $m=42$ the table of [Bo24] gives only the upper bound $50$, the lower
bound $49$ following from $s(41)\ge 49$ (or from [Bo24, Remark~12]).

\begin{theorem}\label{thm:main}
Every $C_4$-free graph on $49$ vertices has minimum degree at most $6$. Equivalently,
$R(C_4,K_{1,42})\le 49$.
\end{theorem}

\begin{corollary}\label{cor:drop}
$f(48)=8$, $f(49)=7$ and $f(50)=8$; moreover $R(C_4,K_{1,41})=R(C_4,K_{1,42})=49$. In
particular $f(n+1)<f(n)$ for $n=48$.
\end{corollary}

\paragraph{Status of the statements.} Theorem~\ref{thm:main} is proved by
Lemmas~\ref{lem:ball}--\ref{lem:pigeon}, the reduction of Section~\ref{sec:sym} (proved by hand)
and a finite computation (Section~\ref{sec:comp}), carried out by two separately written
programs. In Corollary~\ref{cor:drop}, the values $f(48)=f(50)=8$ and $R(C_4,K_{1,41})=49$ are
proved from explicit graphs, independently of Section~\ref{sec:comp}; $f(49)=7$ and $R(C_4,K_{1,42})=49$ rest on
Theorem~\ref{thm:main}. The question of Problem~85, monotonicity for all large $n$, remains
open.

\section{A counting lemma}\label{sec:ball}
All graphs are finite and simple. For a vertex $x$, $N(x)$ is its neighbourhood and $d(x)$ its
degree. In a $C_4$-free graph two distinct vertices have at most one common neighbour.

\begin{lemma}\label{lem:ball}
Let $G$ be $C_4$-free on $n$ vertices and let $x$ be a vertex.
Let $T(x)$ be the number of edges inside $N(x)$. Then
\[ \bigl|\{z: \operatorname{dist}(x,z)\le 2\}\bigr| = 1+d(x)+\sum_{y\in N(x)}(d(y)-1)-2T(x)\le n , \]
the edges inside $N(x)$ form a matching, and every vertex outside $N[x]$ has at most one
neighbour in $N(x)$.
\end{lemma}
\begin{proof}
If $y\in N(x)$ had two neighbours $w,w'\in N(x)$, then $x w y w'$ would be a $C_4$; so the edges
inside $N(x)$ form a matching. A vertex $z\notin N[x]$ with two neighbours in $N(x)$ would close a
$C_4$ through $x$. Hence the sets $N(y)\setminus\{x\}$, $y\in N(x)$, cover each vertex at distance
$2$ exactly once and each vertex of $N(x)$ that lies on an edge inside $N(x)$ exactly once, which
gives the formula.
\end{proof}

\section{The structure for \texorpdfstring{$k^2$}{k\textasciicircum 2} vertices, \texorpdfstring{$k$}{k} odd}\label{sec:struct}
Fix an odd integer $k\ge3$ and let $G$ be a $C_4$-free graph on $k^2$ vertices with minimum degree
at least $k$.

\begin{lemma}\label{lem:tight}
(i) Every vertex has degree $k$ or $k+1$, and some vertex has degree $k+1$.
(ii) If $d(v)=k+1$, then $N(v)$ induces a perfect matching, every $u\in N(v)$ has degree exactly
$k$, and the sets $A_u=N(u)\setminus N[v]$, $u\in N(v)$, have $k-2$ elements each and partition
$V\setminus N[v]$.
(iii) The vertices of degree $k+1$ form an independent set.
(iv) Every vertex of degree $k$ lies on a triangle.
\end{lemma}
\begin{proof}
For a vertex $x$ of degree $r$, Lemma~\ref{lem:ball} with $d(y)\ge k$ and $T(x)\le r/2$ gives
$k^2\ge 1+r+r(k-1)-r=1+r(k-1)$, so $r\le k+1$. The degree sum is even, while $k\cdot k^2$ is odd;
hence not all degrees equal $k$, which proves (i). If $d(v)=k+1$, equality must hold throughout:
$T(v)=(k+1)/2$, every neighbour of $v$ has degree $k$, and every vertex lies within distance $2$
of $v$; this is (ii), and (iii) follows from it. For (iv), if $d(x)=k$ and $t$ neighbours of $x$
have degree $k+1$, Lemma~\ref{lem:ball} gives $k^2\ge 1+k+k(k-1)+t-2T(x)$, so $2T(x)\ge 1+t\ge1$.
\end{proof}

From now on $v$ is a vertex of degree $k+1$, $N(v)=\{u_1,\dots,u_{k+1}\}$ with the matching
$u_{2i-1}u_{2i}$, and $G_i=A_{u_i}$. We call $G_i$ and $G_{i'}$ \emph{partner groups} when
$u_i u_{i'}$ is an edge. The vertices of $\bigcup G_i$ are the \emph{outer} vertices and $H$ is the
graph they induce.

\begin{lemma}\label{lem:outer}
Every outer vertex $x\in G_i$ has exactly one neighbour in $N[v]$, namely $u_i$, and in $H$:
(a) $x$ has at most one neighbour in $G_i$;
(b) $x$ has no neighbour in the partner group of $G_i$;
(c) $x$ has at most one neighbour in every other group;
(d) two vertices of the same group have no common neighbour in $H$;
(e) $H$ is $C_4$-free;
(f) $d_H(x)\in\{k-1,k\}$.
Conversely, a graph $H$ on the $k^2-k-2$ outer vertices satisfying (a)--(f), together with $v$,
$N(v)$, the matching and the attachments, is $C_4$-free with minimum degree at least $k$.
\end{lemma}
\begin{proof}
Each statement is the exclusion of an explicit $4$-cycle: (a) $u_i y x y'$; (b) $x u_i u_{i'} y$;
(c) $x y u_j y'$; (d) $x z y u_i$; (f) follows from (a)--(c) and $d(x)\ge k$, since $x$ has at most
$k$ possible neighbours in $H$ (one in its own group and one in each of the $k-1$ groups that are
neither its own nor its partner).

For the converse, let $C$ be a $4$-cycle of the whole graph and let $j$ be the number of its
vertices in $N[v]$. If $v\in C$, its two neighbours on $C$ are some $u_i,u_l$, and the fourth
vertex is a common neighbour of $u_i,u_l$ other than $v$: it is not in $N(v)$ (the edges inside
$N(v)$ form a matching) and not outer (an outer vertex has one neighbour in $N(v)$); impossible.
So $v\notin C$. If $j=0$, $C$ lies in $H$, excluded by (e). If $j\ge1$, every vertex $u_i$ of $C$
has its two $C$-neighbours in $\{u_{i'}\}\cup G_i$, where $u_{i'}$ is its partner. If $C$ contains
an edge $u_iu_{i'}$, the other two vertices are $x\in G_i$ and $y\in G_{i'}$ adjacent in $H$,
excluded by (b). Otherwise every vertex of $C$ in $N(v)$ has both $C$-neighbours in its own
group; two such vertices $u_i,u_l$ on $C$ would be opposite, with $C$-neighbours in
$G_i\cap G_l=\emptyset$, so $j=1$ and $C=u_i\,x\,z\,y$ with $x,y\in G_i$ and $z$ a common
neighbour of $x,y$ in $H$, excluded by (d). Finally the degrees: an outer vertex has degree
$1+d_H(x)\ge k$, the $u_i$ have degree $k$ and $v$ has degree $k+1$.
\end{proof}

We say that an outer vertex has $k$ \emph{slots}: its own group and the $k-1$ groups that are not
partners of its group. By (a)--(c) it has at most one neighbour per slot, and by (f) at most one
empty slot; it has degree $k+1$ in $G$ exactly when no slot is empty.

\begin{lemma}\label{lem:pigeon}
Let $x$ be an outer vertex and $W$ a group different from the group of $x$. At most $|W|=k-2$
neighbours of $x$ in $H$ have a neighbour in $W$.
\end{lemma}
\begin{proof}
Each $z\in W$ has at most one common neighbour with $x$, and none outside $H$, because the only
neighbour of $z$ in $N[v]$ is the vertex attached to $W$, which is not adjacent to $x$.
\end{proof}

\section{Symmetry reduction}\label{sec:sym}
Fix $k=7$, a vertex $v$ of degree $8$ (Lemma~\ref{lem:tight}), the matching $u_1u_2,u_3u_4,u_5u_6,u_7u_8$
of $N(v)$ and the groups $G_1,\dots,G_8$ of five outer vertices each. The labelling of
$N(v)\cup\bigcup G_i$ is free subject to the matching; we fix it in four steps, each of which
can be achieved by relabelling any solution, so that a solution exists if and only if a
solution satisfying all four conditions exists.

\emph{Step 1 (reference group).} Exactly one of the following holds.
\emph{Case I}: some outer vertex has degree $8$; we let $G_1$ be a group containing one.
\emph{Case II}: no outer vertex has degree $8$; we let $G_1$ be a group with the fewest edges
inside it. In both cases $G_2$ denotes the partner of $G_1$.

\emph{Step 2 (order of the other groups).} The $48$ relabellings of $G_3,\dots,G_8$ that preserve
the partner pairs $\{G_3,G_4\},\{G_5,G_6\},\{G_7,G_8\}$ are applied so that
$m_3\ge m_4$, $m_5\ge m_6$, $m_7\ge m_8$ and $m_3\ge m_5\ge m_7$, where $m_w$ is the number of
edges between $G_1$ and $G_w$.

\emph{Step 3 (inside $G_1$).} The vertices of $G_1$ are numbered $0,\dots,4$ so that the edges
inside $G_1$ are among $\{0,1\},\{2,3\}$, with $\{0,1\}$ used first.

\emph{Step 4 (alignment).} For $w=3,\dots,8$ the vertices of $G_w$ are numbered so that those with
a neighbour in $G_1$ come first, in the order of their neighbour; $G_2$ is numbered in the same way
with respect to $G_3$. By Lemma~\ref{lem:outer}(c) the edges between two non-partner groups form a
matching, so this is always possible, and it leaves no freedom inside the matched part.

After these steps the adjacency of $G_1$ to the whole outer graph is determined by its
\emph{pattern}: the edges inside $G_1$ and, for every vertex of $G_1$, its empty slot if any.
Two patterns are equivalent when they differ by a permutation of the five vertices of $G_1$ and by
one of the $48$ relabellings of Step~2; Steps~3--4 then restore the normal form. A direct
enumeration gives $39$ equivalence classes of patterns, $18$ of which contain a vertex without
empty slot and $21$ of which do not; in Case~I only the former can occur for $G_1$, in Case~II
only the latter. For each class one
representative is fixed (for Program~A one compatible with Steps~2--4); the corresponding
sub-problems are the \emph{cubes}.

\begin{lemma}\label{lem:pairs}
Assume that every outer vertex has exactly one empty slot, and let $i(X)$ be the number of edges
inside a group $X$. Then $i(A)+i(A')\ge 3$ for every pair of partner groups $A,A'$.
\end{lemma}
\begin{proof}
For a group $X$ and a group $Y$ that is neither $X$ nor its partner, let $D(X,Y)$ be the number of
vertices of $X$ whose empty slot is $Y$. Every vertex of $X$ has exactly one neighbour in $Y$
unless its empty slot is $Y$, so there are $5-D(X,Y)$ edges between $X$ and $Y$, and
$D(X,Y)=D(Y,X)$. A vertex has its own slot empty exactly when it lies on no edge inside its group
(the edges inside a group form a matching), so the $2i(X)$ vertices of $X$ on such edges are those
whose empty slot is another group: $\sum_Y D(X,Y)=2i(X)$. Hence the number of vertices outside $X$
whose empty slot is $X$ is $\sum_Y D(Y,X)=2i(X)$.
A pair $(x,z)\in A\times A'$ has no common neighbour in $N[v]\cup A\cup A'$ (there are no edges
between $A$ and $A'$) and at most one common neighbour in all. A vertex $w$ of one of the six other
groups $C$ is adjacent to a vertex of $A$ and to a vertex of $A'$ unless its empty slot is $A$ or
$A'$; distinct such $w$ give distinct pairs. Hence
$25\ge\sum_C\bigl(5-D(C,A)-D(C,A')\bigr)=30-2i(A)-2i(A')$.
\end{proof}

\section{Computation}\label{sec:comp}
\paragraph{Additional valid constraints.} Besides Lemma~\ref{lem:outer}, the following
constraints are imposed. The first two are consequences of Lemmas~\ref{lem:tight}
and~\ref{lem:pigeon} and hold in every solution. The Case~II items express the choice of $G_1$
in Step~1 and two refinements of it; they hold in a suitably relabelled copy of every solution,
because the quantities used for the choice (the number of inner edges of a group, the number
$c(G)$ and the type defined below) do not change under the relabellings of Steps~2--4.
\begin{itemize}
\item (Triangles) every outer vertex lies on a triangle (Lemma~\ref{lem:tight}(iv), and for an
outer vertex of degree $8$ part (ii) applied to it);
\item (Pigeonhole) Lemma~\ref{lem:pigeon} for every outer vertex $x$ and every group $W$;
\item (Case II) every outer vertex has exactly one empty slot, and every group has at least as
many inner edges as $G_1$;
\item (Case II, two inner edges in $G_1$) then every group has exactly two inner edges and
exactly one vertex whose empty slot is its own group, the other four having their empty slot
in another group. Among the groups, $G_1$ is chosen to maximise $c(G)$, the largest number of
vertices of $G$ with the same empty slot. If $A,B$ are non-partner groups, the vertices of $A$
with a neighbour in $B$ are those whose empty slot is not $B$, so the number of edges between
$A$ and $B$ is at least $5-c(A)\ge 5-c(G_1)$. This lower bound is imposed for all such pairs
(by Program~A in $14$ of the $17$ cubes of this kind, by Program~B in all of them).
\item (Case II, one inner edge in $G_1$) then every group has one or two inner edges. If a group
$A$ has exactly one inner edge $xy$, its three other vertices have their empty slot in $A$, and
$x,y$ have their empty slots in groups $b_x,b_y$ different from $A$ and its partner; hence
$m(A,B)=5-[b_x=B]-[b_y=B]$ for every group $B$ that is not $A$ or its partner, where $m(A,B)$
is the number of edges between $A$ and $B$. Say $A$ has type $\alpha$ if $b_x=b_y$, type
$\beta$ if $b_x,b_y$ are partner groups, and type $\gamma$ otherwise. Among the groups with one
inner edge, $G_1$ is chosen of the highest type ($\alpha>\beta>\gamma$). If $G_1$ has type
$\beta$, no group with one inner edge has type $\alpha$, i.e. $m(A,B)\ge4$ for all such $A$
and all groups $B$ other than $A$ and its partner; if $G_1$ has type $\gamma$, in addition
$m(A,B)+m(A,B')\ge 9$ for every partner
pair $B,B'$ of groups different from $A$ and its partner. These implications are imposed through
one switch variable $s_A$ per group: $s_A$ true forces at least two inner edges in $A$, $s_A$
false forces at most one inner edge in $A$ and the conditions above; the bound $i(A)+i(A')\ge3$
of Lemma~\ref{lem:pairs} is also imposed for the cubes of types $\beta$ and $\gamma$. Some nodes
of the search trees of these cubes were refuted on formulas containing only part of these
clauses; a refutation of part of the clauses is a refutation of the whole formula.
\end{itemize}
The choices of $G_1$ (Case~I or II; fewest inner edges; then largest $c$ or highest type) are
made in this order, before Steps~2--4, and do not use any freedom used later.

\paragraph{Program A.} The whole graph on $49$ vertices is encoded in propositional logic, one
variable per pair of vertices, with the structure of Lemma~\ref{lem:tight}(ii) fixed, all
$4$-cycles forbidden, degree constraints encoded by sequential counters, and the constraints
of Section~\ref{sec:sym} and above. For each of the $39$ cubes the formula is either refuted
directly by \textsc{kissat}, or split by the look-ahead solver \textsc{march\_cu} into
sub-cubes, i.e.\ lists of literals added as unit clauses. Every split is accepted only together
with a covering check: a run on the parent formula with the negations of all sub-cubes added as
clauses. Sub-cubes are refuted separately, by \textsc{kissat} or by an incremental
\textsc{CaDiCaL} run under assumptions, within CPU-time limits, or by \textsc{CaDiCaL}~3.0.1
within a limit on the number of conflicts. A sub-cube exceeding its limit
is either split again in the same way or refuted later by a single longer run; a set of
literals contained in several sub-cubes may also be refuted directly, which refutes all of
them. A node of this search tree is thus refuted when it is refuted directly, when it
contains a refuted set of literals, or when its covering check and all its children are
refuted. Every run on which the proof relies returned UNSATISFIABLE, and no run returned
SATISFIABLE (the other runs stopped at their time or conflict limit, or were interrupted).

\paragraph{Program B.} The second program encodes only the outer graph $H$ through
conditions (a)--(f) of Lemma~\ref{lem:outer} (every solution gives such an $H$, and by the
converse part of the lemma nothing is lost). It has its own implementation of the alignment of
Step~4, it does not use Step~2, and it takes as representative of each of the $39$ pattern
classes the lexicographically least element of the class. It has its own implementation of
the triangle, pigeonhole and Case~II conditions, and solves with \textsc{CaDiCaL}, with the
same tree rules (splits by \textsc{march\_cu} with covering checks, CPU-time limits, longer
direct runs) implemented in a separate job manager. For the three cubes of Case~II with one
inner edge in $G_1$, part of the search tree was refuted on the formula augmented by static
symmetry breaking. Some relabellings of the outer vertices map such a cube to itself and fix
$G_2$ and $G_3$ pointwise: the swaps of whole groups among $G_5,\dots,G_8$ that preserve the
partner pairs and the adjacency to $G_1$, and, in the cube of type $\alpha$, the swap of the two
ends of the inner edge of $G_1$ together with the swap of the matching positions in the groups
matched to them. Since all other constraints are stated uniformly, such a relabelling $\pi$
maps solutions to solutions, and the lexicographic-leader clauses $E\le E\circ\pi$ (edge
variables in a fixed order) keep the least solution of every orbit. A node refuted on the
original formula is refuted a fortiori on the augmented one, so the tree refutes the augmented
formula, which is satisfiable whenever the cube formula is. In cubes $4$ and $5$ the exact switch
variables and the bound of Lemma~\ref{lem:pairs} are added on top of these clauses; every
solution satisfies them once $s_A$ is set to true exactly when $A$ has at least two inner edges,
and they are stated uniformly over the groups and the partner pairs, so the relabellings $\pi$ still map
solutions to solutions, and the least solution of every orbit satisfies all the added clauses.
The two programs share the reduction of Sections~\ref{sec:ball}--\ref{sec:sym}, which is proved
by hand, the derived constraints, the authors and the solver \textsc{CaDiCaL}, so they are not
independent in every respect; they differ in the encoding, in the implementation of the symmetry
breaking and in the representatives of the classes.

\paragraph{Runs.} The logs of Program~A record $6\,684$ refutations (covering checks
included) and $362$ runs stopped at their limit; those of Program~B record $1\,122$ and $149$.
The runs were made on two machines, a Linux server and a desktop computer under Windows. The runs marked
\texttt{W} in the logs ($2\,179$ refutations) were distributed as separate tasks, to the desktop
computer or, where marked \texttt{W:cadical-server}, to the server. All of them except $63$ short
ones were made by \textsc{CaDiCaL}~3.0.1 with a limit of $4$ million conflicts ($15$ million for
cube~$5$ of Program~B); the $63$ others, marked \texttt{W} alone, were made by a solver of
\texttt{python-sat} whose name was not logged, and all of them were certified (Checks~(iv)).
For each of these runs the literals
of the leaf were regenerated from the logged splits and compared with the literals sent to the
solver before the result was entered in the log. The other runs
used \textsc{kissat}~4.0.4 and the versions of \textsc{CaDiCaL} included in
\texttt{python-sat}.

\paragraph{Checks.} (i) The $36\,506$ patterns fall into $39$ classes ($18$ in Case~I), and
the cubes of each program contain exactly one pattern of each class; this is verified by two
scripts, one computing canonical forms (for the patterns whose inner edges are $\emptyset$,
$\{0,1\}$ or $\{0,1\},\{2,3\}$, which meet every class) and one computing the classes of all
patterns by union--find from generators of the acting group. (ii) Falsification: with the minimum degree
condition weakened to $6$ for the outer vertices and everything else unchanged, $17$ formulas of
both programs, among them formulas of every kind used (cubes of Case~I and of Case~II, including
the cubes of types $\alpha$, $\beta$ and $\gamma$, with and without the symmetry-breaking and exact
switch clauses), become satisfiable
within seconds, and every model found is
decoded into a $C_4$-free graph on $49$ vertices with minimum degree $6$, checked directly. (iii) The Hoffman--Singleton graph ($50$ vertices,
$7$-regular, girth $5$) is accepted by the graph checker. (iv) Proof certificates: for a fixed
random sample of refuted nodes with short logged runs ($67$ nodes, $6$ of Program~A and $61$ of
Program~B), the formula was rebuilt from the scripts, solved again by \textsc{kissat} with a DRAT
proof, and every proof was verified by the independent checker \textsc{drat-trim}. In separate
runs (not part of the ancillary scripts), $76$ further leaves refuted by runs marked \texttt{W} were certified in the same way: the
$63$ marked \texttt{W} alone, and $13$ others ($12$ of Program~A, $1$ of Program~B), $10$ of them
drawn at random. (v) A separate script reads the logs of both programs and checks
that every cube is refuted according to the rules above. (vi) For the symmetry breaking of Program~B, a script checks that every relabelling
used is an involution preserving groups and partner pairs, maps the fixed literals of the cube
to themselves and fixes $G_2$ and $G_3$ pointwise; on the formulas with weakened minimum degree
it checks moreover that models are mapped to models and that the augmented formulas stay
satisfiable.

The scripts are pure Python and are provided as ancillary files, together with the list of
cubes, the solver logs and the SHA-256 hashes of all formulas used.

\section{Proof of Corollary~\ref{cor:drop}}\label{sec:cor}
\emph{$f(50)=8$.} The Hoffman--Singleton graph [HS60] has $50$ vertices, is $7$-regular and has
girth $5$, so $h(50)\ge7$. A vertex of degree $r\ge8$ in a $C_4$-free graph with minimum degree $8$
would satisfy $1+r+7r-2T(x)\le 50$ by Lemma~\ref{lem:ball}, i.e. $2T(x)\ge 8r-49\ge 15$, which is
impossible since $T(x)\le r/2$ forces $8r-49\le r$, i.e. $r\le 7$. Hence $h(50)\le 7$ and $f(50)=8$.

\emph{$f(48)=8$.} Let $SD_{16}=\langle a,x\mid a^8=x^2=1,\ xax^{-1}=a^3\rangle$ be the
semidihedral group of order $16$, let $c$ generate $C_3$, and let $\Gamma$ be the Cayley graph of
$SD_{16}\times C_3$ with respect to the inverse-closed set
\[ S=\{x,\ a,\ a^{-1},\ axc,\ a^5xc^2,\ a^6xc,\ a^6xc^2\}. \]
$\Gamma$ has $48$ vertices and is $7$-regular. It is $C_4$-free: a Cayley graph
$\mathrm{Cay}(G,S)$ contains a $4$-cycle if and only if $st^{-1}=s't'^{-1}$ for two distinct
ordered pairs $(s,t)\ne(s',t')$ with $s\ne t$, $s'\ne t'$, and the $42$ elements $st^{-1}$
($s\ne t$) are pairwise distinct. (The edge list is provided and checked by two independent
programs.) Hence $h(48)\ge7$. Conversely, by Lemma~\ref{lem:ball}, a $C_4$-free graph on $48$
vertices with minimum degree $8$ would give, for a vertex $x$ of degree $r\ge8$,
$1+r+7r-2T(x)\le48$ with $2T(x)\le r$, i.e. $7r\le 47$, a contradiction. So $h(48)=7$ and $f(48)=8$. In terms of Ramsey numbers, $h(48)\ge7$ means $s(41)\ge49$, and
with the upper bound $s(41)\le 41+\lfloor\sqrt{40}\rfloor+2=49$ of [Pa75] this gives
$R(C_4,K_{1,41})=49$.

\emph{$f(49)=7$.} Theorem~\ref{thm:main} gives $h(49)\le6$. Deleting one vertex of the
Hoffman--Singleton graph leaves a $C_4$-free graph on $49$ vertices with minimum degree $6$, so
$h(49)=6$ and $f(49)=7$. In terms of Ramsey numbers, $h(49)\le 6$ means $s(42)\le 49$, and
$s(42)\ge s(41)=49$; hence $R(C_4,K_{1,42})=49$.

\section{Remarks}
\begin{enumerate}
\item Problem~85 of [EP] asks whether $f(n+1)\ge f(n)$ for all \emph{sufficiently large} $n$. A
single exception does not settle that question, which remains open; the result above only shows
that $f$ is not non-decreasing on all $n\ge4$.
\item By the equivalence $h(N)\ge N-m\iff s(m)\ge N+1$, an index $N\ge4$ with $f(N+1)<f(N)$
exists if and only if $s(m)=s(m+1)$ for some $m\ge2$ (then $N=s(m)-1$). By the tables of [Ra] (and [Bo24]),
$s(m)<s(m+1)$ for $2\le m\le 38$ and for $m=40$, while [Ra] gives $s(39)\in\{46,47\}$; the value
$s(39)=47$ would give the smaller instance $f(47)<f(46)$.
\item In terms of Ramsey numbers the two results read $R(C_4,K_{1,41})=R(C_4,K_{1,42})=49$.
The value $49$ for $n=41$ appears in the tables of [Bo24] and of the dynamic survey of
Radziszowski; the graph $\Gamma$ of Section~\ref{sec:cor} gives an explicit lower-bound construction for it.
Erd\H{o}s also asked whether consecutive values of $R(C_4,K_{1,n})$ coincide for infinitely many
$n$ (Problem~552 of [EP]); $n=41$ is an instance.
\item In $\Gamma$ every vertex has exactly three edges in its neighbourhood: the $48$ triangles
form a configuration $(48_3)$ whose collinearity graph is $C_4$-free, and the remaining $24$
edges form a perfect matching.
\item The page of Problem~85 in [EP] states that the bounds of Problem~552 imply
$f(n)<\sqrt n+1$. This inequality fails for some $n$, already for $n=15$: the line graph of the Petersen graph is $4$-regular and $C_4$-free, so
$f(15)\ge5>\sqrt{15}+1$ (in fact $f(15)=5$ by the bound below); it also fails for $n=48$: $f(48)=8>\sqrt{48}+1\approx 7.93$. Lemma~\ref{lem:ball} gives $\delta(\delta-1)\le n-1$ for the minimum degree $\delta$ of a $C_4$-free graph on $n$ vertices, hence only $f(n)<\sqrt n+3/2$.
\end{enumerate}

\begin{thebibliography}{99}
\bibitem[Bo24]{Bo24} L.~Boza, Exact values and bounds for Ramsey numbers of $C_4$ versus a star graph,
arXiv:2409.12770v2 (2026).
\bibitem[EP]{EP} T.~F.~Bloom, Erd\H{o}s Problems \#85 and \#552, \texttt{https://www.erdosproblems.com}.
\bibitem[Er93]{Er93} P.~Erd\H{o}s, Some of my favorite solved and unsolved problems in graph theory,
Quaestiones Math. 16 (1993), 333--350.
\bibitem[HS60]{HS60} A.~J.~Hoffman, R.~R.~Singleton, On Moore graphs with diameters 2 and 3, IBM J. Res. Develop. 4 (1960), 497--504.
\bibitem[Pa75]{Pa75} T.~D.~Parsons, Ramsey graphs and block designs I, Trans. Amer. Math. Soc. 209 (1975), 33--44.
\bibitem[ZCC17]{ZCC17} X.~Zhang, Y.~Chen, T.~C.~E.~Cheng, Some values of Ramsey numbers for $C_4$ versus
stars, Finite Fields Appl. 45 (2017), 73--85.
\bibitem[Ra]{Ra} S.~P.~Radziszowski, Small Ramsey numbers, Electron. J. Combin., Dynamic Survey DS1, revision 18 (2026).
\end{thebibliography}
\end{document}