{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R643",
  "content_hash": null,
  "slug": "r55-artifact-first-public-42-graph-check",
  "type": "artifact",
  "title": "Exhaustive certificate for the first public 42-vertex graph",
  "summary": "The decoder reproduces both graph digests and checks every five-set in the graph and complement.",
  "relevance": "For A 43-vertex graph for the diagonal Ramsey problem R(5,5), record r55-artifact-first-public-42-graph-check (“Exhaustive certificate for the first public 42-vertex graph”) supplies evidence or a replay used to check the packet. The record states: The decoder reproduces both graph digests and checks every five-set in the graph and complement.",
  "relevance_source": "recorded",
  "body": "The graph6 short header is the byte `i`. Since \\(\\operatorname{ord}(i)-63=42\\), the record has 42 vertices. Its 144 payload characters supply 864 bits. The first \\(\\binom{42}{2}=861\\) bits encode the unordered pairs in graph6 order, and the final three bits are zero padding.\n\nThe graph6-line SHA-256 includes the terminating line feed. For a second digest, the decoder visits edges in graph6 order and serializes each edge \\((u,v)\\) as the two bytes `u,v`. The 425 edges therefore give 850 digest bytes.\n\nThe executable counts the number of induced edges on each five-set. Ten edges would be a \\(K_5\\) in the graph, while zero edges would be a \\(K_5\\) in the complement. Both counts are zero. The complete histogram also fixes every intermediate count and makes the check reproducible without a graph library.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all five-element subsets of the first 42-vertex graph in r55_42some.g6",
    "bounds": {
      "vertex_count": {
        "min": 42,
        "max": 42
      },
      "edge_count": {
        "min": 425,
        "max": 425
      },
      "subset_size": {
        "min": 5,
        "max": 5
      },
      "subsets_checked": {
        "min": 850668,
        "max": 850668
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python3_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3.9 or later, standard library only",
    "citation": {
      "url": "https://users.cecs.anu.edu.au/~bdm/data/r55_42some.g6",
      "locator": "First line of Brendan McKay's r55_42some.g6 collection, retrieved and verified on 2026-07-24"
    },
    "inline_source": [
      "import hashlib",
      "import itertools",
      "import math",
      "",
      "GRAPH6 = r\"i?Udjp^j}?W@`bIRhHgk\\SY~ECeQS\\CniuKP]RQLdsX~F?b|L?h_SvygSNziSVdZ`P|CxamFHKax[PhPyVEYxAqkY\\_xCfYxNscNtb]k_uFsLruaJwr`nPMMc]\\qGhwyhfLjTELQ}T]h@qtuW\"",
      "raw = GRAPH6.encode(\"ascii\")",
      "assert raw[0] - 63 == 42",
      "n = raw[0] - 63",
      "bits = []",
      "for character in raw[1:]:",
      "    value = character - 63",
      "    bits.extend((value >> shift) & 1 for shift in range(5, -1, -1))",
      "needed = n * (n - 1) // 2",
      "assert len(bits) == 864 and needed == 861 and bits[needed:] == [0, 0, 0]",
      "adjacency = [0] * n",
      "edges = []",
      "offset = 0",
      "for v in range(1, n):",
      "    for u in range(v):",
      "        if bits[offset]:",
      "            adjacency[u] |= 1 << v",
      "            adjacency[v] |= 1 << u",
      "            edges.append((u, v))",
      "        offset += 1",
      "degrees = [bin(mask).count(\"1\") for mask in adjacency]",
      "histogram = [0] * 11",
      "for vertices in itertools.combinations(range(n), 5):",
      "    edge_count = sum(",
      "        (adjacency[u] >> v) & 1",
      "        for index, u in enumerate(vertices)",
      "        for v in vertices[index + 1:]",
      "    )",
      "    histogram[edge_count] += 1",
      "line_sha = hashlib.sha256(raw + b\"\\n\").hexdigest()",
      "edge_bytes = bytes(label for edge in edges for label in edge)",
      "edge_sha = hashlib.sha256(edge_bytes).hexdigest()",
      "expected_histogram = [0, 6078, 31577, 99576, 192531, 225712,",
      "                      173847, 87463, 27923, 5961, 0]",
      "assert len(edges) == 425",
      "assert min(degrees) == 19 and max(degrees) == 22 and sum(degrees) == 850",
      "assert histogram == expected_histogram",
      "assert sum(histogram) == math.comb(42, 5) == 850668",
      "assert line_sha == \"ab0b10364ac62ab07f662c0ed4e8b47a44956f63a78356b64ae64ccb6520ecb0\"",
      "assert edge_sha == \"81d4e6e7cf74903f30c847c84fe154f3493e449eb70c4e84ca28db5cb612e6bc\"",
      "print(f\"graph6_vertices {n} payload_chars {len(raw)-1} padding_bits {len(bits)-needed}\")",
      "print(f\"graph6_line_sha256 {line_sha}\")",
      "print(f\"edges {len(edges)} degree_range {min(degrees)} {max(degrees)} degree_sum {sum(degrees)}\")",
      "print(f\"edge_pair_bytes_sha256 {edge_sha}\")",
      "print(\"five_subsets\", sum(histogram), \"histogram\", *histogram)",
      "print(f\"k5_graph {histogram[10]} k5_complement {histogram[0]} lower_bound 43\")"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://users.cecs.anu.edu.au/~bdm/data/r55_42some.g6",
    "locator": "First line of Brendan McKay's r55_42some.g6 collection, retrieved and verified on 2026-07-24"
  },
  "relations": [
    {
      "slug": "R645",
      "title": "The cited public graph certifies R(5,5) at least 43",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "ramsey-55-43-graph",
      "title": "ramsey 55 43 graph",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}