\(\delta(G)\ge N-n\). [a]

For \(n=39\), the published upper bound gives

[b]

Explicit lower-bound certificate

I fetched House of Graphs graph 52632,

a 43-vertex \(C_4\)-free graph used as \(H_{43}\) in Boza's paper. The full

adjacency list is embedded in

erdos552_wave5z_verify.py, so verification

does not depend on the network. Its degree distribution is 37 vertices of

degree 6 and 6 of degree 7.

Add two nonadjacent vertices 43 and 44 with respective neighborhoods

The resulting graph has:

• 45 vertices and 144 edges;
• degree histogram \(\{6:27,\,7:18\}\);
• maximum pair-codegree 1;
• no \(C_4\), checked independently by pair-codegrees and by enumerating all

four-sets and all three cyclic orders;

• \(\Delta(\overline G)=38<39\).

The SHA-256 of the canonical edge text u-v\n, in lexicographic vertex order,

is

9197c5369534fc94766792f2e5134dd24088777725b7e017dbab396b1d4856f5.

These are [d] exhaustive checks. The Ramsey translation then gives

[a+d] This reproduces the known lower endpoint; it is an explicit

independently checkable certificate, not a new numerical bound.

Combining (1) and (2) yields the current interval \(46\)--\(47\).

[b+d]

Elementary reduction of the 46-vertex question

Assume that \(G\) is a \(C_4\)-free graph on 46 vertices with

\(\delta(G)\ge7\). Fix \(v\), put

Lemma 1: \(G\) is 7-regular

For any \(u\in A\), \(u\) has at most one neighbor in \(A\): two such

neighbors together with \(u,v\) would form a \(C_4\). Also, distinct vertices

of \(A\) have disjoint neighborhoods in \(B\): a common \(B\)-neighbor

together with \(v\) would form a \(C_4\). Since every \(u\in A\) has degree at

least 7, it has at least

neighbors in \(B\). Therefore

Hence \(d\le7\). Since \(d\ge\delta(G)\ge7\), \(d=7\). This applies to every

vertex, so \(G\) is 7-regular. [a]

Lemma 2: every vertex lies in two or three triangles

The graph \(G[A]\) has maximum degree at most 1, hence is a matching. Write

Because \(G\) is 7-regular, the number of edges from \(A\) to \(B\) is

No \(B\)-vertex is counted twice, while \(|B|=38\), so

As \(G[A]\) is a matching on seven vertices, \(t_v\le3\). Thus

Each edge of \(G[A]\) is exactly one triangle through \(v\), proving the

claim. [a]

Exhaustive normalization

Relabel \(v=0\) and \(A=\{1,\ldots,7\}\). Any matching of a fixed size on

seven labeled-afterward vertices is isomorphic to the canonical matching

below. The disjoint \(A\)-to-\(B\) neighborhoods can then be relabeled as

consecutive groups. This loses no graphs. [a]

| case | fixed edges inside \(A\) | sizes of the seven \(B\)-groups | \(B\)-vertices in no group |

|---|---|---|---|

| \(t_0=2\) | \(12,34\) | \(5,5,5,5,6,6,6\) | 0 |

| \(t_0=3\) | \(12,34,56\) | \(5,5,5,5,5,5,6\) | 2 |

The exact labels used by the checker are:

• \(t_0=2\): groups

\(8\!:\!12,13\!:\!17,18\!:\!22,23\!:\!27,28\!:\!33,34\!:\!39,40\!:\!45\);

• \(t_0=3\): groups

\(8\!:\!12,13\!:\!17,18\!:\!22,23\!:\!27,28\!:\!32,33\!:\!37,38\!:\!43\),

with vertices 44 and 45 adjacent to no vertex of \(A\).

Here each range is inclusive.

SAT encoding and checked certificate

For every unordered pair \(0\le u

\(x_{uv}\), giving \(\binom{46}{2}=1035\) primary variables.

1. At each vertex, a sequential-counter cardinality encoding imposes degree

exactly 7.

2. For every four-set \(a

orders are forbidden:

cnf.append([-x(a,b), -x(b,c), -x(c,d), -x(a,d)])
cnf.append([-x(a,b), -x(b,d), -x(c,d), -x(a,c)])
cnf.append([-x(a,c), -x(b,c), -x(b,d), -x(a,d)])

3. Unit clauses impose one of the two exhaustive normal forms above.

There are

\(C_4\)-clauses. With the sequential-counter auxiliaries and normalization,

both cases have exactly 25,507 variables and 538,831 clauses. The complete

executable encoding, including all unit clauses, is in the companion Python

file. The graph-to-CNF reduction and the three cycle clauses are [a]; the

exact-degree clauses are [b], modulo PySAT's standard

CardEnc.equals(..., EncType.seqcounter) cardinality encoder; the generated

counts and solver results are [d].

\(t_0=2\): UNSAT, proof checked

PySAT 1.9.dev7 with cadical195 returned UNSAT in 0.85 seconds without proof

logging and 1.66 seconds while regenerating the proof. The generated files

were:

| artifact | bytes | SHA-256 |

|---|---:|---|

| CNF | 11,428,175 | 608ed166fdf4a40cb409a478b4626a78cb831dd8c24f9c71332b2995ad7fb3b5 |

| DRAT, 360,378 lines | 8,463,760 | 80accdd4ad17a582b9cb0509503d24502cab405122b46ee72f55547129ecd954 |

The workspace drat-trim binary has SHA-256

f8d971dc5956a73fa37e655a44ba8f6d128976acfedff7129f2ed251b234af1a;

it returned s VERIFIED. The companion script regenerates both files,

asserts their hashes, invokes the independent checker, and requires the word

VERIFIED. [d]

Because any vertex with \(t_v=2\) could be relabeled as vertex 0, this

certificate excludes every graph having even one such vertex. Therefore

every surviving graph must satisfy

[a+d]

\(t_0=3\): unresolved

The identical base CNF with the second normalization did not terminate under

a 150-second cadical195 cap or a separate 130-second kissat404 cap. No

result is inferred from either timeout. [d]

Exact structure of the remaining case

Assume (4).

1. Every vertex lies in exactly three triangles. Two distinct triangles

cannot share an edge, since their two third vertices and the shared edge's

endpoints would contain a \(C_4\). [a]

2. Counting vertex--triangle incidences gives

\[ \#\{\text{triangles}\}=\frac{46\cdot3}{3}=46. \]

These edge-disjoint triangles use \(46\cdot3=138\) edges. A 7-regular

graph on 46 vertices has \(46\cdot7/2=161\) edges, leaving 23. At each

vertex the three triangles use six incident edges, so the remaining edges

form a perfect matching \(M\). [a]

3. Regard the 46 graph triangles as 3-element blocks on the 46 vertices.

Every point lies in three blocks and any pair is in at most one block.

Thus they form a linear symmetric \(46_3\) configuration. Its bipartite

Levi graph is cubic on 92 vertices and has girth at least 10:

• a Levi 4-cycle repeats a point-pair in two blocks;
• a Levi 6-cycle creates a graph triangle whose three edges already belong

to other blocks, contradicting edge-disjointness of graph triangles;

• a Levi 8-cycle creates a graph \(C_4\).

[a]

4. Let \(L\) be the 6-regular graph consisting of all block-triangle edges.

Every matched pair in \(M\) has \(L\)-distance at least 4: distances 1 and

2 would make the edge a triangle edge (distance 2 also directly forces a

\(C_4\) using its two incident blocks), while a distance-3 path plus the

matching edge is a \(C_4\). In addition, the entire union \(L\cup M\) must

remain \(C_4\)-free. [a]

Conversely, constructing such a \(46_3\) configuration and perfect matching

with \(L\cup M\) 7-regular and \(C_4\)-free gives the missing 46-vertex

Ramsey witness; the SAT encoding is an exact direct search for the same

object. [a]

Therefore the residual decision has an unambiguous consequence:

• a SAT model proves \(R(C_4,K_{1,39})=47\);
• an independently checked UNSAT certificate for the \(t_0=3\) case proves

\(R(C_4,K_{1,39})=46\).

This is the precise finite computation still needed.

Why this does not settle the Erdős question

Even a determination of \(R(C_4,K_{1,39})\) is one isolated value. The page's

question requires infinitely many \(n\), for every fixed \(c>0\), so no finite

table can close it. [a]

The existing standard mechanisms point in opposite but insufficient

directions:

• projective-plane/polarity witnesses, paired with known upper-bound

arguments, explain many exact values with offset 0 or 1 from

\(n+\lceil\sqrt n\rceil\), but do not furnish an infinite family satisfying

the required strict upper inequality;

• the prime-gap construction gives the page's asymptotic lower bound, but its

present error term is unbounded and therefore does not prove

\(R(C_4,S_n)\ge n+\sqrt n-O(1)\).

Thus a uniform solution still needs one of two genuinely new lemmas:

1. positive direction: an infinite construction/upper-bound mechanism

forcing \(R(C_4,S_n)\le n+\sqrt n-c\) for arbitrarily prescribed fixed

\(c\); or

2. negative direction: a uniform lower bound strong enough to exclude

that, for example \(R(C_4,S_n)\ge n+\sqrt n-O(1)\) with the constant

controlled sharply enough.

Neither the local \(n=39\) classification nor the checked literature supplies

such a lemma. This is the theoretical wall. [c]

For the finite residual search, a sensible next experiment is

triangle-aware cube-and-conquer on the \(46_3\) incidence structure rather

than the raw edge CNF. An illustrative budget of 512 cubes at five minutes

each is \(42.7\) core-hours, roughly \$2--\$5 at \$0.05--\$0.10 per core-hour;

4096 such cubes is \(341.3\) core-hours, roughly \$17--\$34. These are budget

calculations, not runtime predictions. A full UNSAT run may also need

multi-gigabyte proof storage. I did not launch it here.

Reproduction

The standalone verifier is

runs/erdos552_wave5z_verify.py, SHA-256

9fbdf2f6f1880298ed6cf092c183a4023cfdee8ceef2facdaba6b224dcc29152.

Its default mode uses only the Python standard library and is network-free:

python3 runs/erdos552_wave5z_verify.py

It recomputes the elementary reduction arithmetic, reconstructs the explicit

45-vertex graph, checks the graph data, and performs two independent exhaustive

\(C_4\) checks.

Optional SAT mode requires python-sat:

python3 runs/erdos552_wave5z_verify.py --sat-case 2

To regenerate and independently check the DRAT proof:

proof_tmp=$(mktemp -d /tmp/erdos552-recheck.XXXXXX)
python3 runs/erdos552_wave5z_verify.py \
  --sat-case 2 \
  --proof-dir "$proof_tmp" \
  --drat-trim sitting_ducks_tierB/hadamard_668/.external-audit.va1jUb/repo/lp333/proof_phase2/tools/drat-trim/drat-trim

The final tested output included:

feasible degrees in the 46-vertex reduction: [7]
feasible t_v values before SAT: [2, 3]
all-t_v=3 counts: 46 triangles, 138 triangle edges, 23 residual edges
base degree histogram: {6: 37, 7: 6}
degree histogram: {6: 27, 7: 18}
maximum pair-codegree: 1
explicit C4 witnesses: 0
maximum complement degree: 38
normalized SAT case t=2: 25507 variables, 538831 clauses
SAT result: UNSAT
DRAT-trim: VERIFIED

python3 -m py_compile passed. git diff --check reports no whitespace error

in either deliverable. Unrelated pre-existing worktree changes were not

modified.

PARTIAL: Reduced the unresolved value \(R(C_4,S_{39})\in\{46,47\}\) to the all-\(t_v=3\) case, DRAT-verified the \(t_v=2\) case impossible, and isolated the remaining \(46_3\)-configuration search; the uniform Erdős question remains open.