{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R582",
  "content_hash": null,
  "slug": "pirw600-artifact-subset-and-incumbent-certificate",
  "type": "artifact",
  "title": "Exact lower-bound and incumbent replay certificate",
  "summary": "A four-second standard-library program certifies rank 426, the interval 8 to 186, and hashes the complete constraint data.",
  "relevance": "For Sparsest degree-600 recurrence for a prime-indicator prefix, record pirw600-artifact-subset-and-incumbent-certificate (“Exact lower-bound and incumbent replay certificate”) supplies evidence or a replay used to check the packet. The record states: A four-second standard-library program certifies rank 426, the interval 8 to 186, and hashes the complete constraint data.",
  "relevance_source": "recorded",
  "body": "The verifier sieves primality through 1025, builds the 424 by 601 binary recurrence matrix, and appends the two endpoint equations. Exact bitwise Gaussian elimination returns rank 426.\n\nFor the lower bound, the program stores all singleton and pair xors among the 599 internal columns. It exhausts 35,641,099 triples to finish the size-five test. The 179,101 pair xors are all distinct. No target representation occurs with zero through five internal columns.\n\nThe same run decodes the incumbent, checks its endpoints and weight, and substitutes it in all 424 equations. The recurrence row matrix, complete column list, and sorted pair-xor table have separate SHA-256 digests. The canonical report has SHA-256 digest `82e26220eae169ac7f57db344802bc55f25db5e9a2d728e06725e0dc586cd74b`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the stated degree-600 binary recurrence system, every internal tap subset of size at most five, and the supplied weight-186 vector",
    "bounds": {
      "degree": {
        "min": 600,
        "max": 600
      },
      "internal_columns": {
        "min": 599,
        "max": 599
      },
      "maximum_exhaustive_internal_subset_size": {
        "min": 5,
        "max": 5
      },
      "triples_checked": {
        "min": 35641099,
        "max": 35641099
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exhaustive_verifier",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://doi.org/10.1109/TIT.1969.1054260",
      "locator": "Inline CPython standard-library exhaustive computation executed on 2026-07-25"
    },
    "runtime_seconds": 4.1,
    "inline_source": [
      "from hashlib import sha256",
      "from itertools import combinations",
      "from json import dumps",
      "from math import comb",
      "",
      "N = 1024",
      "DEGREE = 600",
      "EQUATIONS = 424",
      "INCUMBENT_HEX = '104020000042401000000000000100000010004020001702093a81120945a122179a133c52f6f5d7860361026a5b18b00f8b704122171b46d22ccedce3191b108a19415c43e921a850ae209'",
      "",
      "is_prime = [True] * 1026",
      "is_prime[0] = is_prime[1] = False",
      "for p in range(2, 33):",
      "    if is_prime[p]:",
      "        for multiple in range(p * p, 1026, p):",
      "            is_prime[multiple] = False",
      "sequence = [is_prime[i + 2] for i in range(N)]",
      "",
      "columns = []",
      "for j in range(DEGREE + 1):",
      "    column = 0",
      "    for i in range(EQUATIONS):",
      "        if sequence[i + j]:",
      "            column |= 1 << i",
      "    columns.append(column)",
      "target = columns[0] ^ columns[DEGREE]",
      "internal = columns[1:DEGREE]",
      "",
      "rows = []",
      "for i in range(EQUATIONS):",
      "    row = 0",
      "    for j in range(DEGREE + 1):",
      "        if sequence[i + j]:",
      "            row |= 1 << j",
      "    rows.append(row)",
      "rows.extend((1, 1 << DEGREE))",
      "original_rows = tuple(rows)",
      "rank = 0",
      "for column_index in range(DEGREE + 1):",
      "    pivot = next((r for r in range(rank, len(rows)) if rows[r] >> column_index & 1), None)",
      "    if pivot is None:",
      "        continue",
      "    rows[rank], rows[pivot] = rows[pivot], rows[rank]",
      "    for r in range(len(rows)):",
      "        if r != rank and rows[r] >> column_index & 1:",
      "            rows[r] ^= rows[rank]",
      "    rank += 1",
      "",
      "incumbent = int(INCUMBENT_HEX, 16)",
      "incumbent_weight = bin(incumbent).count('1')",
      "violations = sum(bin(incumbent & row).count('1') & 1 for row in original_rows[:EQUATIONS])",
      "endpoint_ok = bool(incumbent & 1) and bool(incumbent >> DEGREE & 1)",
      "",
      "single_xors = set(internal)",
      "pair_xors = {a ^ b for a, b in combinations(internal, 2)}",
      "hits = {",
      "    0: target == 0,",
      "    1: target in single_xors,",
      "    2: target in pair_xors,",
      "    3: any((target ^ a) in pair_xors for a in internal),",
      "    4: any((target ^ pair) in pair_xors for pair in pair_xors),",
      "}",
      "triple_checks = 0",
      "hit_five = False",
      "for i in range(len(internal) - 2):",
      "    a = internal[i]",
      "    for j in range(i + 1, len(internal) - 1):",
      "        ab = a ^ internal[j]",
      "        for k in range(j + 1, len(internal)):",
      "            triple_checks += 1",
      "            if (target ^ ab ^ internal[k]) in pair_xors:",
      "                hit_five = True",
      "                break",
      "        if hit_five:",
      "            break",
      "    if hit_five:",
      "        break",
      "hits[5] = hit_five",
      "",
      "assert rank == 426",
      "assert incumbent.bit_length() == 601 and incumbent_weight == 186",
      "assert endpoint_ok and violations == 0",
      "assert len(internal) == 599",
      "assert len(single_xors) == 599",
      "assert len(pair_xors) == comb(599, 2)",
      "assert triple_checks == comb(599, 3)",
      "assert hits == {0:False, 1:False, 2:False, 3:False, 4:False, 5:False}",
      "",
      "matrix_sha = sha256(b''.join(row.to_bytes(76, 'little') for row in original_rows)).hexdigest()",
      "columns_sha = sha256(b''.join(column.to_bytes(53, 'little') for column in columns)).hexdigest()",
      "pairs_sha = sha256(b''.join(value.to_bytes(53, 'little') for value in sorted(pair_xors))).hexdigest()",
      "report = {",
      "    'affine_dimension': DEGREE + 1 - rank,",
      "    'columns_sha256_le': columns_sha,",
      "    'constraint_rank': rank,",
      "    'endpoint_ok': endpoint_ok,",
      "    'incumbent_hex': INCUMBENT_HEX,",
      "    'incumbent_weight': incumbent_weight,",
      "    'matrix_sha256_le': matrix_sha,",
      "    'pair_xor_count': len(pair_xors),",
      "    'pair_xors_sha256_le': pairs_sha,",
      "    'recurrence_violations': violations,",
      "    'subsets_excluded_by_internal_size': list(range(6)),",
      "    'triple_checks': triple_checks,",
      "    'weight_interval': [8, 186],",
      "}",
      "payload = dumps(report, sort_keys=True, separators=(',', ':'))",
      "digest = sha256(payload.encode()).hexdigest()",
      "print(payload)",
      "print('sha256=' + digest)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1109/TIT.1969.1054260",
    "locator": "Inline CPython standard-library exhaustive computation executed on 2026-07-25"
  },
  "relations": [
    {
      "slug": "R584",
      "title": "The minimum tap weight lies between 8 and 186",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "prime-indicator-recurrence-weight-600",
      "title": "prime indicator recurrence weight 600",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}