{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R240",
  "content_hash": null,
  "slug": "etc72-artifact-enumerator-replay",
  "type": "artifact",
  "title": "Exact Gleason and 5-design parameter replay",
  "summary": "Standard-library Python expands the forced polynomial and checks all coefficients, symmetry, size, distance, and design divisibilities.",
  "relevance": "For An extremal Type II binary code of length 72, record etc72-artifact-enumerator-replay (“Exact Gleason and 5-design parameter replay”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python expands the forced polynomial and checks all coefficients, symmetry, size, distance, and design divisibilities.",
  "relevance_source": "recorded",
  "body": "The program represents a homogeneous polynomial by its exponent of \\(y\\), since every monomial has total degree 72. It expands the four Gleason-basis terms using exact integers and compares the result with the complete expected distribution.\n\nThe checks certify 13 nonzero coefficients, coefficient sum \\(2^{36}\\), complement symmetry \\(A_w=A_{72-w}\\), and minimum nonzero weight 16. For each nontrivial weight it also evaluates\n\\[\n\\lambda_w=A_w\\binom{w}{5}/\\binom{72}{5}\n\\]\nand verifies integrality. The canonical report has SHA-256 digest `5c244287d06ceec7acd8ef04a7827f61d4214b160a4e7668a3f01db3352c21ea`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the unique degree-72 Type II Gleason polynomial whose coefficients at weights 4, 8, and 12 vanish",
    "bounds": {
      "length": {
        "min": 72,
        "max": 72
      },
      "polynomial_terms": {
        "min": 13,
        "max": 13
      },
      "design_strength": {
        "min": 5,
        "max": 5
      }
    },
    "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": "CPython 3, standard library only",
    "citation": {
      "url": "https://doi.org/10.1109/TIT.1973.1054975",
      "locator": "Sloane 1973 supplies the distribution and minimum-weight design; exact replay written and executed by TheoremDB entry research on 2026-07-25"
    },
    "outputs": "{\"codewords\":68719476736,\"five_design_lambdas\":[[16,78],[20,20064],[24,1406405],[28,30888000],[32,238957796],[36,693996160],[40,780808743],[44,341316800],[48,56658030],[52,3363360],[56,68211]],\"gleason_coefficients\":[1,-126,3015,-4398],\"minimum_nonzero_weight\":16,\"weight_distribution\":[[0,1],[16,249849],[20,18106704],[24,462962955],[28,4397342400],[32,16602715899],[36,25756721120],[40,16602715899],[44,4397342400],[48,462962955],[52,18106704],[56,249849],[72,1]]}\nreport_sha256=5c244287d06ceec7acd8ef04a7827f61d4214b160a4e7668a3f01db3352c21ea\n",
    "inline_source": [
      "from hashlib import sha256",
      "from json import dumps",
      "from math import comb",
      "",
      "def multiply(left, right):",
      "    out = {}",
      "    for i, a in left.items():",
      "        for j, b in right.items():",
      "            out[i + j] = out.get(i + j, 0) + a * b",
      "    return out",
      "",
      "def power(poly, exponent):",
      "    out = {0: 1}",
      "    for _ in range(exponent):",
      "        out = multiply(out, poly)",
      "    return out",
      "",
      "def scaled_sum(terms):",
      "    out = {}",
      "    for scale, poly in terms:",
      "        for exponent, coefficient in poly.items():",
      "            out[exponent] = out.get(exponent, 0) + scale * coefficient",
      "    return {k: v for k, v in out.items() if v}",
      "",
      "A = {0: 1, 4: 14, 8: 1}",
      "B = {4: 1, 8: -4, 12: 6, 16: -4, 20: 1}",
      "W = scaled_sum([",
      "    (1, power(A, 9)),",
      "    (-126, multiply(power(A, 6), B)),",
      "    (3015, multiply(power(A, 3), power(B, 2))),",
      "    (-4398, power(B, 3)),",
      "])",
      "expected = {",
      "    0: 1, 16: 249849, 20: 18106704, 24: 462962955,",
      "    28: 4397342400, 32: 16602715899, 36: 25756721120,",
      "    40: 16602715899, 44: 4397342400, 48: 462962955,",
      "    52: 18106704, 56: 249849, 72: 1,",
      "}",
      "assert W == expected",
      "assert sum(W.values()) == 2**36",
      "assert all(W.get(i, 0) == W.get(72 - i, 0) for i in range(73))",
      "assert min(i for i in W if i) == 16",
      "lambdas = {",
      "    weight: coefficient * comb(weight, 5) // comb(72, 5)",
      "    for weight, coefficient in W.items() if 5 <= weight <= 67",
      "}",
      "assert all(",
      "    coefficient * comb(weight, 5) % comb(72, 5) == 0",
      "    for weight, coefficient in W.items() if 5 <= weight <= 67",
      ")",
      "assert lambdas[16] == 78",
      "report = {",
      "    'gleason_coefficients': [1, -126, 3015, -4398],",
      "    'weight_distribution': [[w, W[w]] for w in sorted(W)],",
      "    'codewords': sum(W.values()),",
      "    'minimum_nonzero_weight': 16,",
      "    'five_design_lambdas': [[w, lambdas[w]] for w in sorted(lambdas)],",
      "}",
      "payload = dumps(report, sort_keys=True, separators=(',', ':'))",
      "digest = sha256(payload.encode()).hexdigest()",
      "assert digest == '5c244287d06ceec7acd8ef04a7827f61d4214b160a4e7668a3f01db3352c21ea'",
      "print(payload)",
      "print('report_sha256=' + digest)"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1109/TIT.1973.1054975",
    "locator": "Sloane 1973 supplies the distribution and minimum-weight design; exact replay written and executed by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R243",
      "title": "Every witness has the same weight enumerator",
      "object_type": "claim",
      "relation": "validates",
      "direction": "outgoing"
    },
    {
      "slug": "extremal-type-ii-code-72",
      "title": "extremal type ii code 72",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}