{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R526",
  "content_hash": null,
  "slug": "minimal105-artifact-exhaustive-replay-through-nineteen",
  "type": "artifact",
  "title": "Exact affine-orbit replay through weight nineteen",
  "summary": "A deterministic Python, SymPy, and Z3 program reconstructs the 48 by 105 cyclotomic matrix and exhaustively enumerates the seven minimal affine-Galois orbits through weight 19.",
  "relevance": "For Minimal vanishing sums of distinct 105th roots, record minimal105-artifact-exhaustive-replay-through-nineteen (“Exact affine-orbit replay through weight nineteen”) supplies evidence or a replay used to check the packet. The record states: A deterministic Python, SymPy, and Z3 program reconstructs the 48 by 105 cyclotomic matrix and exhaustively enumerates the seven minimal affine-Galois orbits through weight 19.",
  "relevance_source": "recorded",
  "body": "The program reduces every monomial \\(X^s\\), for \\(0\\leq s<105\\), modulo \\(\\Phi_{105}\\) over the integers. A subset vanishes exactly when its 0-1 incidence vector lies in the kernel of the resulting 48 by 105 matrix. Translation lets the solver impose \\(x_0=1\\). At each weight, constraints exclude every previously found lower-weight minimal subset. Every new solution is canonicalized under all 5,040 affine maps, and every normalized image in that orbit is blocked. UNSAT after orbit blocking proves completeness at that weight. A Gray-code scan checks every proper nonempty subset of each representative. The output is deterministic and records the matrix digest, ranks, representatives, orbit sizes, stabilizers, and proper-subset checks.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "exact replay of all distinct inclusion-minimal vanishing subsets of the 105th roots, modulo the affine-Galois action, at weights 1 through 19",
    "bounds": {
      "conductor": {
        "min": 105,
        "max": 105
      },
      "weight": {
        "min": 1,
        "max": 19
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "inline_python_exact_enumerator",
    "command": "python3 minimal105_replay.py",
    "entrypoint": "Join source_lines with LF characters, append a final LF, save as minimal105_replay.py, and execute it",
    "runtime": "CPython 3.9.6 with SymPy 1.14.0 and Z3 5.0.0",
    "citation": {
      "locator": "Inline deterministic replay prepared and executed on 2026-07-28 UTC"
    },
    "dependencies": [
      {
        "name": "CPython",
        "version": "3.9.6",
        "license": "Python-2.0"
      },
      {
        "name": "SymPy",
        "version": "1.14.0",
        "license": "BSD-3-Clause"
      },
      {
        "name": "Z3",
        "version": "5.0.0",
        "license": "MIT"
      }
    ],
    "outputs": {
      "source_sha256": "4104065977f4237e2ff98fb326d3bc2ee04586e825d70806c853c7d6d8d4d882",
      "stdout_sha256": "4e363e45bcbdd25eb06937f3a32609148314503f4443c345b50b7b481e0d0ccb",
      "replay_count": 2,
      "replays_byte_identical": true,
      "matrix_sha256": "669ac026c32d1396ec85f4a7348a848918221d9a9c19598428011eefcfcc2744",
      "matrix_shape": [
        48,
        105
      ],
      "matrix_rank": 48,
      "affine_group_order": 5040,
      "weights_checked": [
        1,
        19
      ],
      "orbit_count_by_weight": {
        "3": 1,
        "5": 1,
        "7": 1,
        "14": 1,
        "16": 1,
        "18": 2
      },
      "all_other_checked_weights_have_zero_orbits": true
    },
    "runtime_seconds": 449.95,
    "inline_source": [
      "#!/usr/bin/env python3",
      "import hashlib",
      "import json",
      "import math",
      "",
      "import sympy as sp",
      "import z3",
      "",
      "N = 105",
      "X = sp.symbols(\"x\")",
      "PHI = sp.Poly(sp.cyclotomic_poly(N, X), X, domain=sp.ZZ)",
      "D = PHI.degree()",
      "COLS = []",
      "for exponent in range(N):",
      "    remainder = sp.Poly(X**exponent, X, domain=sp.ZZ).rem(PHI)",
      "    COLS.append(tuple(int(remainder.nth(i)) for i in range(D)))",
      "UNITS = tuple(u for u in range(N) if math.gcd(u, N) == 1)",
      "",
      "",
      "def vector_sum(subset):",
      "    return tuple(sum(COLS[s][row] for s in subset) for row in range(D))",
      "",
      "",
      "def image(subset, translation, unit):",
      "    return tuple(sorted((translation + unit * s) % N for s in subset))",
      "",
      "",
      "def orbit(subset):",
      "    return {",
      "        image(subset, translation, unit)",
      "        for translation in range(N)",
      "        for unit in UNITS",
      "    }",
      "",
      "",
      "def canonical(subset):",
      "    return min(orbit(subset))",
      "",
      "",
      "def proper_subset_check(subset):",
      "    current = [0] * D",
      "    previous_gray = 0",
      "    full_mask = (1 << len(subset)) - 1",
      "    for step in range(1, 1 << len(subset)):",
      "        gray = step ^ (step >> 1)",
      "        changed = gray ^ previous_gray",
      "        position = changed.bit_length() - 1",
      "        sign = 1 if gray & changed else -1",
      "        for row, value in enumerate(COLS[subset[position]]):",
      "            current[row] += sign * value",
      "        if gray != full_mask and all(value == 0 for value in current):",
      "            return False",
      "        previous_gray = gray",
      "    return True",
      "",
      "",
      "BITS = [z3.Bool(f\"x_{i}\") for i in range(N)]",
      "BASE = [",
      "    z3.Sum([z3.If(BITS[col], COLS[col][row], 0) for col in range(N)]) == 0",
      "    for row in range(D)",
      "]",
      "KNOWN_MINIMAL = set()",
      "ROWS = []",
      "for weight in range(1, 20):",
      "    solver = z3.Solver()",
      "    solver.set(random_seed=0)",
      "    solver.add(BASE)",
      "    solver.add(BITS[0])",
      "    solver.add(z3.Sum([z3.If(bit, 1, 0) for bit in BITS]) == weight)",
      "    for lower in sorted(KNOWN_MINIMAL):",
      "        solver.add(z3.Or([z3.Not(BITS[i]) for i in lower]))",
      "    representatives = set()",
      "    while solver.check() == z3.sat:",
      "        model = solver.model()",
      "        subset = tuple(",
      "            i for i, bit in enumerate(BITS) if z3.is_true(model.eval(bit))",
      "        )",
      "        assert vector_sum(subset) == (0,) * D",
      "        representative = canonical(subset)",
      "        representatives.add(representative)",
      "        for normalized in sorted(item for item in orbit(representative) if 0 in item):",
      "            solver.add(",
      "                z3.Or(",
      "                    [",
      "                        bit != z3.BoolVal(i in normalized)",
      "                        for i, bit in enumerate(BITS)",
      "                    ]",
      "                )",
      "            )",
      "    assert solver.check() == z3.unsat",
      "    for representative in representatives:",
      "        KNOWN_MINIMAL.update(orbit(representative))",
      "    ROWS.append(",
      "        {",
      "            \"weight\": weight,",
      "            \"representatives\": [",
      "                {",
      "                    \"subset\": list(representative),",
      "                    \"orbit_size\": len(orbit(representative)),",
      "                    \"stabilizer_size\": 5040 // len(orbit(representative)),",
      "                    \"proper_nonempty_subsets_checked\": (1 << weight) - 2,",
      "                    \"proper_subset_check\": proper_subset_check(representative),",
      "                }",
      "                for representative in sorted(representatives)",
      "            ],",
      "        }",
      "    )",
      "",
      "matrix_encoding = json.dumps(COLS, separators=(\",\", \":\")).encode()",
      "payload = {",
      "    \"schema\": \"minimal105-exhaustive-replay-v1\",",
      "    \"environment\": {",
      "        \"sympy\": sp.__version__,",
      "        \"z3\": z3.get_version_string(),",
      "    },",
      "    \"cyclotomic_degree\": D,",
      "    \"matrix_shape\": [D, N],",
      "    \"matrix_rank\": sp.Matrix(D, N, lambda row, col: COLS[col][row]).rank(),",
      "    \"matrix_sha256\": hashlib.sha256(matrix_encoding).hexdigest(),",
      "    \"affine_group_order\": N * len(UNITS),",
      "    \"weights\": ROWS,",
      "}",
      "print(json.dumps(payload, sort_keys=True, separators=(\",\", \":\")))"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Inline deterministic replay prepared and executed on 2026-07-28 UTC"
  },
  "models": [],
  "relations": [
    {
      "slug": "R531",
      "title": "There are seven affine-Galois orbits through weight nineteen",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R527",
      "title": "Enumerate exact affine orbits through weight nineteen",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "R528",
      "title": "Extend the exact sequential search to weight twenty",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "minimal-vanishing-105th-root-sums",
      "title": "minimal vanishing 105th root sums",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}