{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R191",
  "content_hash": null,
  "slug": "db127-claim-counting-lower-bound-12",
  "type": "claim",
  "title": "Ordered-difference counting forces 12 elements",
  "summary": "An m-element set supplies at most one identity difference and m(m-1) nonidentity differences.",
  "relevance": "For Difference size of Z_127, record db127-claim-counting-lower-bound-12 (“Ordered-difference counting forces 12 elements”) records a bound, answer, status fact, or structural consequence. The record states: An m-element set supplies at most one identity difference and m(m-1) nonidentity differences.",
  "relevance_source": "recorded",
  "body": "Let \\(A\\) have \\(m\\) elements. The identity is represented by \\(a-a\\). The ordered pairs \\((a,b)\\) with \\(a\\ne b\\) number \\(m(m-1)\\), so\n\\[\n|A-A|\\leq1+m(m-1).\n\\]\nCovering a group of order 127 therefore requires\n\\[\nm(m-1)\\geq126.\n\\]\nThis gives \\(m\\geq12\\). At cardinality 12 there are 132 ordered nonzero differences available for 126 residues, leaving an excess of only six. Equivalently, the 66 unordered pairs must cover all 63 inverse classes with at most three repetitions. That small collision budget is the pruning rule used in exhaustive searches for this case.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "universal",
    "statement": "difference bases of finite groups"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1142/S0219498819500816",
      "locator": "Taras Banakh and Volodymyr Gavrylkiv, Difference bases in cyclic groups, Proposition 2.2(1); the ordered-pair proof is reproduced here"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1142/S0219498819500816",
    "locator": "Taras Banakh and Volodymyr Gavrylkiv, Difference bases in cyclic groups, Proposition 2.2(1); the ordered-pair proof is reproduced here"
  },
  "relations": [
    {
      "slug": "R192",
      "title": "The exact difference size of Z/127Z is 13",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "difference-basis-z127",
      "title": "difference basis z127",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}