TheoremDB
R192claimStatus: establishedEvidence: SupportedReplay: source onlyexhaustive over its scope

[#R192] The exact difference size of Z/127Z is 13

claim. A checked 13-element basis attains the value established by two published exhaustive searches.

View evidenceOpen source ↗

1Summary

The least cardinality is \[ \boxed{\Delta[\mathbb Z/127\mathbb Z]=13}. \] One attaining set is \[ A=\{0,1,5,11,19,38,61,78,80,81,93,102,109\}. \] The companion verifier forms all 169 ordered differences and obtains every residue modulo 127. Each nonzero residue occurs at least once.

Elementary counting gives only \(|A|\geq12\): an \(m\)-element set has at most \(m(m-1)\) nonzero ordered differences. The exclusion of cardinality 12 comes from exhaustive computation. Wiedemann computed minimum cyclic difference covers through modulus 133. Haanpää later searched all Abelian groups through order 127 with an orderly backtrack algorithm and reported the same minimum cardinalities as Wiedemann for every cyclic group in that range. Their independent results give 13 at modulus 127. Together with the displayed basis, this settles the value.

Supported evidence. Recorded scope: subsets A of the cyclic group Z/127Z whose ordered differences cover the group.

2Evidence

Evidence package: source only

A verification source is cited. This record has no executable replay attached.

Verification source: cs.uwaterloo.ca ↗, Harri Haanpää, Minimum Sum and Difference Covers of Abelian Groups, Journal of Integer Sequences 7 (2004), Article 04.2.6, Sections 4 and 5; Doug Wiedemann, Cyclic difference covers through 133, Congressus Numerantium 90 (1992), 181-185

3What was measured

Answer
13
Construction
0, 1, 5, 11, 19, 38, 61, 78, 80, 81, 93, 102, 109
Elementary lower bound
12
Exhaustive lower bound
13
Independent published computations
2

4How it connects

Verifies (incoming)

Recorded for

5Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R192",
  "content_hash": null,
  "slug": "db127-claim-exact-minimum-13",
  "type": "claim",
  "title": "The exact difference size of Z/127Z is 13",
  "summary": "A checked 13-element basis attains the value established by two published exhaustive searches.",
  "relevance": "For Difference size of Z_127, record db127-claim-exact-minimum-13 (“The exact difference size of Z/127Z is 13”) records a bound, answer, status fact, or structural consequence. The record states: A checked 13-element basis attains the value established by two published exhaustive searches.",
  "relevance_source": "recorded",
  "body": "The least cardinality is\n\\[\n\\boxed{\\Delta[\\mathbb Z/127\\mathbb Z]=13}.\n\\]\nOne attaining set is\n\\[\nA=\\{0,1,5,11,19,38,61,78,80,81,93,102,109\\}.\n\\]\nThe companion verifier forms all 169 ordered differences and obtains every residue modulo 127. Each nonzero residue occurs at least once.\n\nElementary counting gives only \\(|A|\\geq12\\): an \\(m\\)-element set has at most \\(m(m-1)\\) nonzero ordered differences. The exclusion of cardinality 12 comes from exhaustive computation. Wiedemann computed minimum cyclic difference covers through modulus 133. Haanpää later searched all Abelian groups through order 127 with an orderly backtrack algorithm and reported the same minimum cardinalities as Wiedemann for every cyclic group in that range. Their independent results give 13 at modulus 127. Together with the displayed basis, this settles the value.",
  "status": "established",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "bounded",
    "statement": "subsets A of the cyclic group Z/127Z whose ordered differences cover the group",
    "bounds": {
      "modulus": {
        "min": 127,
        "max": 127
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://cs.uwaterloo.ca/journals/JIS/VOL7/Haanpaa/haanpaa.html",
      "locator": "Harri Haanpää, Minimum Sum and Difference Covers of Abelian Groups, Journal of Integer Sequences 7 (2004), Article 04.2.6, Sections 4 and 5; Doug Wiedemann, Cyclic difference covers through 133, Congressus Numerantium 90 (1992), 181-185"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://cs.uwaterloo.ca/journals/JIS/VOL7/Haanpaa/haanpaa.html",
    "locator": "Harri Haanpää, Minimum Sum and Difference Covers of Abelian Groups, Journal of Integer Sequences 7 (2004), Article 04.2.6, Sections 4 and 5; Doug Wiedemann, Cyclic difference covers through 133, Congressus Numerantium 90 (1992), 181-185"
  },
  "relations": [
    {
      "slug": "R191",
      "title": "Ordered-difference counting forces 12 elements",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R189",
      "title": "Exact verifier for the 13-element difference basis",
      "object_type": "artifact",
      "relation": "verifies",
      "direction": "incoming"
    },
    {
      "slug": "R190",
      "title": "Two exhaustive computations exclude a 12-element cover",
      "object_type": "attempt",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "difference-basis-z127",
      "title": "difference basis z127",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

6Provenance

View source, identifiers, and projection details
Project
difference-basis-z127
Locator
Harri Haanpää, Minimum Sum and Difference Covers of Abelian Groups, Journal of Integer Sequences 7 (2004), Article 04.2.6, Sections 4 and 5; Doug Wiedemann, Cyclic difference covers through 133, Congressus Numerantium 90 (1992), 181-185
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-25
Public record
R192
Stable alias
db127-claim-exact-minimum-13
Projection
Reproduction fields are derived from the immutable record.

A statement this project treats as settled at the recorded evidence grade, with the work that backs it.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.