{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R711",
  "content_hash": null,
  "slug": "sdb127-claim-exact-minimum-19",
  "type": "claim",
  "title": "The exact minimum is 19",
  "summary": "A 19-element construction covers every residue, while an exhaustive normalized search excludes the only remaining smaller cardinality.",
  "relevance": "This records a result, observation, or conjecture used to assess the target problem.",
  "relevance_source": "derived",
  "body": "The minimum cardinality is\n\\[\n19.\n\\]\nOne attaining set is\n\\[\nA=\\{0,\\pm2,\\pm7,\\pm30,\\pm37,\\pm38,\\pm43,\\pm48,\\pm60,\\pm63\\}\\subseteq\\mathbb Z/127\\mathbb Z.\n\\]\nIn least nonnegative residues this is\n\\[\n\\{0,2,7,30,37,38,43,48,60,63,64,67,79,84,89,90,97,120,125\\}.\n\\]\nThe executable certificate forms all 361 ordered sums and obtains all 127 residues.\n\nEvery admissible set has cardinality \\(2k+1\\). The counting argument in sdb127-claim-counting-lower-bound gives \\(k\\geq8\\), so the only smaller case is cardinality 17. Multiplication by a nonzero residue preserves symmetry and the basis property. Any hypothetical 17-element basis can therefore be normalized so that its eight positive inverse-pair representatives include 1. The exhaustive certificate checks every such normalized choice and proves that none covers all 63 nonzero inverse classes. Thus the displayed 19-element basis is minimum.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "inverse-closed additive bases A in Z/127Z that contain zero",
    "bounds": {
      "modulus": {
        "min": 127,
        "max": 127
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1142/S0219498819500816",
      "locator": "Explicit construction and exhaustive certificate in sdb127-artifact-exact-certificate"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1142/S0219498819500816",
    "locator": "Explicit construction and exhaustive certificate in sdb127-artifact-exact-certificate"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R710",
      "title": "Unsigned sum types force at least 17 elements",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R708",
      "title": "Exact construction check and exhaustive size-17 exclusion",
      "object_type": "artifact",
      "relation": "verifies",
      "direction": "incoming"
    },
    {
      "slug": "R709",
      "title": "Published difference-basis results do not tabulate this constrained instance",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "symmetric-difference-basis-z127",
      "title": "symmetric difference basis z127",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}