{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R852",
  "content_hash": null,
  "slug": "zs4fz4-artifact-construction-check",
  "type": "artifact",
  "title": "Exhaustive certificate for the 32-point construction",
  "summary": "The script checks all 35,960 four-subsets and records the equality structure behind the upper bound.",
  "relevance": "This supplies a computation, dataset, or executable check used to assess the target problem.",
  "relevance_source": "derived",
  "body": "The encoded set is\n\\[\n\\{193,236,64,161,245,126,35,107,112,40,215,63,111,237,47,50,174,44,206,10,188,252,218,49,209,194,19,176,83,133,22,189\\}.\n\\]\nThe verifier decodes each integer in base 4, checks every four-element subset, and asserts that none sums to zero coordinatewise modulo 4. It also checks that every parity fiber has size two and that the 16 within-fiber pair sums are exactly \\(\\{0,2\\}^4\\).",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the displayed encoded 32-point subset of (Z/4Z)^4",
    "bounds": {
      "cardinality": {
        "min": 32,
        "max": 32
      },
      "four_subsets_checked": {
        "min": 35960,
        "max": 35960
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3.9 or later",
    "citation": {
      "url": "https://arxiv.org/abs/1607.05718",
      "locator": "Inline CPython standard-library verifier executed on 2026-07-24"
    },
    "outputs": "size=32 four_subsets=35960 forbidden=0\nparity_occupancies=2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2\nwithin_fiber_sums=0,2,8,10,32,34,40,42,128,130,136,138,160,162,168,170\n",
    "inline_source": [
      "from itertools import combinations, product",
      "",
      "A = (193, 236, 64, 161, 245, 126, 35, 107, 112, 40, 215, 63, 111, 237, 47, 50, 174, 44, 206, 10, 188, 252, 218, 49, 209, 194, 19, 176, 83, 133, 22, 189)",
      "",
      "def digits(x):",
      "    return tuple((x >> (2*i)) & 3 for i in range(4))",
      "",
      "def encode(v):",
      "    return sum(x << (2*i) for i, x in enumerate(v))",
      "",
      "def add4(*xs):",
      "    decoded = [digits(x) for x in xs]",
      "    return encode(tuple(sum(v[i] for v in decoded) % 4 for i in range(4)))",
      "",
      "def parity(x):",
      "    v = digits(x)",
      "    return sum((v[i] & 1) << i for i in range(4))",
      "",
      "assert len(A) == len(set(A)) == 32",
      "four_sets = list(combinations(A, 4))",
      "bad = [q for q in four_sets if add4(*q) == 0]",
      "assert len(four_sets) == 35960 and bad == []",
      "",
      "occupancies = [sum(parity(x) == p for x in A) for p in range(16)]",
      "assert occupancies == [2] * 16",
      "within_sums = {add4(x, y) for x, y in combinations(A, 2) if parity(x) == parity(y)}",
      "two_torsion = {encode(v) for v in product((0, 2), repeat=4)}",
      "assert within_sums == two_torsion",
      "print('size=32 four_subsets=35960 forbidden=0')",
      "print('parity_occupancies=' + ','.join(map(str, occupancies)))",
      "print('within_fiber_sums=' + ','.join(map(str, sorted(within_sums))))"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1607.05718",
    "locator": "Inline CPython standard-library verifier executed on 2026-07-24"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R854",
      "title": "The maximum size is 32",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R855",
      "title": "Every extremal set has two points in each parity fiber",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "zero-sum-four-free-z4-four",
      "title": "zero sum four free z4 four",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}