{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R527",
  "content_hash": null,
  "slug": "minimal105-attempt-exact-enumeration-through-nineteen",
  "type": "attempt",
  "title": "Enumerate exact affine orbits through weight nineteen",
  "summary": "Sequential exact solving, orbit blocking, proper-subset scans, and independent matrix construction agree on seven orbits and certify every omitted weight through 19.",
  "relevance": "For Minimal vanishing sums of distinct 105th roots, record minimal105-attempt-exact-enumeration-through-nineteen (“Enumerate exact affine orbits through weight nineteen”) documents a concrete method, search boundary, or failed route. The record states: Sequential exact solving, orbit blocking, proper-subset scans, and independent matrix construction agree on seven orbits and certify every omitted weight through 19.",
  "relevance_source": "recorded",
  "body": "The computation constructs the coefficient vector of each \\(X^s\\bmod\\Phi_{105}\\) and checks that the 48 by 105 matrix has rational rank 48. For each weight in increasing order, Z3 solves \\(Ax=0\\), \\(x_s\\in\\{0,1\\}\\), \\(x_0=1\\), and the exact cardinality constraint. Requiring \\(x_0=1\\) loses no nonempty orbit because translation can move any selected exponent to zero.\n\nEvery nonminimal finite vanishing subset contains an inclusion-minimal vanishing subset of smaller weight. The solver therefore excludes a candidate exactly when it contains a previously enumerated minimal subset. When it finds a minimal subset, it blocks all affine images that contain zero. A final UNSAT result then closes that weight. The sequential replay includes every earlier orbit before moving to the next weight and ends with UNSAT at weight 19.\n\nTwo runs of the compact replay through weight 19 were byte-identical. Two earlier runs through weight 18 were also byte-identical. A standard-library-only cyclotomic construction produced the same matrix digest, and independent Gray-code scans checked all proper nonempty subsets of the weight-14, weight-16, and both weight-18 representatives. A separate targeted weight-19 solve also returned zero orbits. Its blockers included every minimal orbit through weight 16. Omitting the weight-18 blockers is harmless for that targeted check: a vanishing 19-set containing a vanishing 18-set would leave one root whose sum would have to vanish.",
  "status": "completed",
  "evidence_grade": "computational",
  "scope": {
    "kind": "bounded",
    "statement": "complete exact affine-orbit enumeration of distinct inclusion-minimal vanishing subsets of the 105th roots at weights 1 through 19",
    "bounds": {
      "conductor": {
        "min": 105,
        "max": 105
      },
      "weight": {
        "min": 1,
        "max": 19
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "locator": "Execution logs and inline replay artifact, 2026-07-28 UTC"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Execution logs and inline replay artifact, 2026-07-28 UTC"
  },
  "models": [],
  "relations": [
    {
      "slug": "R526",
      "title": "Exact affine-orbit replay through weight nineteen",
      "object_type": "artifact",
      "relation": "uses",
      "direction": "outgoing"
    },
    {
      "slug": "R531",
      "title": "There are seven affine-Galois orbits through weight nineteen",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "minimal-vanishing-105th-root-sums",
      "title": "minimal vanishing 105th root sums",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}