{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R856",
  "content_hash": null,
  "slug": "zsf7s-artifact-thirteen-point-verifier",
  "type": "artifact",
  "title": "Exhaustive verifier for the 13-point construction",
  "summary": "A dependency-free Python program checks the sphere, every nonempty subset, the full nonzero sum image, and a canonical digest.",
  "relevance": "For Zero-sum-free subsets of the unit sphere over F_7, record zsf7s-artifact-thirteen-point-verifier (“Exhaustive verifier for the 13-point construction”) supplies evidence or a replay used to check the packet. The record states: A dependency-free Python program checks the sphere, every nonempty subset, the full nonzero sum image, and a canonical digest.",
  "relevance_source": "recorded",
  "body": "The program enumerates all 343 vectors of \\(\\mathbb F_7^3\\) and confirms that exactly 42 satisfy the unit-sphere equation. It checks that the 13 displayed vectors are distinct sphere points. It then enumerates every nonempty subset by cardinality, reduces its coordinate sum modulo 7, and asserts that zero never occurs.\n\nThe union of the subset-sum images has size 342, equal to the number of nonzero ambient vectors. Across all subset cardinalities, a nonzero vector has between 1 and 52 representations. The numbers of distinct sums at cardinalities 1 through 13 are\n\\[\n13,63,138,199,230,251,251,230,199,138,63,13,1.\n\\]\nThe canonical summary has SHA-256 digest `4c8d575a1977615fcc5205ed8eb14b59f079740153789e32b799a60a4e6fb2a9`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all nonempty subsets of the displayed 13-point set, together with all vectors on the unit sphere in F_7^3",
    "bounds": {
      "sphere_vectors_checked": {
        "min": 343,
        "max": 343
      },
      "sphere_points_found": {
        "min": 42,
        "max": 42
      },
      "nonempty_subsets_checked": {
        "min": 8191,
        "max": 8191
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exhaustive_verifier",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "Python 3 standard library",
    "citation": {
      "url": "https://doi.org/10.1016/0022-314X(69)90021-3",
      "locator": "Inline Python 3 standard-library verifier executed on 2026-07-25"
    },
    "inline_source": [
      "from collections import Counter",
      "from itertools import combinations, product",
      "import hashlib",
      "",
      "P = 7",
      "A = (",
      "    (3, 5, 4), (2, 4, 4), (2, 5, 0), (4, 3, 5), (4, 5, 3),",
      "    (2, 0, 5), (4, 2, 4), (5, 0, 5), (5, 3, 4), (0, 0, 1),",
      "    (2, 3, 3), (0, 2, 5), (5, 5, 0),",
      ")",
      "EXPECTED_DIGEST = '4c8d575a1977615fcc5205ed8eb14b59f079740153789e32b799a60a4e6fb2a9'",
      "",
      "sphere = {v for v in product(range(P), repeat=3)",
      "          if sum(x*x for x in v) % P == 1}",
      "assert len(sphere) == 42",
      "assert len(A) == len(set(A)) == 13",
      "assert set(A) <= sphere",
      "",
      "counts = Counter()",
      "by_size = []",
      "zero = (0, 0, 0)",
      "for size in range(1, len(A) + 1):",
      "    image = Counter(",
      "        tuple(sum(v[j] for v in subset) % P for j in range(3))",
      "        for subset in combinations(A, size)",
      "    )",
      "    assert zero not in image",
      "    by_size.append(len(image))",
      "    counts.update(image)",
      "",
      "nonzero = set(product(range(P), repeat=3)) - {zero}",
      "assert set(counts) == nonzero",
      "assert sum(counts.values()) == 2**len(A) - 1 == 8191",
      "assert by_size == [13, 63, 138, 199, 230, 251, 251, 230, 199, 138, 63, 13, 1]",
      "assert min(counts.values()) == 1 and max(counts.values()) == 52",
      "summary = (",
      "    'sphere=42;size=13;nonempty_subsets=8191;zero_sums=0;'",
      "    'sum_image=342;sum_image_multiplicity_min=1;'",
      "    'sum_image_multiplicity_max=52;by_size=' + ','.join(map(str, by_size))",
      ")",
      "digest = hashlib.sha256(summary.encode()).hexdigest()",
      "assert digest == EXPECTED_DIGEST",
      "print(summary)",
      "print('sha256=' + digest)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/0022-314X(69)90021-3",
    "locator": "Inline Python 3 standard-library verifier executed on 2026-07-25"
  },
  "relations": [
    {
      "slug": "R858",
      "title": "The certified interval is 13 to 18",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R859",
      "title": "The 13-point witness is inclusion-maximal",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "zero-sum-free-f7-sphere",
      "title": "zero sum free f7 sphere",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}