{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R831",
  "content_hash": null,
  "slug": "wfci127-artifact-exact-witness-verifier",
  "type": "artifact",
  "title": "Exact 127-bit cyclic-product verifier",
  "summary": "Standard-library Python checks both product identities, both weights, and the complement upper-bound arithmetic.",
  "relevance": "For Densest inverse of a weight-five binary cyclic polynomial, record wfci127-artifact-exact-witness-verifier (“Exact 127-bit cyclic-product verifier”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python checks both product identities, both weights, and the complement upper-bound arithmetic.",
  "relevance_source": "recorded",
  "body": "The program represents a residue by a 127-bit integer and multiplication by \\(x^k\\) as a cyclic rotation of its coefficient word. It verifies the displayed inverse directly. Setting \\(h=J+g\\), it also checks \\(fh=J+1\\), \\(\\operatorname{wt}(g)=85\\), and \\(\\operatorname{wt}(h)=42\\).\n\nThe eight-line standard output has SHA-256 digest `19774a855b737562d11bd1d30f217e6f0edee0756b2d4668c37a001a0d57161c`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the displayed support, inverse, complement identity, and certified interval at length 127",
    "bounds": {
      "length": {
        "min": 127,
        "max": 127
      },
      "checked_supports": {
        "min": 1,
        "max": 1
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "save code as check.py and run python3 check.py",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://eprint.iacr.org/2012/409",
      "locator": "Independent CPython exact-arithmetic replay executed by TheoremDB entry research on 2026-07-25"
    },
    "inline_source": "from hashlib import sha256\n\nN = 127\nMASK = (1 << N) - 1\nSUPPORT = (0, 45, 49, 53, 94)\nF = sum(1 << i for i in SUPPORT)\nG = int('3bf17593bf175d3fb175d3fb377f3fb3', 16)\n\ndef weight(value):\n    return bin(value).count('1')\n\ndef rotate(value, shift):\n    shift %= N\n    if shift == 0:\n        return value\n    return ((value << shift) & MASK) | (value >> (N - shift))\n\ndef multiply(left, right):\n    product = 0\n    while left:\n        low = left & -left\n        product ^= rotate(right, low.bit_length() - 1)\n        left ^= low\n    return product\n\nJ = MASK\nH = J ^ G\nassert weight(F) == 5\nassert weight(G) == 85\nassert weight(H) == 42\nassert multiply(F, G) == 1\nassert multiply(F, J) == J\nassert multiply(F, H) == J ^ 1\nassert 126 <= 5 * 26\nassert 127 - 26 == 101\noutput = (f'support={SUPPORT}\\n'\n          f'f=0x{F:x}\\n'\n          f'inverse=0x{G:x}\\n'\n          f'inverse_weight={weight(G)}\\n'\n          f'complement_weight={weight(H)}\\n'\n          f'cyclic_product=0x{multiply(F, G):x}\\n'\n          f'complement_product=0x{multiply(F, H):x}\\n'\n          'certified_interval=85..101\\n')\nassert sha256(output.encode()).hexdigest() == '19774a855b737562d11bd1d30f217e6f0edee0756b2d4668c37a001a0d57161c'\nprint(output, end='')\n",
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://eprint.iacr.org/2012/409",
    "locator": "Independent CPython exact-arithmetic replay executed by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R836",
      "title": "A weight-five unit has inverse weight 85",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "R833",
      "title": "The maximum inverse weight lies between 85 and 101",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "weight-five-cyclic-inverse-127",
      "title": "weight five cyclic inverse 127",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}