{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R710",
  "content_hash": null,
  "slug": "sdb127-claim-counting-lower-bound",
  "type": "claim",
  "title": "Unsigned sum types force at least 17 elements",
  "summary": "Eight inverse pairs are necessary because k pairs can cover at most k squared plus k nonzero inverse classes.",
  "relevance": "This records a result, observation, or conjecture used to assess the target problem.",
  "relevance_source": "derived",
  "body": "Write an admissible set as\n\\[\nA=\\{0,\\pm a_1,\\ldots,\\pm a_k\\}.\n\\]\nIdentify each nonzero residue with its inverse pair \\(\\{r,-r\\}\\). Every nonzero class in \\(A+A\\) must occur in one of four forms: \\(a_i\\), \\(2a_i\\), \\(a_i+a_j\\), or \\(a_i-a_j\\), with \\(i<j\\) in the last two forms. There are at most\n\\[\nk+k+2\\binom{k}{2}=k^2+k\n\\]\nsuch classes. The group \\(\\mathbb Z/127\\mathbb Z\\) has 63 nonzero inverse classes, so \\(k^2+k\\geq63\\). Hence \\(k\\geq8\\) and \\(|A|=2k+1\\geq17\\). This count also supplies the collision budget used by the exact search: at \\(k=8\\), the 72 formal sum types may contain at most nine repetitions if all 63 classes are to appear.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "universal",
    "statement": "sets A={0, plus or minus a_1, ..., plus or minus a_k} in a cyclic group of odd order"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1142/S0219498819500816",
      "locator": "Elementary inverse-class counting argument reproduced in this record"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1142/S0219498819500816",
    "locator": "Elementary inverse-class counting argument reproduced in this record"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R711",
      "title": "The exact minimum is 19",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R708",
      "title": "Exact construction check and exhaustive size-17 exclusion",
      "object_type": "artifact",
      "relation": "tests",
      "direction": "incoming"
    },
    {
      "slug": "symmetric-difference-basis-z127",
      "title": "symmetric difference basis z127",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}