{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R832",
  "content_hash": null,
  "slug": "wfci127-artifact-exhaustive-search-template",
  "type": "artifact",
  "title": "Exact exhaustive-search template",
  "summary": "A standard-library program enumerates every support and computes inverses by binary polynomial Euclid, with a streaming result checksum.",
  "relevance": "For Densest inverse of a weight-five binary cyclic polynomial, record wfci127-artifact-exhaustive-search-template (“Exact exhaustive-search template”) supplies evidence or a replay used to check the packet. The record states: A standard-library program enumerates every support and computes inverses by binary polynomial Euclid, with a streaming result checksum.",
  "relevance_source": "recorded",
  "body": "The program below is a replayable exhaustive algorithm. It enumerates the 10,009,125 four-subsets of \\(\\{1,\\ldots,126\\}\\). For each support it applies polynomial extended Euclid against \\(x^{127}+1\\), reduces a unit's Bezout coefficient cyclically, and records its inverse weight. A SHA-256 stream covers one canonical line per support, including nonunits.\n\nThis full sweep was not executed for this fixture. Its output and checksum are therefore deliberately unspecified. The completed certificate is the one-support verifier above, and the exact extremum remains between 85 and 101.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the algorithmic search plan for all normalized weight-five supports at length 127",
    "bounds": {
      "length": {
        "min": 127,
        "max": 127
      },
      "planned_supports": {
        "min": 10009125,
        "max": 10009125
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "save code as exhaustive.py and run python3 exhaustive.py",
    "runtime": "CPython 3, standard library only; the 10,009,125-support run may be lengthy",
    "citation": {
      "url": "https://eprint.iacr.org/2012/409",
      "locator": "Exact unexecuted CPython search template prepared by TheoremDB entry research on 2026-07-25"
    },
    "inline_source": "from collections import Counter\nfrom hashlib import sha256\nfrom itertools import combinations\nfrom math import comb\n\nN = 127\nMODULUS = (1 << N) | 1\nMASK = (1 << N) - 1\n\ndef degree(value):\n    return value.bit_length() - 1\n\ndef multiply_raw(left, right):\n    product = 0\n    while left:\n        low = left & -left\n        product ^= right << (low.bit_length() - 1)\n        left ^= low\n    return product\n\ndef divide(left, right):\n    quotient = 0\n    right_degree = degree(right)\n    while left and degree(left) >= right_degree:\n        shift = degree(left) - right_degree\n        quotient ^= 1 << shift\n        left ^= right << shift\n    return quotient, left\n\ndef reduce_cyclic(value):\n    while degree(value) >= N:\n        value ^= MODULUS << (degree(value) - N)\n    return value\n\ndef inverse(value):\n    r0, r1 = MODULUS, value\n    s0, s1 = 0, 1\n    while r1:\n        quotient, remainder = divide(r0, r1)\n        r0, r1 = r1, remainder\n        s0, s1 = s1, s0 ^ multiply_raw(quotient, s1)\n    if r0 != 1:\n        return None\n    result = reduce_cyclic(s0)\n    assert reduce_cyclic(multiply_raw(value, result)) == 1\n    return result\n\nrecords = sha256()\nhistogram = Counter()\nmaximum = -1\nmaximizers = []\nunits = 0\nchecked = 0\nfor exponents in combinations(range(1, N), 4):\n    value = 1\n    for exponent in exponents:\n        value ^= 1 << exponent\n    result = inverse(value)\n    checked += 1\n    if result is None:\n        records.update((','.join(map(str, exponents)) + ':nonunit\\n').encode())\n        continue\n    units += 1\n    result_weight = bin(result).count('1')\n    histogram[result_weight] += 1\n    records.update((','.join(map(str, exponents)) + f':unit:{result_weight}\\n').encode())\n    if result_weight > maximum:\n        maximum = result_weight\n        maximizers = [(exponents, result)]\n    elif result_weight == maximum:\n        maximizers.append((exponents, result))\nassert checked == comb(126, 4) == 10009125\nprint(f'checked={checked} units={units} maximum={maximum} maximizers={len(maximizers)}')\nprint('histogram=' + ','.join(f'{weight}:{histogram[weight]}' for weight in sorted(histogram)))\nprint('records_sha256=' + records.hexdigest())\nfor support, result in maximizers:\n    print('maximizer=' + ','.join(map(str, (0,) + support)) + f' inverse=0x{result:x}')\n",
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://eprint.iacr.org/2012/409",
    "locator": "Exact unexecuted CPython search template prepared by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R833",
      "title": "The maximum inverse weight lies between 85 and 101",
      "object_type": "claim",
      "relation": "informs",
      "direction": "outgoing"
    },
    {
      "slug": "weight-five-cyclic-inverse-127",
      "title": "weight five cyclic inverse 127",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}