{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R189",
  "content_hash": null,
  "slug": "db127-artifact-construction-verifier",
  "type": "artifact",
  "title": "Exact verifier for the 13-element difference basis",
  "summary": "Standard-library Python checks distinctness, full coverage, multiplicities, and fixed digests.",
  "relevance": "For Difference size of Z_127, record db127-artifact-construction-verifier (“Exact verifier for the 13-element difference basis”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python checks distinctness, full coverage, multiplicities, and fixed digests.",
  "relevance_source": "recorded",
  "body": "The program computes every residue \\((a-b)\\bmod127\\) for the displayed set. It verifies 127 covered residues and checks all 126 nonzero multiplicities. Among the nonzero residues, 100 occur once, 24 occur twice, and two occur four times. These multiplicities sum to the expected \\(13\\cdot12=156\\) ordered nonzero differences.\n\nThe canonical JSON report has SHA-256 digest `6d0696cd6efd39a3229fda9f0fdd62322c403484e2caccc722b2ee845dda6609`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all ordered differences of the displayed 13-element subset of Z/127Z",
    "bounds": {
      "modulus": {
        "min": 127,
        "max": 127
      },
      "basis_size": {
        "min": 13,
        "max": 13
      },
      "ordered_pairs": {
        "min": 169,
        "max": 169
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "Python 3 standard library",
    "citation": {
      "url": "https://cs.uwaterloo.ca/journals/JIS/VOL7/Haanpaa/haanpaa.html",
      "locator": "Exact Python 3 standard-library replay executed by TheoremDB entry research on 2026-07-25"
    },
    "inline_source": [
      "from collections import Counter",
      "from hashlib import sha256",
      "from json import dumps",
      "",
      "MODULUS = 127",
      "basis = [0, 1, 5, 11, 19, 38, 61, 78, 80, 81, 93, 102, 109]",
      "assert len(basis) == len(set(basis)) == 13",
      "assert all(0 <= value < MODULUS for value in basis)",
      "",
      "all_differences = {(a - b) % MODULUS for a in basis for b in basis}",
      "multiplicities = Counter(",
      "    (a - b) % MODULUS for a in basis for b in basis if a != b",
      ")",
      "histogram = sorted(Counter(multiplicities.values()).items())",
      "assert all_differences == set(range(MODULUS))",
      "assert len(multiplicities) == 126",
      "assert sum(multiplicities.values()) == 156",
      "assert histogram == [(1, 100), (2, 24), (4, 2)]",
      "",
      "basis_sha = sha256(('\\n'.join(map(str, basis)) + '\\n').encode()).hexdigest()",
      "assert basis_sha == '6f03be727558d4eace3ec15bde81a7f99a19cf44e4e46193159e1f6f7489937e'",
      "report = {",
      "    'basis': basis,",
      "    'basis_sha256': basis_sha,",
      "    'basis_size': len(basis),",
      "    'covered_residues': len(all_differences),",
      "    'maximum_nonzero_multiplicity': max(multiplicities.values()),",
      "    'minimum_nonzero_multiplicity': min(multiplicities.values()),",
      "    'multiplicity_histogram': histogram,",
      "    'ordered_nonzero_differences': sum(multiplicities.values()),",
      "}",
      "payload = dumps(report, sort_keys=True, separators=(',', ':'))",
      "assert sha256(payload.encode()).hexdigest() == '6d0696cd6efd39a3229fda9f0fdd62322c403484e2caccc722b2ee845dda6609'",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://cs.uwaterloo.ca/journals/JIS/VOL7/Haanpaa/haanpaa.html",
    "locator": "Exact Python 3 standard-library replay executed by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R192",
      "title": "The exact difference size of Z/127Z is 13",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "difference-basis-z127",
      "title": "difference basis z127",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}